*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Reasoning with the option type*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 28 Apr 2015 11:56:31 +0200*In-reply-to*: <CAAPnxw0m+0cE8mTy0ABpFuBR45_iuF2-ipjkAXREaUTJb55=YA@mail.gmail.com>*References*: <CAAPnxw2YxsozyTqNnsmZghfdRa6_6f9mVTcPT7fqC7SCtp42qg@mail.gmail.com> <553F5055.2080009@cs.stonybrook.edu> <CAAPnxw0m+0cE8mTy0ABpFuBR45_iuF2-ipjkAXREaUTJb55=YA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

So let's apply it and see what we end up with: theorem "l â u â sumO l u f = Some (âk=l..u. f k)" apply (induction l u f rule: sumO.induct) apply simp_all The remaining goal is then something like ân m f. n < m â f m + setsum f {n..m - 1} = setsum f {n..m}

lemma setsum_last_int: "(n::int) < m â f m + setsum f {n..m - 1} = setsum f {n..m}"

Now the proof is fully automatic: theorem "l â u â sumO l u f = Some (âk=l..u. f k)" by (induction l u f rule: sumO.induct) (simp_all add: setsum_last_int) Cheers, Manuel On 28/04/15 11:34, Alfio Martini wrote:

Hi Eugene, Thank you for your feedback. Indeed it looks much shorter, since the simplifier takes care of the many intermediate steps I wrote it down. Anyway, at least for these exercises, I try to use Isabelle to check my handwritten proofs (or any handwritten proof that is made without assuming automated tools). That is why they look unnecessary long. But I will use some of your suggestions in order to improve its presentation. Best! On Tue, Apr 28, 2015 at 6:18 AM, Eugene W. Stark <stark at cs.stonybrook.edu> wrote:I am not very experienced, but I looked at your proof. It seems very long, and there are lots of apparently unnecessary assumptions that float in and out. I came up with the attached, which is rather shorter. I did not see how the use of the option type introduces any complication here. Hopefully I did not misunderstand something important. - Gene Stark On 04/27/2015 11:55 PM, Alfio Martini wrote:Dear Isabelle Users, In a previous thread (Isabelle: A logic of partial functions?) I asked some questions about the use of the constant "undefined" when dealing with partial functions, which have to be made total according to the foundations of Isabelle. The long thread about my difficulties with Sledgehammer made me realize that my definition was not general enough. And after looking into the very well written tutorial on Code Generation, I was convinced that I had to deal with the option type. I'm also very grateful to all that reply my original messages with many insightful and helpful observations. So, if some novice is interested I include here (my) proof of the total correctness of that sum algorithm. I only ask the evaluation of some more experienced user, if this is the correct way to reason with the option type. It looks a bit clumsy. The thy file is attached. Many thanks for any remarks! Best!

**Follow-Ups**:**Re: [isabelle] Reasoning with the option type***From:*Alfio Martini

**References**:**[isabelle] Reasoning with the option type***From:*Alfio Martini

**Re: [isabelle] Reasoning with the option type***From:*Eugene W. Stark

**Re: [isabelle] Reasoning with the option type***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Install c-parser-to-simpl
- Next by Date: Re: [isabelle] What is sumC?
- Previous by Thread: Re: [isabelle] Reasoning with the option type
- Next by Thread: Re: [isabelle] Reasoning with the option type
- 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