*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Difficulties with "setsum"*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Wed, 22 Apr 2015 18:07:12 +0100*Cc*: Manuel Eberl <eberlm at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAPnxw0yO6hUhoWMBb+LLuEqifQ_tHAPuOxW5_zJ6rPaffMnig@mail.gmail.com>*References*: <CAAPnxw0x5zBbRJHKZmOahydu+p=AugWjtz_NoGdsPVsxhFAeuQ@mail.gmail.com> <5537B772.9080209@in.tum.de> <CAAPnxw0yO6hUhoWMBb+LLuEqifQ_tHAPuOxW5_zJ6rPaffMnig@mail.gmail.com>*User-agent*: Roundcube Webmail/1.0.2

Hi Alfio, Your sorry can be proved by: also have "... = (â k=l..i+1. k)" proof - have "{l..i + 1} = insert (i+1) {l..i}" using hip02 by auto thus ?thesis by simp qed Also note, goals like this: lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"

Cheers, Wenda On 2015-04-22 17:24, Alfio Martini wrote:

Hi, I think that the main problem is that the automatic methods cannot cope with following triviallemmas, although both sides evaluate correctly with the command'value',value "(setsum id {1::int..2}) + (3::int)" value "(setsum id {1::int..3})" lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3" oops value "(setsum id {-3::int..3})" value "(setsum id {-3::int..2}) + 3" lemma "(setsum id {-3::int..3}) = (setsum id {-3..2}) + 3" oopsI tried sledgehammer but it does not find anything. Anyway, the lasttimesledgehammer worked fine for me was with Isabelle 2012. Best!On Wed, Apr 22, 2015 at 12:00 PM, Manuel Eberl <eberlm at in.tum.de>wrote:The problem is that in order to "unroll" the setsum, you first have tobring the numerals (e.g. 2, 3, 4) into successor notation. One way todothis is to add eval_nat_numeral to your simpset, e.g. apply (auto simp: eval_nat_numeral)Most of your example work automatically with these, but you will havetomassage expressions like "(â k::nat â {j. 1âj â jâ3}. k)" by hand abitfirst, e.g. by proving that "{j. 1âj â jâ3} = {1..3}". One could easily write simplification rules that unroll setsums overconstant intervals like these automatically or even write a simprocthatdoes that, but I don't think that would be very helpful in practice. Cheers, Manuel On 22/04/15 16:46, Alfio Martini wrote:Dear Isabelle Users,While trying to prove the correctness of a simple function thatreturnsthe sum of the values between integers l and u, I stumbled upon an unexpected problem: I was ano able to prove that (Sum k=l..(u+1). k) = (u+1) + (Sum k=l...u) if l<u+1, which should hold by the definition of an indexed sum.My thy file is attached and, in the proof, is the only line with"sorry".I would very grateful if anyone could take a quick look at that.To get a better feeling of what are the underlying simplificationrules,I performed some tests with setsum, but the results weredisappointing.(see below). Besides, acoording to "What is is Main", setsum is defined in "Finite_Set", but in Isabelle 2014 it is defined in "Groups_Big". (* Testing the setsum function *) fun i2n::"int â nat" where "i2n x = (if x â 0 then 0 else Suc (i2n (x - 1)))" value "int (setsum id {1::nat..5})" (* this works *) lemma "setsum id {1::nat..2} = (Suc (Suc (Suc 0)))" apply (auto) oops lemma "setsum id {1::nat..5}= i2n 15" apply (auto) oops lemma "(setsum id {1::nat..2})= Suc (Suc (Suc 0))" apply (auto) oops lemma "(â k::nat â {j. 1âj â jâ3}. k) = 6" apply oops lemma "(â k::nat | kâ1 â kâ2 . k) = Suc (Suc (Suc 0))" apply (auto) oops lemma "(â k::nat=1..3. k)= (â k=1..2. k) + 3" oops term "â k=1..n. k" value "â k::nat = 2 ..1. k" (* this works *) (* end of test *) All the Best!

-- Wenda Li PhD Candidate Computer Laboratory University of Cambridge

**Follow-Ups**:**Re: [isabelle] Difficulties with "setsum"***From:*Lars Hupel

**References**:**[isabelle] Difficulties with "setsum"***From:*Alfio Martini

**Re: [isabelle] Difficulties with "setsum"***From:*Manuel Eberl

**Re: [isabelle] Difficulties with "setsum"***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Difficulties with "setsum"
- Next by Date: [isabelle] Fwd: Difficulties with "setsum"
- Previous by Thread: Re: [isabelle] Difficulties with "setsum"
- Next by Thread: [isabelle] Fwd: Difficulties with "setsum"
- 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