[isabelle] statespace again



Hello Norbert,

We recently asked a question about state spaces on the mailing list
that you kindly answered, but still questions arise :-)

We are working on a formalization of a low-level language with a proof
calculus in Isabelle/HOL. So far this formalization was defined
concrete, i.e. the operational semantics were defined as inductive
function of type "record => instruction => record => bool". Currently
it is our goal to make the formalization more abstract, i.e. as an
abstract base function " 's => instruction =>' s => bool" and to
define the concrete semantics of a command (e.g. "s (add VX VY VZ) t")
by reducing to the abstract definition (rather like in Simpl, e.g. "s
(Basic f) t"). We still want to use statespace construct.

The problem we're facing now is how we can quantify over variables
within a specific statespace environment (e.g. statespace st = VX::nat
VY::nat VZ::nat) . For example, if we want to show the lemma (in st)
"Opsem s (add VX VY VZ) t", we want to reduce the semantics of add to
the general rule that represents the relationship between the states s
and t (the equivalent of [ta = sb + sc ] ==> Opsem s (add a b c) t).
As variables in statespace are distinguished according to their
abstract names, we could not come up with a solution. It seems as if
this happens in Simpl in the ML code. do we have to learn ML to do
this?

For ideas or suggestions where we might find this a starting point, we
would be very grateful.

Thank you and best regards,
Nils and Björn





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