# [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.*