171 by (case_tac a, auto split:if_splits) |
171 by (case_tac a, auto split:if_splits) |
172 |
172 |
173 lemma last_set_unique: |
173 lemma last_set_unique: |
174 "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk> |
174 "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk> |
175 \<Longrightarrow> th1 = th2" |
175 \<Longrightarrow> th1 = th2" |
176 apply (induct s, auto) |
176 apply (induct s, auto) |
177 by (case_tac a, auto split:if_splits dest:last_set_lt) |
177 by (case_tac a, auto split:if_splits dest:last_set_lt) |
178 |
178 |
179 lemma preced_unique : |
179 lemma preced_unique : |
180 assumes pcd_eq: "preced th1 s = preced th2 s" |
180 assumes pcd_eq: "preced th1 s = preced th2 s" |
181 and th_in1: "th1 \<in> threads s" |
181 and th_in1: "th1 \<in> threads s" |
1050 context valid_trace_create |
1050 context valid_trace_create |
1051 begin |
1051 begin |
1052 |
1052 |
1053 lemma wq_kept [simp]: |
1053 lemma wq_kept [simp]: |
1054 shows "wq (e#s) cs' = wq s cs'" |
1054 shows "wq (e#s) cs' = wq s cs'" |
1055 using assms unfolding is_create wq_def |
1055 unfolding is_create wq_def |
1056 by (auto simp:Let_def) |
1056 by (auto simp:Let_def) |
1057 |
1057 |
1058 lemma wq_distinct_kept: |
1058 lemma wq_distinct_kept: |
1059 assumes "distinct (wq s cs')" |
1059 assumes "distinct (wq s cs')" |
1060 shows "distinct (wq (e#s) cs')" |
1060 shows "distinct (wq (e#s) cs')" |
1064 context valid_trace_exit |
1064 context valid_trace_exit |
1065 begin |
1065 begin |
1066 |
1066 |
1067 lemma wq_kept [simp]: |
1067 lemma wq_kept [simp]: |
1068 shows "wq (e#s) cs' = wq s cs'" |
1068 shows "wq (e#s) cs' = wq s cs'" |
1069 using assms unfolding is_exit wq_def |
1069 unfolding is_exit wq_def |
1070 by (auto simp:Let_def) |
1070 by (auto simp:Let_def) |
1071 |
1071 |
1072 lemma wq_distinct_kept: |
1072 lemma wq_distinct_kept: |
1073 assumes "distinct (wq s cs')" |
1073 assumes "distinct (wq s cs')" |
1074 shows "distinct (wq (e#s) cs')" |
1074 shows "distinct (wq (e#s) cs')" |
1169 context valid_trace_set |
1169 context valid_trace_set |
1170 begin |
1170 begin |
1171 |
1171 |
1172 lemma wq_kept [simp]: |
1172 lemma wq_kept [simp]: |
1173 shows "wq (e#s) cs' = wq s cs'" |
1173 shows "wq (e#s) cs' = wq s cs'" |
1174 using assms unfolding is_set wq_def |
1174 unfolding is_set wq_def |
1175 by (auto simp:Let_def) |
1175 by (auto simp:Let_def) |
1176 |
1176 |
1177 lemma wq_distinct_kept: |
1177 lemma wq_distinct_kept: |
1178 assumes "distinct (wq s cs')" |
1178 assumes "distinct (wq s cs')" |
1179 shows "distinct (wq (e#s) cs')" |
1179 shows "distinct (wq (e#s) cs')" |
3718 unfolding the_preced_def |
3718 unfolding the_preced_def |
3719 by meson |
3719 by meson |
3720 |
3720 |
3721 lemma KK: |
3721 lemma KK: |
3722 shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})" |
3722 shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})" |
3723 (* and "\<Union>" *) |
|
3724 by (simp_all add: Setcompr_eq_image) |
3723 by (simp_all add: Setcompr_eq_image) |
3725 |
3724 |
3726 lemma Max_Segments: |
3725 lemma Max_Segments: |
3727 assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}" |
3726 assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}" |
3728 shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}" |
3727 shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}" |
3729 using assms |
3728 using assms |
3730 apply(subst KK(1)) |
3729 apply(subst KK(1)) |
3731 apply(subst Max_Union) |
3730 apply(subst Max_Union) |
3732 apply(auto)[3] |
3731 apply(auto)[3] |
3733 apply(simp add: Setcompr_eq_image) |
3732 apply(simp add: Setcompr_eq_image) |
3734 apply(simp add: image_eq_UN) |
3733 apply(auto simp add: image_image) |
3735 done |
3734 done |
3736 |
3735 |
3737 lemma max_cp_readys_max_preced_tG: |
3736 lemma max_cp_readys_max_preced_tG: |
3738 shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R") |
3737 shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R") |
3739 proof(cases "readys s = {}") |
3738 proof(cases "readys s = {}") |
4568 by (unfold readys_def, auto) |
4567 by (unfold readys_def, auto) |
4569 qed |
4568 qed |
4570 |
4569 |
4571 lemma readys_simp [simp]: |
4570 lemma readys_simp [simp]: |
4572 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
4571 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
4573 using readys_kept1[OF assms] readys_kept2[OF assms] |
4572 using readys_kept1 readys_kept2 |
4574 by metis |
4573 by metis |
4575 |
4574 |
4576 lemma cnp_cnv_cncs_kept: |
4575 lemma cnp_cnv_cncs_kept: |
4577 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
4576 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
4578 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
4577 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
5107 |
5106 |
5108 lemma eq_pv_subtree: |
5107 lemma eq_pv_subtree: |
5109 assumes eq_pv: "cntP s th = cntV s th" |
5108 assumes eq_pv: "cntP s th = cntV s th" |
5110 shows "subtree (RAG s) (Th th) = {Th th}" |
5109 shows "subtree (RAG s) (Th th) = {Th th}" |
5111 using eq_pv_children[OF assms] |
5110 using eq_pv_children[OF assms] |
5112 by (unfold subtree_children, simp) |
5111 apply(subst subtree_children) |
|
5112 apply(simp) |
|
5113 done |
5113 |
5114 |
5114 lemma count_eq_RAG_plus: |
5115 lemma count_eq_RAG_plus: |
5115 assumes "cntP s th = cntV s th" |
5116 assumes "cntP s th = cntV s th" |
5116 shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
5117 shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
5117 proof(rule ccontr) |
5118 proof(rule ccontr) |
5318 assumes "x = Th th" |
5319 assumes "x = Th th" |
5319 shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)" |
5320 shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)" |
5320 proof(cases "children (tRAG s) x = {}") |
5321 proof(cases "children (tRAG s) x = {}") |
5321 case True |
5322 case True |
5322 show ?thesis |
5323 show ?thesis |
5323 by (unfold True cp_gen_def subtree_children, simp add:assms) |
5324 apply(subst True) |
|
5325 apply(subst cp_gen_def) |
|
5326 apply(subst subtree_children) |
|
5327 apply(simp add: assms) |
|
5328 using True assms by auto |
5324 next |
5329 next |
5325 case False |
5330 case False |
5326 hence [simp]: "children (tRAG s) x \<noteq> {}" by auto |
5331 hence [simp]: "children (tRAG s) x \<noteq> {}" by auto |
5327 note fsbttRAGs.finite_subtree[simp] |
5332 note fsbttRAGs.finite_subtree[simp] |
5328 have [simp]: "finite (children (tRAG s) x)" |
5333 have [simp]: "finite (children (tRAG s) x)" |
5347 let ?L1 = "?f ` \<Union>(?g ` ?B)" |
5352 let ?L1 = "?f ` \<Union>(?g ` ?B)" |
5348 have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" |
5353 have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" |
5349 proof - |
5354 proof - |
5350 have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp |
5355 have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp |
5351 also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto |
5356 also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto |
5352 finally have "Max ?L1 = Max ..." by simp |
5357 finally have "Max ?L1 = Max ..." |
|
5358 by (simp add: \<open>(the_preced s \<circ> the_thread) ` (\<Union>x\<in>children (tRAG s) x. subtree (tRAG s) x) = (\<Union>x\<in>children (tRAG s) x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x)\<close>) |
5353 also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)" |
5359 also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)" |
5354 by (subst Max_UNION, simp+) |
5360 by(subst Max_Union, auto) |
5355 also have "... = Max (cp_gen s ` children (tRAG s) x)" |
5361 also have "... = Max (cp_gen s ` children (tRAG s) x)" |
5356 by (unfold image_comp cp_gen_alt_def, simp) |
5362 by (unfold image_comp cp_gen_alt_def, simp) |
5357 finally show ?thesis . |
5363 finally show ?thesis . |
5358 qed |
5364 qed |
5359 show ?thesis |
5365 show ?thesis |
5484 moreover have "?R = 1 + ?T t" |
5490 moreover have "?R = 1 + ?T t" |
5485 proof - |
5491 proof - |
5486 have "?R = length (actions_of {actor e} (e # t)) + |
5492 have "?R = length (actions_of {actor e} (e # t)) + |
5487 (\<Sum>th'\<in>A - {actor e}. length (actions_of {th'} (e # t)))" |
5493 (\<Sum>th'\<in>A - {actor e}. length (actions_of {th'} (e # t)))" |
5488 (is "_ = ?F (e#t) + ?G (e#t)") |
5494 (is "_ = ?F (e#t) + ?G (e#t)") |
5489 by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", |
5495 by (meson True assms sum.remove) |
5490 OF assms True], simp) |
|
5491 moreover have "?F (e#t) = 1 + ?F t" using True |
5496 moreover have "?F (e#t) = 1 + ?F t" using True |
5492 by (simp add:actions_of_def) |
5497 by (simp add:actions_of_def) |
5493 moreover have "?G (e#t) = ?G t" |
5498 moreover have "?G (e#t) = ?G t" |
5494 by (rule setsum.cong, auto simp:actions_of_def) |
5499 by (auto simp:actions_of_def) |
5495 moreover have "?F t + ?G t = ?T t" |
5500 moreover have "?F t + ?G t = ?T t" |
5496 by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", |
5501 by (metis (no_types, lifting) True assms sum.remove) |
5497 OF assms True], simp) |
5502 ultimately show ?thesis |
5498 ultimately show ?thesis by simp |
5503 by simp |
5499 qed |
5504 qed |
5500 ultimately show ?thesis by simp |
5505 ultimately show ?thesis by simp |
5501 next |
5506 next |
5502 case False |
5507 case False |
5503 hence "?L = length (actions_of A t)" |
5508 hence "?L = length (actions_of A t)" |
5504 by (simp add:actions_of_def) |
5509 by (simp add:actions_of_def) |
5505 also have "... = (\<Sum>th'\<in>A. length (actions_of {th'} t))" by (simp add: h) |
5510 also have "... = (\<Sum>th'\<in>A. length (actions_of {th'} t))" by (simp add: h) |
5506 also have "... = ?R" |
5511 also have "... = ?R" |
5507 by (rule setsum.cong; insert False, auto simp:actions_of_def) |
5512 unfolding actions_of_def |
|
5513 by (metis (no_types, lifting) False filter.simps(2) singletonD sum.cong) |
5508 finally show ?thesis . |
5514 finally show ?thesis . |
5509 qed |
5515 qed |
5510 qed (auto simp:actions_of_def) |
5516 qed (auto simp:actions_of_def) |
5511 |
5517 |
5512 lemma threads_Exit: |
5518 lemma threads_Exit: |