src/HOL/Library/State_Monad.thy
author haftmann
Thu, 22 Jul 2010 12:07:30 +0200
changeset 37932 d00a3f47b607
parent 37817 71e5546b1965
child 38345 8b8fc27c1872
permissions -rw-r--r--
more generous memory settings for scala check
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/State_Monad.thy
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     3
*)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     4
27487
c8a6ce181805 absolute imports of HOL/*.thy theories
haftmann
parents: 27368
diff changeset
     5
header {* Combinator syntax for generic, open state monads (single threaded monads) *}
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     6
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     7
theory State_Monad
37932
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
     8
imports Main Monad_Syntax
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     9
begin
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    10
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    11
subsection {* Motivation *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    12
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    13
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    14
  The logic HOL has no notion of constructor classes, so
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    15
  it is not possible to model monads the Haskell way
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    16
  in full genericity in Isabelle/HOL.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    17
  
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    18
  However, this theory provides substantial support for
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    19
  a very common class of monads: \emph{state monads}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    20
  (or \emph{single-threaded monads}, since a state
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    21
  is transformed single-threaded).
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    22
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    23
  To enter from the Haskell world,
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    24
  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    25
  makes a good motivating start.  Here we just sketch briefly
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    26
  how those monads enter the game of Isabelle/HOL.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    27
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    28
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    29
subsection {* State transformations and combinators *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    30
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    31
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    32
  We classify functions operating on states into two categories:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    33
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    34
  \begin{description}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    35
    \item[transformations]
26266
haftmann
parents: 26260
diff changeset
    36
      with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    37
      transforming a state.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    38
    \item[``yielding'' transformations]
26266
haftmann
parents: 26260
diff changeset
    39
      with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    40
      ``yielding'' a side result while transforming a state.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    41
    \item[queries]
26266
haftmann
parents: 26260
diff changeset
    42
      with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    43
      computing a result dependent on a state.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    44
  \end{description}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    45
26266
haftmann
parents: 26260
diff changeset
    46
  By convention we write @{text "\<sigma>"} for types representing states
haftmann
parents: 26260
diff changeset
    47
  and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    48
  for types representing side results.  Type changes due
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    49
  to transformations are not excluded in our scenario.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    50
26266
haftmann
parents: 26260
diff changeset
    51
  We aim to assert that values of any state type @{text "\<sigma>"}
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    52
  are used in a single-threaded way: after application
26266
haftmann
parents: 26260
diff changeset
    53
  of a transformation on a value of type @{text "\<sigma>"}, the
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    54
  former value should not be used again.  To achieve this,
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    55
  we use a set of monad combinators:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    56
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    57
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 35115
diff changeset
    58
notation fcomp (infixl "\<circ>>" 60)
37817
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
    59
notation scomp (infixl "\<circ>\<rightarrow>" 60)
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    60
26588
d83271bfaba5 removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents: 26266
diff changeset
    61
abbreviation (input)
d83271bfaba5 removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents: 26266
diff changeset
    62
  "return \<equiv> Pair"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    63
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    64
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    65
  Given two transformations @{term f} and @{term g}, they
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 35115
diff changeset
    66
  may be directly composed using the @{term "op \<circ>>"} combinator,
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 35115
diff changeset
    67
  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    68
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    69
  After any yielding transformation, we bind the side result
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    70
  immediately using a lambda abstraction.  This 
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 35115
diff changeset
    71
  is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 35115
diff changeset
    72
  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    73
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    74
  For queries, the existing @{term "Let"} is appropriate.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    75
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    76
  Naturally, a computation may yield a side result by pairing
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    77
  it to the state from the left;  we introduce the
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    78
  suggestive abbreviation @{term return} for this purpose.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    79
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    80
  The most crucial distinction to Haskell is that we do
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    81
  not need to introduce distinguished type constructors
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    82
  for different kinds of state.  This has two consequences:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    83
  \begin{itemize}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    84
    \item The monad model does not state anything about
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    85
       the kind of state; the model for the state is
26260
haftmann
parents: 26141
diff changeset
    86
       completely orthogonal and may be
haftmann
parents: 26141
diff changeset
    87
       specified completely independently.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    88
    \item There is no distinguished type constructor
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    89
       encapsulating away the state transformation, i.e.~transformations
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    90
       may be applied directly without using any lifting
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    91
       or providing and dropping units (``open monad'').
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    92
    \item The type of states may change due to a transformation.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    93
  \end{itemize}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    94
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    95
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    96
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    97
subsection {* Monad laws *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    98
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    99
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   100
  The common monadic laws hold and may also be used
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   101
  as normalization rules for monadic expressions:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   102
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   103
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 27487
diff changeset
   104
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 27487
diff changeset
   105
  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   106
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   107
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   108
  Evaluation of monadic expressions by force:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   109
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   110
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 27487
diff changeset
   111
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
26260
haftmann
parents: 26141
diff changeset
   112
37817
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   113
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   114
subsection {* Do-syntax *}
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   115
37932
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   116
nonterminals
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   117
  sdo_binds sdo_bind
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   118
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   119
syntax
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   120
  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   121
  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   122
  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   123
  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   124
  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   125
  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   126
37932
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   127
syntax (xsymbols)
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   128
  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   129
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   130
translations
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   131
  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   132
    == "CONST scomp t (\<lambda>p. e)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   133
  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   134
    == "CONST fcomp t e"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   135
  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   136
    == "let p = t in _sdo_block bs"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   137
  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   138
    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   139
  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   140
    == "_sdo_final (let p = t in s)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   141
  "_sdo_block (_sdo_final e)" => "e"
37817
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   142
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   143
text {*
31033
c46d52fee219 fixed broken link
haftmann
parents: 30738
diff changeset
   144
  For an example, see HOL/Extraction/Higman.thy.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   145
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   146
22664
e965391e2864 do translation: CONST;
wenzelm
parents: 22492
diff changeset
   147
end