author haftmann Thu, 04 Nov 2010 13:42:36 +0100 changeset 40359 84388bba911d parent 40358 b6ed3364753d child 40360 1a73b5b90a3c
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
--- a/src/HOL/Library/State_Monad.thy	Thu Nov 04 13:42:36 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy	Thu Nov 04 13:42:36 2010 +0100
@@ -2,7 +2,7 @@
Author:     Florian Haftmann, TU Muenchen
*)

-header {* Combinator syntax for generic, open state monads (single threaded monads) *}
+header {* Combinator syntax for generic, open state monads (single-threaded monads) *}

theory State_Monad
imports Main Monad_Syntax
@@ -11,19 +11,18 @@
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.
+  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).
+  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-threadedly).

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.
+  \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 *}
@@ -32,64 +31,66 @@
We classify functions operating on states into two categories:

\begin{description}
-    \item[transformations]
-      with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
+
+    \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
transforming a state.
-    \item[yielding'' transformations]
-      with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
-      yielding'' a side result while transforming a state.
-    \item[queries]
-      with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
-      computing a result dependent on a state.
+
+    \item[yielding'' transformations] with type signature @{text "\<sigma>
+      \<Rightarrow> \<alpha> \<times> \<sigma>'"}, yielding'' a side result while transforming a
+      state.
+
+    \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
+      result dependent on a state.
+
\end{description}

-  By convention we write @{text "\<sigma>"} for types representing states
-  and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
-  for types representing side results.  Type changes due
-  to transformations are not excluded in our scenario.
+  By convention we write @{text "\<sigma>"} for types representing states and
+  @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<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 @{text "\<sigma>"}
-  are used in a single-threaded way: after application
-  of a transformation on a value of type @{text "\<sigma>"}, the
-  former value should not be used again.  To achieve this,
-  we use a set of monad combinators:
+  We aim to assert that values of any state type @{text "\<sigma>"} are used
+  in a single-threaded way: after application of a transformation on a
+  value of type @{text "\<sigma>"}, the former value should not be used
+  again.  To achieve this, we use a set of monad combinators:
*}

notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)

-abbreviation (input)
-  "return \<equiv> Pair"
-
text {*
-  Given two transformations @{term f} and @{term g}, they
-  may be directly composed using the @{term "op \<circ>>"} combinator,
-  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
+  Given two transformations @{term f} and @{term g}, they may be
+  directly composed using the @{term "op \<circ>>"} combinator, forming a
+  forward composition: @{prop "(f \<circ>> 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 \<circ>\<rightarrow>"} combinator:
-  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
+  immediately using a lambda abstraction.  This is the purpose of the
+  @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<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.
+  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 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:
+  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 may be
-       specified completely independently.
-    \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 monad model does not state anything about the kind of
+       state; the model for the state is completely orthogonal and may
+       be specified completely independently.
+
+    \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}
*}

@@ -97,8 +98,8 @@
subsection {* Monad laws *}

text {*
-  The common monadic laws hold and may also be used
-  as normalization rules for monadic expressions:
+  The common monadic laws hold and may also be used as normalization
+  rules for monadic expressions:
*}

lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
@@ -145,7 +146,7 @@
"_sdo_block (_sdo_final e)" => "e"

text {*
-  For an example, see HOL/Extraction/Higman.thy.
+  For an example, see @{text HOL/Proofs/Extraction/Higman.thy}.
*}

end
--- a/src/HOL/Proofs/Extraction/Higman.thy	Thu Nov 04 13:42:36 2010 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Thu Nov 04 13:42:36 2010 +0100
@@ -352,11 +352,11 @@
function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_aux k = exec {
i \<leftarrow> Random.range 10;
-     (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
+     (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
else exec {
let l = (if i mod 2 = 0 then A else B);
ls \<leftarrow> mk_word_aux (Suc k);
-       return (l # ls)
+       Pair (l # ls)
})}"
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto