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.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) =
```