author haftmann Thu Nov 04 13:42:36 2010 +0100 (2010-11-04) changeset 40359 84388bba911d parent 40358 b6ed3364753d child 40360 1a73b5b90a3c
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
     1.1 --- a/src/HOL/Library/State_Monad.thy	Thu Nov 04 13:42:36 2010 +0100
1.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Nov 04 13:42:36 2010 +0100
1.3 @@ -2,7 +2,7 @@
1.4      Author:     Florian Haftmann, TU Muenchen
1.5  *)
1.6
1.9
1.12 @@ -11,19 +11,18 @@
1.13  subsection {* Motivation *}
1.14
1.15  text {*
1.16 -  The logic HOL has no notion of constructor classes, so
1.17 -  it is not possible to model monads the Haskell way
1.18 -  in full genericity in Isabelle/HOL.
1.19 +  The logic HOL has no notion of constructor classes, so it is not
1.20 +  possible to model monads the Haskell way in full genericity in
1.21 +  Isabelle/HOL.
1.22
1.23 -  However, this theory provides substantial support for
1.27 +  However, this theory provides substantial support for a very common
1.30
1.31    To enter from the Haskell world,
1.33 -  makes a good motivating start.  Here we just sketch briefly
1.34 -  how those monads enter the game of Isabelle/HOL.
1.36 +  a good motivating start.  Here we just sketch briefly how those
1.37 +  monads enter the game of Isabelle/HOL.
1.38  *}
1.39
1.40  subsection {* State transformations and combinators *}
1.41 @@ -32,64 +31,66 @@
1.42    We classify functions operating on states into two categories:
1.43
1.44    \begin{description}
1.45 -    \item[transformations]
1.46 -      with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
1.47 +
1.48 +    \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
1.49        transforming a state.
1.50 -    \item[yielding'' transformations]
1.51 -      with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
1.52 -      yielding'' a side result while transforming a state.
1.53 -    \item[queries]
1.54 -      with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
1.55 -      computing a result dependent on a state.
1.56 +
1.57 +    \item[yielding'' transformations] with type signature @{text "\<sigma>
1.58 +      \<Rightarrow> \<alpha> \<times> \<sigma>'"}, yielding'' a side result while transforming a
1.59 +      state.
1.60 +
1.61 +    \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a
1.62 +      result dependent on a state.
1.63 +
1.64    \end{description}
1.65
1.66 -  By convention we write @{text "\<sigma>"} for types representing states
1.67 -  and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
1.68 -  for types representing side results.  Type changes due
1.69 -  to transformations are not excluded in our scenario.
1.70 +  By convention we write @{text "\<sigma>"} for types representing states and
1.71 +  @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types
1.72 +  representing side results.  Type changes due to transformations are
1.73 +  not excluded in our scenario.
1.74
1.75 -  We aim to assert that values of any state type @{text "\<sigma>"}
1.76 -  are used in a single-threaded way: after application
1.77 -  of a transformation on a value of type @{text "\<sigma>"}, the
1.78 -  former value should not be used again.  To achieve this,
1.79 -  we use a set of monad combinators:
1.80 +  We aim to assert that values of any state type @{text "\<sigma>"} are used
1.81 +  in a single-threaded way: after application of a transformation on a
1.82 +  value of type @{text "\<sigma>"}, the former value should not be used
1.83 +  again.  To achieve this, we use a set of monad combinators:
1.84  *}
1.85
1.86  notation fcomp (infixl "\<circ>>" 60)
1.87  notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.88
1.89 -abbreviation (input)
1.90 -  "return \<equiv> Pair"
1.91 -
1.92  text {*
1.93 -  Given two transformations @{term f} and @{term g}, they
1.94 -  may be directly composed using the @{term "op \<circ>>"} combinator,
1.95 -  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
1.96 +  Given two transformations @{term f} and @{term g}, they may be
1.97 +  directly composed using the @{term "op \<circ>>"} combinator, forming a
1.98 +  forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
1.99
1.100    After any yielding transformation, we bind the side result
1.101 -  immediately using a lambda abstraction.  This
1.102 -  is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
1.103 -  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
1.104 +  immediately using a lambda abstraction.  This is the purpose of the
1.105 +  @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
1.106 +  = f s in g s')"}.
1.107
1.108    For queries, the existing @{term "Let"} is appropriate.
1.109
1.110 -  Naturally, a computation may yield a side result by pairing
1.111 -  it to the state from the left;  we introduce the
1.112 -  suggestive abbreviation @{term return} for this purpose.
1.113 +  Naturally, a computation may yield a side result by pairing it to
1.114 +  the state from the left; we introduce the suggestive abbreviation
1.115 +  @{term return} for this purpose.
1.116
1.117 -  The most crucial distinction to Haskell is that we do
1.118 -  not need to introduce distinguished type constructors
1.119 -  for different kinds of state.  This has two consequences:
1.120 +  The most crucial distinction to Haskell is that we do not need to
1.121 +  introduce distinguished type constructors for different kinds of
1.122 +  state.  This has two consequences:
1.123 +
1.124    \begin{itemize}
1.126 -       the kind of state; the model for the state is
1.127 -       completely orthogonal and may be
1.128 -       specified completely independently.
1.129 -    \item There is no distinguished type constructor
1.130 -       encapsulating away the state transformation, i.e.~transformations
1.131 -       may be applied directly without using any lifting
1.132 -       or providing and dropping units (open monad'').
1.133 +
1.134 +    \item The monad model does not state anything about the kind of
1.135 +       state; the model for the state is completely orthogonal and may
1.136 +       be specified completely independently.
1.137 +
1.138 +    \item There is no distinguished type constructor encapsulating
1.139 +       away the state transformation, i.e.~transformations may be
1.140 +       applied directly without using any lifting or providing and
1.141 +       dropping units (open monad'').
1.142 +
1.143      \item The type of states may change due to a transformation.
1.144 +
1.145    \end{itemize}
1.146  *}
1.147
1.148 @@ -97,8 +98,8 @@
1.149  subsection {* Monad laws *}
1.150
1.151  text {*
1.152 -  The common monadic laws hold and may also be used
1.153 -  as normalization rules for monadic expressions:
1.154 +  The common monadic laws hold and may also be used as normalization
1.155 +  rules for monadic expressions:
1.156  *}
1.157
1.158  lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
1.159 @@ -145,7 +146,7 @@
1.160    "_sdo_block (_sdo_final e)" => "e"
1.161
1.162  text {*
1.163 -  For an example, see HOL/Extraction/Higman.thy.
1.164 +  For an example, see @{text HOL/Proofs/Extraction/Higman.thy}.
1.165  *}
1.166
1.167  end

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