[isabelle] Feature request modification



I have just tried:
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)
into my Isabelle2014 on the Mac, and it works.
Tobias, this is a feature request. Would you please put the above two lines into Isabelle2015 (but call it some name other than aux -- perhaps setsum_atLeastAtMost_int or something like that)?

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

--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.