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