Re: [isabelle] about longer computation syntax sugar

Hi Liu,

you need to do the rest as well, see lines 125-192 in HOL/Library/StateMonad.thy. The file is part of Isabelle2008 already, I believe, if not, you can find it in the Isabelle development snapshot.

Specifically, you will need _scomp (and _fcomp if you want to leave out the
"_ <-" part) and for printing also the ML print translation. Florian Haftmann wrote that specific theory, he'll be able to explain in more detail how it works.


Liu Jian wrote:
Thanks Gerwin! following your direction, I write the following statements

types ('s, 'a)state_monad = " 's => ('a , 's)"

constdefs bind :: "('s, 'a)state_monad =>('a => ('s, 'b)state_monad)
=>('s, 'b)state_monad" (infixr ">>=" 60)
" f >>= g  == % s . let  (v, s') = f s in g v s'"


  "_bind"       :: "[pttrn, 'a] => dobind"              ("(2_ <-/ _)" 10)
  "_do"         :: "[dobind, 'a] =>  'b"               ("( do _ ;/ _
od )" [0,0] 10)

 " do x <- f ; g od" == " f >>= (% x. g)"

Now, binding two monads is easy. But How to bind three or more monads
in a "do ... od"
statement? Moreover, what is the association attribute of "bind"
operator? infixr or infixl.
In the above definition I use the former. But I can not hold the
difference between them.


Liu Jian

On Wed, Nov 26, 2008 at 6:49 PM, Gerwin Klein <gerwin.klein at> wrote:
Liu Jian wrote:
 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")
It's fairly standard syntax black magic and works roughly like the normal
let bindings in Isabelle (e.g. see HOL/HOL.thy).

A more complex example directly with "do" syntax can be found in
HOL/Library/StateMonad.thy. It's slightly different from the one in our
papers, but the effect is the same.


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