changeset 28145 af3923ed4786 parent 27487 c8a6ce181805 child 29799 7c7f759c438e
```     1.1 --- a/src/HOL/Library/State_Monad.thy	Fri Sep 05 11:50:35 2008 +0200
1.2 +++ b/src/HOL/Library/State_Monad.thy	Sat Sep 06 14:02:36 2008 +0200
1.3 @@ -56,31 +56,23 @@
1.4    we use a set of monad combinators:
1.5  *}
1.6
1.7 -notation fcomp (infixl ">>" 60)
1.8 -notation (xsymbols) fcomp (infixl "\<guillemotright>" 60)
1.9 -notation scomp (infixl ">>=" 60)
1.10 -notation (xsymbols) scomp (infixl "\<guillemotright>=" 60)
1.11 +notation fcomp (infixl "o>" 60)
1.12 +notation (xsymbols) fcomp (infixl "o>" 60)
1.13 +notation scomp (infixl "o->" 60)
1.14 +notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
1.15
1.16  abbreviation (input)
1.17    "return \<equiv> Pair"
1.18
1.19 -definition
1.20 -  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
1.21 -  "run f = f"
1.22 -
1.23 -print_ast_translation {*
1.24 -  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
1.25 -*}
1.26 -
1.27  text {*
1.28    Given two transformations @{term f} and @{term g}, they
1.29 -  may be directly composed using the @{term "op \<guillemotright>"} combinator,
1.30 -  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
1.31 +  may be directly composed using the @{term "op o>"} combinator,
1.32 +  forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
1.33
1.34    After any yielding transformation, we bind the side result
1.35    immediately using a lambda abstraction.  This
1.36 -  is the purpose of the @{term "op \<guillemotright>="} combinator:
1.37 -  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
1.38 +  is the purpose of the @{term "op o\<rightarrow>"} combinator:
1.39 +  @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
1.40
1.41    For queries, the existing @{term "Let"} is appropriate.
1.42
1.43 @@ -88,8 +80,6 @@
1.44    it to the state from the left;  we introduce the
1.45    suggestive abbreviation @{term return} for this purpose.
1.46
1.47 -  The @{const run} ist just a marker.
1.48 -
1.49    The most crucial distinction to Haskell is that we do
1.50    not need to introduce distinguished type constructors
1.51    for different kinds of state.  This has two consequences:
1.52 @@ -107,22 +97,6 @@
1.53  *}
1.54
1.55
1.56 -subsection {* Obsolete runs *}
1.57 -
1.58 -text {*
1.59 -  @{term run} is just a doodle and should not occur nested:
1.60 -*}
1.61 -
1.62 -lemma run_simp [simp]:
1.63 -  "\<And>f. run (run f) = run f"
1.64 -  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
1.65 -  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
1.66 -  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
1.67 -  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
1.68 -  "\<And>f. f = run f \<longleftrightarrow> True"
1.69 -  "\<And>f. run f = f \<longleftrightarrow> True"
1.70 -  unfolding run_def by rule+
1.71 -
1.72  subsection {* Monad laws *}
1.73
1.74  text {*
1.75 @@ -130,66 +104,14 @@
1.76    as normalization rules for monadic expressions:
1.77  *}
1.78
1.79 -lemma
1.80 -  return_scomp [simp]: "return x \<guillemotright>= f = f x"
1.81 -  unfolding scomp_def by (simp add: expand_fun_eq)
1.82 -
1.83 -lemma
1.84 -  scomp_return [simp]: "x \<guillemotright>= return = x"
1.85 -  unfolding scomp_def by (simp add: expand_fun_eq split_Pair)
1.86 -
1.87 -lemma
1.88 -  id_fcomp [simp]: "id \<guillemotright> f = f"
1.89 -  unfolding fcomp_def by simp
1.90 -
1.91 -lemma
1.92 -  fcomp_id [simp]: "f \<guillemotright> id = f"
1.93 -  unfolding fcomp_def by simp
1.94 -
1.95 -lemma
1.96 -  scomp_scomp [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
1.97 -  unfolding scomp_def by (simp add: split_def expand_fun_eq)
1.98 -
1.99 -lemma
1.100 -  scomp_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
1.101 -  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
1.102 -
1.103 -lemma
1.104 -  fcomp_scomp [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
1.105 -  unfolding scomp_def fcomp_def by (simp add: split_def expand_fun_eq)
1.106 -
1.107 -lemma
1.108 -  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
1.109 -  unfolding fcomp_def o_assoc ..
1.110 -
1.111 -lemmas monad_simp = run_simp return_scomp scomp_return id_fcomp fcomp_id
1.112 -  scomp_scomp scomp_fcomp fcomp_scomp fcomp_fcomp
1.113 +lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
1.114 +  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
1.115
1.116  text {*
1.117    Evaluation of monadic expressions by force:
1.118  *}
1.119
1.121 -  scomp_def fcomp_def run_def
1.122 -
1.123 -subsection {* ML abstract operations *}
1.124 -
1.125 -ML {*
1.127 -struct
1.128 -
1.129 -fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
1.130 -fun liftT' sT = sT --> sT;
1.131 -
1.132 -fun return T sT x = Const (@{const_name return}, T --> liftT T sT) \$ x;
1.133 -
1.134 -fun scomp T1 T2 sT f g = Const (@{const_name scomp},
1.135 -  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) \$ f \$ g;
1.136 -
1.137 -fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) \$ f;
1.138 -
1.139 -end;
1.140 -*}
1.142
1.143
1.144  subsection {* Syntax *}
1.145 @@ -211,7 +133,7 @@
1.146      ("_;// _" [13, 12] 12)
1.147    "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
1.148      ("let _ = _;// _" [1000, 13, 12] 12)
1.149 -  "_nil" :: "'a \<Rightarrow> do_expr"
1.150 +  "_done" :: "'a \<Rightarrow> do_expr"
1.151      ("_" [12] 12)
1.152
1.153  syntax (xsymbols)
1.154 @@ -219,95 +141,55 @@
1.155      ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
1.156
1.157  translations
1.158 -  "_do f" => "CONST run f"
1.159 -  "_scomp x f g" => "f \<guillemotright>= (\<lambda>x. g)"
1.160 -  "_fcomp f g" => "f \<guillemotright> g"
1.161 +  "_do f" => "f"
1.162 +  "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
1.163 +  "_fcomp f g" => "f o> g"
1.164    "_let x t f" => "CONST Let t (\<lambda>x. f)"
1.165 -  "_nil f" => "f"
1.166 +  "_done f" => "f"
1.167
1.168  print_translation {*
1.169  let
1.170    fun dest_abs_eta (Abs (abs as (_, ty, _))) =
1.171          let
1.172            val (v, t) = Syntax.variant_abs abs;
1.173 -        in ((v, ty), t) end
1.174 +        in (Free (v, ty), t) end
1.175      | dest_abs_eta t =
1.176          let
1.177            val (v, t) = Syntax.variant_abs ("", dummyT, t \$ Bound 0);
1.178 -        in ((v, dummyT), t) end
1.179 +        in (Free (v, dummyT), t) end;
1.180    fun unfold_monad (Const (@{const_syntax scomp}, _) \$ f \$ g) =
1.181          let
1.182 -          val ((v, ty), g') = dest_abs_eta g;
1.183 -        in Const ("_scomp", dummyT) \$ Free (v, ty) \$ f \$ unfold_monad g' end
1.184 +          val (v, g') = dest_abs_eta g;
1.185 +        in Const ("_scomp", dummyT) \$ v \$ f \$ unfold_monad g' end
1.186      | unfold_monad (Const (@{const_syntax fcomp}, _) \$ f \$ g) =
1.187          Const ("_fcomp", dummyT) \$ f \$ unfold_monad g
1.188      | unfold_monad (Const (@{const_syntax Let}, _) \$ f \$ g) =
1.189          let
1.190 -          val ((v, ty), g') = dest_abs_eta g;
1.191 -        in Const ("_let", dummyT) \$ Free (v, ty) \$ f \$ unfold_monad g' end
1.192 +          val (v, g') = dest_abs_eta g;
1.193 +        in Const ("_let", dummyT) \$ v \$ f \$ unfold_monad g' end
1.194      | unfold_monad (Const (@{const_syntax Pair}, _) \$ f) =
1.195          Const ("return", dummyT) \$ f
1.196      | unfold_monad f = f;
1.197 -  fun tr' (f::ts) =
1.198 -    list_comb (Const ("_do", dummyT) \$ unfold_monad f, ts)
1.199 -in [(@{const_syntax "run"}, tr')] end;
1.200 +  fun contains_scomp (Const (@{const_syntax scomp}, _) \$ _ \$ _) = true
1.201 +    | contains_scomp (Const (@{const_syntax fcomp}, _) \$ _ \$ t) =
1.202 +        contains_scomp t
1.203 +    | contains_scomp (Const (@{const_syntax Let}, _) \$ _ \$ Abs (_, _, t)) =
1.204 +        contains_scomp t;
1.205 +  fun scomp_monad_tr' (f::g::ts) = list_comb
1.206 +    (Const ("_do", dummyT) \$ unfold_monad (Const (@{const_syntax scomp}, dummyT) \$ f \$ g), ts);
1.207 +  fun fcomp_monad_tr' (f::g::ts) = if contains_scomp g then list_comb
1.208 +      (Const ("_do", dummyT) \$ unfold_monad (Const (@{const_syntax fcomp}, dummyT) \$ f \$ g), ts)
1.209 +    else raise Match;
1.210 +  fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_scomp g' then list_comb
1.211 +      (Const ("_do", dummyT) \$ unfold_monad (Const (@{const_syntax Let}, dummyT) \$ f \$ g), ts)
1.212 +    else raise Match;
1.213 +in [
1.217 +] end;
1.218  *}
1.219
1.220 -
1.221 -subsection {* Combinators *}
1.222 -
1.223 -definition
1.224 -  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
1.225 -  "lift f x = return (f x)"
1.226 -
1.227 -primrec
1.228 -  list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
1.229 -  "list f [] = id"
1.230 -| "list f (x#xs) = (do f x; list f xs done)"
1.231 -
1.232 -primrec
1.233 -  list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
1.234 -  "list_yield f [] = return []"
1.235 -| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
1.236 -
1.237 -definition
1.238 -  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
1.239 -  "collapse f = (do g \<leftarrow> f; g done)"
1.240 -
1.241 -text {* combinator properties *}
1.242 -
1.243 -lemma list_append [simp]:
1.244 -  "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
1.245 -  by (induct xs) (simp_all del: id_apply)
1.246 -
1.247 -lemma list_cong [fundef_cong, recdef_cong]:
1.248 -  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
1.249 -    \<Longrightarrow> list f xs = list g ys"
1.250 -proof (induct xs arbitrary: ys)
1.251 -  case Nil then show ?case by simp
1.252 -next
1.253 -  case (Cons x xs)
1.254 -  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
1.255 -  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
1.256 -  with Cons have "list f xs = list g xs" by auto
1.257 -  with Cons have "list f (x # xs) = list g (x # xs)" by auto
1.258 -  with Cons show "list f (x # xs) = list g ys" by auto
1.259 -qed
1.260 -
1.261 -lemma list_yield_cong [fundef_cong, recdef_cong]:
1.262 -  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
1.263 -    \<Longrightarrow> list_yield f xs = list_yield g ys"
1.264 -proof (induct xs arbitrary: ys)
1.265 -  case Nil then show ?case by simp
1.266 -next
1.267 -  case (Cons x xs)
1.268 -  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
1.269 -  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
1.270 -  with Cons have "list_yield f xs = list_yield g xs" by auto
1.271 -  with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
1.272 -  with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
1.273 -qed
1.274 -
1.275  text {*
1.276    For an example, see HOL/ex/Random.thy.
1.277  *}
```