# Re: [isabelle] Reasoning with the option type

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

```

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