dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
authorhaftmann
Thu Nov 04 13:42:36 2010 +0100 (2010-11-04)
changeset 4035984388bba911d
parent 40358 b6ed3364753d
child 40360 1a73b5b90a3c
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
src/HOL/Library/State_Monad.thy
src/HOL/Proofs/Extraction/Higman.thy
     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.7 -header {* Combinator syntax for generic, open state monads (single threaded monads) *}
     1.8 +header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
     1.9  
    1.10  theory State_Monad
    1.11  imports Main Monad_Syntax
    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.24 -  a very common class of monads: \emph{state monads}
    1.25 -  (or \emph{single-threaded monads}, since a state
    1.26 -  is transformed single-threaded).
    1.27 +  However, this theory provides substantial support for a very common
    1.28 +  class of monads: \emph{state monads} (or \emph{single-threaded
    1.29 +  monads}, since a state is transformed single-threadedly).
    1.30  
    1.31    To enter from the Haskell world,
    1.32 -  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
    1.33 -  makes a good motivating start.  Here we just sketch briefly
    1.34 -  how those monads enter the game of Isabelle/HOL.
    1.35 +  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
    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.125 -    \item The monad model does not state anything about
   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