[isabelle] statespace



Hello,

want to use the statespace construct to model state spaces and i have
some questions:

0) is there some reference to statespace which might answer my
questions? until now i only have "State Spaces - The Locale Way" and
in there i could not find the answers to the following questions. (and
i found StateSpaceEx.thy which has similar examples)

1) before, i tried to model the statespace as a record. I defined
operational semantics of the type "record => instruction => record =>
bool" to have a function that indicates, whether the transition from
one state to another via an instruction is allowed. How can I do this
with statespaces, as they are not a variable type?

2) is there a way to instantiate such a statespace? Or is there no
need to? i'm still thinking in terms of records or functions, whose
variables could be updated bit by bit, but maybe
this just not the way statespaces are meant to be.

3) i played around with the variable renaming of statespaces. here's my example
statespace A = a::nat
statespace B = A + b::nat
statespace C = B[a=z] --- does not work

so my perception is, that i can only rename variables, that were
introduced in the named statespace, not in its parents.
why is it like this? is there some conceptual meaning?


thanks in advance
best regards
Nils





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