373 |
373 |
374 end |
374 end |
375 |
375 |
376 context valid_trace_p_w |
376 context valid_trace_p_w |
377 begin |
377 begin |
378 |
|
379 interpretation vat_e: valid_trace "e#s" |
|
380 by (unfold_locales, insert vt_e, simp) |
|
381 |
378 |
382 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s" |
379 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s" |
383 using holding_s_holder |
380 using holding_s_holder |
384 by (unfold s_RAG_def, fold holding_eq, auto) |
381 by (unfold s_RAG_def, fold holding_eq, auto) |
385 |
382 |
426 assumes "u \<in> ancestors (tRAG (e#s)) (Th th)" |
423 assumes "u \<in> ancestors (tRAG (e#s)) (Th th)" |
427 and "cp_gen (e#s) u = cp_gen s u" |
424 and "cp_gen (e#s) u = cp_gen s u" |
428 and "y \<in> ancestors (tRAG (e#s)) u" |
425 and "y \<in> ancestors (tRAG (e#s)) u" |
429 shows "cp_gen (e#s) y = cp_gen s y" |
426 shows "cp_gen (e#s) y = cp_gen s y" |
430 using assms(3) |
427 using assms(3) |
431 proof(induct rule:wf_induct[OF vat_e.fsbttRAGs.wf]) |
428 proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf]) |
432 case (1 x) |
429 case (1 x) |
433 show ?case (is "?L = ?R") |
430 show ?case (is "?L = ?R") |
434 proof - |
431 proof - |
435 from tRAG_ancestorsE[OF 1(2)] |
432 from tRAG_ancestorsE[OF 1(2)] |
436 obtain th2 where eq_x: "x = Th th2" by blast |
433 obtain th2 where eq_x: "x = Th th2" by blast |
437 from vat_e.cp_gen_rec[OF this] |
434 from vat_es.cp_gen_rec[OF this] |
438 have "?L = |
435 have "?L = |
439 Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . |
436 Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . |
440 also have "... = |
437 also have "... = |
441 Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" |
438 Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" |
442 proof - |
439 proof - |
452 show "x \<notin> Range {(Th th, Th holder)}" |
449 show "x \<notin> Range {(Th th, Th holder)}" |
453 proof |
450 proof |
454 assume "x \<in> Range {(Th th, Th holder)}" |
451 assume "x \<in> Range {(Th th, Th holder)}" |
455 hence eq_x: "x = Th holder" using RangeE by auto |
452 hence eq_x: "x = Th holder" using RangeE by auto |
456 show False |
453 show False |
457 proof(cases rule:vat_e.ancestors_headE[OF assms(1) start]) |
454 proof(cases rule:vat_es.ancestors_headE[OF assms(1) start]) |
458 case 1 |
455 case 1 |
459 from x_u[folded this, unfolded eq_x] vat_e.acyclic_tRAG |
456 from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG |
460 show ?thesis by (auto simp:ancestors_def acyclic_def) |
457 show ?thesis by (auto simp:ancestors_def acyclic_def) |
461 next |
458 next |
462 case 2 |
459 case 2 |
463 with x_u[unfolded eq_x] |
460 with x_u[unfolded eq_x] |
464 have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def) |
461 have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def) |
465 with vat_e.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) |
462 with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) |
466 qed |
463 qed |
467 qed |
464 qed |
468 qed |
465 qed |
469 moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = |
466 moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = |
470 cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A") |
467 cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A") |
471 proof(rule f_image_eq) |
468 proof(rule f_image_eq) |
472 fix a |
469 fix a |
473 assume a_in: "a \<in> ?A" |
470 assume a_in: "a \<in> ?A" |
474 from 1(2) |
471 from 1(2) |
475 show "?f a = ?g a" |
472 show "?f a = ?g a" |
476 proof(cases rule:vat_e.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) |
473 proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) |
477 case in_ch |
474 case in_ch |
478 show ?thesis |
475 show ?thesis |
479 proof(cases "a = u") |
476 proof(cases "a = u") |
480 case True |
477 case True |
481 from assms(2)[folded this] show ?thesis . |
478 from assms(2)[folded this] show ?thesis . |
483 case False |
480 case False |
484 have a_not_in: "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
481 have a_not_in: "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
485 proof |
482 proof |
486 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
483 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
487 have "a = u" |
484 have "a = u" |
488 proof(rule vat_e.rtree_s.ancestors_children_unique) |
485 proof(rule vat_es.rtree_s.ancestors_children_unique) |
489 from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
486 from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
490 RTree.children (tRAG (e#s)) x" by auto |
487 RTree.children (tRAG (e#s)) x" by auto |
491 next |
488 next |
492 from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
489 from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
493 RTree.children (tRAG (e#s)) x" by auto |
490 RTree.children (tRAG (e#s)) x" by auto |
517 by (auto simp:RTree.children_def tRAG_alt_def) |
514 by (auto simp:RTree.children_def tRAG_alt_def) |
518 have "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
515 have "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
519 proof |
516 proof |
520 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
517 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
521 have "a = z" |
518 have "a = z" |
522 proof(rule vat_e.rtree_s.ancestors_children_unique) |
519 proof(rule vat_es.rtree_s.ancestors_children_unique) |
523 from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" |
520 from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" |
524 by (auto simp:ancestors_def) |
521 by (auto simp:ancestors_def) |
525 with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
522 with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
526 RTree.children (tRAG (e#s)) x" by auto |
523 RTree.children (tRAG (e#s)) x" by auto |
527 next |
524 next |
567 |
564 |
568 section {* The @{term Create} operation *} |
565 section {* The @{term Create} operation *} |
569 |
566 |
570 context valid_trace_create |
567 context valid_trace_create |
571 begin |
568 begin |
572 |
|
573 interpretation vat_e: valid_trace "e#s" |
|
574 by (unfold_locales, insert vt_e, simp) |
|
575 |
569 |
576 lemma tRAG_kept: "tRAG (e#s) = tRAG s" |
570 lemma tRAG_kept: "tRAG (e#s) = tRAG s" |
577 by (unfold tRAG_alt_def RAG_unchanged, auto) |
571 by (unfold tRAG_alt_def RAG_unchanged, auto) |
578 |
572 |
579 lemma preced_kept: |
573 lemma preced_kept: |
630 by (unfold Field_def tRAG_kept, auto) |
624 by (unfold Field_def tRAG_kept, auto) |
631 } thus ?thesis by auto |
625 } thus ?thesis by auto |
632 qed |
626 qed |
633 |
627 |
634 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" |
628 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" |
635 by (unfold vat_e.cp_rec children_of_th, simp add:the_preced_def) |
629 by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def) |
636 |
630 |
637 end |
631 end |
638 |
632 |
639 |
633 |
640 context valid_trace_exit |
634 context valid_trace_exit |