Re: [isabelle] formalising abstract machines
On 28/01/2014 12:10, Buday Gergely wrote:
> 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
> What is the standard way of defining an interpreter and its partial correctness in Isabelle?
> - Gergely
This archive was generated by a fusion of
Pipermail (Mailman edition) and