Re: [isabelle] Difficulties with "setsum" (Alfio Martini)

On 28/04/2015 06:58, W. Douglas Maurer wrote:
 >  Lemmas I tried with sledgehammer

 lemma "[a] = [b] ? a = b" oops
 >> lemma aux: "m < n+1 ?setsum f {m..n+1} = setsum f {m..n} + f (n+1 :: int)"

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 ;-)


 >> oops

I've been following the 'Difficulties with "setsum"' thread for some time now,
and, after much discussion, I still don't know what the best way is, to
introduce the lemma 'aux:' above into my proofs. I need it in order, for
example, to prove:
"1^2-2^2+3^2-4^2+...+(-1)^(n+1)*n^2 = ((-1)^(n+1))*n*(n+1)/2"
This one has to be done by using int, not nat, because the answer might be
negative. There are over a dozen others, given as exercises on pp. 49-50 of
Johnsonbaugh, R., "Discrete Mathematics" (2nd edition). My ultimate goal (which
will probably take over a year to get off the ground) is for students of
discrete mathematics to get started with at least the lowest-level features of
Isar as part of their study. I can get them through proofs by contradiction,
proofs by cases, and (if they involve exponents, such as proving that 8^k - 2^k
is always divisible by 6), proofs by induction, since exponents are natural
numbers; but I'm stuck, on more general proofs by induction, until I can somehow
introduce this one fact (aux: above). -WDMaurer

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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