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

 >  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)"
 >> 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
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.