# HG changeset patch
# User haftmann
# Date 1162826913 -3600
# Node ID 5fe5cd5fede7ed54362afbd889d16791e1d63916
# Parent  c00161fbf9905702c332739bbece1b86a90906aa
added state monad to HOL library

diff -r c00161fbf990 -r 5fe5cd5fede7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 06 16:28:31 2006 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 06 16:28:33 2006 +0100
@@ -206,7 +206,7 @@
   Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
   Library/MLString.thy Library/Infinite_Set.thy \
   Library/FuncSet.thy Library/Library.thy \
-  Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
+  Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
   Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
   Library/Nat_Infinity.thy Library/Word.thy Library/word_setup.ML \
   Library/README.html Library/Continuity.thy \
diff -r c00161fbf990 -r 5fe5cd5fede7 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Nov 06 16:28:31 2006 +0100
+++ b/src/HOL/Library/Library.thy	Mon Nov 06 16:28:33 2006 +0100
@@ -25,6 +25,7 @@
   Coinductive_List
   AssocList
   Infinite_Set
+  State_Monad
 begin
 end
 (*>*)
diff -r c00161fbf990 -r 5fe5cd5fede7 src/HOL/Library/Library/document/root.tex
--- a/src/HOL/Library/Library/document/root.tex	Mon Nov 06 16:28:31 2006 +0100
+++ b/src/HOL/Library/Library/document/root.tex	Mon Nov 06 16:28:33 2006 +0100
@@ -21,6 +21,7 @@
 
 \renewcommand{\isamarkupheader}[1]%
 {\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\isasymguillemotright}{$\gg$}
 
 \parindent 0pt \parskip 0.5ex
 \input{session}
