12 as well as for deriving more advance properties concerning |
12 as well as for deriving more advance properties concerning |
13 the correctness and implementation of PIP. |
13 the correctness and implementation of PIP. |
14 *} |
14 *} |
15 |
15 |
16 |
16 |
17 section {* Generic aulxiliary lemmas *} |
17 section {* Generic auxiliary lemmas *} |
18 |
18 |
19 lemma rel_eqI: |
19 lemma rel_eqI: |
20 assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B" |
20 assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B" |
21 and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A" |
21 and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A" |
22 shows "A = B" |
22 shows "A = B" |
538 qed |
538 qed |
539 hence "th' \<in> ?L" by auto |
539 hence "th' \<in> ?L" by auto |
540 } ultimately show ?thesis by blast |
540 } ultimately show ?thesis by blast |
541 qed |
541 qed |
542 |
542 |
|
543 lemma image_eq: |
|
544 assumes "A = B" |
|
545 shows "f ` A = f ` B" |
|
546 using assms by auto |
|
547 |
543 lemma tRAG_trancl_eq_Th: |
548 lemma tRAG_trancl_eq_Th: |
544 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
549 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
545 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
550 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
546 using tRAG_trancl_eq by auto |
551 using tRAG_trancl_eq by auto |
547 |
552 |
571 from rtranclD[OF this(2)] |
576 from rtranclD[OF this(2)] |
572 have "n \<in> ?L" |
577 have "n \<in> ?L" |
573 proof |
578 proof |
574 assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+" |
579 assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+" |
575 with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto |
580 with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto |
576 thus ?thesis using subtree_def tRAG_trancl_eq by fastforce |
581 thus ?thesis using subtree_def tRAG_trancl_eq |
|
582 by fastforce (* ccc *) |
577 qed (insert h, auto simp:subtree_def) |
583 qed (insert h, auto simp:subtree_def) |
578 } ultimately show ?thesis by auto |
584 } ultimately show ?thesis by auto |
579 qed |
585 qed |
580 |
586 |
581 lemma threads_set_eq: |
587 lemma threads_set_eq: |
4872 apply(simp add: Domain_iff Range_iff) |
4878 apply(simp add: Domain_iff Range_iff) |
4873 apply(simp add: wq_def) |
4879 apply(simp add: wq_def) |
4874 apply(auto) |
4880 apply(auto) |
4875 done |
4881 done |
4876 |
4882 |
|
4883 lemma detached_cp_the_preced: |
|
4884 assumes "detached s th" |
|
4885 shows "cp s th = the_preced s th" (is "?L = ?R") |
|
4886 proof - |
|
4887 have "?L = Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
4888 by (unfold cp_alt_def, simp) |
|
4889 moreover have "{th'. Th th' \<in> subtree (RAG s) (Th th)} = {th}" |
|
4890 proof - |
|
4891 { fix n |
|
4892 assume "n \<in> subtree (RAG s) (Th th)" |
|
4893 hence "n = Th th" |
|
4894 proof(cases rule:subtreeE) |
|
4895 case 2 |
|
4896 from 2(2) have "Th th \<in> Range (RAG s)" |
|
4897 by (elim ancestors_Field, simp) |
|
4898 moreover from assms[unfolded detached_test] have "Th th \<notin> Field (RAG s)" . |
|
4899 ultimately have False by (auto simp:Field_def) |
|
4900 thus ?thesis by simp |
|
4901 qed simp |
|
4902 } thus ?thesis by auto |
|
4903 qed |
|
4904 ultimately show ?thesis by auto |
|
4905 qed |
|
4906 |
|
4907 lemma detached_cp_preced: |
|
4908 assumes "detached s th" |
|
4909 shows "cp s th = preced th s" |
|
4910 using detached_cp_the_preced[OF assms] |
|
4911 by (simp add:the_preced_def) |
|
4912 |
4877 context valid_trace |
4913 context valid_trace |
4878 begin |
4914 begin |
4879 |
4915 |
4880 lemma detached_intro: |
4916 lemma detached_intro: |
4881 assumes eq_pv: "cntP s th = cntV s th" |
4917 assumes eq_pv: "cntP s th = cntV s th" |
5069 qed |
5105 qed |
5070 qed |
5106 qed |
5071 |
5107 |
5072 end |
5108 end |
5073 |
5109 |
5074 end |
5110 lemma PIP_actorE: |
|
5111 assumes "PIP s e" |
|
5112 and "actor e = th" |
|
5113 and "\<not> isCreate e" |
|
5114 shows "th \<in> runing s" |
|
5115 using assms |
|
5116 by (cases, auto) |
|
5117 |
|
5118 |
|
5119 lemma holdents_RAG: |
|
5120 assumes "holdents s th = {}" |
|
5121 shows "Th th \<notin> Range (RAG s)" |
|
5122 proof |
|
5123 assume "Th th \<in> Range (RAG s)" |
|
5124 thus False |
|
5125 proof(rule RangeE) |
|
5126 fix a |
|
5127 assume "(a, Th th) \<in> RAG s" |
|
5128 with assms[unfolded holdents_test] |
|
5129 show False |
|
5130 by (cases a, auto simp:cs_RAG_raw s_RAG_abv) |
|
5131 qed |
|
5132 qed |
|
5133 |
|
5134 lemma readys_RAG: |
|
5135 assumes "th \<in> readys s" |
|
5136 shows "Th th \<notin> Domain (RAG s)" |
|
5137 proof |
|
5138 assume "Th th \<in> Domain (RAG s)" |
|
5139 thus False |
|
5140 proof(rule DomainE) |
|
5141 fix b |
|
5142 assume "(Th th, b) \<in> RAG s" |
|
5143 with assms[unfolded readys_def s_waiting_def] |
|
5144 show False |
|
5145 by (cases b, auto simp:cs_RAG_raw s_RAG_abv cs_waiting_raw) |
|
5146 qed |
|
5147 qed |
|
5148 |
|
5149 lemma readys_holdents_detached: |
|
5150 assumes "th \<in> readys s" |
|
5151 and "holdents s th = {}" |
|
5152 shows "detached s th" |
|
5153 proof - |
|
5154 from readys_RAG[OF assms(1)] holdents_RAG[OF assms(2)] |
|
5155 show ?thesis |
|
5156 by (unfold detached_test Field_def, auto) |
|
5157 qed |
|
5158 |
|
5159 lemma len_actions_of_sigma: |
|
5160 assumes "finite A" |
|
5161 shows "length (actions_of A t) = (\<Sum> th' \<in> A. length (actions_of {th'} t))" |
|
5162 proof(induct t) |
|
5163 case h: (Cons e t) |
|
5164 thus ?case (is "?L = ?R" is "_ = ?T (e#t)") |
|
5165 proof(cases "actor e \<in> A") |
|
5166 case True |
|
5167 have "?L = 1 + ?T t" |
|
5168 by (fold h, insert True, simp add:actions_of_def) |
|
5169 moreover have "?R = 1 + ?T t" |
|
5170 proof - |
|
5171 have "?R = length (actions_of {actor e} (e # t)) + |
|
5172 (\<Sum>th'\<in>A - {actor e}. length (actions_of {th'} (e # t)))" |
|
5173 (is "_ = ?F (e#t) + ?G (e#t)") |
|
5174 by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", |
|
5175 OF assms True], simp) |
|
5176 moreover have "?F (e#t) = 1 + ?F t" using True |
|
5177 by (simp add:actions_of_def) |
|
5178 moreover have "?G (e#t) = ?G t" |
|
5179 by (rule setsum.cong, auto simp:actions_of_def) |
|
5180 moreover have "?F t + ?G t = ?T t" |
|
5181 by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", |
|
5182 OF assms True], simp) |
|
5183 ultimately show ?thesis by simp |
|
5184 qed |
|
5185 ultimately show ?thesis by simp |
|
5186 next |
|
5187 case False |
|
5188 hence "?L = length (actions_of A t)" |
|
5189 by (simp add:actions_of_def) |
|
5190 also have "... = (\<Sum>th'\<in>A. length (actions_of {th'} t))" by (simp add: h) |
|
5191 also have "... = ?R" |
|
5192 by (rule setsum.cong; insert False, auto simp:actions_of_def) |
|
5193 finally show ?thesis . |
|
5194 qed |
|
5195 qed (auto simp:actions_of_def) |
|
5196 |
|
5197 lemma threads_Exit: |
|
5198 assumes "th \<in> threads s" |
|
5199 and "th \<notin> threads (e#s)" |
|
5200 shows "e = Exit th" |
|
5201 using assms |
|
5202 by (cases e, auto) |
|
5203 |
|
5204 end |