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