Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Feature request modification

Email Gateway (Aug 22 2022 at 09:32):

From: "W. Douglas Maurer" <maurer@gwu.edu>
Oops -- typo at the end of the requested feature, and it also needs
to start with m <= n+1, not m < n+1. So it should be (and the proof
goes through, this way):
lemma aux: "m <= n+1 ==> setsum f {m..n+1} = setsum f {m..n} + f (n+1 :: int)"
by (simp add: add.commute atLeastAtMostPlus1_int_conv)
The case m = n+1 is necessary in order to interact properly with the
base case, which is "setsum f {n+(1::int)..n} = 0" by simp . Setting
m = n+1, we get:
setsum f {n+1..n+1} [that is, setsum f {m..m}]
= setsum f {n+1..n} [that is, 0, by the base case]

• f(n+1 :: int) [that is, f(m::int)]
  In other words, setsum f {m..m} = f(m::int), which is as it should
  be. Without the case m = n+1, you'd need a separate proof of that
  case. -Douglas

Email Gateway (Aug 22 2022 at 10:10):

From: Tobias Nipkow <nipkow@in.tum.de>
I considered this suggestion carefully but decided against it. Adding something
that can be derived easily needs a strong argument, otherwise the library
explodes. Here a single lemma does not do the job anyway: on type nat, +1
becomes Suc and floats to the top, at least in sums. This is not the case for
type int, where "n+1" is not a canonical form. You will have to put that lemma
into a basis theory for your students.

Tobias
smime.p7s

Last updated: May 06 2024 at 20:16 UTC