*To*: Alfio Martini <alfio.martini at acm.org>, "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*: "Eugene W. Stark" <stark at cs.stonybrook.edu>*Date*: Tue, 28 Apr 2015 05:18:13 -0400*In-reply-to*: <CAAPnxw2YxsozyTqNnsmZghfdRa6_6f9mVTcPT7fqC7SCtp42qg@mail.gmail.com>*References*: <CAAPnxw2YxsozyTqNnsmZghfdRa6_6f9mVTcPT7fqC7SCtp42qg@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

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! >

theory SumIntOption imports Main begin function sumO:: "int \<Rightarrow> int \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int option" where "sumO l l f = Some (f l)" | "n < m \<Longrightarrow> sumO n m f = (case sumO n (m - 1) f of None \<Rightarrow> None | Some v \<Rightarrow> Some ((f m) + v))"| "n>m \<Longrightarrow> sumO n m f = None" by (atomize_elim, auto) termination sumO by (relation "measure (\<lambda>(l,u,f). nat ((u+1) - l))") auto theorem fixes u::int and l::int assumes "l\<le>u" shows "sumO l u f = Some (\<Sum> k=l..u. f k)" (is "?P u") using assms proof (induct u rule: int_ge_induct) show "?P l" by simp next fix i::int assume "l\<le>i" and "?P i" show "?P (i+1)" proof - from `?P i` have "sumO l (i+1) f = Some (f (i+1) + (\<Sum> k=l..i. f k))" using `l\<le>i` by simp also have "f (i+1) + (\<Sum> k=l..i. f k) = (\<Sum> k=l..i+1. f k)" proof - have "{l..i+1} = insert (i+1) {l..i}" using `l\<le>i` by auto thus ?thesis by simp qed finally show ?thesis by auto qed qed end

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

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

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

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