# [isabelle] about longer computation syntax sugar

Dear All,
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,
'b) state-monad
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
High-Performance Microkernel")
activateThread ==
do thread <- getCurThread;
state <- getWaitState thread;
case state of
NotWaiting => return ()
| WaitingToSend eptr badge fault cap =>
if cap = None then
doIPCTransfer thread (waitingIPCPartner state)
else arbitrary
| WaitinToRecieve eptr =>
doIPCTransfer (waitingIPCPartner state) thread
| => arbitrary
od
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?
cheers:)
Liu Jian
--
email to: gjk.liu at gmail.com

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