Re: [isabelle] Reasoning with the option type

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.


On Tue, Apr 28, 2015 at 6:18 AM, Eugene W. Stark <stark at>

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