--- 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 \
--- 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
(*>*)
--- 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}
--- /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
--- 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