Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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: Mar 29 2024 at 01:04 UTC