394 proof - |
394 proof - |
395 from assms[unfolded tRAG_alt_def Field_def Domain_def Range_def] |
395 from assms[unfolded tRAG_alt_def Field_def Domain_def Range_def] |
396 show ?thesis using that by auto |
396 show ?thesis using that by auto |
397 qed |
397 qed |
398 |
398 |
|
399 |
399 lemma trancl_tG_tRAG: |
400 lemma trancl_tG_tRAG: |
400 assumes "(th1, th2) \<in> (tG s)^+" |
401 assumes "(th1, th2) \<in> (tG s)^+" |
401 shows "(Th th1, Th th2) \<in> (tRAG s)^+" |
402 shows "(Th th1, Th th2) \<in> (tRAG s)^+" |
402 proof - |
403 using assms unfolding tRAG_def_tG |
403 have "inj_on the_thread (Field (tRAG s))" |
404 proof(induct rule:trancl_induct) |
404 by (unfold inj_on_def Field_def tRAG_alt_def, auto) |
405 case (step y z) |
405 from map_prod_tranclE[OF assms[unfolded tG_def] this] |
406 from step(2) have "(Th y, Th z) \<in> map_prod Th Th ` (tG s)" by auto |
406 obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+" |
407 with step(3) |
407 by auto |
408 show ?case by auto |
408 hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def) |
409 qed auto |
409 from this[unfolded trancl_domain trancl_range] |
|
410 have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)" |
|
411 by (unfold Field_def, auto) |
|
412 then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'" |
|
413 by (auto elim!:Field_tRAGE) |
|
414 with h have "th1' = th1" "th2' = th2" by (auto) |
|
415 from h(3)[unfolded h' this] |
|
416 show ?thesis by (auto simp:ancestors_def) |
|
417 qed |
|
418 |
410 |
419 lemma rtrancl_tG_tRAG: |
411 lemma rtrancl_tG_tRAG: |
420 assumes "(th1, th2) \<in> (tG s)^*" |
412 assumes "(th1, th2) \<in> (tG s)^*" |
421 shows "(Th th1, Th th2) \<in> (tRAG s)^*" |
413 shows "(Th th1, Th th2) \<in> (tRAG s)^*" |
422 proof - |
414 proof - |
704 which is based on the notion of subtrees in @{term RAG} and |
696 which is based on the notion of subtrees in @{term RAG} and |
705 is handy to use once the abstract theory of {\em relational graph} |
697 is handy to use once the abstract theory of {\em relational graph} |
706 (and specifically {\em relational tree} and {\em relational forest}) |
698 (and specifically {\em relational tree} and {\em relational forest}) |
707 are in place. |
699 are in place. |
708 *} |
700 *} |
|
701 |
|
702 lemma cp_s_def: "cp s th = Max (preceds (subtree (tG s) th) s)" |
|
703 by (unfold cp_eq cpreced_def s_tG_abv, simp) |
|
704 |
709 lemma cp_alt_def: |
705 lemma cp_alt_def: |
710 "cp s th = Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
706 "cp s th = Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
711 proof - |
707 apply (unfold cp_s_def subtree_tG_tRAG threads_set_eq) |
712 have "Max (the_preced s ` ({th} \<union> dependants s th)) = |
708 by (smt Collect_cong Setcompr_eq_image the_preced_def) |
713 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
714 (is "Max (_ ` ?L) = Max (_ ` ?R)") |
|
715 proof - |
|
716 have "?L = ?R" |
|
717 unfolding subtree_def |
|
718 apply(auto) |
|
719 apply (simp add: s_RAG_abv s_dependants_def wq_def) |
|
720 by (simp add: rtrancl_eq_or_trancl s_RAG_abv s_dependants_def wq_def) |
|
721 thus ?thesis by simp |
|
722 qed |
|
723 thus ?thesis |
|
724 by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq |
|
725 s_dependants_abv the_preced_def) |
|
726 qed |
|
727 |
709 |
728 text {* |
710 text {* |
729 The following is another definition of @{term cp}. |
711 The following is another definition of @{term cp}. |
730 *} |
712 *} |
731 lemma cp_alt_def1: |
713 lemma cp_alt_def1: |
800 ultimately show ?thesis |
782 ultimately show ?thesis |
801 by (unfold eq_n tRAG_alt_def, auto) |
783 by (unfold eq_n tRAG_alt_def, auto) |
802 qed |
784 qed |
803 } ultimately show ?thesis by auto |
785 } ultimately show ?thesis by auto |
804 qed |
786 qed |
805 |
|
806 text {* |
|
807 The following lemmas gives an alternative definition @{term dependants} |
|
808 in terms of @{term tRAG}. |
|
809 *} |
|
810 |
|
811 lemma dependants_alt_def: |
|
812 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
|
813 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
|
814 |
|
815 text {* |
|
816 The following lemmas gives another alternative definition @{term dependants} |
|
817 in terms of @{term RAG}. |
|
818 *} |
|
819 |
|
820 lemma dependants_alt_def1: |
|
821 "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}" |
|
822 using dependants_alt_def tRAG_trancl_eq by auto |
|
823 |
|
824 text {* |
|
825 Another definition of dependants based on @{term tG}: |
|
826 *} |
|
827 lemma dependants_alt_tG: |
|
828 "dependants s th = {th'. (th', th) \<in> (tG s)^+}" (is "?L = ?R") |
|
829 proof - |
|
830 have "?L = {th'. (Th th', Th th) \<in> (tRAG s)\<^sup>+}" |
|
831 by (unfold dependants_alt_def, simp) |
|
832 also have "... = ?R" (is "?LL = ?RR") |
|
833 proof - |
|
834 { fix th' |
|
835 assume "th' \<in> ?LL" |
|
836 hence "(Th th', Th th) \<in> (tRAG s)\<^sup>+" by simp |
|
837 from trancl_tRAG_tG[OF this] |
|
838 have "th' \<in> ?RR" by auto |
|
839 } moreover { |
|
840 fix th' |
|
841 assume "th' \<in> ?RR" |
|
842 hence "(th', th) \<in> (tG s)\<^sup>+" by simp |
|
843 from trancl_tG_tRAG[OF this] |
|
844 have "th' \<in> ?LL" by auto |
|
845 } ultimately show ?thesis by auto |
|
846 qed |
|
847 finally show ?thesis . |
|
848 qed |
|
849 |
|
850 lemma dependants_alt_def_tG_ancestors: |
|
851 "dependants s th = {th'. th \<in> ancestors (tG s) th'}" |
|
852 by (unfold dependants_alt_tG ancestors_def, simp) |
|
853 |
|
854 |
|
855 |
787 |
856 section {* Locales used to investigate the execution of PIP *} |
788 section {* Locales used to investigate the execution of PIP *} |
857 |
789 |
858 text {* |
790 text {* |
859 The following locale @{text valid_trace} is used to constrain the |
791 The following locale @{text valid_trace} is used to constrain the |
2541 have "finite (wRAG s)" "finite (hRAG s)" by auto |
2473 have "finite (wRAG s)" "finite (hRAG s)" by auto |
2542 from finite_relcomp[OF this] tRAG_def |
2474 from finite_relcomp[OF this] tRAG_def |
2543 show ?thesis by simp |
2475 show ?thesis by simp |
2544 qed |
2476 qed |
2545 |
2477 |
|
2478 find_theorems inj finite "_ ` _" |
|
2479 |
|
2480 find_theorems tG tRAG |
|
2481 |
|
2482 thm tRAG_def_tG |
|
2483 |
|
2484 find_theorems "finite (?f ` ?A)" "finite ?A" |
|
2485 |
2546 lemma finite_tG: "finite (tG s)" |
2486 lemma finite_tG: "finite (tG s)" |
2547 by (unfold tG_def, insert finite_tRAG, auto) |
2487 proof(rule finite_imageD) |
|
2488 from finite_tRAG[unfolded tRAG_def_tG] |
|
2489 show "finite (map_prod Th Th ` tG s)" . |
|
2490 next |
|
2491 show "inj_on (map_prod Th Th) (tG s)" |
|
2492 using inj_on_def by fastforce |
|
2493 qed |
2548 |
2494 |
2549 end |
2495 end |
2550 |
2496 |
2551 subsection {* Uniqueness of waiting *} |
2497 subsection {* Uniqueness of waiting *} |
2552 |
2498 |
3106 proof(rule rel_map_acyclic [OF acyclic_tRAG]) |
3052 proof(rule rel_map_acyclic [OF acyclic_tRAG]) |
3107 show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))" |
3053 show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))" |
3108 by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto) |
3054 by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto) |
3109 qed |
3055 qed |
3110 thus ?thesis |
3056 thus ?thesis |
3111 by (unfold tG_def, fold rel_map_alt_def, simp) |
3057 by (unfold tG_def_tRAG, fold rel_map_alt_def, simp) |
3112 qed |
3058 qed |
3113 |
3059 |
3114 lemma sgv_wRAG: "single_valued (wRAG s)" |
3060 lemma sgv_wRAG: "single_valued (wRAG s)" |
3115 using waiting_unique |
3061 using waiting_unique |
3116 by (unfold single_valued_def wRAG_def, auto) |
3062 by (unfold single_valued_def wRAG_def, auto) |
3342 assumes th_in: "th \<in> threads s" |
3288 assumes th_in: "th \<in> threads s" |
3343 shows "\<exists>th'\<in> nancestors (tG s) th. th' \<in> readys s" |
3289 shows "\<exists>th'\<in> nancestors (tG s) th. th' \<in> readys s" |
3344 proof - |
3290 proof - |
3345 from th_chain_to_ready[OF assms] |
3291 from th_chain_to_ready[OF assms] |
3346 show ?thesis |
3292 show ?thesis |
3347 using dependants_alt_def1 dependants_alt_tG |
3293 proof |
3348 unfolding nancestors_def ancestors_def |
3294 assume "th \<in> readys s" |
3349 by blast |
3295 thus ?thesis by (unfold nancestors_def, auto) |
|
3296 next |
|
3297 assume "\<exists>th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)\<^sup>+" |
|
3298 then obtain th' where h: "th' \<in> readys s" "(Th th, Th th') \<in> (RAG s)\<^sup>+" by auto |
|
3299 from h(2) tRAG_trancl_eq |
|
3300 have "(Th th, Th th') \<in> (tRAG s)^+" by auto |
|
3301 hence "(th, th') \<in> (tG s)^+" |
|
3302 by (metis the_thread.simps trancl_tRAG_tG) |
|
3303 with h(1) |
|
3304 show ?thesis |
|
3305 using ancestors_def mem_Collect_eq nancestors2 by fastforce |
|
3306 qed |
3350 qed |
3307 qed |
3351 |
3308 |
3352 |
3309 |
3353 text {* |
3310 text {* |
3354 The following lemma is a technical one to show |
3311 The following lemma is a technical one to show |
3752 the maximum precedence of its own subtree, by applying |
3709 the maximum precedence of its own subtree, by applying |
3753 the absorbing property of @{term Max} (lemma @{thm Max_UNION}) |
3710 the absorbing property of @{term Max} (lemma @{thm Max_UNION}) |
3754 over the union of subtrees, the following equation can be derived: |
3711 over the union of subtrees, the following equation can be derived: |
3755 *} |
3712 *} |
3756 |
3713 |
3757 |
|
3758 lemma cp_alt_def3: |
3714 lemma cp_alt_def3: |
3759 shows "cp s th = Max (preceds (subtree (tG s) th) s)" |
3715 shows "cp s th = Max (preceds (subtree (tG s) th) s)" |
3760 unfolding cp_alt_def2 |
3716 unfolding cp_alt_def2 |
3761 unfolding image_def |
3717 unfolding image_def |
3762 unfolding the_preced_def |
3718 unfolding the_preced_def |
5171 lemma count_eq_RAG_plus_Th: |
5127 lemma count_eq_RAG_plus_Th: |
5172 assumes "cntP s th = cntV s th" |
5128 assumes "cntP s th = cntV s th" |
5173 shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
5129 shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
5174 using count_eq_RAG_plus[OF assms] by auto |
5130 using count_eq_RAG_plus[OF assms] by auto |
5175 |
5131 |
5176 lemma eq_pv_dependants: |
|
5177 assumes eq_pv: "cntP s th = cntV s th" |
|
5178 shows "dependants s th = {}" |
|
5179 proof - |
|
5180 from count_eq_RAG_plus[OF assms, folded dependants_alt_def1] |
|
5181 show ?thesis . |
|
5182 qed |
|
5183 |
5132 |
5184 lemma count_eq_tRAG_plus: |
5133 lemma count_eq_tRAG_plus: |
5185 assumes "cntP s th = cntV s th" |
5134 assumes "cntP s th = cntV s th" |
5186 shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
5135 shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
5187 using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast |
5136 using count_eq_RAG_plus_Th[OF assms] |
5188 |
5137 using tRAG_trancl_eq by auto |
|
5138 |
5189 lemma count_eq_tRAG_plus_Th: |
5139 lemma count_eq_tRAG_plus_Th: |
5190 assumes "cntP s th = cntV s th" |
5140 assumes "cntP s th = cntV s th" |
5191 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
5141 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
5192 using count_eq_tRAG_plus[OF assms] by auto |
5142 using count_eq_tRAG_plus[OF assms] by auto |
5193 |
5143 |