[isabelle] formalising abstract machines
I am formalising an abstract machine. For being able to prove pattern completeness, I defined the function to evalute to
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. 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?
What is the standard way of defining an interpreter and its partial correctness in Isabelle?
This archive was generated by a fusion of
Pipermail (Mailman edition) and