src/HOL/Library/State_Monad.thy
changeset 26260 23ce0d32de11
parent 26141 e1b3a6953cdc
child 26266 35ae83ca190a
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Mar 12 08:47:35 2008 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Mar 12 08:47:36 2008 +0100
     1.3 @@ -115,8 +115,8 @@
     1.4    \begin{itemize}
     1.5      \item The monad model does not state anything about
     1.6         the kind of state; the model for the state is
     1.7 -       completely orthogonal and has to (or may) be
     1.8 -       specified completely independent.
     1.9 +       completely orthogonal and may be
    1.10 +       specified completely independently.
    1.11      \item There is no distinguished type constructor
    1.12         encapsulating away the state transformation, i.e.~transformations
    1.13         may be applied directly without using any lifting
    1.14 @@ -191,6 +191,26 @@
    1.15  lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
    1.16    mbind_def fcomp_def run_def
    1.17  
    1.18 +subsection {* ML abstract operations *}
    1.19 +
    1.20 +ML {*
    1.21 +structure StateMonad =
    1.22 +struct
    1.23 +
    1.24 +fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    1.25 +fun liftT' sT = sT --> sT;
    1.26 +
    1.27 +fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
    1.28 +
    1.29 +fun mbind T1 T2 sT f g = Const (@{const_name mbind},
    1.30 +  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    1.31 +
    1.32 +fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
    1.33 +
    1.34 +end;
    1.35 +*}
    1.36 +
    1.37 +
    1.38  subsection {* Syntax *}
    1.39  
    1.40  text {*
    1.41 @@ -270,8 +290,7 @@
    1.42  | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
    1.43  
    1.44  definition
    1.45 -  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
    1.46 -  where
    1.47 +  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    1.48    "collapse f = (do g \<leftarrow> f; g done)"
    1.49  
    1.50  text {* combinator properties *}