src/HOL/Library/State_Monad.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63680 6e1e8b5abbfa
child 66258 2b83dd24b301
permissions -rw-r--r--
tuned proofs;
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    11
subsection \<open>Motivation\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    12
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    13
text \<open>
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    14
  The logic HOL has no notion of constructor classes, so it is not
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    15
  possible to model monads the Haskell way in full genericity in
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    16
  Isabelle/HOL.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    17
  
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    18
  However, this theory provides substantial support for a very common
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    19
  class of monads: \emph{state monads} (or \emph{single-threaded
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    20
  monads}, since a state is transformed single-threadedly).
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    21
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    22
  To enter from the Haskell world,
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63362
diff changeset
    23
  \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    24
  a good motivating start.  Here we just sketch briefly how those
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    25
  monads enter the game of Isabelle/HOL.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    26
\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    27
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    28
subsection \<open>State transformations and combinators\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    29
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    30
text \<open>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    31
  We classify functions operating on states into two categories:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    32
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    33
  \begin{description}
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    34
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    35
    \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>,
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    36
      transforming a state.
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    37
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    38
    \item[``yielding'' transformations] with type signature \<open>\<sigma>
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    39
      \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    40
      state.
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    41
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    42
    \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    43
      result dependent on a state.
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    44
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    45
  \end{description}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    46
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    47
  By convention we write \<open>\<sigma>\<close> for types representing states and
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    48
  \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    49
  representing side results.  Type changes due to transformations are
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    50
  not excluded in our scenario.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    51
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    52
  We aim to assert that values of any state type \<open>\<sigma>\<close> are used
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    53
  in a single-threaded way: after application of a transformation on a
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    54
  value of type \<open>\<sigma>\<close>, the former value should not be used
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    55
  again.  To achieve this, we use a set of monad combinators:
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    56
\<close>
21192
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    61
text \<open>
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    62
  Given two transformations @{term f} and @{term g}, they may be
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    63
  directly composed using the @{term "op \<circ>>"} combinator, forming a
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    64
  forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    65
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    66
  After any yielding transformation, we bind the side result
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    67
  immediately using a lambda abstraction.  This is the purpose of the
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    68
  @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    69
  = f s in g s')"}.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    70
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    71
  For queries, the existing @{term "Let"} is appropriate.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    72
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    73
  Naturally, a computation may yield a side result by pairing it to
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    74
  the state from the left; we introduce the suggestive abbreviation
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    75
  @{term return} for this purpose.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    76
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    77
  The most crucial distinction to Haskell is that we do not need to
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    78
  introduce distinguished type constructors for different kinds of
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    79
  state.  This has two consequences:
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    80
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    81
  \begin{itemize}
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    82
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    83
    \item The monad model does not state anything about the kind of
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    84
       state; the model for the state is completely orthogonal and may
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    85
       be specified completely independently.
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    86
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    87
    \item There is no distinguished type constructor encapsulating
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    88
       away the state transformation, i.e.~transformations may be
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    89
       applied directly without using any lifting or providing and
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    90
       dropping units (``open monad'').
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    91
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    92
    \item The type of states may change due to a transformation.
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
    93
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    94
  \end{itemize}
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    95
\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    96
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    97
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    98
subsection \<open>Monad laws\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    99
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   100
text \<open>
40359
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
   101
  The common monadic laws hold and may also be used as normalization
84388bba911d dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann
parents: 38345
diff changeset
   102
  rules for monadic expressions:
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   103
\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   104
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 27487
diff changeset
   105
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 27487
diff changeset
   106
  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   107
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   108
text \<open>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   109
  Evaluation of monadic expressions by force:
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   110
\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   111
28145
af3923ed4786 dropped "run" marker in monad syntax
haftmann
parents: 27487
diff changeset
   112
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
26260
haftmann
parents: 26141
diff changeset
   113
37817
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   114
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   115
subsection \<open>Do-syntax\<close>
37817
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   116
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 40361
diff changeset
   117
nonterminal sdo_binds and sdo_bind
37932
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)
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61585
diff changeset
   121
  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
37932
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
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61585
diff changeset
   127
syntax (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61585
diff changeset
   128
  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
37932
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))"
38345
8b8fc27c1872 print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents: 37932
diff changeset
   134
    => "CONST fcomp t e"
8b8fc27c1872 print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents: 37932
diff changeset
   135
  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
8b8fc27c1872 print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents: 37932
diff changeset
   136
    <= "_sdo_final (CONST fcomp t e)"
8b8fc27c1872 print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents: 37932
diff changeset
   137
  "_sdo_block (_sdo_cons (_sdo_then t) e)"
8b8fc27c1872 print fcomp combinator only monadic in connection with other monadic expressions
haftmann
parents: 37932
diff changeset
   138
    <= "CONST fcomp t (_sdo_block e)"
37932
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   139
  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   140
    == "let p = t in _sdo_block bs"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   141
  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   142
    == "_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
   143
  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   144
    == "_sdo_final (let p = t in s)"
d00a3f47b607 more generous memory settings for scala check
haftmann
parents: 37817
diff changeset
   145
  "_sdo_block (_sdo_final e)" => "e"
37817
71e5546b1965 tuned infix syntax
haftmann
parents: 37791
diff changeset
   146
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   147
text \<open>
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63362
diff changeset
   148
  For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   149
\<close>
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   150
22664
e965391e2864 do translation: CONST;
wenzelm
parents: 22492
diff changeset
   151
end