1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 09 10:08:10 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 09 16:58:44 2010 +0200
1.3 @@ -10,7 +10,7 @@
1.4
1.5 subsection {* The monad *}
1.6
1.7 -subsubsection {* Monad combinators *}
1.8 +subsubsection {* Monad construction *}
1.9
1.10 text {* Monadic heap actions either produce values
1.11 and transform the heap, or fail *}
1.12 @@ -19,6 +19,13 @@
1.13 primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
1.14 [code del]: "execute (Heap f) = f"
1.15
1.16 +lemma Heap_cases [case_names succeed fail]:
1.17 + fixes f and h
1.18 + assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
1.19 + assumes fail: "execute f h = None \<Longrightarrow> P"
1.20 + shows P
1.21 + using assms by (cases "execute f h") auto
1.22 +
1.23 lemma Heap_execute [simp]:
1.24 "Heap (execute f) = f" by (cases f) simp_all
1.25
1.26 @@ -26,43 +33,98 @@
1.27 "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
1.28 by (cases f, cases g) (auto simp: expand_fun_eq)
1.29
1.30 -lemma Heap_eqI':
1.31 - "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
1.32 - by (auto simp: expand_fun_eq intro: Heap_eqI)
1.33 +ML {* structure Execute_Simps = Named_Thms(
1.34 + val name = "execute_simps"
1.35 + val description = "simplification rules for execute"
1.36 +) *}
1.37 +
1.38 +setup Execute_Simps.setup
1.39 +
1.40 +lemma execute_Let [simp, execute_simps]:
1.41 + "execute (let x = t in f x) = (let x = t in execute (f x))"
1.42 + by (simp add: Let_def)
1.43 +
1.44 +
1.45 +subsubsection {* Specialised lifters *}
1.46 +
1.47 +definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
1.48 + [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
1.49 +
1.50 +lemma execute_tap [simp, execute_simps]:
1.51 + "execute (tap f) h = Some (f h, h)"
1.52 + by (simp add: tap_def)
1.53
1.54 definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
1.55 [code del]: "heap f = Heap (Some \<circ> f)"
1.56
1.57 -lemma execute_heap [simp]:
1.58 +lemma execute_heap [simp, execute_simps]:
1.59 "execute (heap f) = Some \<circ> f"
1.60 by (simp add: heap_def)
1.61
1.62 definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
1.63 [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
1.64
1.65 -lemma execute_guard [simp]:
1.66 +lemma execute_guard [execute_simps]:
1.67 "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
1.68 "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
1.69 by (simp_all add: guard_def)
1.70
1.71 -lemma heap_cases [case_names succeed fail]:
1.72 - fixes f and h
1.73 - assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
1.74 - assumes fail: "execute f h = None \<Longrightarrow> P"
1.75 - shows P
1.76 - using assms by (cases "execute f h") auto
1.77 +
1.78 +subsubsection {* Predicate classifying successful computations *}
1.79 +
1.80 +definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
1.81 + "success f h \<longleftrightarrow> execute f h \<noteq> None"
1.82 +
1.83 +lemma successI:
1.84 + "execute f h \<noteq> None \<Longrightarrow> success f h"
1.85 + by (simp add: success_def)
1.86 +
1.87 +lemma successE:
1.88 + assumes "success f h"
1.89 + obtains r h' where "execute f h = Some (r, h')"
1.90 + using assms by (auto simp add: success_def)
1.91 +
1.92 +ML {* structure Success_Intros = Named_Thms(
1.93 + val name = "success_intros"
1.94 + val description = "introduction rules for success"
1.95 +) *}
1.96 +
1.97 +setup Success_Intros.setup
1.98 +
1.99 +lemma success_tapI [iff, success_intros]:
1.100 + "success (tap f) h"
1.101 + by (rule successI) simp
1.102 +
1.103 +lemma success_heapI [iff, success_intros]:
1.104 + "success (heap f) h"
1.105 + by (rule successI) simp
1.106 +
1.107 +lemma success_guardI [success_intros]:
1.108 + "P h \<Longrightarrow> success (guard P f) h"
1.109 + by (rule successI) (simp add: execute_guard)
1.110 +
1.111 +lemma success_LetI [success_intros]:
1.112 + "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
1.113 + by (simp add: Let_def)
1.114 +
1.115 +
1.116 +subsubsection {* Monad combinators *}
1.117
1.118 definition return :: "'a \<Rightarrow> 'a Heap" where
1.119 [code del]: "return x = heap (Pair x)"
1.120
1.121 -lemma execute_return [simp]:
1.122 +lemma execute_return [simp, execute_simps]:
1.123 "execute (return x) = Some \<circ> Pair x"
1.124 by (simp add: return_def)
1.125
1.126 +lemma success_returnI [iff, success_intros]:
1.127 + "success (return x) h"
1.128 + by (rule successI) simp
1.129 +
1.130 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
1.131 [code del]: "raise s = Heap (\<lambda>_. None)"
1.132
1.133 -lemma execute_raise [simp]:
1.134 +lemma execute_raise [simp, execute_simps]:
1.135 "execute (raise s) = (\<lambda>_. None)"
1.136 by (simp add: raise_def)
1.137
1.138 @@ -73,14 +135,18 @@
1.139
1.140 notation bind (infixl "\<guillemotright>=" 54)
1.141
1.142 -lemma execute_bind [simp]:
1.143 +lemma execute_bind [execute_simps]:
1.144 "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
1.145 "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
1.146 by (simp_all add: bind_def)
1.147
1.148 -lemma execute_bind_heap [simp]:
1.149 - "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
1.150 - by (simp add: bind_def split_def)
1.151 +lemma success_bindI [success_intros]:
1.152 + "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
1.153 + by (auto intro!: successI elim!: successE simp add: bind_def)
1.154 +
1.155 +lemma execute_bind_successI [execute_simps]:
1.156 + "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
1.157 + by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
1.158
1.159 lemma execute_eq_SomeI:
1.160 assumes "Heap_Monad.execute f h = Some (x, h')"
1.161 @@ -89,7 +155,7 @@
1.162 using assms by (simp add: bind_def)
1.163
1.164 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
1.165 - by (rule Heap_eqI) simp
1.166 + by (rule Heap_eqI) (simp add: execute_bind)
1.167
1.168 lemma bind_return [simp]: "f \<guillemotright>= return = f"
1.169 by (rule Heap_eqI) (simp add: bind_def split: option.splits)
1.170 @@ -98,7 +164,7 @@
1.171 by (rule Heap_eqI) (simp add: bind_def split: option.splits)
1.172
1.173 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
1.174 - by (rule Heap_eqI) simp
1.175 + by (rule Heap_eqI) (simp add: execute_bind)
1.176
1.177 abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
1.178 "f >> g \<equiv> f >>= (\<lambda>_. g)"
1.179 @@ -187,24 +253,31 @@
1.180 *}
1.181
1.182
1.183 -subsection {* Monad properties *}
1.184 +subsection {* Generic combinators *}
1.185
1.186 -subsection {* Generic combinators *}
1.187 +subsubsection {* Assertions *}
1.188
1.189 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
1.190 "assert P x = (if P x then return x else raise ''assert'')"
1.191
1.192 -lemma execute_assert [simp]:
1.193 +lemma execute_assert [execute_simps]:
1.194 "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
1.195 "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
1.196 by (simp_all add: assert_def)
1.197
1.198 +lemma success_assertI [success_intros]:
1.199 + "P x \<Longrightarrow> success (assert P x) h"
1.200 + by (rule successI) (simp add: execute_assert)
1.201 +
1.202 lemma assert_cong [fundef_cong]:
1.203 assumes "P = P'"
1.204 assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
1.205 shows "(assert P x >>= f) = (assert P' x >>= f')"
1.206 by (rule Heap_eqI) (insert assms, simp add: assert_def)
1.207
1.208 +
1.209 +subsubsection {* Plain lifting *}
1.210 +
1.211 definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
1.212 "lift f = return o f"
1.213
1.214 @@ -216,6 +289,9 @@
1.215 "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
1.216 by (simp add: lift_def comp_def)
1.217
1.218 +
1.219 +subsubsection {* Iteration -- warning: this is rarely useful! *}
1.220 +
1.221 primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
1.222 "fold_map f [] = return []"
1.223 | "fold_map f (x # xs) = do
1.224 @@ -228,7 +304,7 @@
1.225 "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
1.226 by (induct xs) simp_all
1.227
1.228 -lemma execute_fold_map_unchanged_heap:
1.229 +lemma execute_fold_map_unchanged_heap [execute_simps]:
1.230 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
1.231 shows "execute (fold_map f xs) h =
1.232 Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
1.233 @@ -527,6 +603,6 @@
1.234 code_const return (Haskell "return")
1.235 code_const Heap_Monad.raise' (Haskell "error/ _")
1.236
1.237 -hide_const (open) Heap heap guard execute raise' fold_map
1.238 +hide_const (open) Heap heap guard raise' fold_map
1.239
1.240 end