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