*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Fwd: Difficulties with "setsum"*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Wed, 22 Apr 2015 11:52:16 -0300*In-reply-to*: <CAAPnxw0x5zBbRJHKZmOahydu+p=AugWjtz_NoGdsPVsxhFAeuQ@mail.gmail.com>*References*: <CAAPnxw0x5zBbRJHKZmOahydu+p=AugWjtz_NoGdsPVsxhFAeuQ@mail.gmail.com>*Sender*: alfio.martini at gmail.com

Sorry, there was a typo in the previous theory file. It is attached again. Best! ---------- Forwarded message ---------- From: Alfio Martini <alfio.martini at acm.org> Date: Wed, Apr 22, 2015 at 11:46 AM Subject: Difficulties with "setsum" To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk> 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! -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

**Attachment:
SumInt.thy**

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

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