1 theory Implementation |
1 theory Implementation |
2 imports PIPBasics |
2 imports PIPBasics |
3 begin |
3 begin |
4 |
4 |
5 section {* |
5 text {* |
6 This file contains lemmas used to guide the recalculation of current precedence |
6 |
7 after every step of execution (or system operation, or event), |
7 This file contains lemmas used to guide the recalculation of current |
|
8 precedence after every step of execution (or system operation, or event), |
8 which is the most tricky part in the implementation of PIP. |
9 which is the most tricky part in the implementation of PIP. |
9 |
10 |
10 Following convention, lemmas are grouped into locales corresponding to |
11 Following convention, lemmas are grouped into locales corresponding to |
11 system operations, each explained in a separate section. |
12 system operations, each explained in a separate section. *} |
12 *} |
|
13 |
13 |
14 text {* |
14 text {* |
15 The following two lemmas are general about any valid system state, |
15 The following two lemmas are general about any valid system state, |
16 but are used in the derivation in more specific system operations. |
16 but are used in the derivation in more specific system operations. |
17 *} |
17 *} |
20 begin |
20 begin |
21 |
21 |
22 lemma readys_root: |
22 lemma readys_root: |
23 assumes "th \<in> readys s" |
23 assumes "th \<in> readys s" |
24 shows "root (RAG s) (Th th)" |
24 shows "root (RAG s) (Th th)" |
25 proof - |
25 unfolding root_def ancestors_def |
26 { fix x |
26 using readys_RAG assms |
27 assume "x \<in> ancestors (RAG s) (Th th)" |
27 by (metis Collect_empty_eq Domain.DomainI trancl_domain) |
28 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
29 from tranclD[OF this] |
|
30 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
31 with assms(1) have False |
|
32 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw) |
|
33 by (fold wq_def, blast) |
|
34 } thus ?thesis by (unfold root_def, auto) |
|
35 qed |
|
36 |
28 |
37 lemma readys_in_no_subtree: |
29 lemma readys_in_no_subtree: |
38 assumes "th \<in> readys s" |
30 assumes "th \<in> readys s" |
39 and "th' \<noteq> th" |
31 and "th' \<noteq> th" |
40 shows "Th th \<notin> subtree (RAG s) (Th th')" |
32 shows "Th th \<notin> subtree (RAG s) (Th th')" |
666 lemma th_RAG: "Th th \<notin> Field (RAG s)" |
658 lemma th_RAG: "Th th \<notin> Field (RAG s)" |
667 proof - |
659 proof - |
668 have "Th th \<notin> Range (RAG s)" |
660 have "Th th \<notin> Range (RAG s)" |
669 proof |
661 proof |
670 assume "Th th \<in> Range (RAG s)" |
662 assume "Th th \<in> Range (RAG s)" |
671 then obtain cs where "holding_raw (wq s) th cs" |
663 then obtain cs where "holding s th cs" |
672 by (unfold Range_iff s_RAG_def, auto) |
664 by (simp add: holdents_RAG holdents_th_s) |
673 with holdents_th_s[unfolded holdents_def] |
665 then show False by (unfold holding_eq, auto) |
674 show False by (unfold holding_eq, auto) |
|
675 qed |
666 qed |
676 moreover have "Th th \<notin> Domain (RAG s)" |
667 moreover have "Th th \<notin> Domain (RAG s)" |
677 proof |
668 proof |
678 assume "Th th \<in> Domain (RAG s)" |
669 assume "Th th \<in> Domain (RAG s)" |
679 then obtain cs where "waiting_raw (wq s) th cs" |
670 then obtain cs where "waiting s th cs" |
680 by (unfold Domain_iff s_RAG_def, auto) |
671 by (simp add: readys_RAG) |
681 with th_ready_s show False by (unfold readys_def waiting_eq, auto) |
672 then show False |
|
673 using RAG_es \<open>Th th \<in> Domain (RAG s)\<close> |
|
674 th_not_live_es valid_trace.dm_RAG_threads vat_es.valid_trace_axioms by blast |
682 qed |
675 qed |
683 ultimately show ?thesis by (auto simp:Field_def) |
676 ultimately show ?thesis by (auto simp:Field_def) |
684 qed |
677 qed |
685 |
678 |
686 lemma th_tRAG: "(Th th) \<notin> Field (tRAG s)" |
679 lemma th_tRAG: "(Th th) \<notin> Field (tRAG s)" |