src/HOL/Library/State_Monad.thy
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.120 -lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   1.121 -  scomp_def fcomp_def run_def
   1.122 -
   1.123 -subsection {* ML abstract operations *}
   1.124 -
   1.125 -ML {*
   1.126 -structure StateMonad =
   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.141 +lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
   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.214 +  (@{const_syntax scomp}, scomp_monad_tr'),
   1.215 +  (@{const_syntax fcomp}, fcomp_monad_tr'),
   1.216 +  (@{const_syntax Let}, Let_monad_tr')
   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  *}