added state monad to HOL library
authorhaftmann
Mon Nov 06 16:28:33 2006 +0100 (2006-11-06)
changeset 211925fe5cd5fede7
parent 21191 c00161fbf990
child 21193 25a5ab43a5ff
added state monad to HOL library
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Library/document/root.tex
src/HOL/Library/State_Monad.thy
src/HOL/ex/CodeRandom.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Nov 06 16:28:31 2006 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 06 16:28:33 2006 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
     1.5    Library/MLString.thy Library/Infinite_Set.thy \
     1.6    Library/FuncSet.thy Library/Library.thy \
     1.7 -  Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
     1.8 +  Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
     1.9    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
    1.10    Library/Nat_Infinity.thy Library/Word.thy Library/word_setup.ML \
    1.11    Library/README.html Library/Continuity.thy \
     2.1 --- a/src/HOL/Library/Library.thy	Mon Nov 06 16:28:31 2006 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Mon Nov 06 16:28:33 2006 +0100
     2.3 @@ -25,6 +25,7 @@
     2.4    Coinductive_List
     2.5    AssocList
     2.6    Infinite_Set
     2.7 +  State_Monad
     2.8  begin
     2.9  end
    2.10  (*>*)
     3.1 --- a/src/HOL/Library/Library/document/root.tex	Mon Nov 06 16:28:31 2006 +0100
     3.2 +++ b/src/HOL/Library/Library/document/root.tex	Mon Nov 06 16:28:33 2006 +0100
     3.3 @@ -21,6 +21,7 @@
     3.4  
     3.5  \renewcommand{\isamarkupheader}[1]%
     3.6  {\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
     3.7 +\renewcommand{\isasymguillemotright}{$\gg$}
     3.8  
     3.9  \parindent 0pt \parskip 0.5ex
    3.10  \input{session}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Nov 06 16:28:33 2006 +0100
     4.3 @@ -0,0 +1,248 @@
     4.4 +(*  Title:      HOL/Library/State_Monad.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Florian Haftmann, TU Muenchen
     4.7 +*)
     4.8 +
     4.9 +header {* Combinators syntax for generic, open state monads (single threaded monads) *}
    4.10 +
    4.11 +theory State_Monad
    4.12 +imports Main
    4.13 +begin
    4.14 +
    4.15 +section {* Generic, open state monads *}
    4.16 +
    4.17 +subsection {* Motivation *}
    4.18 +
    4.19 +text {*
    4.20 +  The logic HOL has no notion of constructor classes, so
    4.21 +  it is not possible to model monads the Haskell way
    4.22 +  in full genericity in Isabelle/HOL.
    4.23 +  
    4.24 +  However, this theory provides substantial support for
    4.25 +  a very common class of monads: \emph{state monads}
    4.26 +  (or \emph{single-threaded monads}, since a state
    4.27 +  is transformed single-threaded).
    4.28 +
    4.29 +  To enter from the Haskell world,
    4.30 +  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
    4.31 +  makes a good motivating start.  Here we just sketch briefly
    4.32 +  how those monads enter the game of Isabelle/HOL.
    4.33 +*}
    4.34 +
    4.35 +subsection {* State transformations and combinators *}
    4.36 +
    4.37 +(*<*)
    4.38 +typedecl \<alpha>
    4.39 +typedecl \<beta>
    4.40 +typedecl \<gamma>
    4.41 +typedecl \<sigma>
    4.42 +typedecl \<sigma>'
    4.43 +(*>*)
    4.44 +
    4.45 +text {*
    4.46 +  We classify functions operating on states into two categories:
    4.47 +
    4.48 +  \begin{description}
    4.49 +    \item[transformations]
    4.50 +      with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
    4.51 +      transforming a state.
    4.52 +    \item[``yielding'' transformations]
    4.53 +      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
    4.54 +      ``yielding'' a side result while transforming a state.
    4.55 +    \item[queries]
    4.56 +      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
    4.57 +      computing a result dependent on a state.
    4.58 +  \end{description}
    4.59 +
    4.60 +  By convention we write @{typ "\<sigma>"} for types representing states
    4.61 +  and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
    4.62 +  for types representing side results.  Type changes due
    4.63 +  to transformations are not excluded in our scenario.
    4.64 +
    4.65 +  We aim to assert that values of any state type @{typ "\<sigma>"}
    4.66 +  are used in a single-threaded way: after application
    4.67 +  of a transformation on a value of type @{typ "\<sigma>"}, the
    4.68 +  former value should not be used again.  To achieve this,
    4.69 +  we use a set of monad combinators:
    4.70 +*}
    4.71 +
    4.72 +definition
    4.73 +  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    4.74 +    (infixl "\<guillemotright>=" 60)
    4.75 +  "f \<guillemotright>= g = split g \<circ> f"
    4.76 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    4.77 +    (infixl "\<guillemotright>" 60)
    4.78 +  "f \<guillemotright> g = g \<circ> f"
    4.79 +  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    4.80 +  "run f = f"
    4.81 +
    4.82 +syntax (input)
    4.83 +  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
    4.84 +    (infixl ">>=" 60)
    4.85 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
    4.86 +    (infixl ">>" 60)
    4.87 +
    4.88 +abbreviation (input)
    4.89 +  "return \<equiv> Pair"
    4.90 +
    4.91 +text {*
    4.92 +  Given two transformations @{term f} and @{term g}, they
    4.93 +  may be directly composed using the @{term "op \<guillemotright>"} combinator,
    4.94 +  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
    4.95 +
    4.96 +  After any yielding transformation, we bind the side result
    4.97 +  immediately using a lambda abstraction.  This 
    4.98 +  is the purpose of the @{term "op \<guillemotright>="} combinator:
    4.99 +  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
   4.100 +
   4.101 +  For queries, the existing @{term "Let"} is appropriate.
   4.102 +
   4.103 +  Naturally, a computation may yield a side result by pairing
   4.104 +  it to the state from the left;  we introduce the
   4.105 +  suggestive abbreviation @{term return} for this purpose.
   4.106 +
   4.107 +  The @{const run} ist just a marker.
   4.108 +
   4.109 +  The most crucial distinction to Haskell is that we do
   4.110 +  not need to introduce distinguished type constructors
   4.111 +  for different kinds of state.  This has two consequences:
   4.112 +  \begin{itemize}
   4.113 +    \item The monad model does not state anything about
   4.114 +       the kind of state; the model for the state is
   4.115 +       completely orthogonal and has (or may) be
   4.116 +       specified completely independent.
   4.117 +    \item There is no distinguished type constructor
   4.118 +       encapsulating away the state transformation, i.e.~transformations
   4.119 +       may be applied directly without using any lifting
   4.120 +       or providing and dropping units (``open monad'').
   4.121 +    \item The type of states may change due to a transformation.
   4.122 +  \end{itemize}
   4.123 +*}
   4.124 +
   4.125 +
   4.126 +subsection {* Obsolete runs *}
   4.127 +
   4.128 +text {*
   4.129 +  @{term run} is just a doodle and should not occur nested:
   4.130 +*}
   4.131 +
   4.132 +lemma run_simp [simp]:
   4.133 +  "\<And>f. run (run f) = run f"
   4.134 +  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
   4.135 +  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
   4.136 +  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
   4.137 +  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
   4.138 +  "\<And>f. f = run f \<longleftrightarrow> True"
   4.139 +  "\<And>f. run f = f \<longleftrightarrow> True"
   4.140 +  unfolding run_def by rule+
   4.141 +
   4.142 +
   4.143 +subsection {* Monad laws *}
   4.144 +
   4.145 +text {*
   4.146 +  The common monadic laws hold and may also be used
   4.147 +  as normalization rules for monadic expressions:
   4.148 +*}
   4.149 +
   4.150 +lemma
   4.151 +  return_mbind [simp]: "return x \<guillemotright>= f = f x"
   4.152 +  unfolding mbind_def by (simp add: expand_fun_eq)
   4.153 +
   4.154 +lemma
   4.155 +  mbind_return [simp]: "x \<guillemotright>= return = x"
   4.156 +  unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
   4.157 +
   4.158 +lemma
   4.159 +  mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
   4.160 +  unfolding mbind_def by (simp add: split_def expand_fun_eq)
   4.161 +
   4.162 +lemma
   4.163 +  mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
   4.164 +  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   4.165 +
   4.166 +lemma
   4.167 +  fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
   4.168 +  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
   4.169 +
   4.170 +lemma
   4.171 +  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
   4.172 +  unfolding fcomp_def o_assoc ..
   4.173 +
   4.174 +lemmas monad_simp = run_simp return_mbind mbind_return
   4.175 +  mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
   4.176 +
   4.177 +text {*
   4.178 +  Evaluation of monadic expressions by force:
   4.179 +*}
   4.180 +
   4.181 +lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
   4.182 +  mbind_def fcomp_def run_def
   4.183 +
   4.184 +subsection {* Syntax *}
   4.185 +
   4.186 +text {*
   4.187 +  We provide a convenient do-notation for monadic expressions
   4.188 +  well-known from Haskell.  @{const Let} is printed
   4.189 +  specially in do-expressions.
   4.190 +*}
   4.191 +
   4.192 +nonterminals do_expr
   4.193 +
   4.194 +syntax
   4.195 +  "_do" :: "do_expr \<Rightarrow> 'a"
   4.196 +    ("do _ done" [12] 12)
   4.197 +  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   4.198 +    ("_ <- _;// _" [1000, 13, 12] 12)
   4.199 +  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   4.200 +    ("_;// _" [13, 12] 12)
   4.201 +  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   4.202 +    ("let _ = _;// _" [1000, 13, 12] 12)
   4.203 +  "_nil" :: "'a \<Rightarrow> do_expr"
   4.204 +    ("_" [12] 12)
   4.205 +
   4.206 +syntax (xsymbols)
   4.207 +  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   4.208 +    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
   4.209 +
   4.210 +translations
   4.211 +  "_do f" => "State_Monad.run f"
   4.212 +  "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   4.213 +  "_fcomp f g" => "f \<guillemotright> g"
   4.214 +  "_let x t f" => "Let t (\<lambda>x. f)"
   4.215 +  "_nil f" => "f"
   4.216 +
   4.217 +print_translation {*
   4.218 +let
   4.219 +  val syntax_name = Sign.const_syntax_name (the_context ());
   4.220 +  val name_mbind = syntax_name "State_Monad.mbind";
   4.221 +  val name_fcomp = syntax_name "State_Monad.fcomp";
   4.222 +  fun unfold_monad (t as Const (name, _) $ f $ g) =
   4.223 +        if name = name_mbind then let
   4.224 +            val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   4.225 +          in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   4.226 +        else if name = name_fcomp then
   4.227 +          Const ("_fcomp", dummyT) $ f $ unfold_monad g
   4.228 +        else t
   4.229 +    | unfold_monad (Const ("Let", _) $ f $ g) =
   4.230 +        let
   4.231 +          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
   4.232 +        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
   4.233 +    | unfold_monad (Const ("Pair", _) $ f) =
   4.234 +        Const ("return", dummyT) $ f
   4.235 +    | unfold_monad f = f;
   4.236 +  fun tr' (f::ts) =
   4.237 +    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
   4.238 +in [
   4.239 +  (syntax_name "State_Monad.run", tr')
   4.240 +] end;
   4.241 +*}
   4.242 +
   4.243 +print_ast_translation {*[
   4.244 +  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
   4.245 +]*}
   4.246 +
   4.247 +text {*
   4.248 +  For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
   4.249 +*}
   4.250 +
   4.251 +end
   4.252 \ No newline at end of file
     5.1 --- a/src/HOL/ex/CodeRandom.thy	Mon Nov 06 16:28:31 2006 +0100
     5.2 +++ b/src/HOL/ex/CodeRandom.thy	Mon Nov 06 16:28:33 2006 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* A simple random engine *}
     5.5  
     5.6  theory CodeRandom
     5.7 -imports CodeRevappl
     5.8 +imports State_Monad
     5.9  begin
    5.10  
    5.11  section {* A simple random engine *}
    5.12 @@ -46,20 +46,20 @@
    5.13  
    5.14  definition
    5.15    select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
    5.16 -  [simp]: "select xs s =
    5.17 -    s
    5.18 -    \<triangleright> random (length xs)
    5.19 -    \<turnstile>\<triangleright> (\<lambda>n. Pair (nth xs n))"
    5.20 +  [simp]: "select xs = (do
    5.21 +      n \<leftarrow> random (length xs);
    5.22 +      return (nth xs n)
    5.23 +    done)"
    5.24    select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
    5.25 -  [simp]: "select_weight xs s =
    5.26 -    s
    5.27 -    \<triangleright> random (foldl (op +) 0 (map fst xs))
    5.28 -    \<turnstile>\<triangleright> (\<lambda>n. Pair (pick xs n))"
    5.29 +  [simp]: "select_weight xs = (do
    5.30 +      n \<leftarrow> random (foldl (op +) 0 (map fst xs));
    5.31 +      return (pick xs n)
    5.32 +    done)"
    5.33  
    5.34  lemma
    5.35    "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
    5.36  proof (induct xs)
    5.37 -  case Nil show ?case by (simp add: revappl random_def)
    5.38 +  case Nil show ?case by (simp add: monad_collapse random_def)
    5.39  next
    5.40    have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
    5.41    proof -
    5.42 @@ -113,18 +113,22 @@
    5.43      from pick_nth [OF bound] show
    5.44        "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
    5.45    qed
    5.46 +  have pick_nth_random_do:
    5.47 +    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
    5.48 +      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
    5.49 +  unfolding monad_collapse split_def unfolding pick_nth_random ..
    5.50    case (Cons x xs) then show ?case
    5.51 -    unfolding select_weight_def sum_length revappl_split pick_nth_random
    5.52 -    by (simp add: revappl_split)
    5.53 +    unfolding select_weight_def sum_length pick_nth_random_do
    5.54 +    by simp
    5.55  qed
    5.56  
    5.57  definition
    5.58    random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
    5.59 -  "random_int k s = (let (l, s') = random (nat k) s in (int l, s'))"
    5.60 +  "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
    5.61  
    5.62  lemma random_nat [code]:
    5.63 -  "random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
    5.64 -unfolding random_int_def Let_def split_def random_def by simp
    5.65 +  "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
    5.66 +unfolding random_int_def by simp
    5.67  
    5.68  axiomatization
    5.69    run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
    5.70 @@ -184,4 +188,6 @@
    5.71  code_gen select select_weight
    5.72    (SML *)
    5.73  
    5.74 +code_gen (SML -)
    5.75 +
    5.76  end
    5.77 \ No newline at end of file