[isabelle] Reasoning with the option type

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!


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

Attachment: SumIntOption.thy
Description: Binary data

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