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

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
*From*: "W. Douglas Maurer" <maurer at gwu.edu>
*Date*: Tue, 28 Apr 2015 00:58:44 -0400
*Cc*: maurer at gwu.edu
*In-reply-to*: <mailman.41271.1429951441.13101.cl-isabelle-users@lists.cam.ac.uk>
*References*: <mailman.41271.1429951441.13101.cl-isabelle-users@lists.cam.ac.uk>

> 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.*