src/HOL/Library/State_Monad.thy
changeset 26588 d83271bfaba5
parent 26266 35ae83ca190a
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Apr 09 08:10:09 2008 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Apr 09 08:10:11 2008 +0200
     1.3 @@ -56,29 +56,18 @@
     1.4    we use a set of monad combinators:
     1.5  *}
     1.6  
     1.7 -definition
     1.8 -  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
     1.9 -    (infixl ">>=" 60) where
    1.10 -  "f >>= g = split g \<circ> f"
    1.11 +notation fcomp (infixl ">>" 60)
    1.12 +notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)
    1.13 +notation scomp (infixl ">>=" 60)
    1.14 +notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)
    1.15  
    1.16 -definition
    1.17 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.18 -    (infixl ">>" 60) where
    1.19 -  "f >> g = g \<circ> f"
    1.20 +abbreviation (input)
    1.21 +  "return \<equiv> Pair"
    1.22  
    1.23  definition
    1.24    run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.25    "run f = f"
    1.26  
    1.27 -syntax (xsymbols)
    1.28 -  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    1.29 -    (infixl "\<guillemotright>=" 60)
    1.30 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.31 -    (infixl "\<guillemotright>" 60)
    1.32 -
    1.33 -abbreviation (input)
    1.34 -  "return \<equiv> Pair"
    1.35 -
    1.36  print_ast_translation {*
    1.37    [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
    1.38  *}
    1.39 @@ -142,12 +131,12 @@
    1.40  *}
    1.41  
    1.42  lemma
    1.43 -  return_mbind [simp]: "return x \<guillemotright>= f = f x"
    1.44 -  unfolding mbind_def by (simp add: expand_fun_eq)
    1.45 +  return_scomp [simp]: "return x \<guillemotright>= f = f x"
    1.46 +  unfolding scomp_def by (simp add: expand_fun_eq)
    1.47  
    1.48  lemma
    1.49 -  mbind_return [simp]: "x \<guillemotright>= return = x"
    1.50 -  unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
    1.51 +  scomp_return [simp]: "x \<guillemotright>= return = x"
    1.52 +  unfolding scomp_def by (simp add: expand_fun_eq split_Pair)
    1.53  
    1.54  lemma
    1.55    id_fcomp [simp]: "id \<guillemotright> f = f"
    1.56 @@ -158,30 +147,30 @@
    1.57    unfolding fcomp_def by simp
    1.58  
    1.59  lemma
    1.60 -  mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
    1.61 -  unfolding mbind_def by (simp add: split_def expand_fun_eq)
    1.62 +  scomp_scomp [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
    1.63 +  unfolding scomp_def by (simp add: split_def expand_fun_eq)
    1.64  
    1.65  lemma
    1.66 -  mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
    1.67 -  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
    1.68 +  scomp_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
    1.69 +  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
    1.70  
    1.71  lemma
    1.72 -  fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
    1.73 -  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
    1.74 +  fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
    1.75 +  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
    1.76  
    1.77  lemma
    1.78    fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
    1.79    unfolding fcomp_def o_assoc ..
    1.80  
    1.81 -lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
    1.82 -  mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
    1.83 +lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id
    1.84 +  scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp
    1.85  
    1.86  text {*
    1.87    Evaluation of monadic expressions by force:
    1.88  *}
    1.89  
    1.90  lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
    1.91 -  mbind_def fcomp_def run_def
    1.92 +  scomp_def fcomp_def run_def
    1.93  
    1.94  subsection {* ML abstract operations *}
    1.95  
    1.96 @@ -194,7 +183,7 @@
    1.97  
    1.98  fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
    1.99  
   1.100 -fun mbind T1 T2 sT f g = Const (@{const_name mbind},
   1.101 +fun scomp T1 T2 sT f g = Const (@{const_name scomp},
   1.102    liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   1.103  
   1.104  fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
   1.105 @@ -216,7 +205,7 @@
   1.106  syntax
   1.107    "_do" :: "do_expr \<Rightarrow> 'a"
   1.108      ("do _ done" [12] 12)
   1.109 -  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.110 +  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.111      ("_ <- _;// _" [1000, 13, 12] 12)
   1.112    "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.113      ("_;// _" [13, 12] 12)
   1.114 @@ -226,12 +215,12 @@
   1.115      ("_" [12] 12)
   1.116  
   1.117  syntax (xsymbols)
   1.118 -  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.119 +  "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.120      ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   1.121  
   1.122  translations
   1.123    "_do f" => "CONST run f"
   1.124 -  "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   1.125 +  "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   1.126    "_fcomp f g" => "f \<guillemotright> g"
   1.127    "_let x t f" => "CONST Let t (\<lambda>x. f)"
   1.128    "_nil f" => "f"
   1.129 @@ -246,10 +235,10 @@
   1.130          let
   1.131            val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
   1.132          in ((v, dummyT), t) end
   1.133 -  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
   1.134 +  fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
   1.135          let
   1.136            val ((v, ty), g') = dest_abs_eta g;
   1.137 -        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   1.138 +        in Const ("_scomp", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   1.139      | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
   1.140          Const ("_fcomp", dummyT) $ f $ unfold_monad g
   1.141      | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =