Re: [isabelle] formalising abstract machines



On 28/01/2014 12:10, Buday Gergely wrote:
> Hi,
> 
> I am formalising an abstract machine. For being able to prove pattern completeness, I defined the function to evalute to
> 
>     value option
> 
> and added a last clause that returns None if all the other patterns fail.
>
> But it is not clear how this interplays with
> 
>    abstract_machine_dom arguments => (abstract_machine arguments) meets specification
> 
> type theorems.

If you have a dom predicate, you don't need the option type because the
predicate should guaratee you never get into an underdefined situation.
Conversely, with option you can formulate your theorem like this:

abstract_machine arguments = Some result ==> results meets spec

> Would it be better to simply make an infinite recursive call as a last pattern?
> 
> | abstract_machine arguments = abstract_machine arguments
> 
> letting it not to terminate at all?

You would not be able to define this with "fun" and would need to use
"partial_function (option)". However, you should only do this if it is a genuine
case of nontermination and not failed pattern-matching turned into artificial
nontermination.

Tobias

> What is the standard way of defining an interpreter and its partial correctness in Isabelle?
> 
> Cheers
> 
> - Gergely
> 




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