*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 28 Apr 2015 08:02:23 +0200*In-reply-to*: <a0620071cd164bfddde5d@[192.168.1.6]>*References*: <mailman.41271.1429951441.13101.cl-isabelle-users@lists.cam.ac.uk> <a0620071cd164bfddde5d@[192.168.1.6]>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

On 28/04/2015 06:58, W. Douglas Maurer wrote:

> Lemmas I tried with sledgehammerlemma "[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 ;-) Tobias

>> oopsI'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**

**References**:**Re: [isabelle] Difficulties with "setsum" (Alfio Martini)***From:*W. Douglas Maurer

- Previous by Date: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Next by Date: Re: [isabelle] What is sumC?
- Previous by Thread: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Next by Thread: [isabelle] CfP HOFM Workshop @ SEFM 2015 (York, UK)
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list