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