Re: [isabelle] statespace
On 08.11.2010, at 21:19, Nils Jähnig wrote:
> 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)
I thought everything is said in that paper ;)
> 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?
As a statespace is just a locale, you
can define the function in the context of the statespace / locale using the "local-theory" concepts of Isabelle e.g.:
statespace state = ...
"myfun s = use s with selectors and updates here"
> 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.
Yes by the standard means of locale instantiation.
There is currently not more automation.
For example you can define a record with all the fields, then instantiate the statespace-locale which leaves you with the obligation to proof that the record selector / update functions fulfill the locale assumptions, which they should.
> 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
This seems to be a bug or missing feature, but no conceptual thing.
Hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and