src/HOL/Library/State_Monad.thy
changeset 24195 7d1a16c77f7c
parent 22664 e965391e2864
child 24224 a5c95bbeb31d
     1.1 --- a/src/HOL/Library/State_Monad.thy	Thu Aug 09 15:52:42 2007 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Aug 09 15:52:45 2007 +0200
     1.3 @@ -221,26 +221,22 @@
     1.4    "_do f" => "CONST run f"
     1.5    "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
     1.6    "_fcomp f g" => "f \<guillemotright> g"
     1.7 -  "_let x t f" => "Let t (\<lambda>x. f)"
     1.8 +  "_let x t f" => "CONST Let t (\<lambda>x. f)"
     1.9    "_nil f" => "f"
    1.10  
    1.11  print_translation {*
    1.12  let
    1.13 -  val name_mbind = @{const_syntax "mbind"};
    1.14 -  val name_fcomp = @{const_syntax "fcomp"};
    1.15 -  fun unfold_monad (t as Const (name, _) $ f $ g) =
    1.16 -        if name = name_mbind then let
    1.17 -            val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.18 -          in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.19 -        else if name = name_fcomp then
    1.20 -          Const ("_fcomp", dummyT) $ f $ unfold_monad g
    1.21 -        else t
    1.22 -    | unfold_monad (Const ("Let", _) $ f $ g) =
    1.23 +  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
    1.24          let
    1.25 -          
    1.26 +          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.27 +        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.28 +    | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
    1.29 +        Const ("_fcomp", dummyT) $ f $ unfold_monad g
    1.30 +    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
    1.31 +        let
    1.32            val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
    1.33          in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
    1.34 -    | unfold_monad (Const ("Pair", _) $ f) =
    1.35 +    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
    1.36          Const ("return", dummyT) $ f
    1.37      | unfold_monad f = f;
    1.38    fun tr' (f::ts) =
    1.39 @@ -248,6 +244,7 @@
    1.40  in [(@{const_syntax "run"}, tr')] end;
    1.41  *}
    1.42  
    1.43 +
    1.44  subsection {* Combinators *}
    1.45  
    1.46  definition
    1.47 @@ -258,12 +255,10 @@
    1.48    list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.49    "list f [] = id"
    1.50  | "list f (x#xs) = (do f x; list f xs done)"
    1.51 -lemmas [code] = list.simps
    1.52  
    1.53  fun list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
    1.54    "list_yield f [] = return []"
    1.55  | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    1.56 -lemmas [code] = list_yield.simps
    1.57    
    1.58  text {* combinator properties *}
    1.59  
    1.60 @@ -304,7 +299,7 @@
    1.61  *}
    1.62  
    1.63  text {*
    1.64 -  For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
    1.65 +  For an example, see HOL/ex/Random.thy.
    1.66  *}
    1.67  
    1.68  end