*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Difficulties with "setsum"*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 22 Apr 2015 17:00:02 +0200*In-reply-to*: <CAAPnxw0x5zBbRJHKZmOahydu+p=AugWjtz_NoGdsPVsxhFAeuQ@mail.gmail.com>*References*: <CAAPnxw0x5zBbRJHKZmOahydu+p=AugWjtz_NoGdsPVsxhFAeuQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

apply (auto simp: eval_nat_numeral)

Cheers, Manuel On 22/04/15 16:46, Alfio Martini wrote:

Dear Isabelle Users, While trying to prove the correctness of a simple function that returns the 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 simplification rules, I performed some tests with setsum, but the results were disappointing. (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!

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

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

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

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