Re: [isabelle] Cl-isabelle-users Digest, Vol 118, Issue 47

I asked sledgehammer and it told me

by (simp add: add.commute atLeastAtMostPlus1_int_conv)

Maybe my s/h is bigger (or more recent) than yours ;-)


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)? For now I'm going to ask my students to include these two lines without their even trying to understand what they mean. But when I update my write-up to cover Isabelle2015, and they start using that, I will want them to treat this as built in to the system. This will give them a much better handle on proofs by induction (of the kind that they meet in a discrete mathematics course) than they have ever had before. Many thanks! -WDMaurer
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.