src/HOL/Library/State_Monad.thy
author haftmann
Wed, 12 Mar 2008 08:47:36 +0100
changeset 26260 23ce0d32de11
parent 26141 e1b3a6953cdc
child 26266 35ae83ca190a
permissions -rw-r--r--
tuned
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
    ID:         $Id$
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     4
*)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     5
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     6
header {* Combinators syntax for generic, open state monads (single threaded monads) *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     7
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
     8
theory State_Monad
25595
6c48275f9c76 switched import from Main to List
haftmann
parents: 24253
diff changeset
     9
imports List
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    10
begin
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    11
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    12
subsection {* Motivation *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    13
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    14
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    15
  The logic HOL has no notion of constructor classes, so
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    16
  it is not possible to model monads the Haskell way
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    17
  in full genericity in Isabelle/HOL.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    18
  
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    19
  However, this theory provides substantial support for
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    20
  a very common class of monads: \emph{state monads}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    21
  (or \emph{single-threaded monads}, since a state
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    22
  is transformed single-threaded).
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    23
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    24
  To enter from the Haskell world,
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    25
  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    26
  makes a good motivating start.  Here we just sketch briefly
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    27
  how those monads enter the game of Isabelle/HOL.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    28
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    29
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    30
subsection {* State transformations and combinators *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    31
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    32
(*<*)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    33
typedecl \<alpha>
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    34
typedecl \<beta>
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    35
typedecl \<gamma>
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    36
typedecl \<sigma>
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    37
typedecl \<sigma>'
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    38
(*>*)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    39
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    40
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    41
  We classify functions operating on states into two categories:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    42
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    43
  \begin{description}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    44
    \item[transformations]
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    45
      with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    46
      transforming a state.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    47
    \item[``yielding'' transformations]
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    48
      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    49
      ``yielding'' a side result while transforming a state.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    50
    \item[queries]
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    51
      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    52
      computing a result dependent on a state.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    53
  \end{description}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    54
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    55
  By convention we write @{typ "\<sigma>"} for types representing states
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    56
  and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    57
  for types representing side results.  Type changes due
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    58
  to transformations are not excluded in our scenario.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    59
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    60
  We aim to assert that values of any state type @{typ "\<sigma>"}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    61
  are used in a single-threaded way: after application
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    62
  of a transformation on a value of type @{typ "\<sigma>"}, the
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    63
  former value should not be used again.  To achieve this,
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    64
  we use a set of monad combinators:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    65
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    66
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    67
definition
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    68
  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    69
    (infixl ">>=" 60) where
21283
b15355b9a59d improved syntax
haftmann
parents: 21192
diff changeset
    70
  "f >>= g = split g \<circ> f"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    71
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    72
definition
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    73
  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    74
    (infixl ">>" 60) where
21283
b15355b9a59d improved syntax
haftmann
parents: 21192
diff changeset
    75
  "f >> g = g \<circ> f"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    76
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    77
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21283
diff changeset
    78
  run :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    79
  "run f = f"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    80
21283
b15355b9a59d improved syntax
haftmann
parents: 21192
diff changeset
    81
syntax (xsymbols)
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    82
  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"
21283
b15355b9a59d improved syntax
haftmann
parents: 21192
diff changeset
    83
    (infixl "\<guillemotright>=" 60)
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    84
  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"
21283
b15355b9a59d improved syntax
haftmann
parents: 21192
diff changeset
    85
    (infixl "\<guillemotright>" 60)
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    86
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    87
abbreviation (input)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    88
  "return \<equiv> Pair"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    89
22377
61610b1beedf tuned ML setup;
wenzelm
parents: 21835
diff changeset
    90
print_ast_translation {*
61610b1beedf tuned ML setup;
wenzelm
parents: 21835
diff changeset
    91
  [(@{const_syntax "run"}, fn (f::ts) => Syntax.mk_appl f ts)]
61610b1beedf tuned ML setup;
wenzelm
parents: 21835
diff changeset
    92
*}
21835
84fd5de0691c whitespace correction
haftmann
parents: 21818
diff changeset
    93
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    94
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    95
  Given two transformations @{term f} and @{term g}, they
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    96
  may be directly composed using the @{term "op \<guillemotright>"} combinator,
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    97
  forming a forward composition: @{prop "(f \<guillemotright> g) s = f (g s)"}.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    98
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
    99
  After any yielding transformation, we bind the side result
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   100
  immediately using a lambda abstraction.  This 
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   101
  is the purpose of the @{term "op \<guillemotright>="} combinator:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   102
  @{prop "(f \<guillemotright>= (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   103
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   104
  For queries, the existing @{term "Let"} is appropriate.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   105
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   106
  Naturally, a computation may yield a side result by pairing
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   107
  it to the state from the left;  we introduce the
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   108
  suggestive abbreviation @{term return} for this purpose.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   109
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   110
  The @{const run} ist just a marker.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   111
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   112
  The most crucial distinction to Haskell is that we do
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   113
  not need to introduce distinguished type constructors
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   114
  for different kinds of state.  This has two consequences:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   115
  \begin{itemize}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   116
    \item The monad model does not state anything about
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   117
       the kind of state; the model for the state is
26260
haftmann
parents: 26141
diff changeset
   118
       completely orthogonal and may be
haftmann
parents: 26141
diff changeset
   119
       specified completely independently.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   120
    \item There is no distinguished type constructor
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   121
       encapsulating away the state transformation, i.e.~transformations
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   122
       may be applied directly without using any lifting
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   123
       or providing and dropping units (``open monad'').
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   124
    \item The type of states may change due to a transformation.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   125
  \end{itemize}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   126
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   127
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   128
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   129
subsection {* Obsolete runs *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   130
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   131
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   132
  @{term run} is just a doodle and should not occur nested:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   133
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   134
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   135
lemma run_simp [simp]:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   136
  "\<And>f. run (run f) = run f"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   137
  "\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   138
  "\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   139
  "\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   140
  "\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   141
  "\<And>f. f = run f \<longleftrightarrow> True"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   142
  "\<And>f. run f = f \<longleftrightarrow> True"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   143
  unfolding run_def by rule+
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   144
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   145
subsection {* Monad laws *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   146
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   147
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   148
  The common monadic laws hold and may also be used
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   149
  as normalization rules for monadic expressions:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   150
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   151
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   152
lemma
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   153
  return_mbind [simp]: "return x \<guillemotright>= f = f x"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   154
  unfolding mbind_def by (simp add: expand_fun_eq)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   155
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   156
lemma
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   157
  mbind_return [simp]: "x \<guillemotright>= return = x"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   158
  unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   159
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   160
lemma
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   161
  id_fcomp [simp]: "id \<guillemotright> f = f"
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   162
  unfolding fcomp_def by simp
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   163
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   164
lemma
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   165
  fcomp_id [simp]: "f \<guillemotright> id = f"
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   166
  unfolding fcomp_def by simp
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   167
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   168
lemma
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   169
  mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   170
  unfolding mbind_def by (simp add: split_def expand_fun_eq)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   171
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   172
lemma
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   173
  mbind_fcomp [simp]: "(f \<guillemotright>= g) \<guillemotright> h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright> h)"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   174
  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   175
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   176
lemma
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   177
  fcomp_mbind [simp]: "(f \<guillemotright> g) \<guillemotright>= h = f \<guillemotright> (g \<guillemotright>= h)"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   178
  unfolding mbind_def fcomp_def by (simp add: split_def expand_fun_eq)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   179
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   180
lemma
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   181
  fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   182
  unfolding fcomp_def o_assoc ..
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   183
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   184
lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   185
  mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   186
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   187
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   188
  Evaluation of monadic expressions by force:
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   189
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   190
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   191
lemmas monad_collapse = monad_simp o_apply o_assoc split_Pair split_comp
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   192
  mbind_def fcomp_def run_def
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   193
26260
haftmann
parents: 26141
diff changeset
   194
subsection {* ML abstract operations *}
haftmann
parents: 26141
diff changeset
   195
haftmann
parents: 26141
diff changeset
   196
ML {*
haftmann
parents: 26141
diff changeset
   197
structure StateMonad =
haftmann
parents: 26141
diff changeset
   198
struct
haftmann
parents: 26141
diff changeset
   199
haftmann
parents: 26141
diff changeset
   200
fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
haftmann
parents: 26141
diff changeset
   201
fun liftT' sT = sT --> sT;
haftmann
parents: 26141
diff changeset
   202
haftmann
parents: 26141
diff changeset
   203
fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
haftmann
parents: 26141
diff changeset
   204
haftmann
parents: 26141
diff changeset
   205
fun mbind T1 T2 sT f g = Const (@{const_name mbind},
haftmann
parents: 26141
diff changeset
   206
  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
haftmann
parents: 26141
diff changeset
   207
haftmann
parents: 26141
diff changeset
   208
fun run T sT f = Const (@{const_name run}, liftT' (liftT T sT)) $ f;
haftmann
parents: 26141
diff changeset
   209
haftmann
parents: 26141
diff changeset
   210
end;
haftmann
parents: 26141
diff changeset
   211
*}
haftmann
parents: 26141
diff changeset
   212
haftmann
parents: 26141
diff changeset
   213
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   214
subsection {* Syntax *}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   215
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   216
text {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   217
  We provide a convenient do-notation for monadic expressions
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   218
  well-known from Haskell.  @{const Let} is printed
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   219
  specially in do-expressions.
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   220
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   221
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   222
nonterminals do_expr
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   223
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   224
syntax
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   225
  "_do" :: "do_expr \<Rightarrow> 'a"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   226
    ("do _ done" [12] 12)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   227
  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   228
    ("_ <- _;// _" [1000, 13, 12] 12)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   229
  "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   230
    ("_;// _" [13, 12] 12)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   231
  "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   232
    ("let _ = _;// _" [1000, 13, 12] 12)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   233
  "_nil" :: "'a \<Rightarrow> do_expr"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   234
    ("_" [12] 12)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   235
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   236
syntax (xsymbols)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   237
  "_mbind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   238
    ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   239
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   240
translations
22664
e965391e2864 do translation: CONST;
wenzelm
parents: 22492
diff changeset
   241
  "_do f" => "CONST run f"
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   242
  "_mbind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   243
  "_fcomp f g" => "f \<guillemotright> g"
24195
haftmann
parents: 22664
diff changeset
   244
  "_let x t f" => "CONST Let t (\<lambda>x. f)"
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   245
  "_nil f" => "f"
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   246
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   247
print_translation {*
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   248
let
24253
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   249
  fun dest_abs_eta (Abs (abs as (_, ty, _))) =
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   250
        let
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   251
          val (v, t) = Syntax.variant_abs abs;
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   252
        in ((v, ty), t) end
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   253
    | dest_abs_eta t =
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   254
        let
24253
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   255
          val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   256
        in ((v, dummyT), t) end
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   257
  fun unfold_monad (Const (@{const_syntax mbind}, _) $ f $ g) =
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   258
        let
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   259
          val ((v, ty), g') = dest_abs_eta g;
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   260
        in Const ("_mbind", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
24195
haftmann
parents: 22664
diff changeset
   261
    | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
haftmann
parents: 22664
diff changeset
   262
        Const ("_fcomp", dummyT) $ f $ unfold_monad g
24253
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   263
    | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
24195
haftmann
parents: 22664
diff changeset
   264
        let
24253
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   265
          val ((v, ty), g') = dest_abs_eta g;
3d7f74fd9fd9 fixed syntax
haftmann
parents: 24224
diff changeset
   266
        in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end
24195
haftmann
parents: 22664
diff changeset
   267
    | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   268
        Const ("return", dummyT) $ f
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   269
    | unfold_monad f = f;
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   270
  fun tr' (f::ts) =
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   271
    list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)
22377
61610b1beedf tuned ML setup;
wenzelm
parents: 21835
diff changeset
   272
in [(@{const_syntax "run"}, tr')] end;
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   273
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   274
24195
haftmann
parents: 22664
diff changeset
   275
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   276
subsection {* Combinators *}
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   277
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   278
definition
21601
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21418
diff changeset
   279
  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   280
  "lift f x = return (f x)"
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   281
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   282
primrec
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   283
  list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   284
  "list f [] = id"
22492
43545e640877 Unified function syntax
krauss
parents: 22377
diff changeset
   285
| "list f (x#xs) = (do f x; list f xs done)"
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   286
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   287
primrec
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   288
  list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   289
  "list_yield f [] = return []"
22492
43545e640877 Unified function syntax
krauss
parents: 22377
diff changeset
   290
| "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
26141
e1b3a6953cdc operation collapse
haftmann
parents: 25765
diff changeset
   291
e1b3a6953cdc operation collapse
haftmann
parents: 25765
diff changeset
   292
definition
26260
haftmann
parents: 26141
diff changeset
   293
  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
26141
e1b3a6953cdc operation collapse
haftmann
parents: 25765
diff changeset
   294
  "collapse f = (do g \<leftarrow> f; g done)"
e1b3a6953cdc operation collapse
haftmann
parents: 25765
diff changeset
   295
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   296
text {* combinator properties *}
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   297
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   298
lemma list_append [simp]:
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   299
  "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
26141
e1b3a6953cdc operation collapse
haftmann
parents: 25765
diff changeset
   300
  by (induct xs) (simp_all del: id_apply)
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   301
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   302
lemma list_cong [fundef_cong, recdef_cong]:
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   303
  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   304
    \<Longrightarrow> list f xs = list g ys"
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   305
proof (induct xs arbitrary: ys)
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   306
  case Nil then show ?case by simp
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   307
next
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   308
  case (Cons x xs)
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   309
  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   310
  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   311
  with Cons have "list f xs = list g xs" by auto
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   312
  with Cons have "list f (x # xs) = list g (x # xs)" by auto
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   313
  with Cons show "list f (x # xs) = list g ys" by auto
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   314
qed
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   315
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   316
lemma list_yield_cong [fundef_cong, recdef_cong]:
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   317
  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   318
    \<Longrightarrow> list_yield f xs = list_yield g ys"
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   319
proof (induct xs arbitrary: ys)
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   320
  case Nil then show ?case by simp
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   321
next
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   322
  case (Cons x xs)
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   323
  from Cons have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   324
  then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
25765
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   325
  with Cons have "list_yield f xs = list_yield g xs" by auto
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   326
  with Cons have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
49580bd58a21 some more primrec
haftmann
parents: 25595
diff changeset
   327
  with Cons show "list_yield f (x # xs) = list_yield g ys" by auto
21418
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   328
qed
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   329
4bc2882f80af added combinators and lemmas
haftmann
parents: 21404
diff changeset
   330
text {*
24195
haftmann
parents: 22664
diff changeset
   331
  For an example, see HOL/ex/Random.thy.
21192
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   332
*}
5fe5cd5fede7 added state monad to HOL library
haftmann
parents:
diff changeset
   333
22664
e965391e2864 do translation: CONST;
wenzelm
parents: 22492
diff changeset
   334
end