src/HOL/Library/State_Monad.thy
changeset 21192 5fe5cd5fede7
child 21283 b15355b9a59d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Nov 06 16:28:33 2006 +0100
     1.3 @@ -0,0 +1,248 @@
     1.4 +(*  Title:      HOL/Library/State_Monad.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Combinators syntax for generic, open state monads (single threaded monads) *}
    1.10 +
    1.11 +theory State_Monad
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +section {* Generic, open state monads *}
    1.16 +
    1.17 +subsection {* Motivation *}
    1.18 +
    1.19 +text {*
    1.20 +  The logic HOL has no notion of constructor classes, so
    1.21 +  it is not possible to model monads the Haskell way
    1.22 +  in full genericity in Isabelle/HOL.
    1.23 +  
    1.24 +  However, this theory provides substantial support for
    1.25 +  a very common class of monads: \emph{state monads}
    1.26 +  (or \emph{single-threaded monads}, since a state
    1.27 +  is transformed single-threaded).
    1.28 +
    1.29 +  To enter from the Haskell world,
    1.30 +  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
    1.31 +  makes a good motivating start.  Here we just sketch briefly
    1.32 +  how those monads enter the game of Isabelle/HOL.
    1.33 +*}
    1.34 +
    1.35 +subsection {* State transformations and combinators *}
    1.36 +
    1.37 +(*<*)
    1.38 +typedecl \<alpha>
    1.39 +typedecl \<beta>
    1.40 +typedecl \<gamma>
    1.41 +typedecl \<sigma>
    1.42 +typedecl \<sigma>'
    1.43 +(*>*)
    1.44 +
    1.45 +text {*
    1.46 +  We classify functions operating on states into two categories:
    1.47 +
    1.48 +  \begin{description}
    1.49 +    \item[transformations]
    1.50 +      with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
    1.51 +      transforming a state.
    1.52 +    \item[``yielding'' transformations]
    1.53 +      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
    1.54 +      ``yielding'' a side result while transforming a state.
    1.55 +    \item[queries]
    1.56 +      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
    1.57 +      computing a result dependent on a state.
    1.58 +  \end{description}
    1.59 +
    1.60 +  By convention we write @{typ "\<sigma>"} for types representing states
    1.61 +  and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
    1.62 +  for types representing side results.  Type changes due
    1.63 +  to transformations are not excluded in our scenario.
    1.64 +
    1.65 +  We aim to assert that values of any state type @{typ "\<sigma>"}
    1.66 +  are used in a single-threaded way: after application
    1.67 +  of a transformation on a value of type @{typ "\<sigma>"}, the
    1.68 +  former value should not be used again.  To achieve this,
    1.69 +  we use a set of monad combinators:
    1.70 +*}
    1.71 +
    1.72 +definition
    1.73 +  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    1.74 +    (infixl "\<guillemotright>=" 60)
    1.75 +  "f \<guillemotright>= g = split g \<circ> f"
    1.76 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.77 +    (infixl "\<guillemotright>" 60)
    1.78 +  "f \<guillemotright> g = g \<circ> f"
    1.79 +  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.80 +  "run f = f"
    1.81 +
    1.82 +syntax (input)
    1.83 +  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    1.84 +    (infixl ">>=" 60)
    1.85 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    1.86 +    (infixl ">>" 60)
    1.87 +
    1.88 +abbreviation (input)
    1.89 +  "return \<equiv> Pair"
    1.90 +
    1.91 +text {*
    1.92 +  Given two transformations @{term f} and @{term g}, they
    1.93 +  may be directly composed using the @{term "op \<guillemotright>"} combinator,
    1.94 +  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
    1.95 +
    1.96 +  After any yielding transformation, we bind the side result
    1.97 +  immediately using a lambda abstraction.  This 
    1.98 +  is the purpose of the @{term "op \<guillemotright>="} combinator:
    1.99 +  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
   1.100 +
   1.101 +  For queries, the existing @{term "Let"} is appropriate.
   1.102 +
   1.103 +  Naturally, a computation may yield a side result by pairing
   1.104 +  it to the state from the left;  we introduce the
   1.105 +  suggestive abbreviation @{term return} for this purpose.
   1.106 +
   1.107 +  The @{const run} ist just a marker.
   1.108 +
   1.109 +  The most crucial distinction to Haskell is that we do
   1.110 +  not need to introduce distinguished type constructors
   1.111 +  for different kinds of state.  This has two consequences:
   1.112 +  \begin{itemize}
   1.113 +    \item The monad model does not state anything about
   1.114 +       the kind of state; the model for the state is
   1.115 +       completely orthogonal and has (or may) be
   1.116 +       specified completely independent.
   1.117 +    \item There is no distinguished type constructor
   1.118 +       encapsulating away the state transformation, i.e.~transformations
   1.119 +       may be applied directly without using any lifting
   1.120 +       or providing and dropping units (``open monad'').
   1.121 +    \item The type of states may change due to a transformation.
   1.122 +  \end{itemize}
   1.123 +*}
   1.124 +
   1.125 +
   1.126 +subsection {* Obsolete runs *}
   1.127 +
   1.128 +text {*
   1.129 +  @{term run} is just a doodle and should not occur nested:
   1.130 +*}
   1.131 +
   1.132 +lemma run_simp [simp]:
   1.133 +  "\<And>f. run (run f) = run f"
   1.134 +  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
   1.135 +  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
   1.136 +  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
   1.137 +  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
   1.138 +  "\<And>f. f = run f \<longleftrightarrow> True"
   1.139 +  "\<And>f. run f = f \<longleftrightarrow> True"
   1.140 +  unfolding run_def by rule+
   1.141 +
   1.142 +
   1.143 +subsection {* Monad laws *}
   1.144 +
   1.145 +text {*
   1.146 +  The common monadic laws hold and may also be used
   1.147 +  as normalization rules for monadic expressions:
   1.148 +*}
   1.149 +
   1.150 +lemma
   1.151 +  return_mbind [simp]: "return x \<guillemotright>= f = f x"
   1.152 +  unfolding mbind_def by (simp add: expand_fun_eq)
   1.153 +
   1.154 +lemma
   1.155 +  mbind_return [simp]: "x \<guillemotright>= return = x"
   1.156 +  unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
   1.157 +
   1.158 +lemma
   1.159 +  mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
   1.160 +  unfolding mbind_def by (simp add: split_def expand_fun_eq)
   1.161 +
   1.162 +lemma
   1.163 +  mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
   1.164 +  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   1.165 +
   1.166 +lemma
   1.167 +  fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
   1.168 +  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   1.169 +
   1.170 +lemma
   1.171 +  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
   1.172 +  unfolding fcomp_def o_assoc ..
   1.173 +
   1.174 +lemmas monad_simp = run_simp return_mbind mbind_return
   1.175 +  mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
   1.176 +
   1.177 +text {*
   1.178 +  Evaluation of monadic expressions by force:
   1.179 +*}
   1.180 +
   1.181 +lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   1.182 +  mbind_def fcomp_def run_def
   1.183 +
   1.184 +subsection {* Syntax *}
   1.185 +
   1.186 +text {*
   1.187 +  We provide a convenient do-notation for monadic expressions
   1.188 +  well-known from Haskell.  @{const Let} is printed
   1.189 +  specially in do-expressions.
   1.190 +*}
   1.191 +
   1.192 +nonterminals do_expr
   1.193 +
   1.194 +syntax
   1.195 +  "_do" :: "do_expr \<Rightarrow> 'a"
   1.196 +    ("do _ done" [12] 12)
   1.197 +  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.198 +    ("_ <- _;// _" [1000, 13, 12] 12)
   1.199 +  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.200 +    ("_;// _" [13, 12] 12)
   1.201 +  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.202 +    ("let _ = _;// _" [1000, 13, 12] 12)
   1.203 +  "_nil" :: "'a \<Rightarrow> do_expr"
   1.204 +    ("_" [12] 12)
   1.205 +
   1.206 +syntax (xsymbols)
   1.207 +  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   1.208 +    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   1.209 +
   1.210 +translations
   1.211 +  "_do f" => "State_Monad.run f"
   1.212 +  "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   1.213 +  "_fcomp f g" => "f \<guillemotright> g"
   1.214 +  "_let x t f" => "Let t (\<lambda>x. f)"
   1.215 +  "_nil f" => "f"
   1.216 +
   1.217 +print_translation {*
   1.218 +let
   1.219 +  val syntax_name = Sign.const_syntax_name (the_context ());
   1.220 +  val name_mbind = syntax_name "State_Monad.mbind";
   1.221 +  val name_fcomp = syntax_name "State_Monad.fcomp";
   1.222 +  fun unfold_monad (t as Const (name, _) $ f $ g) =
   1.223 +        if name = name_mbind then let
   1.224 +            val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   1.225 +          in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   1.226 +        else if name = name_fcomp then
   1.227 +          Const ("_fcomp", dummyT) $ f $ unfold_monad g
   1.228 +        else t
   1.229 +    | unfold_monad (Const ("Let", _) $ f $ g) =
   1.230 +        let
   1.231 +          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   1.232 +        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   1.233 +    | unfold_monad (Const ("Pair", _) $ f) =
   1.234 +        Const ("return", dummyT) $ f
   1.235 +    | unfold_monad f = f;
   1.236 +  fun tr' (f::ts) =
   1.237 +    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   1.238 +in [
   1.239 +  (syntax_name "State_Monad.run", tr')
   1.240 +] end;
   1.241 +*}
   1.242 +
   1.243 +print_ast_translation {*[
   1.244 +  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
   1.245 +]*}
   1.246 +
   1.247 +text {*
   1.248 +  For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
   1.249 +*}
   1.250 +
   1.251 +end
   1.252 \ No newline at end of file