[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

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?


   Liu Jian

email to: gjk.liu at gmail.com

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