# Re: [isabelle] Reasoning with the option type

```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.
>
> 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
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.