[isabelle] formalising abstract machines


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. 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?


- Gergely

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