Re: [isabelle] statespace

Hello Nils,

On 08.11.2010, at 21:19, Nils Jähnig wrote:

> 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)

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

context state

fun myfun 
"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 MHonArc.