81 have "?R = Max (insert y A)" by simp |
81 have "?R = Max (insert y A)" by simp |
82 also from assms have "... = ?L" |
82 also from assms have "... = ?L" |
83 by (subst Max.insert, simp+) |
83 by (subst Max.insert, simp+) |
84 finally show ?thesis by simp |
84 finally show ?thesis by simp |
85 qed |
85 qed |
|
86 |
|
87 lemma birth_time_lt: |
|
88 assumes "s \<noteq> []" |
|
89 shows "last_set th s < length s" |
|
90 using assms |
|
91 proof(induct s) |
|
92 case (Cons a s) |
|
93 show ?case |
|
94 proof(cases "s \<noteq> []") |
|
95 case False |
|
96 thus ?thesis |
|
97 by (cases a, auto) |
|
98 next |
|
99 case True |
|
100 show ?thesis using Cons(1)[OF True] |
|
101 by (cases a, auto) |
|
102 qed |
|
103 qed simp |
|
104 |
|
105 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []" |
|
106 by (induct s, auto) |
|
107 |
|
108 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s" |
|
109 by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt) |
86 |
110 |
87 lemma eq_RAG: |
111 lemma eq_RAG: |
88 "RAG (wq s) = RAG s" |
112 "RAG (wq s) = RAG s" |
89 by (unfold cs_RAG_def s_RAG_def, auto) |
113 by (unfold cs_RAG_def s_RAG_def, auto) |
90 |
114 |
2243 simp add: finite_threads, |
2267 simp add: finite_threads, |
2244 simp add: le_cp the_preced_def) |
2268 simp add: le_cp the_preced_def) |
2245 ultimately show ?thesis by auto |
2269 ultimately show ?thesis by auto |
2246 qed |
2270 qed |
2247 |
2271 |
2248 lemma max_cp_eq_the_preced: |
|
2249 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" |
|
2250 using max_cp_eq using the_preced_def by presburger |
|
2251 |
|
2252 lemma wf_RAG_converse: |
2272 lemma wf_RAG_converse: |
2253 shows "wf ((RAG s)^-1)" |
2273 shows "wf ((RAG s)^-1)" |
2254 proof(rule finite_acyclic_wf_converse) |
2274 proof(rule finite_acyclic_wf_converse) |
2255 from finite_RAG |
2275 from finite_RAG |
2256 show "finite (RAG s)" . |
2276 show "finite (RAG s)" . |
4442 assumes nt1: "next_th s th cs th1" |
4462 assumes nt1: "next_th s th cs th1" |
4443 and nt2: "next_th s th cs th2" |
4463 and nt2: "next_th s th cs th2" |
4444 shows "th1 = th2" |
4464 shows "th1 = th2" |
4445 using assms by (unfold next_th_def, auto) |
4465 using assms by (unfold next_th_def, auto) |
4446 |
4466 |
|
4467 context valid_trace |
|
4468 begin |
|
4469 |
|
4470 thm th_chain_to_ready |
|
4471 |
|
4472 find_theorems subtree Th RAG |
|
4473 |
|
4474 lemma threads_alt_def: |
|
4475 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
4476 (is "?L = ?R") |
|
4477 proof - |
|
4478 { fix th1 |
|
4479 assume "th1 \<in> ?L" |
|
4480 from th_chain_to_ready[OF this] |
|
4481 have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" . |
|
4482 hence "th1 \<in> ?R" by (auto simp:subtree_def) |
|
4483 } moreover |
|
4484 { fix th' |
|
4485 assume "th' \<in> ?R" |
|
4486 then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)" |
|
4487 by auto |
|
4488 from this(2) |
|
4489 have "th' \<in> ?L" |
|
4490 proof(cases rule:subtreeE) |
|
4491 case 1 |
|
4492 with h(1) show ?thesis by (auto simp:readys_def) |
|
4493 next |
|
4494 case 2 |
|
4495 from tranclD[OF this(2)[unfolded ancestors_def, simplified]] |
|
4496 have "Th th' \<in> Domain (RAG s)" by auto |
|
4497 from dm_RAG_threads[OF this] |
|
4498 show ?thesis . |
|
4499 qed |
|
4500 } ultimately show ?thesis by auto |
|
4501 qed |
|
4502 |
|
4503 lemma finite_readys [simp]: "finite (readys s)" |
|
4504 using finite_threads readys_threads rev_finite_subset by blast |
|
4505 |
|
4506 text {* (* ccc *) \noindent |
|
4507 Since the current precedence of the threads in ready queue will always be boosted, |
|
4508 there must be one inside it has the maximum precedence of the whole system. |
|
4509 *} |
|
4510 lemma max_cp_readys_threads: |
|
4511 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") |
|
4512 proof(cases "readys s = {}") |
|
4513 case False |
|
4514 have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp) |
|
4515 also have "... = |
|
4516 Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
|
4517 by (unfold threads_alt_def, simp) |
|
4518 also have "... = |
|
4519 Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
|
4520 by (unfold image_UN, simp) |
|
4521 also have "... = |
|
4522 Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" |
|
4523 proof(rule Max_UNION) |
|
4524 show "\<forall>M\<in>(\<lambda>x. the_preced s ` |
|
4525 {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M" |
|
4526 using finite_subtree_threads by auto |
|
4527 qed (auto simp:False subtree_def) |
|
4528 also have "... = |
|
4529 Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" |
|
4530 by (unfold image_comp, simp) |
|
4531 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") |
|
4532 proof - |
|
4533 have "(?f ` ?A) = (?g ` ?A)" |
|
4534 proof(rule f_image_eq) |
|
4535 fix th1 |
|
4536 assume "th1 \<in> ?A" |
|
4537 thus "?f th1 = ?g th1" |
|
4538 by (unfold cp_alt_def, simp) |
|
4539 qed |
|
4540 thus ?thesis by simp |
|
4541 qed |
|
4542 finally show ?thesis by simp |
|
4543 qed (auto simp:threads_alt_def) |
|
4544 |
4447 end |
4545 end |
4448 |
4546 |
|
4547 end |
|
4548 |