1.1 --- a/src/HOL/Imperative_HOL/Array.thy Fri Jul 09 16:32:25 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Array.thy Fri Jul 09 17:00:42 2010 +0200
1.3 @@ -56,7 +56,7 @@
1.4 [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
1.5
1.6 definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
1.7 - [code del]: "len a = Heap_Monad.heap (\<lambda>h. (length a h, h))"
1.8 + [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
1.9
1.10 definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
1.11 [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
1.12 @@ -75,7 +75,7 @@
1.13 (\<lambda>h. (get_array a h ! i, change a i x h))"
1.14
1.15 definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
1.16 - [code del]: "freeze a = Heap_Monad.heap (\<lambda>h. (get_array a h, h))"
1.17 + [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
1.18
1.19
1.20 subsection {* Properties *}
1.21 @@ -83,6 +83,8 @@
1.22 text {* FIXME: Does there exist a "canonical" array axiomatisation in
1.23 the literature? *}
1.24
1.25 +text {* Primitives *}
1.26 +
1.27 lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
1.28 and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
1.29 unfolding noteq_arrs_def by auto
1.30 @@ -153,50 +155,89 @@
1.31 "array_present a (change b i v h) = array_present a h"
1.32 by (simp add: change_def array_present_def set_array_def get_array_def)
1.33
1.34 -lemma execute_new [simp]:
1.35 - "Heap_Monad.execute (new n x) h = Some (array (replicate n x) h)"
1.36 +
1.37 +text {* Monad operations *}
1.38 +
1.39 +lemma execute_new [simp, execute_simps]:
1.40 + "execute (new n x) h = Some (array (replicate n x) h)"
1.41 by (simp add: new_def)
1.42
1.43 -lemma execute_of_list [simp]:
1.44 - "Heap_Monad.execute (of_list xs) h = Some (array xs h)"
1.45 +lemma success_newI [iff, success_intros]:
1.46 + "success (new n x) h"
1.47 + by (simp add: new_def)
1.48 +
1.49 +lemma execute_of_list [simp, execute_simps]:
1.50 + "execute (of_list xs) h = Some (array xs h)"
1.51 by (simp add: of_list_def)
1.52
1.53 -lemma execute_make [simp]:
1.54 - "Heap_Monad.execute (make n f) h = Some (array (map f [0 ..< n]) h)"
1.55 +lemma success_of_listI [iff, success_intros]:
1.56 + "success (of_list xs) h"
1.57 + by (simp add: of_list_def)
1.58 +
1.59 +lemma execute_make [simp, execute_simps]:
1.60 + "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
1.61 by (simp add: make_def)
1.62
1.63 -lemma execute_len [simp]:
1.64 - "Heap_Monad.execute (len a) h = Some (length a h, h)"
1.65 +lemma success_makeI [iff, success_intros]:
1.66 + "success (make n f) h"
1.67 + by (simp add: make_def)
1.68 +
1.69 +lemma execute_len [simp, execute_simps]:
1.70 + "execute (len a) h = Some (length a h, h)"
1.71 by (simp add: len_def)
1.72
1.73 -lemma execute_nth [simp]:
1.74 +lemma success_lenI [iff, success_intros]:
1.75 + "success (len a) h"
1.76 + by (simp add: len_def)
1.77 +
1.78 +lemma execute_nth [execute_simps]:
1.79 "i < length a h \<Longrightarrow>
1.80 - Heap_Monad.execute (nth a i) h = Some (get_array a h ! i, h)"
1.81 - "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
1.82 - by (simp_all add: nth_def)
1.83 + execute (nth a i) h = Some (get_array a h ! i, h)"
1.84 + "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
1.85 + by (simp_all add: nth_def execute_simps)
1.86
1.87 -lemma execute_upd [simp]:
1.88 +lemma success_nthI [success_intros]:
1.89 + "i < length a h \<Longrightarrow> success (nth a i) h"
1.90 + by (auto intro: success_intros simp add: nth_def)
1.91 +
1.92 +lemma execute_upd [execute_simps]:
1.93 "i < length a h \<Longrightarrow>
1.94 - Heap_Monad.execute (upd i x a) h = Some (a, change a i x h)"
1.95 - "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
1.96 - by (simp_all add: upd_def)
1.97 + execute (upd i x a) h = Some (a, change a i x h)"
1.98 + "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
1.99 + by (simp_all add: upd_def execute_simps)
1.100
1.101 -lemma execute_map_entry [simp]:
1.102 +lemma success_updI [success_intros]:
1.103 + "i < length a h \<Longrightarrow> success (upd i x a) h"
1.104 + by (auto intro: success_intros simp add: upd_def)
1.105 +
1.106 +lemma execute_map_entry [execute_simps]:
1.107 "i < length a h \<Longrightarrow>
1.108 - Heap_Monad.execute (map_entry i f a) h =
1.109 + execute (map_entry i f a) h =
1.110 Some (a, change a i (f (get_array a h ! i)) h)"
1.111 - "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
1.112 - by (simp_all add: map_entry_def)
1.113 + "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
1.114 + by (simp_all add: map_entry_def execute_simps)
1.115
1.116 -lemma execute_swap [simp]:
1.117 +lemma success_map_entryI [success_intros]:
1.118 + "i < length a h \<Longrightarrow> success (map_entry i f a) h"
1.119 + by (auto intro: success_intros simp add: map_entry_def)
1.120 +
1.121 +lemma execute_swap [execute_simps]:
1.122 "i < length a h \<Longrightarrow>
1.123 - Heap_Monad.execute (swap i x a) h =
1.124 + execute (swap i x a) h =
1.125 Some (get_array a h ! i, change a i x h)"
1.126 - "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
1.127 - by (simp_all add: swap_def)
1.128 + "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
1.129 + by (simp_all add: swap_def execute_simps)
1.130
1.131 -lemma execute_freeze [simp]:
1.132 - "Heap_Monad.execute (freeze a) h = Some (get_array a h, h)"
1.133 +lemma success_swapI [success_intros]:
1.134 + "i < length a h \<Longrightarrow> success (swap i x a) h"
1.135 + by (auto intro: success_intros simp add: swap_def)
1.136 +
1.137 +lemma execute_freeze [simp, execute_simps]:
1.138 + "execute (freeze a) h = Some (get_array a h, h)"
1.139 + by (simp add: freeze_def)
1.140 +
1.141 +lemma success_freezeI [iff, success_intros]:
1.142 + "success (freeze a) h"
1.143 by (simp add: freeze_def)
1.144
1.145 lemma upd_return:
1.146 @@ -265,7 +306,7 @@
1.147 x \<leftarrow> nth a i;
1.148 upd i (f x) a
1.149 done)"
1.150 - by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def)
1.151 + by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
1.152
1.153 lemma [code]:
1.154 "swap i x a = (do
1.155 @@ -273,7 +314,7 @@
1.156 upd i x a;
1.157 return y
1.158 done)"
1.159 - by (rule Heap_eqI) (simp add: bind_def guard_def swap_def)
1.160 + by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
1.161
1.162 lemma [code]:
1.163 "freeze a = (do
1.164 @@ -288,18 +329,18 @@
1.165 [0..<length a h] =
1.166 List.map (List.nth (get_array a h)) [0..<length a h]"
1.167 by simp
1.168 - have "Heap_Monad.execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
1.169 + have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
1.170 Some (get_array a h, h)"
1.171 apply (subst execute_fold_map_unchanged_heap)
1.172 apply (simp_all add: nth_def guard_def *)
1.173 apply (simp add: length_def map_nth)
1.174 done
1.175 - then have "Heap_Monad.execute (do
1.176 + then have "execute (do
1.177 n \<leftarrow> len a;
1.178 Heap_Monad.fold_map (Array.nth a) [0..<n]
1.179 done) h = Some (get_array a h, h)"
1.180 by (auto intro: execute_eq_SomeI)
1.181 - then show "Heap_Monad.execute (freeze a) h = Heap_Monad.execute (do
1.182 + then show "execute (freeze a) h = execute (do
1.183 n \<leftarrow> len a;
1.184 Heap_Monad.fold_map (Array.nth a) [0..<n]
1.185 done) h" by simp
2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 09 16:32:25 2010 +0200
2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 09 17:00:42 2010 +0200
2.3 @@ -10,7 +10,7 @@
2.4
2.5 subsection {* The monad *}
2.6
2.7 -subsubsection {* Monad combinators *}
2.8 +subsubsection {* Monad construction *}
2.9
2.10 text {* Monadic heap actions either produce values
2.11 and transform the heap, or fail *}
2.12 @@ -19,6 +19,13 @@
2.13 primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
2.14 [code del]: "execute (Heap f) = f"
2.15
2.16 +lemma Heap_cases [case_names succeed fail]:
2.17 + fixes f and h
2.18 + assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
2.19 + assumes fail: "execute f h = None \<Longrightarrow> P"
2.20 + shows P
2.21 + using assms by (cases "execute f h") auto
2.22 +
2.23 lemma Heap_execute [simp]:
2.24 "Heap (execute f) = f" by (cases f) simp_all
2.25
2.26 @@ -26,43 +33,98 @@
2.27 "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
2.28 by (cases f, cases g) (auto simp: expand_fun_eq)
2.29
2.30 -lemma Heap_eqI':
2.31 - "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
2.32 - by (auto simp: expand_fun_eq intro: Heap_eqI)
2.33 +ML {* structure Execute_Simps = Named_Thms(
2.34 + val name = "execute_simps"
2.35 + val description = "simplification rules for execute"
2.36 +) *}
2.37 +
2.38 +setup Execute_Simps.setup
2.39 +
2.40 +lemma execute_Let [simp, execute_simps]:
2.41 + "execute (let x = t in f x) = (let x = t in execute (f x))"
2.42 + by (simp add: Let_def)
2.43 +
2.44 +
2.45 +subsubsection {* Specialised lifters *}
2.46 +
2.47 +definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
2.48 + [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
2.49 +
2.50 +lemma execute_tap [simp, execute_simps]:
2.51 + "execute (tap f) h = Some (f h, h)"
2.52 + by (simp add: tap_def)
2.53
2.54 definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
2.55 [code del]: "heap f = Heap (Some \<circ> f)"
2.56
2.57 -lemma execute_heap [simp]:
2.58 +lemma execute_heap [simp, execute_simps]:
2.59 "execute (heap f) = Some \<circ> f"
2.60 by (simp add: heap_def)
2.61
2.62 definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
2.63 [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
2.64
2.65 -lemma execute_guard [simp]:
2.66 +lemma execute_guard [execute_simps]:
2.67 "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
2.68 "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
2.69 by (simp_all add: guard_def)
2.70
2.71 -lemma heap_cases [case_names succeed fail]:
2.72 - fixes f and h
2.73 - assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
2.74 - assumes fail: "execute f h = None \<Longrightarrow> P"
2.75 - shows P
2.76 - using assms by (cases "execute f h") auto
2.77 +
2.78 +subsubsection {* Predicate classifying successful computations *}
2.79 +
2.80 +definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
2.81 + "success f h \<longleftrightarrow> execute f h \<noteq> None"
2.82 +
2.83 +lemma successI:
2.84 + "execute f h \<noteq> None \<Longrightarrow> success f h"
2.85 + by (simp add: success_def)
2.86 +
2.87 +lemma successE:
2.88 + assumes "success f h"
2.89 + obtains r h' where "execute f h = Some (r, h')"
2.90 + using assms by (auto simp add: success_def)
2.91 +
2.92 +ML {* structure Success_Intros = Named_Thms(
2.93 + val name = "success_intros"
2.94 + val description = "introduction rules for success"
2.95 +) *}
2.96 +
2.97 +setup Success_Intros.setup
2.98 +
2.99 +lemma success_tapI [iff, success_intros]:
2.100 + "success (tap f) h"
2.101 + by (rule successI) simp
2.102 +
2.103 +lemma success_heapI [iff, success_intros]:
2.104 + "success (heap f) h"
2.105 + by (rule successI) simp
2.106 +
2.107 +lemma success_guardI [success_intros]:
2.108 + "P h \<Longrightarrow> success (guard P f) h"
2.109 + by (rule successI) (simp add: execute_guard)
2.110 +
2.111 +lemma success_LetI [success_intros]:
2.112 + "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
2.113 + by (simp add: Let_def)
2.114 +
2.115 +
2.116 +subsubsection {* Monad combinators *}
2.117
2.118 definition return :: "'a \<Rightarrow> 'a Heap" where
2.119 [code del]: "return x = heap (Pair x)"
2.120
2.121 -lemma execute_return [simp]:
2.122 +lemma execute_return [simp, execute_simps]:
2.123 "execute (return x) = Some \<circ> Pair x"
2.124 by (simp add: return_def)
2.125
2.126 +lemma success_returnI [iff, success_intros]:
2.127 + "success (return x) h"
2.128 + by (rule successI) simp
2.129 +
2.130 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
2.131 [code del]: "raise s = Heap (\<lambda>_. None)"
2.132
2.133 -lemma execute_raise [simp]:
2.134 +lemma execute_raise [simp, execute_simps]:
2.135 "execute (raise s) = (\<lambda>_. None)"
2.136 by (simp add: raise_def)
2.137
2.138 @@ -73,14 +135,18 @@
2.139
2.140 notation bind (infixl "\<guillemotright>=" 54)
2.141
2.142 -lemma execute_bind [simp]:
2.143 +lemma execute_bind [execute_simps]:
2.144 "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
2.145 "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
2.146 by (simp_all add: bind_def)
2.147
2.148 -lemma execute_bind_heap [simp]:
2.149 - "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
2.150 - by (simp add: bind_def split_def)
2.151 +lemma success_bindI [success_intros]:
2.152 + "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
2.153 + by (auto intro!: successI elim!: successE simp add: bind_def)
2.154 +
2.155 +lemma execute_bind_successI [execute_simps]:
2.156 + "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
2.157 + by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
2.158
2.159 lemma execute_eq_SomeI:
2.160 assumes "Heap_Monad.execute f h = Some (x, h')"
2.161 @@ -89,7 +155,7 @@
2.162 using assms by (simp add: bind_def)
2.163
2.164 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
2.165 - by (rule Heap_eqI) simp
2.166 + by (rule Heap_eqI) (simp add: execute_bind)
2.167
2.168 lemma bind_return [simp]: "f \<guillemotright>= return = f"
2.169 by (rule Heap_eqI) (simp add: bind_def split: option.splits)
2.170 @@ -98,7 +164,7 @@
2.171 by (rule Heap_eqI) (simp add: bind_def split: option.splits)
2.172
2.173 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
2.174 - by (rule Heap_eqI) simp
2.175 + by (rule Heap_eqI) (simp add: execute_bind)
2.176
2.177 abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
2.178 "f >> g \<equiv> f >>= (\<lambda>_. g)"
2.179 @@ -187,24 +253,31 @@
2.180 *}
2.181
2.182
2.183 -subsection {* Monad properties *}
2.184 +subsection {* Generic combinators *}
2.185
2.186 -subsection {* Generic combinators *}
2.187 +subsubsection {* Assertions *}
2.188
2.189 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
2.190 "assert P x = (if P x then return x else raise ''assert'')"
2.191
2.192 -lemma execute_assert [simp]:
2.193 +lemma execute_assert [execute_simps]:
2.194 "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
2.195 "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
2.196 by (simp_all add: assert_def)
2.197
2.198 +lemma success_assertI [success_intros]:
2.199 + "P x \<Longrightarrow> success (assert P x) h"
2.200 + by (rule successI) (simp add: execute_assert)
2.201 +
2.202 lemma assert_cong [fundef_cong]:
2.203 assumes "P = P'"
2.204 assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
2.205 shows "(assert P x >>= f) = (assert P' x >>= f')"
2.206 by (rule Heap_eqI) (insert assms, simp add: assert_def)
2.207
2.208 +
2.209 +subsubsection {* Plain lifting *}
2.210 +
2.211 definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
2.212 "lift f = return o f"
2.213
2.214 @@ -216,6 +289,9 @@
2.215 "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
2.216 by (simp add: lift_def comp_def)
2.217
2.218 +
2.219 +subsubsection {* Iteration -- warning: this is rarely useful! *}
2.220 +
2.221 primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
2.222 "fold_map f [] = return []"
2.223 | "fold_map f (x # xs) = do
2.224 @@ -228,7 +304,7 @@
2.225 "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
2.226 by (induct xs) simp_all
2.227
2.228 -lemma execute_fold_map_unchanged_heap:
2.229 +lemma execute_fold_map_unchanged_heap [execute_simps]:
2.230 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
2.231 shows "execute (fold_map f xs) h =
2.232 Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
2.233 @@ -527,6 +603,6 @@
2.234 code_const return (Haskell "return")
2.235 code_const Heap_Monad.raise' (Haskell "error/ _")
2.236
2.237 -hide_const (open) Heap heap guard execute raise' fold_map
2.238 +hide_const (open) Heap heap guard raise' fold_map
2.239
2.240 end
3.1 --- a/src/HOL/Imperative_HOL/Ref.thy Fri Jul 09 16:32:25 2010 +0200
3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Fri Jul 09 17:00:42 2010 +0200
3.3 @@ -42,7 +42,7 @@
3.4 [code del]: "ref v = Heap_Monad.heap (alloc v)"
3.5
3.6 definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
3.7 - [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get h r, h))"
3.8 + [code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)"
3.9
3.10 definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where
3.11 [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
3.12 @@ -58,6 +58,8 @@
3.13
3.14 subsection {* Properties *}
3.15
3.16 +text {* Primitives *}
3.17 +
3.18 lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r"
3.19 and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
3.20 by (auto simp add: noteq_def)
3.21 @@ -126,26 +128,44 @@
3.22 "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'"
3.23 by (auto simp add: noteq_def present_def)
3.24
3.25 -lemma execute_ref [simp]:
3.26 - "Heap_Monad.execute (ref v) h = Some (alloc v h)"
3.27 +
3.28 +text {* Monad operations *}
3.29 +
3.30 +lemma execute_ref [simp, execute_simps]:
3.31 + "execute (ref v) h = Some (alloc v h)"
3.32 by (simp add: ref_def)
3.33
3.34 -lemma execute_lookup [simp]:
3.35 +lemma success_refI [iff, success_intros]:
3.36 + "success (ref v) h"
3.37 + by (auto simp add: ref_def)
3.38 +
3.39 +lemma execute_lookup [simp, execute_simps]:
3.40 "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
3.41 by (simp add: lookup_def)
3.42
3.43 -lemma execute_update [simp]:
3.44 +lemma success_lookupI [iff, success_intros]:
3.45 + "success (lookup r) h"
3.46 + by (auto simp add: lookup_def)
3.47 +
3.48 +lemma execute_update [simp, execute_simps]:
3.49 "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
3.50 by (simp add: update_def)
3.51
3.52 -lemma execute_change [simp]:
3.53 +lemma success_updateI [iff, success_intros]:
3.54 + "success (update r v) h"
3.55 + by (auto simp add: update_def)
3.56 +
3.57 +lemma execute_change [simp, execute_simps]:
3.58 "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
3.59 - by (cases "!r" h rule: heap_cases)
3.60 - (simp_all only: change_def execute_bind, auto simp add: Let_def)
3.61 + by (simp add: change_def bind_def Let_def)
3.62 +
3.63 +lemma success_changeI [iff, success_intros]:
3.64 + "success (change f r) h"
3.65 + by (auto intro!: success_intros simp add: change_def)
3.66
3.67 lemma lookup_chain:
3.68 "(!r \<guillemotright> f) = f"
3.69 - by (rule Heap_eqI) (simp add: lookup_def)
3.70 + by (rule Heap_eqI) (auto simp add: lookup_def execute_simps)
3.71
3.72 lemma update_change [code]:
3.73 "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
3.74 @@ -233,4 +253,4 @@
3.75 code_const Ref.lookup (Haskell "Heap.readSTRef")
3.76 code_const Ref.update (Haskell "Heap.writeSTRef")
3.77
3.78 -end
3.79 \ No newline at end of file
3.80 +end
4.1 --- a/src/HOL/Imperative_HOL/Relational.thy Fri Jul 09 16:32:25 2010 +0200
4.2 +++ b/src/HOL/Imperative_HOL/Relational.thy Fri Jul 09 17:00:42 2010 +0200
4.3 @@ -23,6 +23,11 @@
4.4 text {* For all commands, we define simple elimination rules. *}
4.5 (* FIXME: consumes 1 necessary ?? *)
4.6
4.7 +lemma crel_tap:
4.8 + assumes "crel (Heap_Monad.tap f) h h' r"
4.9 + obtains "h' = h" "r = f h"
4.10 + using assms by (simp add: crel_def)
4.11 +
4.12 lemma crel_heap:
4.13 assumes "crel (Heap_Monad.heap f) h h' r"
4.14 obtains "h' = snd (f h)" "r = fst (f h)"
4.15 @@ -31,7 +36,7 @@
4.16 lemma crel_guard:
4.17 assumes "crel (Heap_Monad.guard P f) h h' r"
4.18 obtains "h' = snd (f h)" "r = fst (f h)" "P h"
4.19 - using assms by (cases "f h", cases "P h") (simp_all add: crel_def)
4.20 + using assms by (cases "f h", cases "P h") (simp_all add: crel_def execute_simps)
4.21
4.22
4.23 subsection {* Elimination rules for basic monadic commands *}
4.24 @@ -121,7 +126,7 @@
4.25 assumes "crel (len a) h h' r"
4.26 obtains "h = h'" "r = Array.length a h'"
4.27 using assms unfolding Array.len_def
4.28 - by (elim crel_heap) simp
4.29 + by (elim crel_tap) simp
4.30
4.31 lemma crel_nth[consumes 1]:
4.32 assumes "crel (nth a i) h h' r"
4.33 @@ -184,7 +189,7 @@
4.34 assumes "crel (Array.freeze a) h h' xs"
4.35 obtains "h = h'" "xs = get_array a h"
4.36 using assms unfolding freeze_def
4.37 - by (elim crel_heap) simp
4.38 + by (elim crel_tap) simp
4.39
4.40 lemma crel_fold_map_map_entry_remains:
4.41 assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
4.42 @@ -314,23 +319,20 @@
4.43 lemma crel_lookup:
4.44 assumes "crel (!r') h h' r"
4.45 obtains "h = h'" "r = Ref.get h r'"
4.46 -using assms
4.47 -unfolding Ref.lookup_def
4.48 -by (auto elim: crel_heap)
4.49 + using assms unfolding Ref.lookup_def
4.50 + by (auto elim: crel_tap)
4.51
4.52 lemma crel_update:
4.53 assumes "crel (r' := v) h h' r"
4.54 obtains "h' = Ref.set r' v h" "r = ()"
4.55 -using assms
4.56 -unfolding Ref.update_def
4.57 -by (auto elim: crel_heap)
4.58 + using assms unfolding Ref.update_def
4.59 + by (auto elim: crel_heap)
4.60
4.61 lemma crel_change:
4.62 assumes "crel (Ref.change f r') h h' r"
4.63 obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
4.64 -using assms
4.65 -unfolding Ref.change_def Let_def
4.66 -by (auto elim!: crelE crel_lookup crel_update crel_return)
4.67 + using assms unfolding Ref.change_def Let_def
4.68 + by (auto elim!: crelE crel_lookup crel_update crel_return)
4.69
4.70 subsection {* Elimination rules for the assert command *}
4.71
4.72 @@ -388,6 +390,11 @@
4.73 using assms
4.74 by (auto split: option.split)
4.75
4.76 +lemma crel_tapI:
4.77 + assumes "h' = h" "r = f h"
4.78 + shows "crel (Heap_Monad.tap f) h h' r"
4.79 + using assms by (simp add: crel_def)
4.80 +
4.81 lemma crel_heapI:
4.82 shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
4.83 by (simp add: crel_def apfst_def split_def prod_fun_def)
4.84 @@ -401,7 +408,7 @@
4.85 lemma crel_guardI:
4.86 assumes "P h" "h' = snd (f h)" "r = fst (f h)"
4.87 shows "crel (Heap_Monad.guard P f) h h' r"
4.88 - using assms by (simp add: crel_def)
4.89 + using assms by (simp add: crel_def execute_simps)
4.90
4.91 lemma crelI2:
4.92 assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
4.93 @@ -418,8 +425,7 @@
4.94
4.95 lemma crel_lengthI:
4.96 shows "crel (Array.len a) h h (Array.length a h)"
4.97 - unfolding len_def
4.98 - by (rule crel_heapI') auto
4.99 + unfolding len_def by (rule crel_tapI) simp_all
4.100
4.101 (* thm crel_newI for Array.new is missing *)
4.102
4.103 @@ -449,7 +455,7 @@
4.104
4.105 lemma crel_lookupI:
4.106 shows "crel (!r) h h (Ref.get h r)"
4.107 - unfolding lookup_def by (auto intro!: crel_heapI')
4.108 + unfolding lookup_def by (auto intro!: crel_tapI)
4.109
4.110 lemma crel_updateI:
4.111 shows "crel (r := v) h (Ref.set r v h) ()"
4.112 @@ -457,7 +463,7 @@
4.113
4.114 lemma crel_changeI:
4.115 shows "crel (Ref.change f r) h (Ref.set r (f (Ref.get h r)) h) (f (Ref.get h r))"
4.116 -unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
4.117 + unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
4.118
4.119 subsubsection {* Introduction rules for the assert command *}
4.120
4.121 @@ -487,173 +493,26 @@
4.122 next
4.123 qed (auto simp add: assms(2)[unfolded crel_def])
4.124
4.125 -section {* Definition of the noError predicate *}
4.126
4.127 -text {* We add a simple definitional setting for crel intro rules
4.128 - where we only would like to show that the computation does not result in a exception for heap h,
4.129 - but we do not care about statements about the resulting heap and return value.*}
4.130 -
4.131 -definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
4.132 -where
4.133 - "noError c h \<longleftrightarrow> (\<exists>r h'. Some (r, h') = Heap_Monad.execute c h)"
4.134 -
4.135 -lemma noError_def': -- FIXME
4.136 - "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = Some (r, h'))"
4.137 - unfolding noError_def apply auto proof -
4.138 - fix r h'
4.139 - assume "Some (r, h') = Heap_Monad.execute c h"
4.140 - then have "Heap_Monad.execute c h = Some (r, h')" ..
4.141 - then show "\<exists>r h'. Heap_Monad.execute c h = Some (r, h')" by blast
4.142 -qed
4.143 -
4.144 -subsection {* Introduction rules for basic monadic commands *}
4.145 -
4.146 -lemma noErrorI:
4.147 - assumes "noError f h"
4.148 - assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
4.149 - shows "noError (f \<guillemotright>= g) h"
4.150 - using assms
4.151 - by (auto simp add: noError_def' crel_def' bind_def)
4.152 -
4.153 -lemma noErrorI':
4.154 - assumes "noError f h"
4.155 - assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
4.156 - shows "noError (f \<guillemotright> g) h"
4.157 - using assms
4.158 - by (auto simp add: noError_def' crel_def' bind_def)
4.159 -
4.160 -lemma noErrorI2:
4.161 -"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
4.162 -\<Longrightarrow> noError (f \<guillemotright>= g) h"
4.163 -by (auto simp add: noError_def' crel_def' bind_def)
4.164 -
4.165 -lemma noError_return:
4.166 - shows "noError (return x) h"
4.167 - unfolding noError_def return_def
4.168 - by auto
4.169 -
4.170 -lemma noError_if:
4.171 - assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
4.172 - shows "noError (if c then t else e) h"
4.173 - using assms
4.174 - unfolding noError_def
4.175 - by auto
4.176 -
4.177 -lemma noError_option_case:
4.178 - assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
4.179 - assumes "noError n h"
4.180 - shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
4.181 -using assms
4.182 -by (auto split: option.split)
4.183 -
4.184 -lemma noError_fold_map:
4.185 -assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)"
4.186 -shows "noError (Heap_Monad.fold_map f xs) h"
4.187 -using assms
4.188 -proof (induct xs)
4.189 - case Nil
4.190 - thus ?case
4.191 - unfolding fold_map.simps by (intro noError_return)
4.192 -next
4.193 - case (Cons x xs)
4.194 - thus ?case
4.195 - unfolding fold_map.simps
4.196 - by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
4.197 -qed
4.198 -
4.199 -lemma noError_heap [simp]:
4.200 - "noError (Heap_Monad.heap f) h"
4.201 - by (simp add: noError_def')
4.202 -
4.203 -lemma noError_guard [simp]:
4.204 - "P h \<Longrightarrow> noError (Heap_Monad.guard P f) h"
4.205 - by (simp add: noError_def')
4.206 -
4.207 -subsection {* Introduction rules for array commands *}
4.208 -
4.209 -lemma noError_length:
4.210 - shows "noError (Array.len a) h"
4.211 - by (simp add: len_def)
4.212 -
4.213 -lemma noError_new:
4.214 - shows "noError (Array.new n v) h"
4.215 - by (simp add: Array.new_def)
4.216 -
4.217 -lemma noError_upd:
4.218 - assumes "i < Array.length a h"
4.219 - shows "noError (Array.upd i v a) h"
4.220 - using assms by (simp add: upd_def)
4.221 -
4.222 -lemma noError_nth:
4.223 - assumes "i < Array.length a h"
4.224 - shows "noError (Array.nth a i) h"
4.225 - using assms by (simp add: nth_def)
4.226 -
4.227 -lemma noError_of_list:
4.228 - "noError (of_list ls) h"
4.229 - by (simp add: of_list_def)
4.230 -
4.231 -lemma noError_map_entry:
4.232 - assumes "i < Array.length a h"
4.233 - shows "noError (map_entry i f a) h"
4.234 - using assms by (simp add: map_entry_def)
4.235 -
4.236 -lemma noError_swap:
4.237 - assumes "i < Array.length a h"
4.238 - shows "noError (swap i x a) h"
4.239 - using assms by (simp add: swap_def)
4.240 -
4.241 -lemma noError_make:
4.242 - "noError (make n f) h"
4.243 - by (simp add: make_def)
4.244 -
4.245 -lemma noError_freeze:
4.246 - "noError (freeze a) h"
4.247 - by (simp add: freeze_def)
4.248 -
4.249 -lemma noError_fold_map_map_entry:
4.250 +lemma success_fold_map_map_entry:
4.251 assumes "n \<le> Array.length a h"
4.252 - shows "noError (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
4.253 + shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
4.254 using assms
4.255 proof (induct n arbitrary: h)
4.256 case 0
4.257 - thus ?case by (auto intro: noError_return)
4.258 + thus ?case by (auto intro: success_returnI)
4.259 next
4.260 case (Suc n)
4.261 - from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
4.262 + from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] =
4.263 + (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
4.264 by (simp add: upt_conv_Cons')
4.265 - with Suc.hyps[of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case
4.266 - by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
4.267 + with Suc.hyps [of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case apply -
4.268 + apply (auto simp add: execute_simps intro!: successI success_returnI success_map_entryI elim: crel_map_entry)
4.269 + apply (subst execute_bind) apply (auto simp add: execute_simps)
4.270 + done
4.271 qed
4.272
4.273
4.274 -subsection {* Introduction rules for the reference commands *}
4.275 -
4.276 -lemma noError_Ref_new:
4.277 - shows "noError (ref v) h"
4.278 - by (simp add: Ref.ref_def)
4.279 -
4.280 -lemma noError_lookup:
4.281 - shows "noError (!r) h"
4.282 - by (simp add: lookup_def)
4.283 -
4.284 -lemma noError_update:
4.285 - shows "noError (r := v) h"
4.286 - by (simp add: update_def)
4.287 -
4.288 -lemma noError_change:
4.289 - shows "noError (Ref.change f r) h"
4.290 - by (simp add: change_def)
4.291 - (auto intro!: noErrorI2 noError_lookup noError_update noError_return crel_lookupI crel_updateI simp add: Let_def)
4.292 -
4.293 -subsection {* Introduction rules for the assert command *}
4.294 -
4.295 -lemma noError_assert:
4.296 - assumes "P x"
4.297 - shows "noError (assert P x) h"
4.298 - using assms unfolding assert_def
4.299 - by (auto intro: noError_if noError_return)
4.300 -
4.301 section {* Cumulative lemmas *}
4.302
4.303 lemmas crel_elim_all =
4.304 @@ -668,10 +527,5 @@
4.305 (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
4.306 crel_assert
4.307
4.308 -lemmas noError_intro_all =
4.309 - noErrorI noErrorI' noError_return noError_if noError_option_case
4.310 - noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze
4.311 - noError_Ref_new noError_lookup noError_update noError_change
4.312 - noError_assert
4.313
4.314 end
4.315 \ No newline at end of file
5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Fri Jul 09 16:32:25 2010 +0200
5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Fri Jul 09 17:00:42 2010 +0200
5.3 @@ -575,23 +575,35 @@
5.4 text {* We have proved that quicksort sorts (if no exceptions occur).
5.5 We will now show that exceptions do not occur. *}
5.6
5.7 -lemma noError_part1:
5.8 +lemma success_part1I:
5.9 assumes "l < Array.length a h" "r < Array.length a h"
5.10 - shows "noError (part1 a l r p) h"
5.11 + shows "success (part1 a l r p) h"
5.12 using assms
5.13 proof (induct a l r p arbitrary: h rule: part1.induct)
5.14 case (1 a l r p)
5.15 thus ?case
5.16 unfolding part1.simps [of a l r] swap_def
5.17 - by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
5.18 + by (auto simp add: execute_simps intro!: success_intros elim!: crelE crel_upd crel_nth crel_return)
5.19 qed
5.20
5.21 -lemma noError_partition:
5.22 +lemma success_ifI: (*FIXME move*)
5.23 + assumes "c \<Longrightarrow> success t h" "\<not> c \<Longrightarrow> success e h"
5.24 + shows "success (if c then t else e) h"
5.25 + using assms
5.26 + unfolding success_def
5.27 + by auto
5.28 +
5.29 +lemma success_bindI' [success_intros]: (*FIXME move*)
5.30 + assumes "success f h"
5.31 + assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
5.32 + shows "success (f \<guillemotright>= g) h"
5.33 + using assms by (auto intro!: successI elim!: successE simp add: bind_def crel_def success_def) blast
5.34 +
5.35 +lemma success_partitionI:
5.36 assumes "l < r" "l < Array.length a h" "r < Array.length a h"
5.37 - shows "noError (partition a l r) h"
5.38 -using assms
5.39 -unfolding partition.simps swap_def
5.40 -apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
5.41 + shows "success (partition a l r) h"
5.42 +using assms unfolding partition.simps swap_def
5.43 +apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crelE crel_upd crel_nth crel_return simp add:)
5.44 apply (frule part_length_remains)
5.45 apply (frule part_returns_index_in_bounds)
5.46 apply auto
5.47 @@ -602,15 +614,15 @@
5.48 apply auto
5.49 done
5.50
5.51 -lemma noError_quicksort:
5.52 +lemma success_quicksortI:
5.53 assumes "l < Array.length a h" "r < Array.length a h"
5.54 - shows "noError (quicksort a l r) h"
5.55 + shows "success (quicksort a l r) h"
5.56 using assms
5.57 proof (induct a l r arbitrary: h rule: quicksort.induct)
5.58 case (1 a l ri h)
5.59 thus ?case
5.60 unfolding quicksort.simps [of a l ri]
5.61 - apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
5.62 + apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI)
5.63 apply (frule partition_returns_index_in_bounds)
5.64 apply auto
5.65 apply (frule partition_returns_index_in_bounds)
5.66 @@ -620,7 +632,7 @@
5.67 apply (erule disjE)
5.68 apply auto
5.69 unfolding quicksort.simps [of a "Suc ri" ri]
5.70 - apply (auto intro!: noError_if noError_return)
5.71 + apply (auto intro!: success_ifI success_returnI)
5.72 done
5.73 qed
5.74