Re: [isabelle] Reasoning with the option type
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 cs.stonybrook.edu>
> 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