Email Gateway (Aug 22 2022 at 09:32): Email Gateway (Aug 22 2022 at 09:32):From: "W. Douglas Maurer" <maurer@gwu.edu>
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
Last updated: Nov 21 2024 at 12:39 UTC