5 section{* Definition of the Relational framework *}
7 text {* The crel predicate states that when a computation c runs with the heap h
8 will result in return value r and a heap h' (if no exception occurs). *}
10 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
12 crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
14 lemma crel_def: -- FIXME
15 "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
16 unfolding crel_def' by auto
18 lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
19 unfolding crel_def' by auto
21 section {* Elimination rules *}
23 text {* For all commands, we define simple elimination rules. *}
24 (* FIXME: consumes 1 necessary ?? *)
26 subsection {* Elimination rules for basic monadic commands *}
28 lemma crelE[consumes 1]:
29 assumes "crel (f >>= g) h h'' r'"
30 obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
32 by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
34 lemma crelE'[consumes 1]:
35 assumes "crel (f >> g) h h'' r'"
36 obtains h' r where "crel f h h' r" "crel g h' h'' r'"
40 lemma crel_return[consumes 1]:
41 assumes "crel (return x) h h' r"
42 obtains "r = x" "h = h'"
44 unfolding crel_def return_def by simp
46 lemma crel_raise[consumes 1]:
47 assumes "crel (raise x) h h' r"
50 unfolding crel_def raise_def by simp
53 assumes "crel (if c then t else e) h h' r"
54 obtains "c" "crel t h h' r"
55 | "\<not>c" "crel e h h' r"
57 unfolding crel_def by auto
59 lemma crel_option_case:
60 assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
61 obtains "x = None" "crel n h h' r"
62 | y where "x = Some y" "crel (s y) h h' r"
64 unfolding crel_def by auto
67 assumes "crel (mapM f xs) h h' r"
68 assumes "\<And>h h'. P f [] h h' []"
69 assumes "\<And>h h1 h' x xs y ys. \<lbrakk> crel (f x) h h1 y; crel (mapM f xs) h1 h' ys; P f xs h1 h' ys \<rbrakk> \<Longrightarrow> P f (x#xs) h h' (y#ys)"
72 proof (induct xs arbitrary: h h' r)
73 case Nil with assms(2) show ?case
74 by (auto elim: crel_return)
77 from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
78 and crel_mapM: "crel (mapM f xs) h1 h' ys"
81 by (auto elim!: crelE crel_return)
82 from Cons(1)[OF crel_mapM] crel_mapM crel_f assms(3) r_def
87 assumes "crel (Heap_Monad.heap f) h h' r"
88 obtains "h' = snd (f h)" "r = fst (f h)"
90 unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
92 subsection {* Elimination rules for array commands *}
95 assumes "crel (length a) h h' r"
96 obtains "h = h'" "r = Heap.length a h'"
99 by (elim crel_heap) simp
101 (* Strong version of the lemma for this operation is missing *)
103 assumes "crel (Array.new n v) h h' r"
104 obtains "get_array r h' = List.replicate n v"
105 using assms unfolding Array.new_def
106 by (elim crel_heap) (auto simp:Heap.array_def Let_def split_def)
108 lemma crel_nth[consumes 1]:
109 assumes "crel (nth a i) h h' r"
110 obtains "r = (get_array a h) ! i" "h = h'" "i < Heap.length a h"
113 by (auto elim!: crelE crel_if crel_raise crel_length crel_heap)
115 lemma crel_upd[consumes 1]:
116 assumes "crel (upd i v a) h h' r"
117 obtains "r = a" "h' = Heap.upd a i v h"
120 by (elim crelE crel_if crel_return crel_raise
121 crel_length crel_heap) auto
123 (* Strong version of the lemma for this operation is missing *)
124 lemma crel_of_list_weak:
125 assumes "crel (Array.of_list xs) h h' r"
126 obtains "get_array r h' = xs"
128 unfolding of_list_def
129 by (elim crel_heap) (simp add:get_array_init_array_list)
131 lemma crel_map_entry:
132 assumes "crel (Array.map_entry i f a) h h' r"
133 obtains "r = a" "h' = Heap.upd a i (f (get_array a h ! i)) h"
135 unfolding Array.map_entry_def
136 by (elim crelE crel_upd crel_nth) auto
139 assumes "crel (Array.swap i x a) h h' r"
140 obtains "r = get_array a h ! i" "h' = Heap.upd a i x h"
142 unfolding Array.swap_def
143 by (elim crelE crel_upd crel_nth crel_return) auto
145 (* Strong version of the lemma for this operation is missing *)
146 lemma crel_make_weak:
147 assumes "crel (Array.make n f) h h' r"
148 obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
150 unfolding Array.make_def
151 by (elim crel_of_list_weak) auto
153 lemma upt_conv_Cons':
154 assumes "Suc a \<le> b"
155 shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
157 from assms have l: "b - Suc a < b" by arith
158 from assms have "Suc (b - Suc a) = b - a" by arith
159 with l show ?thesis by (simp add: upt_conv_Cons)
164 "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' xs"
165 assumes "n \<le> Heap.length a h"
166 shows "h = h' \<and> xs = drop (Heap.length a h - n) (get_array a h)"
168 proof (induct n arbitrary: xs h h')
170 by (auto elim!: crel_return simp add: Heap.length_def)
173 from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
174 by (simp add: upt_conv_Cons')
175 with Suc(2) obtain r where
176 crel_mapM: "crel (mapM (Array.nth a) [Heap.length a h - n..<Heap.length a h]) h h' r"
177 and xs_def: "xs = get_array a h ! (Heap.length a h - Suc n) # r"
178 by (auto elim!: crelE crel_nth crel_return)
179 from Suc(3) have "Heap.length a h - n = Suc (Heap.length a h - Suc n)"
181 with Suc.hyps[OF crel_mapM] xs_def show ?case
182 unfolding Heap.length_def
183 by (auto simp add: nth_drop')
187 assumes "crel (Array.freeze a) h h' xs"
188 obtains "h = h'" "xs = get_array a h"
190 from assms have "crel (mapM (Array.nth a) [0..<Heap.length a h]) h h' xs"
192 by (auto elim: crelE crel_length)
193 hence "crel (mapM (Array.nth a) [(Heap.length a h - Heap.length a h)..<Heap.length a h]) h h' xs"
195 from crel_mapM_nth[OF this] show "h = h'" and "xs = get_array a h" by auto
198 lemma crel_mapM_map_entry_remains:
199 assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
200 assumes "i < Heap.length a h - n"
201 shows "get_array a h ! i = get_array a h' ! i"
203 proof (induct n arbitrary: h h' r)
206 by (auto elim: crel_return)
209 let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
210 from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
211 by (simp add: upt_conv_Cons')
212 from Suc(2) this obtain r where
213 crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
214 by (auto simp add: elim!: crelE crel_map_entry crel_return)
215 have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
216 from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
218 from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
221 lemma crel_mapM_map_entry_changes:
222 assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
223 assumes "n \<le> Heap.length a h"
224 assumes "i \<ge> Heap.length a h - n"
225 assumes "i < Heap.length a h"
226 shows "get_array a h' ! i = f (get_array a h ! i)"
228 proof (induct n arbitrary: h h' r)
231 by (auto elim!: crel_return)
234 let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
235 from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
236 by (simp add: upt_conv_Cons')
237 from Suc(2) this obtain r where
238 crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
239 by (auto simp add: elim!: crelE crel_map_entry crel_return)
240 have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
241 from Suc(3) have less: "Heap.length a h - Suc n < Heap.length a h - n" by arith
242 from Suc(3) have less2: "Heap.length a h - Suc n < Heap.length a h" by arith
243 from Suc(4) length_remains have cases: "i = Heap.length a ?h1 - Suc n \<or> i \<ge> Heap.length a ?h1 - n" by arith
244 from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
246 from Suc(1)[OF this] cases Suc(3) Suc(5) length_remains
247 crel_mapM_map_entry_remains[OF this, of "Heap.length a h - Suc n", symmetric] less less2
249 by (auto simp add: nth_list_update_eq Heap.length_def)
252 lemma crel_mapM_map_entry_length:
253 assumes "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h h' r"
254 assumes "n \<le> Heap.length a h"
255 shows "Heap.length a h' = Heap.length a h"
257 proof (induct n arbitrary: h h' r)
259 thus ?case by (auto elim!: crel_return)
262 let ?h1 = "Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h"
263 from Suc(3) have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
264 by (simp add: upt_conv_Cons')
265 from Suc(2) this obtain r where
266 crel_mapM: "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) ?h1 h' r"
267 by (auto elim!: crelE crel_map_entry crel_return)
268 have length_remains: "Heap.length a ?h1 = Heap.length a h" by simp
269 from crel_mapM have crel_mapM': "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a ?h1 - n..<Heap.length a ?h1]) ?h1 h' r"
271 from Suc(1)[OF this] length_remains Suc(3) show ?case by simp
274 lemma crel_mapM_map_entry:
275 assumes "crel (mapM (\<lambda>n. map_entry n f a) [0..<Heap.length a h]) h h' r"
276 shows "get_array a h' = List.map f (get_array a h)"
278 from assms have "crel (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - Heap.length a h..<Heap.length a h]) h h' r" by simp
279 from crel_mapM_map_entry_length[OF this]
280 crel_mapM_map_entry_changes[OF this] show ?thesis
281 unfolding Heap.length_def
282 by (auto intro: nth_equalityI)
286 assumes crel_map: "crel (Array.map f a) h h' r"
287 obtains "r = a" "get_array a h' = List.map f (get_array a h)"
289 from assms crel_mapM_map_entry show "get_array a h' = List.map f (get_array a h)"
290 unfolding Array.map_def
291 by (fastsimp elim!: crelE crel_length crel_return)
292 from assms show "r = a"
293 unfolding Array.map_def
294 by (elim crelE crel_return)
297 subsection {* Elimination rules for reference commands *}
300 maybe introduce a new predicate "extends h' h x"
301 which means h' extends h with a new reference x.
302 Then crel_new: would be
303 assumes "crel (Ref.new v) h h' x"
304 obtains "get_ref x h' = v"
307 and we would need further rules for extends:
308 extends h' h x \<Longrightarrow> \<not> ref_present x h
309 extends h' h x \<Longrightarrow> ref_present x h'
310 extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
311 extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
312 extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
316 assumes "crel (Ref.new v) h h' x"
317 obtains "get_ref x h' = v"
318 and "\<not> ref_present x h"
319 and "ref_present x h'"
320 and "\<forall>y. ref_present y h \<longrightarrow> get_ref y h = get_ref y h'"
321 (* and "lim h' = Suc (lim h)" *)
322 and "\<forall>y. ref_present y h \<longrightarrow> ref_present y h'"
324 unfolding Ref.new_def
325 apply (elim crel_heap)
326 unfolding Heap.ref_def
327 apply (simp add: Let_def)
328 unfolding Heap.new_ref_def
329 apply (simp add: Let_def)
330 unfolding ref_present_def
332 unfolding get_ref_def set_ref_def
337 assumes "crel (!ref) h h' r"
338 obtains "h = h'" "r = get_ref ref h"
340 unfolding Ref.lookup_def
341 by (auto elim: crel_heap)
344 assumes "crel (ref := v) h h' r"
345 obtains "h' = set_ref ref v h" "r = ()"
347 unfolding Ref.update_def
348 by (auto elim: crel_heap)
351 assumes "crel (Ref.change f ref) h h' r"
352 obtains "h' = set_ref ref (f (get_ref ref h)) h" "r = f (get_ref ref h)"
354 unfolding Ref.change_def Let_def
355 by (auto elim!: crelE crel_lookup crel_update crel_return)
357 subsection {* Elimination rules for the assert command *}
359 lemma crel_assert[consumes 1]:
360 assumes "crel (assert P x) h h' r"
361 obtains "P x" "r = x" "h = h'"
364 by (elim crel_if crel_return crel_raise) auto
366 lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
367 unfolding crel_def bindM_def Let_def assert_def
368 raise_def return_def prod_case_beta
371 apply (simp add: expand_fun_eq split_def)
373 apply (case_tac "fst (fun x)")
374 apply (simp_all add: Pair_fst_snd_eq)
375 apply (erule_tac x="x" in meta_allE)
379 section {* Introduction rules *}
381 subsection {* Introduction rules for basic monadic commands *}
384 assumes "crel f h h' r" "crel (g r) h' h'' r'"
385 shows "crel (f >>= g) h h'' r'"
386 using assms by (simp add: crel_def' bindM_def)
389 assumes "crel f h h' r" "crel g h' h'' r'"
390 shows "crel (f >> g) h h'' r'"
391 using assms by (intro crelI) auto
394 shows "crel (return x) h h x"
395 unfolding crel_def return_def by simp
398 shows "\<not> (crel (raise x) h h' r)"
399 unfolding crel_def raise_def by simp
402 assumes "c \<longrightarrow> crel t h h' r"
403 "\<not>c \<longrightarrow> crel e h h' r"
404 shows "crel (if c then t else e) h h' r"
406 unfolding crel_def by auto
408 lemma crel_option_caseI:
409 assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
410 assumes "x = None \<Longrightarrow> crel n h h' r"
411 shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
413 by (auto split: option.split)
416 shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
417 by (simp add: crel_def apfst_def split_def prod_fun_def)
420 assumes "h' = snd (f h)" "r = fst (f h)"
421 shows "crel (Heap_Monad.heap f) h h' r"
423 by (simp add: crel_def split_def apfst_def prod_fun_def)
426 assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
427 shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
431 assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
432 "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
433 shows "\<exists> h' r. crel (if c then t else e) h h' r"
436 subsection {* Introduction rules for array commands *}
439 shows "crel (length a) h h (Heap.length a h)"
441 by (rule crel_heapI') auto
443 (* thm crel_newI for Array.new is missing *)
446 assumes "i < Heap.length a h"
447 shows "crel (nth a i) h h ((get_array a h) ! i)"
450 by (auto intro!: crelI crel_ifI crel_raiseI crel_lengthI crel_heapI')
453 assumes "i < Heap.length a h"
454 shows "crel (upd i v a) h (Heap.upd a i v h) a"
457 by (auto intro!: crelI crel_ifI crel_returnI crel_raiseI
458 crel_lengthI crel_heapI')
460 (* thm crel_of_listI is missing *)
462 (* thm crel_map_entryI is missing *)
464 (* thm crel_swapI is missing *)
466 (* thm crel_makeI is missing *)
468 (* thm crel_freezeI is missing *)
470 (* thm crel_mapI is missing *)
472 subsection {* Introduction rules for reference commands *}
475 shows "crel (!ref) h h (get_ref ref h)"
476 unfolding lookup_def by (auto intro!: crel_heapI')
479 shows "crel (ref := v) h (set_ref ref v h) ()"
480 unfolding update_def by (auto intro!: crel_heapI')
483 shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
484 unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
486 subsection {* Introduction rules for the assert command *}
490 shows "crel (assert P x) h h x"
493 by (auto intro!: crel_ifI crel_returnI crel_raiseI)
495 section {* Defintion of the noError predicate *}
497 text {* We add a simple definitional setting for crel intro rules
498 where we only would like to show that the computation does not result in a exception for heap h,
499 but we do not care about statements about the resulting heap and return value.*}
501 definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
503 "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
505 lemma noError_def': -- FIXME
506 "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
507 unfolding noError_def apply auto proof -
509 assume "(Inl r, h') = Heap_Monad.execute c h"
510 then have "Heap_Monad.execute c h = (Inl r, h')" ..
511 then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
514 subsection {* Introduction rules for basic monadic commands *}
517 assumes "noError f h"
518 assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
519 shows "noError (f \<guillemotright>= g) h"
521 by (auto simp add: noError_def' crel_def' bindM_def)
524 assumes "noError f h"
525 assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
526 shows "noError (f \<guillemotright> g) h"
528 by (auto simp add: noError_def' crel_def' bindM_def)
531 "\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
532 \<Longrightarrow> noError (f \<guillemotright>= g) h"
533 by (auto simp add: noError_def' crel_def' bindM_def)
535 lemma noError_return:
536 shows "noError (return x) h"
537 unfolding noError_def return_def
541 assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
542 shows "noError (if c then t else e) h"
544 unfolding noError_def
547 lemma noError_option_case:
548 assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
549 assumes "noError n h"
550 shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
552 by (auto split: option.split)
555 assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)"
556 shows "noError (mapM f xs) h"
561 unfolding mapM.simps by (intro noError_return)
566 by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
570 shows "noError (Heap_Monad.heap f) h"
571 by (simp add: noError_def' apfst_def prod_fun_def split_def)
573 subsection {* Introduction rules for array commands *}
575 lemma noError_length:
576 shows "noError (Array.length a) h"
578 by (intro noError_heap)
581 shows "noError (Array.new n v) h"
582 unfolding Array.new_def by (intro noError_heap)
585 assumes "i < Heap.length a h"
586 shows "noError (Array.upd i v a) h"
589 by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
592 assumes "i < Heap.length a h"
593 shows "noError (Array.nth a i) h"
596 by (auto intro!: noErrorI noError_if noError_return noError_length noError_heap) (auto elim: crel_length)
598 lemma noError_of_list:
599 shows "noError (of_list ls) h"
600 unfolding of_list_def by (rule noError_heap)
602 lemma noError_map_entry:
603 assumes "i < Heap.length a h"
604 shows "noError (map_entry i f a) h"
606 unfolding map_entry_def
607 by (auto elim: crel_nth intro!: noErrorI noError_nth noError_upd)
610 assumes "i < Heap.length a h"
611 shows "noError (swap i x a) h"
614 by (auto elim: crel_nth intro!: noErrorI noError_return noError_nth noError_upd)
617 shows "noError (make n f) h"
619 by (auto intro: noError_of_list)
621 (*TODO: move to HeapMonad *)
623 "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
624 by (induct xs) (simp_all add: monad_simp)
626 lemma noError_freeze:
627 shows "noError (freeze a) h"
629 by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]
630 noError_nth crel_nthI elim: crel_length)
632 lemma noError_mapM_map_entry:
633 assumes "n \<le> Heap.length a h"
634 shows "noError (mapM (\<lambda>n. map_entry n f a) [Heap.length a h - n..<Heap.length a h]) h"
636 proof (induct n arbitrary: h)
638 thus ?case by (auto intro: noError_return)
641 from Suc.prems have "[Heap.length a h - Suc n..<Heap.length a h] = (Heap.length a h - Suc n)#[Heap.length a h - n..<Heap.length a h]"
642 by (simp add: upt_conv_Cons')
643 with Suc.hyps[of "(Heap.upd a (Heap.length a h - Suc n) (f (get_array a h ! (Heap.length a h - Suc n))) h)"] Suc.prems show ?case
644 by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
648 shows "noError (Array.map f a) h"
649 using noError_mapM_map_entry[of "Heap.length a h" a h]
650 unfolding Array.map_def
651 by (auto intro: noErrorI noError_length noError_return elim!: crel_length)
653 subsection {* Introduction rules for the reference commands *}
655 lemma noError_Ref_new:
656 shows "noError (Ref.new v) h"
657 unfolding Ref.new_def by (intro noError_heap)
659 lemma noError_lookup:
660 shows "noError (!ref) h"
661 unfolding lookup_def by (intro noError_heap)
663 lemma noError_update:
664 shows "noError (ref := v) h"
665 unfolding update_def by (intro noError_heap)
667 lemma noError_change:
668 shows "noError (Ref.change f ref) h"
669 unfolding Ref.change_def Let_def by (intro noErrorI noError_lookup noError_update noError_return)
671 subsection {* Introduction rules for the assert command *}
673 lemma noError_assert:
675 shows "noError (assert P x) h"
678 by (auto intro: noError_if noError_return)
680 section {* Cumulative lemmas *}
682 lemmas crel_elim_all =
683 crelE crelE' crel_return crel_raise crel_if crel_option_case
684 crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze crel_map_weak
685 crel_Ref_new crel_lookup crel_update crel_change
688 lemmas crel_intro_all =
689 crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
690 crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
691 (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
694 lemmas noError_intro_all =
695 noErrorI noErrorI' noError_return noError_if noError_option_case
696 noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze noError_map
697 noError_Ref_new noError_lookup noError_update noError_change