[isabelle] about longer computation syntax sugar
I am now interested in the work of the following paper
David Cock, Gerwin Klein and Thomas Sewell "Secure Microkernels, State
Monads nad Scalable Refinement"
But a question about how to define a longer computation for "bind"
operator of State monad
As the paper says "bind" can be defined as following:
bind :: ('s, 'a) state-monad => ('a => ('s, 'b) state-mond) => ('s,
bind f g == % s. let (v, s') = f s in g v s'
And, "The expression bind f g is abbreivated as f >>= g, To allow
concise description for longer computations,
we define a do syntax in sa similar fashion to Haskell"
do x <- f; g x od == f >>= g
But how to write the real isabelle statements for the above
definition? (Note there is parameter "x")
Moreover, from the above syntax, we can write the following monad code:
(in Kevin Elphinstoen, Gerwin Klein etc. "Formalising a
do thread <- getCurThread;
state <- getWaitState thread;
case state of
NotWaiting => return ()
| WaitingToSend eptr badge fault cap =>
if cap = None then
doIPCTransfer thread (waitingIPCPartner state)
| WaitinToRecieve eptr =>
doIPCTransfer (waitingIPCPartner state) thread
| => arbitrary
Note that there are three monad binded in the above definition. But in
the "do ... od" statement definition only contain two,
How to deal with it? If possible could you give a example real
isabelle definition for above definition?
email to: gjk.liu at gmail.com
This archive was generated by a fusion of
Pipermail (Mailman edition) and