*To*: "Eugene W. Stark" <stark at cs.stonybrook.edu>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Reasoning with the option type*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 28 Apr 2015 13:48:33 -0300*In-reply-to*: <553F5055.2080009@cs.stonybrook.edu>*References*: <CAAPnxw2YxsozyTqNnsmZghfdRa6_6f9mVTcPT7fqC7SCtp42qg@mail.gmail.com> <553F5055.2080009@cs.stonybrook.edu>*Sender*: alfio.martini at gmail.com

Hi Eugene, and there are lots of apparently unnecessary > assumptions that float in and out. You are completely right. My original (long) version would be like this without the unnecessary assumptions. theorem fixes u::int and l::int assumes assm: "lâu" shows "sumO l u f = Some (â k=l..u. (f k))" (is "?P u") using assms proof (induct u rule: int_ge_induct) show "?P l" proof - have "sumO l l f = Some (f l)" by simp also have "... = Some (â k=l..l. (f k))" by simp finally show "sumO l l f = Some (â k=l..l. (f k))" by this qed next fix i::int assume hip01: "iâl" and HI:"?P i" show "sumO l (i+1) f = Some (â k=l..i+1. (f k))" proof - have "sumO l (i+1) f = (case sumO l i f of None â None | Some v â Some ((f (i+1) + v)))" using hip01 by simp also have "... = Some (f (i+1) + (â k=l..i. (f k)))" using HI and hip01 by simp also have "... = Some (â k=l..i+1. (f k))" proof - have "{l..i + 1} = insert (i+1) {l..i}" using hip01 by auto thus ?thesis by simp qed finally show "sumO l (i+1) f = Some (â k=l..i+1. (f k))" by this qed qed 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! > > > > -- 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

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

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

- Previous by Date: Re: [isabelle] Conditional simplification of constants
- Next by Date: Re: [isabelle] accessing ML definitions in isabelle_process
- Previous by Thread: Re: [isabelle] Reasoning with the option type
- Next by Thread: [isabelle] Postdoc positions at Inria-Saclay
- 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