diff -r c00161fbf990 -r 5fe5cd5fede7 src/HOL/Library/State_Monad.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/State_Monad.thy	Mon Nov 06 16:28:33 2006 +0100
@@ -0,0 +1,248 @@
+(*  Title:      HOL/Library/State_Monad.thy
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Combinators syntax for generic, open state monads (single threaded monads) *}
+
+theory State_Monad
+imports Main
+begin
+
+section {* Generic, open state monads *}
+
+subsection {* Motivation *}
+
+text {*
+  The logic HOL has no notion of constructor classes, so
+  it is not possible to model monads the Haskell way
+  in full genericity in Isabelle/HOL.
+  
+  However, this theory provides substantial support for
+  a very common class of monads: \emph{state monads}
+  (or \emph{single-threaded monads}, since a state
+  is transformed single-threaded).
+
+  To enter from the Haskell world,
+  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
+  makes a good motivating start.  Here we just sketch briefly
+  how those monads enter the game of Isabelle/HOL.
+*}
+
+subsection {* State transformations and combinators *}
+
+(*<*)
+typedecl \<alpha>
+typedecl \<beta>
+typedecl \<gamma>
+typedecl \<sigma>
+typedecl \<sigma>'
+(*>*)
+
+text {*
+  We classify functions operating on states into two categories:
+
+  \begin{description}
+    \item[transformations]
+      with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
+      transforming a state.
+    \item[``yielding'' transformations]
+      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
+      ``yielding'' a side result while transforming a state.
+    \item[queries]
+      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
+      computing a result dependent on a state.
+  \end{description}
+
+  By convention we write @{typ "\<sigma>"} for types representing states
+  and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
+  for types representing side results.  Type changes due
+  to transformations are not excluded in our scenario.
+
+  We aim to assert that values of any state type @{typ "\<sigma>"}
+  are used in a single-threaded way: after application
+  of a transformation on a value of type @{typ "\<sigma>"}, the
+  former value should not be used again.  To achieve this,
+  we use a set of monad combinators:
+*}
+
+definition
+  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
+    (infixl "\<guillemotright>=" 60)
+  "f \<guillemotright>= g = split g \<circ> f"
+  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
+    (infixl "\<guillemotright>" 60)
+  "f \<guillemotright> g = g \<circ> f"
+  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  "run f = f"
+
+syntax (input)
+  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
+    (infixl ">>=" 60)
+  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
+    (infixl ">>" 60)
+
+abbreviation (input)
+  "return \<equiv> Pair"
+
+text {*
+  Given two transformations @{term f} and @{term g}, they
+  may be directly composed using the @{term "op \<guillemotright>"} combinator,
+  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
+
+  After any yielding transformation, we bind the side result
+  immediately using a lambda abstraction.  This 
+  is the purpose of the @{term "op \<guillemotright>="} combinator:
+  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+
+  For queries, the existing @{term "Let"} is appropriate.
+
+  Naturally, a computation may yield a side result by pairing
+  it to the state from the left;  we introduce the
+  suggestive abbreviation @{term return} for this purpose.
+
+  The @{const run} ist just a marker.
+
+  The most crucial distinction to Haskell is that we do
+  not need to introduce distinguished type constructors
+  for different kinds of state.  This has two consequences:
+  \begin{itemize}
+    \item The monad model does not state anything about
+       the kind of state; the model for the state is
+       completely orthogonal and has (or may) be
+       specified completely independent.
+    \item There is no distinguished type constructor
+       encapsulating away the state transformation, i.e.~transformations
+       may be applied directly without using any lifting
+       or providing and dropping units (``open monad'').
+    \item The type of states may change due to a transformation.
+  \end{itemize}
+*}
+
+
+subsection {* Obsolete runs *}
+
+text {*
+  @{term run} is just a doodle and should not occur nested:
+*}
+
+lemma run_simp [simp]:
+  "\<And>f. run (run f) = run f"
+  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
+  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
+  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
+  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
+  "\<And>f. f = run f \<longleftrightarrow> True"
+  "\<And>f. run f = f \<longleftrightarrow> True"
+  unfolding run_def by rule+
+
+
+subsection {* Monad laws *}
+
+text {*
+  The common monadic laws hold and may also be used
+  as normalization rules for monadic expressions:
+*}
+
+lemma
+  return_mbind [simp]: "return x \<guillemotright>= f = f x"
+  unfolding mbind_def by (simp add: expand_fun_eq)
+
+lemma
+  mbind_return [simp]: "x \<guillemotright>= return = x"
+  unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
+
+lemma
+  mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
+  unfolding mbind_def by (simp add: split_def expand_fun_eq)
+
+lemma
+  mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
+  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
+
+lemma
+  fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
+  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
+
+lemma
+  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
+  unfolding fcomp_def o_assoc ..
+
+lemmas monad_simp = run_simp return_mbind mbind_return
+  mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
+
+text {*
+  Evaluation of monadic expressions by force:
+*}
+
+lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
+  mbind_def fcomp_def run_def
+
+subsection {* Syntax *}
+
+text {*
+  We provide a convenient do-notation for monadic expressions
+  well-known from Haskell.  @{const Let} is printed
+  specially in do-expressions.
+*}
+
+nonterminals do_expr
+
+syntax
+  "_do" :: "do_expr \<Rightarrow> 'a"
+    ("do _ done" [12] 12)
+  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+    ("_ <- _;// _" [1000, 13, 12] 12)
+  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+    ("_;// _" [13, 12] 12)
+  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+    ("let _ = _;// _" [1000, 13, 12] 12)
+  "_nil" :: "'a \<Rightarrow> do_expr"
+    ("_" [12] 12)
+
+syntax (xsymbols)
+  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
+    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
+
+translations
+  "_do f" => "State_Monad.run f"
+  "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
+  "_fcomp f g" => "f \<guillemotright> g"
+  "_let x t f" => "Let t (\<lambda>x. f)"
+  "_nil f" => "f"
+
+print_translation {*
+let
+  val syntax_name = Sign.const_syntax_name (the_context ());
+  val name_mbind = syntax_name "State_Monad.mbind";
+  val name_fcomp = syntax_name "State_Monad.fcomp";
+  fun unfold_monad (t as Const (name, _) $ f $ g) =
+        if name = name_mbind then let
+            val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
+          in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+        else if name = name_fcomp then
+          Const ("_fcomp", dummyT) $ f $ unfold_monad g
+        else t
+    | unfold_monad (Const ("Let", _) $ f $ g) =
+        let
+          val ([(v, ty)], g') = Term.strip_abs_eta 1 g;
+        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
+    | unfold_monad (Const ("Pair", _) $ f) =
+        Const ("return", dummyT) $ f
+    | unfold_monad f = f;
+  fun tr' (f::ts) =
+    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
+in [
+  (syntax_name "State_Monad.run", tr')
+] end;
+*}
+
+print_ast_translation {*[
+  (Sign.const_syntax_name (the_context ()) "State_Monad.run", fn (f::ts) => Syntax.mk_appl f ts)
+]*}
+
+text {*
+  For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
+*}
+
+end
\ No newline at end of file
diff -r c00161fbf990 -r 5fe5cd5fede7 src/HOL/ex/CodeRandom.thy
--- a/src/HOL/ex/CodeRandom.thy	Mon Nov 06 16:28:31 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy	Mon Nov 06 16:28:33 2006 +0100
@@ -5,7 +5,7 @@
 header {* A simple random engine *}
 
 theory CodeRandom
-imports CodeRevappl
+imports State_Monad
 begin
 
 section {* A simple random engine *}
@@ -46,20 +46,20 @@
 
 definition
   select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
-  [simp]: "select xs s =
-    s
-    \<triangleright> random (length xs)
-    \<turnstile>\<triangleright> (\<lambda>n. Pair (nth xs n))"
+  [simp]: "select xs = (do
+      n \<leftarrow> random (length xs);
+      return (nth xs n)
+    done)"
   select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
-  [simp]: "select_weight xs s =
-    s
-    \<triangleright> random (foldl (op +) 0 (map fst xs))
-    \<turnstile>\<triangleright> (\<lambda>n. Pair (pick xs n))"
+  [simp]: "select_weight xs = (do
+      n \<leftarrow> random (foldl (op +) 0 (map fst xs));
+      return (pick xs n)
+    done)"
 
 lemma
   "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
 proof (induct xs)
-  case Nil show ?case by (simp add: revappl random_def)
+  case Nil show ?case by (simp add: monad_collapse random_def)
 next
   have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
   proof -
@@ -113,18 +113,22 @@
     from pick_nth [OF bound] show
       "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
   qed
+  have pick_nth_random_do:
+    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
+      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
+  unfolding monad_collapse split_def unfolding pick_nth_random ..
   case (Cons x xs) then show ?case
-    unfolding select_weight_def sum_length revappl_split pick_nth_random
-    by (simp add: revappl_split)
+    unfolding select_weight_def sum_length pick_nth_random_do
+    by simp
 qed
 
 definition
   random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
-  "random_int k s = (let (l, s') = random (nat k) s in (int l, s'))"
+  "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
 
 lemma random_nat [code]:
-  "random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
-unfolding random_int_def Let_def split_def random_def by simp
+  "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
+unfolding random_int_def by simp
 
 axiomatization
   run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
@@ -184,4 +188,6 @@
 code_gen select select_weight
   (SML *)
 
+code_gen (SML -)
+
 end
\ No newline at end of file