# 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
• 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.