61 |
61 |
62 section {* Proving correctness with relational abstraction *} |
62 section {* Proving correctness with relational abstraction *} |
63 |
63 |
64 subsection {* Definition of list_of, list_of', refs_of and refs_of' *} |
64 subsection {* Definition of list_of, list_of', refs_of and refs_of' *} |
65 |
65 |
66 fun list_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a list \<Rightarrow> bool" |
66 primrec list_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a list \<Rightarrow> bool" |
67 where |
67 where |
68 "list_of h r [] = (r = Empty)" |
68 "list_of h r [] = (r = Empty)" |
69 | "list_of h r (a#as) = (case r of Empty \<Rightarrow> False | Node b bs \<Rightarrow> (a = b \<and> list_of h (get_ref bs h) as))" |
69 | "list_of h r (a#as) = (case r of Empty \<Rightarrow> False | Node b bs \<Rightarrow> (a = b \<and> list_of h (Ref.get h bs) as))" |
70 |
70 |
71 definition list_of' :: "heap \<Rightarrow> ('a::heap) node ref \<Rightarrow> 'a list \<Rightarrow> bool" |
71 definition list_of' :: "heap \<Rightarrow> ('a::heap) node ref \<Rightarrow> 'a list \<Rightarrow> bool" |
72 where |
72 where |
73 "list_of' h r xs = list_of h (get_ref r h) xs" |
73 "list_of' h r xs = list_of h (Ref.get h r) xs" |
74 |
74 |
75 fun refs_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a node ref list \<Rightarrow> bool" |
75 primrec refs_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a node ref list \<Rightarrow> bool" |
76 where |
76 where |
77 "refs_of h r [] = (r = Empty)" |
77 "refs_of h r [] = (r = Empty)" |
78 | "refs_of h r (x#xs) = (case r of Empty \<Rightarrow> False | Node b bs \<Rightarrow> (x = bs) \<and> refs_of h (get_ref bs h) xs)" |
78 | "refs_of h r (x#xs) = (case r of Empty \<Rightarrow> False | Node b bs \<Rightarrow> (x = bs) \<and> refs_of h (Ref.get h bs) xs)" |
79 |
79 |
80 fun refs_of' :: "heap \<Rightarrow> ('a::heap) node ref \<Rightarrow> 'a node ref list \<Rightarrow> bool" |
80 primrec refs_of' :: "heap \<Rightarrow> ('a::heap) node ref \<Rightarrow> 'a node ref list \<Rightarrow> bool" |
81 where |
81 where |
82 "refs_of' h r [] = False" |
82 "refs_of' h r [] = False" |
83 | "refs_of' h r (x#xs) = ((x = r) \<and> refs_of h (get_ref x h) xs)" |
83 | "refs_of' h r (x#xs) = ((x = r) \<and> refs_of h (Ref.get h x) xs)" |
84 |
84 |
85 |
85 |
86 subsection {* Properties of these definitions *} |
86 subsection {* Properties of these definitions *} |
87 |
87 |
88 lemma list_of_Empty[simp]: "list_of h Empty xs = (xs = [])" |
88 lemma list_of_Empty[simp]: "list_of h Empty xs = (xs = [])" |
89 by (cases xs, auto) |
89 by (cases xs, auto) |
90 |
90 |
91 lemma list_of_Node[simp]: "list_of h (Node x ps) xs = (\<exists>xs'. (xs = x # xs') \<and> list_of h (get_ref ps h) xs')" |
91 lemma list_of_Node[simp]: "list_of h (Node x ps) xs = (\<exists>xs'. (xs = x # xs') \<and> list_of h (Ref.get h ps) xs')" |
92 by (cases xs, auto) |
92 by (cases xs, auto) |
93 |
93 |
94 lemma list_of'_Empty[simp]: "get_ref q h = Empty \<Longrightarrow> list_of' h q xs = (xs = [])" |
94 lemma list_of'_Empty[simp]: "Ref.get h q = Empty \<Longrightarrow> list_of' h q xs = (xs = [])" |
95 unfolding list_of'_def by simp |
95 unfolding list_of'_def by simp |
96 |
96 |
97 lemma list_of'_Node[simp]: "get_ref q h = Node x ps \<Longrightarrow> list_of' h q xs = (\<exists>xs'. (xs = x # xs') \<and> list_of' h ps xs')" |
97 lemma list_of'_Node[simp]: "Ref.get h q = Node x ps \<Longrightarrow> list_of' h q xs = (\<exists>xs'. (xs = x # xs') \<and> list_of' h ps xs')" |
98 unfolding list_of'_def by simp |
98 unfolding list_of'_def by simp |
99 |
99 |
100 lemma list_of'_Nil: "list_of' h q [] \<Longrightarrow> get_ref q h = Empty" |
100 lemma list_of'_Nil: "list_of' h q [] \<Longrightarrow> Ref.get h q = Empty" |
101 unfolding list_of'_def by simp |
101 unfolding list_of'_def by simp |
102 |
102 |
103 lemma list_of'_Cons: |
103 lemma list_of'_Cons: |
104 assumes "list_of' h q (x#xs)" |
104 assumes "list_of' h q (x#xs)" |
105 obtains n where "get_ref q h = Node x n" and "list_of' h n xs" |
105 obtains n where "Ref.get h q = Node x n" and "list_of' h n xs" |
106 using assms unfolding list_of'_def by (auto split: node.split_asm) |
106 using assms unfolding list_of'_def by (auto split: node.split_asm) |
107 |
107 |
108 lemma refs_of_Empty[simp] : "refs_of h Empty xs = (xs = [])" |
108 lemma refs_of_Empty[simp] : "refs_of h Empty xs = (xs = [])" |
109 by (cases xs, auto) |
109 by (cases xs, auto) |
110 |
110 |
111 lemma refs_of_Node[simp]: "refs_of h (Node x ps) xs = (\<exists>prs. xs = ps # prs \<and> refs_of h (get_ref ps h) prs)" |
111 lemma refs_of_Node[simp]: "refs_of h (Node x ps) xs = (\<exists>prs. xs = ps # prs \<and> refs_of h (Ref.get h ps) prs)" |
112 by (cases xs, auto) |
112 by (cases xs, auto) |
113 |
113 |
114 lemma refs_of'_def': "refs_of' h p ps = (\<exists>prs. (ps = (p # prs)) \<and> refs_of h (get_ref p h) prs)" |
114 lemma refs_of'_def': "refs_of' h p ps = (\<exists>prs. (ps = (p # prs)) \<and> refs_of h (Ref.get h p) prs)" |
115 by (cases ps, auto) |
115 by (cases ps, auto) |
116 |
116 |
117 lemma refs_of'_Node: |
117 lemma refs_of'_Node: |
118 assumes "refs_of' h p xs" |
118 assumes "refs_of' h p xs" |
119 assumes "get_ref p h = Node x pn" |
119 assumes "Ref.get h p = Node x pn" |
120 obtains pnrs |
120 obtains pnrs |
121 where "xs = p # pnrs" and "refs_of' h pn pnrs" |
121 where "xs = p # pnrs" and "refs_of' h pn pnrs" |
122 using assms |
122 using assms |
123 unfolding refs_of'_def' by auto |
123 unfolding refs_of'_def' by auto |
124 |
124 |
262 by (fastsimp simp add: refs_of_distinct refs_of_next) |
262 by (fastsimp simp add: refs_of_distinct refs_of_next) |
263 |
263 |
264 |
264 |
265 subsection {* Interaction of these predicates with our heap transitions *} |
265 subsection {* Interaction of these predicates with our heap transitions *} |
266 |
266 |
267 lemma list_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> list_of (set_ref p v h) q as = list_of h q as" |
267 lemma list_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> list_of (Ref.set p v h) q as = list_of h q as" |
268 using assms |
268 using assms |
269 proof (induct as arbitrary: q rs) |
269 proof (induct as arbitrary: q rs) |
270 case Nil thus ?case by simp |
270 case Nil thus ?case by simp |
271 next |
271 next |
272 case (Cons x xs) |
272 case (Cons x xs) |
273 thus ?case |
273 thus ?case |
274 proof (cases q) |
274 proof (cases q) |
275 case Empty thus ?thesis by auto |
275 case Empty thus ?thesis by auto |
276 next |
276 next |
277 case (Node a ref) |
277 case (Node a ref) |
278 from Cons(2) Node obtain rs' where 1: "refs_of h (get_ref ref h) rs'" and rs_rs': "rs = ref # rs'" by auto |
278 from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto |
279 from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp |
279 from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp |
280 hence ref_eq: "get_ref ref (set_ref p v h) = (get_ref ref h)" by (auto simp add: ref_get_set_neq) |
280 hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq) |
281 from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp |
281 from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp |
282 from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by simp |
282 from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by simp |
283 qed |
283 qed |
284 qed |
284 qed |
285 |
285 |
286 lemma refs_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> refs_of (set_ref p v h) q as = refs_of h q as" |
286 lemma refs_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> refs_of (Ref.set p v h) q as = refs_of h q as" |
287 proof (induct as arbitrary: q rs) |
287 proof (induct as arbitrary: q rs) |
288 case Nil thus ?case by simp |
288 case Nil thus ?case by simp |
289 next |
289 next |
290 case (Cons x xs) |
290 case (Cons x xs) |
291 thus ?case |
291 thus ?case |
292 proof (cases q) |
292 proof (cases q) |
293 case Empty thus ?thesis by auto |
293 case Empty thus ?thesis by auto |
294 next |
294 next |
295 case (Node a ref) |
295 case (Node a ref) |
296 from Cons(2) Node obtain rs' where 1: "refs_of h (get_ref ref h) rs'" and rs_rs': "rs = ref # rs'" by auto |
296 from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto |
297 from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp |
297 from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp |
298 hence ref_eq: "get_ref ref (set_ref p v h) = (get_ref ref h)" by (auto simp add: ref_get_set_neq) |
298 hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq) |
299 from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp |
299 from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp |
300 from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by auto |
300 from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by auto |
301 qed |
301 qed |
302 qed |
302 qed |
303 |
303 |
304 lemma refs_of_set_ref2: "refs_of (set_ref p v h) q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> refs_of (set_ref p v h) q rs = refs_of h q rs" |
304 lemma refs_of_set_ref2: "refs_of (Ref.set p v h) q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> refs_of (Ref.set p v h) q rs = refs_of h q rs" |
305 proof (induct rs arbitrary: q) |
305 proof (induct rs arbitrary: q) |
306 case Nil thus ?case by simp |
306 case Nil thus ?case by simp |
307 next |
307 next |
308 case (Cons x xs) |
308 case (Cons x xs) |
309 thus ?case |
309 thus ?case |
310 proof (cases q) |
310 proof (cases q) |
311 case Empty thus ?thesis by auto |
311 case Empty thus ?thesis by auto |
312 next |
312 next |
313 case (Node a ref) |
313 case (Node a ref) |
314 from Cons(2) Node have 1:"refs_of (set_ref p v h) (get_ref ref (set_ref p v h)) xs" and x_ref: "x = ref" by auto |
314 from Cons(2) Node have 1:"refs_of (Ref.set p v h) (Ref.get (Ref.set p v h) ref) xs" and x_ref: "x = ref" by auto |
315 from Cons(3) this have "ref \<noteq> p" by fastsimp |
315 from Cons(3) this have "ref \<noteq> p" by fastsimp |
316 hence ref_eq: "get_ref ref (set_ref p v h) = (get_ref ref h)" by (auto simp add: ref_get_set_neq) |
316 hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq) |
317 from Cons(3) have 2: "p \<notin> set xs" by simp |
317 from Cons(3) have 2: "p \<notin> set xs" by simp |
318 with Cons.hyps 1 2 Node ref_eq show ?thesis |
318 with Cons.hyps 1 2 Node ref_eq show ?thesis |
319 by simp |
319 by simp |
320 qed |
320 qed |
321 qed |
321 qed |
322 |
322 |
323 lemma list_of'_set_ref: |
323 lemma list_of'_set_ref: |
324 assumes "refs_of' h q rs" |
324 assumes "refs_of' h q rs" |
325 assumes "p \<notin> set rs" |
325 assumes "p \<notin> set rs" |
326 shows "list_of' (set_ref p v h) q as = list_of' h q as" |
326 shows "list_of' (Ref.set p v h) q as = list_of' h q as" |
327 proof - |
327 proof - |
328 from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E) |
328 from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E) |
329 with assms show ?thesis |
329 with assms show ?thesis |
330 unfolding list_of'_def refs_of'_def' |
330 unfolding list_of'_def refs_of'_def' |
331 by (auto simp add: list_of_set_ref) |
331 by (auto simp add: list_of_set_ref) |
332 qed |
332 qed |
333 |
333 |
334 lemma list_of'_set_next_ref_Node[simp]: |
334 lemma list_of'_set_next_ref_Node[simp]: |
335 assumes "list_of' h r xs" |
335 assumes "list_of' h r xs" |
336 assumes "get_ref p h = Node x r'" |
336 assumes "Ref.get h p = Node x r'" |
337 assumes "refs_of' h r rs" |
337 assumes "refs_of' h r rs" |
338 assumes "p \<notin> set rs" |
338 assumes "p \<notin> set rs" |
339 shows "list_of' (set_ref p (Node x r) h) p (x#xs) = list_of' h r xs" |
339 shows "list_of' (Ref.set p (Node x r) h) p (x#xs) = list_of' h r xs" |
340 using assms |
340 using assms |
341 unfolding list_of'_def refs_of'_def' |
341 unfolding list_of'_def refs_of'_def' |
342 by (auto simp add: list_of_set_ref noteq_refs_sym) |
342 by (auto simp add: list_of_set_ref Ref.noteq_sym) |
343 |
343 |
344 lemma refs_of'_set_ref: |
344 lemma refs_of'_set_ref: |
345 assumes "refs_of' h q rs" |
345 assumes "refs_of' h q rs" |
346 assumes "p \<notin> set rs" |
346 assumes "p \<notin> set rs" |
347 shows "refs_of' (set_ref p v h) q as = refs_of' h q as" |
347 shows "refs_of' (Ref.set p v h) q as = refs_of' h q as" |
348 using assms |
348 using assms |
349 proof - |
349 proof - |
350 from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E) |
350 from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E) |
351 with assms show ?thesis |
351 with assms show ?thesis |
352 unfolding refs_of'_def' |
352 unfolding refs_of'_def' |
353 by (auto simp add: refs_of_set_ref) |
353 by (auto simp add: refs_of_set_ref) |
354 qed |
354 qed |
355 |
355 |
356 lemma refs_of'_set_ref2: |
356 lemma refs_of'_set_ref2: |
357 assumes "refs_of' (set_ref p v h) q rs" |
357 assumes "refs_of' (Ref.set p v h) q rs" |
358 assumes "p \<notin> set rs" |
358 assumes "p \<notin> set rs" |
359 shows "refs_of' (set_ref p v h) q as = refs_of' h q as" |
359 shows "refs_of' (Ref.set p v h) q as = refs_of' h q as" |
360 using assms |
360 using assms |
361 proof - |
361 proof - |
362 from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E) |
362 from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E) |
363 with assms show ?thesis |
363 with assms show ?thesis |
364 unfolding refs_of'_def' |
364 unfolding refs_of'_def' |
365 apply auto |
365 apply auto |
366 apply (subgoal_tac "prs = prsa") |
366 apply (subgoal_tac "prs = prsa") |
367 apply (insert refs_of_set_ref2[of p v h "get_ref q h"]) |
367 apply (insert refs_of_set_ref2[of p v h "Ref.get h q"]) |
368 apply (erule_tac x="prs" in meta_allE) |
368 apply (erule_tac x="prs" in meta_allE) |
369 apply auto |
369 apply auto |
370 apply (auto dest: refs_of_is_fun) |
370 apply (auto dest: refs_of_is_fun) |
371 done |
371 done |
372 qed |
372 qed |
373 |
373 |
374 lemma refs_of'_set_next_ref: |
374 lemma refs_of'_set_next_ref: |
375 assumes "get_ref p h1 = Node x pn" |
375 assumes "Ref.get h1 p = Node x pn" |
376 assumes "refs_of' (set_ref p (Node x r1) h1) p rs" |
376 assumes "refs_of' (Ref.set p (Node x r1) h1) p rs" |
377 obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s" |
377 obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s" |
378 using assms |
378 using assms |
379 proof - |
379 proof - |
380 from assms refs_of'_distinct[OF assms(2)] have "\<exists> r1s. rs = (p # r1s) \<and> refs_of' h1 r1 r1s" |
380 from assms refs_of'_distinct[OF assms(2)] have "\<exists> r1s. rs = (p # r1s) \<and> refs_of' h1 r1 r1s" |
381 apply - |
381 apply - |
382 unfolding refs_of'_def'[of _ p] |
382 unfolding refs_of'_def'[of _ p] |
383 apply (auto, frule refs_of_set_ref2) by (auto dest: noteq_refs_sym) |
383 apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym) |
384 with prems show thesis by auto |
384 with prems show thesis by auto |
385 qed |
385 qed |
386 |
386 |
387 section {* Proving make_llist and traverse correct *} |
387 section {* Proving make_llist and traverse correct *} |
388 |
388 |
389 lemma refs_of_invariant: |
389 lemma refs_of_invariant: |
390 assumes "refs_of h (r::('a::heap) node) xs" |
390 assumes "refs_of h (r::('a::heap) node) xs" |
391 assumes "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref \<in> set refs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h')" |
391 assumes "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" |
392 shows "refs_of h' r xs" |
392 shows "refs_of h' r xs" |
393 using assms |
393 using assms |
394 proof (induct xs arbitrary: r) |
394 proof (induct xs arbitrary: r) |
395 case Nil thus ?case by simp |
395 case Nil thus ?case by simp |
396 next |
396 next |
397 case (Cons x xs') |
397 case (Cons x xs') |
398 from Cons(2) obtain v where Node: "r = Node v x" by (cases r, auto) |
398 from Cons(2) obtain v where Node: "r = Node v x" by (cases r, auto) |
399 from Cons(2) Node have refs_of_next: "refs_of h (get_ref x h) xs'" by simp |
399 from Cons(2) Node have refs_of_next: "refs_of h (Ref.get h x) xs'" by simp |
400 from Cons(2-3) Node have ref_eq: "get_ref x h = get_ref x h'" by auto |
400 from Cons(2-3) Node have ref_eq: "Ref.get h x = Ref.get h' x" by auto |
401 from ref_eq refs_of_next have 1: "refs_of h (get_ref x h') xs'" by simp |
401 from ref_eq refs_of_next have 1: "refs_of h (Ref.get h' x) xs'" by simp |
402 from Cons(2) Cons(3) have "\<forall>ref \<in> set xs'. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h'" |
402 from Cons(2) Cons(3) have "\<forall>ref \<in> set xs'. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref" |
403 by fastsimp |
403 by fastsimp |
404 with Cons(3) 1 have 2: "\<forall>refs. refs_of h (get_ref x h') refs \<longrightarrow> (\<forall>ref \<in> set refs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h')" |
404 with Cons(3) 1 have 2: "\<forall>refs. refs_of h (Ref.get h' x) refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" |
405 by (fastsimp dest: refs_of_is_fun) |
405 by (fastsimp dest: refs_of_is_fun) |
406 from Cons.hyps[OF 1 2] have "refs_of h' (get_ref x h') xs'" . |
406 from Cons.hyps[OF 1 2] have "refs_of h' (Ref.get h' x) xs'" . |
407 with Node show ?case by simp |
407 with Node show ?case by simp |
408 qed |
408 qed |
409 |
409 |
410 lemma refs_of'_invariant: |
410 lemma refs_of'_invariant: |
411 assumes "refs_of' h r xs" |
411 assumes "refs_of' h r xs" |
412 assumes "\<forall>refs. refs_of' h r refs \<longrightarrow> (\<forall>ref \<in> set refs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h')" |
412 assumes "\<forall>refs. refs_of' h r refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" |
413 shows "refs_of' h' r xs" |
413 shows "refs_of' h' r xs" |
414 using assms |
414 using assms |
415 proof - |
415 proof - |
416 from assms obtain prs where refs:"refs_of h (get_ref r h) prs" and xs_def: "xs = r # prs" |
416 from assms obtain prs where refs:"refs_of h (Ref.get h r) prs" and xs_def: "xs = r # prs" |
417 unfolding refs_of'_def' by auto |
417 unfolding refs_of'_def' by auto |
418 from xs_def assms have x_eq: "get_ref r h = get_ref r h'" by fastsimp |
418 from xs_def assms have x_eq: "Ref.get h r = Ref.get h' r" by fastsimp |
419 from refs assms xs_def have 2: "\<forall>refs. refs_of h (get_ref r h) refs \<longrightarrow> |
419 from refs assms xs_def have 2: "\<forall>refs. refs_of h (Ref.get h r) refs \<longrightarrow> |
420 (\<forall>ref\<in>set refs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h')" |
420 (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" |
421 by (fastsimp dest: refs_of_is_fun) |
421 by (fastsimp dest: refs_of_is_fun) |
422 from refs_of_invariant [OF refs 2] xs_def x_eq show ?thesis |
422 from refs_of_invariant [OF refs 2] xs_def x_eq show ?thesis |
423 unfolding refs_of'_def' by auto |
423 unfolding refs_of'_def' by auto |
424 qed |
424 qed |
425 |
425 |
426 lemma list_of_invariant: |
426 lemma list_of_invariant: |
427 assumes "list_of h (r::('a::heap) node) xs" |
427 assumes "list_of h (r::('a::heap) node) xs" |
428 assumes "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref \<in> set refs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h')" |
428 assumes "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" |
429 shows "list_of h' r xs" |
429 shows "list_of h' r xs" |
430 using assms |
430 using assms |
431 proof (induct xs arbitrary: r) |
431 proof (induct xs arbitrary: r) |
432 case Nil thus ?case by simp |
432 case Nil thus ?case by simp |
433 next |
433 next |
435 |
435 |
436 from Cons(2) obtain ref where Node: "r = Node x ref" |
436 from Cons(2) obtain ref where Node: "r = Node x ref" |
437 by (cases r, auto) |
437 by (cases r, auto) |
438 from Cons(2) obtain rs where rs_def: "refs_of h r rs" by (rule list_of_refs_of) |
438 from Cons(2) obtain rs where rs_def: "refs_of h r rs" by (rule list_of_refs_of) |
439 from Node rs_def obtain rss where refs_of: "refs_of h r (ref#rss)" and rss_def: "rs = ref#rss" by auto |
439 from Node rs_def obtain rss where refs_of: "refs_of h r (ref#rss)" and rss_def: "rs = ref#rss" by auto |
440 from Cons(3) Node refs_of have ref_eq: "get_ref ref h = get_ref ref h'" |
440 from Cons(3) Node refs_of have ref_eq: "Ref.get h ref = Ref.get h' ref" |
441 by auto |
441 by auto |
442 from Cons(2) ref_eq Node have 1: "list_of h (get_ref ref h') xs'" by simp |
442 from Cons(2) ref_eq Node have 1: "list_of h (Ref.get h' ref) xs'" by simp |
443 from refs_of Node ref_eq have refs_of_ref: "refs_of h (get_ref ref h') rss" by simp |
443 from refs_of Node ref_eq have refs_of_ref: "refs_of h (Ref.get h' ref) rss" by simp |
444 from Cons(3) rs_def have rs_heap_eq: "\<forall>ref\<in>set rs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h'" by simp |
444 from Cons(3) rs_def have rs_heap_eq: "\<forall>ref\<in>set rs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref" by simp |
445 from refs_of_ref rs_heap_eq rss_def have 2: "\<forall>refs. refs_of h (get_ref ref h') refs \<longrightarrow> |
445 from refs_of_ref rs_heap_eq rss_def have 2: "\<forall>refs. refs_of h (Ref.get h' ref) refs \<longrightarrow> |
446 (\<forall>ref\<in>set refs. ref_present ref h \<and> ref_present ref h' \<and> get_ref ref h = get_ref ref h')" |
446 (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" |
447 by (auto dest: refs_of_is_fun) |
447 by (auto dest: refs_of_is_fun) |
448 from Cons(1)[OF 1 2] |
448 from Cons(1)[OF 1 2] |
449 have "list_of h' (get_ref ref h') xs'" . |
449 have "list_of h' (Ref.get h' ref) xs'" . |
450 with Node show ?case |
450 with Node show ?case |
451 unfolding list_of'_def |
451 unfolding list_of'_def |
452 by simp |
452 by simp |
453 qed |
453 qed |
454 |
454 |
455 lemma make_llist: |
455 lemma make_llist: |
456 assumes "crel (make_llist xs) h h' r" |
456 assumes "crel (make_llist xs) h h' r" |
457 shows "list_of h' r xs \<and> (\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref \<in> (set rs). ref_present ref h'))" |
457 shows "list_of h' r xs \<and> (\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref \<in> (set rs). Ref.present h' ref))" |
458 using assms |
458 using assms |
459 proof (induct xs arbitrary: h h' r) |
459 proof (induct xs arbitrary: h h' r) |
460 case Nil thus ?case by (auto elim: crel_return simp add: make_llist.simps) |
460 case Nil thus ?case by (auto elim: crel_return simp add: make_llist.simps) |
461 next |
461 next |
462 case (Cons x xs') |
462 case (Cons x xs') |
463 from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1" |
463 from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1" |
464 and crel_refnew:"crel (Ref.new r1) h1 h' r'" and Node: "r = Node x r'" |
464 and crel_refnew:"crel (ref r1) h1 h' r'" and Node: "r = Node x r'" |
465 unfolding make_llist.simps |
465 unfolding make_llist.simps |
466 by (auto elim!: crelE crel_return) |
466 by (auto elim!: crelE crel_return) |
467 from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" .. |
467 from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" .. |
468 from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of) |
468 from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of) |
469 from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. ref_present ref h1" by simp |
469 from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. Ref.present h1 ref" by simp |
470 from crel_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow> |
470 from crel_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow> |
471 (\<forall>ref\<in>set refs. ref_present ref h1 \<and> ref_present ref h' \<and> get_ref ref h1 = get_ref ref h')" |
471 (\<forall>ref\<in>set refs. Ref.present h1 ref \<and> Ref.present h' ref \<and> Ref.get h1 ref = Ref.get h' ref)" |
472 by (auto elim!: crel_Ref_new dest: refs_of_is_fun) |
472 by (auto elim!: crel_ref dest: refs_of_is_fun) |
473 with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')" |
473 with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')" |
474 unfolding list_of.simps |
474 unfolding list_of.simps |
475 by (auto elim!: crel_Ref_new) |
475 by (auto elim!: crel_ref) |
476 from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. ref_present ref h'" by auto |
476 from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto |
477 from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present |
477 from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present |
478 have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. ref_present ref h')" |
478 have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)" |
479 by (fastsimp elim!: crel_Ref_new dest: refs_of_is_fun) |
479 by (fastsimp elim!: crel_ref dest: refs_of_is_fun) |
480 from fstgoal sndgoal show ?case .. |
480 from fstgoal sndgoal show ?case .. |
481 qed |
481 qed |
482 |
482 |
483 lemma traverse: "list_of h n r \<Longrightarrow> crel (traverse n) h h r" |
483 lemma traverse: "list_of h n r \<Longrightarrow> crel (traverse n) h h r" |
484 proof (induct r arbitrary: n) |
484 proof (induct r arbitrary: n) |
554 by (auto elim!: crelE crel_lookup crel_return) |
554 by (auto elim!: crelE crel_lookup crel_return) |
555 next |
555 next |
556 case (Cons x xs) |
556 case (Cons x xs) |
557 (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*) |
557 (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*) |
558 from Cons(4) obtain ref where |
558 from Cons(4) obtain ref where |
559 p_is_Node: "get_ref p h = Node x ref" |
559 p_is_Node: "Ref.get h p = Node x ref" |
560 (*and "ref_present ref h"*) |
560 (*and "ref_present ref h"*) |
561 and list_of'_ref: "list_of' h ref xs" |
561 and list_of'_ref: "list_of' h ref xs" |
562 unfolding list_of'_def by (cases "get_ref p h", auto) |
562 unfolding list_of'_def by (cases "Ref.get h p", auto) |
563 from p_is_Node Cons(2) have crel_rev': "crel (rev' (p, ref)) (set_ref p (Node x q) h) h' v" |
563 from p_is_Node Cons(2) have crel_rev': "crel (rev' (p, ref)) (Ref.set p (Node x q) h) h' v" |
564 by (auto simp add: rev'_simps [of q p] elim!: crelE crel_lookup crel_update) |
564 by (auto simp add: rev'_simps [of q p] elim!: crelE crel_lookup crel_update) |
565 from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of') |
565 from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of') |
566 from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of') |
566 from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of') |
567 from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp |
567 from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp |
568 from qrs_def prs_def distinct_pointers refs_of'E have p_notin_qrs: "p \<notin> set qrs" by fastsimp |
568 from qrs_def prs_def distinct_pointers refs_of'E have p_notin_qrs: "p \<notin> set qrs" by fastsimp |
569 from Cons(3) qrs_def this have 1: "list_of' (set_ref p (Node x q) h) p (x#qs)" |
569 from Cons(3) qrs_def this have 1: "list_of' (Ref.set p (Node x q) h) p (x#qs)" |
570 unfolding list_of'_def |
570 unfolding list_of'_def |
571 apply (simp) |
571 apply (simp) |
572 unfolding list_of'_def[symmetric] |
572 unfolding list_of'_def[symmetric] |
573 by (simp add: list_of'_set_ref) |
573 by (simp add: list_of'_set_ref) |
574 from list_of'_refs_of'2[OF Cons(4)] p_is_Node prs_def obtain refs where refs_def: "refs_of' h ref refs" and prs_refs: "prs = p # refs" |
574 from list_of'_refs_of'2[OF Cons(4)] p_is_Node prs_def obtain refs where refs_def: "refs_of' h ref refs" and prs_refs: "prs = p # refs" |
575 unfolding refs_of'_def' by auto |
575 unfolding refs_of'_def' by auto |
576 from prs_refs prs_def have p_not_in_refs: "p \<notin> set refs" |
576 from prs_refs prs_def have p_not_in_refs: "p \<notin> set refs" |
577 by (fastsimp dest!: refs_of'_distinct) |
577 by (fastsimp dest!: refs_of'_distinct) |
578 with refs_def p_is_Node list_of'_ref have 2: "list_of' (set_ref p (Node x q) h) ref xs" |
578 with refs_def p_is_Node list_of'_ref have 2: "list_of' (Ref.set p (Node x q) h) ref xs" |
579 by (auto simp add: list_of'_set_ref) |
579 by (auto simp add: list_of'_set_ref) |
580 from p_notin_qrs qrs_def have refs_of1: "refs_of' (set_ref p (Node x q) h) p (p#qrs)" |
580 from p_notin_qrs qrs_def have refs_of1: "refs_of' (Ref.set p (Node x q) h) p (p#qrs)" |
581 unfolding refs_of'_def' |
581 unfolding refs_of'_def' |
582 apply (simp) |
582 apply (simp) |
583 unfolding refs_of'_def'[symmetric] |
583 unfolding refs_of'_def'[symmetric] |
584 by (simp add: refs_of'_set_ref) |
584 by (simp add: refs_of'_set_ref) |
585 from p_not_in_refs p_is_Node refs_def have refs_of2: "refs_of' (set_ref p (Node x q) h) ref refs" |
585 from p_not_in_refs p_is_Node refs_def have refs_of2: "refs_of' (Ref.set p (Node x q) h) ref refs" |
586 by (simp add: refs_of'_set_ref) |
586 by (simp add: refs_of'_set_ref) |
587 from p_not_in_refs refs_of1 refs_of2 distinct_pointers prs_refs have 3: "\<forall>qrs prs. refs_of' (set_ref p (Node x q) h) p qrs \<and> refs_of' (set_ref p (Node x q) h) ref prs \<longrightarrow> set prs \<inter> set qrs = {}" |
587 from p_not_in_refs refs_of1 refs_of2 distinct_pointers prs_refs have 3: "\<forall>qrs prs. refs_of' (Ref.set p (Node x q) h) p qrs \<and> refs_of' (Ref.set p (Node x q) h) ref prs \<longrightarrow> set prs \<inter> set qrs = {}" |
588 apply - apply (rule allI)+ apply (rule impI) apply (erule conjE) |
588 apply - apply (rule allI)+ apply (rule impI) apply (erule conjE) |
589 apply (drule refs_of'_is_fun) back back apply assumption |
589 apply (drule refs_of'_is_fun) back back apply assumption |
590 apply (drule refs_of'_is_fun) back back apply assumption |
590 apply (drule refs_of'_is_fun) back back apply assumption |
591 apply auto done |
591 apply auto done |
592 from Cons.hyps [OF crel_rev' 1 2 3] show ?case by simp |
592 from Cons.hyps [OF crel_rev' 1 2 3] show ?case by simp |
593 qed |
593 qed |
594 |
594 |
595 |
595 |
596 lemma rev_correctness: |
596 lemma rev_correctness: |
597 assumes list_of_h: "list_of h r xs" |
597 assumes list_of_h: "list_of h r xs" |
598 assumes validHeap: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>r \<in> set refs. ref_present r h)" |
598 assumes validHeap: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>r \<in> set refs. Ref.present h r)" |
599 assumes crel_rev: "crel (rev r) h h' r'" |
599 assumes crel_rev: "crel (rev r) h h' r'" |
600 shows "list_of h' r' (List.rev xs)" |
600 shows "list_of h' r' (List.rev xs)" |
601 using assms |
601 using assms |
602 proof (cases r) |
602 proof (cases r) |
603 case Empty |
603 case Empty |
604 with list_of_h crel_rev show ?thesis |
604 with list_of_h crel_rev show ?thesis |
605 by (auto simp add: list_of_Empty elim!: crel_return) |
605 by (auto simp add: list_of_Empty elim!: crel_return) |
606 next |
606 next |
607 case (Node x ps) |
607 case (Node x ps) |
608 with crel_rev obtain p q h1 h2 h3 v where |
608 with crel_rev obtain p q h1 h2 h3 v where |
609 init: "crel (Ref.new Empty) h h1 q" |
609 init: "crel (ref Empty) h h1 q" |
610 "crel (Ref.new (Node x ps)) h1 h2 p" |
610 "crel (ref (Node x ps)) h1 h2 p" |
611 and crel_rev':"crel (rev' (q, p)) h2 h3 v" |
611 and crel_rev':"crel (rev' (q, p)) h2 h3 v" |
612 and lookup: "crel (!v) h3 h' r'" |
612 and lookup: "crel (!v) h3 h' r'" |
613 using rev.simps |
613 using rev.simps |
614 by (auto elim!: crelE) |
614 by (auto elim!: crelE) |
615 from init have a1:"list_of' h2 q []" |
615 from init have a1:"list_of' h2 q []" |
616 unfolding list_of'_def |
616 unfolding list_of'_def |
617 by (auto elim!: crel_Ref_new) |
617 by (auto elim!: crel_ref) |
618 from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of) |
618 from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of) |
619 from validHeap init refs_def have heap_eq: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref\<in>set refs. ref_present ref h \<and> ref_present ref h2 \<and> get_ref ref h = get_ref ref h2)" |
619 from validHeap init refs_def have heap_eq: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)" |
620 by (fastsimp elim!: crel_Ref_new dest: refs_of_is_fun) |
620 by (fastsimp elim!: crel_ref dest: refs_of_is_fun) |
621 from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" . |
621 from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" . |
622 from init this Node have a2: "list_of' h2 p xs" |
622 from init this Node have a2: "list_of' h2 p xs" |
623 apply - |
623 apply - |
624 unfolding list_of'_def |
624 unfolding list_of'_def |
625 apply (auto elim!: crel_Ref_new) |
625 apply (auto elim!: crel_ref) |
626 done |
626 done |
627 from init have refs_of_q: "refs_of' h2 q [q]" |
627 from init have refs_of_q: "refs_of' h2 q [q]" |
628 by (auto elim!: crel_Ref_new) |
628 by (auto elim!: crel_ref) |
629 from refs_def Node have refs_of'_ps: "refs_of' h ps refs" |
629 from refs_def Node have refs_of'_ps: "refs_of' h ps refs" |
630 by (auto simp add: refs_of'_def'[symmetric]) |
630 by (auto simp add: refs_of'_def'[symmetric]) |
631 from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. ref_present r h" by simp |
631 from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. Ref.present h r" by simp |
632 from init refs_of'_ps Node this have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. ref_present ref h \<and> ref_present ref h2 \<and> get_ref ref h = get_ref ref h2)" |
632 from init refs_of'_ps Node this have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)" |
633 by (fastsimp elim!: crel_Ref_new dest: refs_of'_is_fun) |
633 by (fastsimp elim!: crel_ref dest: refs_of'_is_fun) |
634 from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" . |
634 from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" . |
635 with init have refs_of_p: "refs_of' h2 p (p#refs)" |
635 with init have refs_of_p: "refs_of' h2 p (p#refs)" |
636 by (auto elim!: crel_Ref_new simp add: refs_of'_def') |
636 by (auto elim!: crel_ref simp add: refs_of'_def') |
637 with init all_ref_present have q_is_new: "q \<notin> set (p#refs)" |
637 with init all_ref_present have q_is_new: "q \<notin> set (p#refs)" |
638 by (auto elim!: crel_Ref_new intro!: noteq_refsI) |
638 by (auto elim!: crel_ref intro!: Ref.noteq_I) |
639 from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}" |
639 from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}" |
640 by (fastsimp simp only: set.simps dest: refs_of'_is_fun) |
640 by (fastsimp simp only: set.simps dest: refs_of'_is_fun) |
641 from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (get_ref v h3) (List.rev xs)" |
641 from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" |
642 unfolding list_of'_def by auto |
642 unfolding list_of'_def by auto |
643 with lookup show ?thesis |
643 with lookup show ?thesis |
644 by (auto elim: crel_lookup) |
644 by (auto elim: crel_lookup) |
645 qed |
645 qed |
646 |
646 |
732 text {* From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate *} |
732 text {* From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate *} |
733 |
733 |
734 lemma merge_induct2: |
734 lemma merge_induct2: |
735 assumes "list_of' h (p::'a::{heap, ord} node ref) xs" |
735 assumes "list_of' h (p::'a::{heap, ord} node ref) xs" |
736 assumes "list_of' h q ys" |
736 assumes "list_of' h q ys" |
737 assumes "\<And> ys p q. \<lbrakk> list_of' h p []; list_of' h q ys; get_ref p h = Empty \<rbrakk> \<Longrightarrow> P p q [] ys" |
737 assumes "\<And> ys p q. \<lbrakk> list_of' h p []; list_of' h q ys; Ref.get h p = Empty \<rbrakk> \<Longrightarrow> P p q [] ys" |
738 assumes "\<And> x xs' p q pn. \<lbrakk> list_of' h p (x#xs'); list_of' h q []; get_ref p h = Node x pn; get_ref q h = Empty \<rbrakk> \<Longrightarrow> P p q (x#xs') []" |
738 assumes "\<And> x xs' p q pn. \<lbrakk> list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty \<rbrakk> \<Longrightarrow> P p q (x#xs') []" |
739 assumes "\<And> x xs' y ys' p q pn qn. |
739 assumes "\<And> x xs' y ys' p q pn qn. |
740 \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); get_ref p h = Node x pn; get_ref q h = Node y qn; |
740 \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn; |
741 x \<le> y; P pn q xs' (y#ys') \<rbrakk> |
741 x \<le> y; P pn q xs' (y#ys') \<rbrakk> |
742 \<Longrightarrow> P p q (x#xs') (y#ys')" |
742 \<Longrightarrow> P p q (x#xs') (y#ys')" |
743 assumes "\<And> x xs' y ys' p q pn qn. |
743 assumes "\<And> x xs' y ys' p q pn qn. |
744 \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); get_ref p h = Node x pn; get_ref q h = Node y qn; |
744 \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn; |
745 \<not> x \<le> y; P p qn (x#xs') ys'\<rbrakk> |
745 \<not> x \<le> y; P p qn (x#xs') ys'\<rbrakk> |
746 \<Longrightarrow> P p q (x#xs') (y#ys')" |
746 \<Longrightarrow> P p q (x#xs') (y#ys')" |
747 shows "P p q xs ys" |
747 shows "P p q xs ys" |
748 using assms(1-2) |
748 using assms(1-2) |
749 proof (induct xs ys arbitrary: p q rule: Lmerge.induct) |
749 proof (induct xs ys arbitrary: p q rule: Lmerge.induct) |
750 case (2 ys) |
750 case (2 ys) |
751 from 2(1) have "get_ref p h = Empty" unfolding list_of'_def by simp |
751 from 2(1) have "Ref.get h p = Empty" unfolding list_of'_def by simp |
752 with 2(1-2) assms(3) show ?case by blast |
752 with 2(1-2) assms(3) show ?case by blast |
753 next |
753 next |
754 case (3 x xs') |
754 case (3 x xs') |
755 from 3(1) obtain pn where Node: "get_ref p h = Node x pn" by (rule list_of'_Cons) |
755 from 3(1) obtain pn where Node: "Ref.get h p = Node x pn" by (rule list_of'_Cons) |
756 from 3(2) have "get_ref q h = Empty" unfolding list_of'_def by simp |
756 from 3(2) have "Ref.get h q = Empty" unfolding list_of'_def by simp |
757 with Node 3(1-2) assms(4) show ?case by blast |
757 with Node 3(1-2) assms(4) show ?case by blast |
758 next |
758 next |
759 case (1 x xs' y ys') |
759 case (1 x xs' y ys') |
760 from 1(3) obtain pn where pNode:"get_ref p h = Node x pn" |
760 from 1(3) obtain pn where pNode:"Ref.get h p = Node x pn" |
761 and list_of'_pn: "list_of' h pn xs'" by (rule list_of'_Cons) |
761 and list_of'_pn: "list_of' h pn xs'" by (rule list_of'_Cons) |
762 from 1(4) obtain qn where qNode:"get_ref q h = Node y qn" |
762 from 1(4) obtain qn where qNode:"Ref.get h q = Node y qn" |
763 and list_of'_qn: "list_of' h qn ys'" by (rule list_of'_Cons) |
763 and list_of'_qn: "list_of' h qn ys'" by (rule list_of'_Cons) |
764 show ?case |
764 show ?case |
765 proof (cases "x \<le> y") |
765 proof (cases "x \<le> y") |
766 case True |
766 case True |
767 from 1(1)[OF True list_of'_pn 1(4)] assms(5) 1(3-4) pNode qNode True |
767 from 1(1)[OF True list_of'_pn 1(4)] assms(5) 1(3-4) pNode qNode True |