1 theory Implementation |
1 theory Implementation |
2 imports PIPBasics |
2 imports PIPBasics |
3 begin |
3 begin |
|
4 |
|
5 |
|
6 context valid_trace |
|
7 begin |
|
8 |
|
9 lemma readys_root: |
|
10 assumes "th \<in> readys s" |
|
11 shows "root (RAG s) (Th th)" |
|
12 proof - |
|
13 { fix x |
|
14 assume "x \<in> ancestors (RAG s) (Th th)" |
|
15 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
16 from tranclD[OF this] |
|
17 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
18 with assms(1) have False |
|
19 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
20 by (fold wq_def, blast) |
|
21 } thus ?thesis by (unfold root_def, auto) |
|
22 qed |
|
23 |
|
24 lemma readys_in_no_subtree: |
|
25 assumes "th \<in> readys s" |
|
26 and "th' \<noteq> th" |
|
27 shows "Th th \<notin> subtree (RAG s) (Th th')" |
|
28 proof |
|
29 assume "Th th \<in> subtree (RAG s) (Th th')" |
|
30 thus False |
|
31 proof(cases rule:subtreeE) |
|
32 case 1 |
|
33 with assms show ?thesis by auto |
|
34 next |
|
35 case 2 |
|
36 with readys_root[OF assms(1)] |
|
37 show ?thesis by (auto simp:root_def) |
|
38 qed |
|
39 qed |
|
40 |
|
41 end |
4 |
42 |
5 section {* |
43 section {* |
6 This file contains lemmas used to guide the recalculation of current precedence |
44 This file contains lemmas used to guide the recalculation of current precedence |
7 after every system call (or system operation) |
45 after every system call (or system operation) |
8 *} |
46 *} |
9 |
|
10 section {* Recursive calculation of @{term "cp"} *} |
|
11 |
|
12 definition "cp_gen s x = |
|
13 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
|
14 |
|
15 lemma cp_gen_alt_def: |
|
16 "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" |
|
17 by (auto simp:cp_gen_def) |
|
18 |
|
19 lemma cp_gen_def_cond: |
|
20 assumes "x = Th th" |
|
21 shows "cp s th = cp_gen s (Th th)" |
|
22 by (unfold cp_alt_def1 cp_gen_def, simp) |
|
23 |
|
24 lemma cp_gen_over_set: |
|
25 assumes "\<forall> x \<in> A. \<exists> th. x = Th th" |
|
26 shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A" |
|
27 proof(rule f_image_eq) |
|
28 fix a |
|
29 assume "a \<in> A" |
|
30 from assms[rule_format, OF this] |
|
31 obtain th where eq_a: "a = Th th" by auto |
|
32 show "cp_gen s a = (cp s \<circ> the_thread) a" |
|
33 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
|
34 qed |
|
35 |
|
36 |
|
37 context valid_trace |
|
38 begin |
|
39 (* ddd *) |
|
40 lemma cp_gen_rec: |
|
41 assumes "x = Th th" |
|
42 shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)" |
|
43 proof(cases "children (tRAG s) x = {}") |
|
44 case True |
|
45 show ?thesis |
|
46 by (unfold True cp_gen_def subtree_children, simp add:assms) |
|
47 next |
|
48 case False |
|
49 hence [simp]: "children (tRAG s) x \<noteq> {}" by auto |
|
50 note fsbttRAGs.finite_subtree[simp] |
|
51 have [simp]: "finite (children (tRAG s) x)" |
|
52 by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], |
|
53 rule children_subtree) |
|
54 { fix r x |
|
55 have "subtree r x \<noteq> {}" by (auto simp:subtree_def) |
|
56 } note this[simp] |
|
57 have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}" |
|
58 proof - |
|
59 from False obtain q where "q \<in> children (tRAG s) x" by blast |
|
60 moreover have "subtree (tRAG s) q \<noteq> {}" by simp |
|
61 ultimately show ?thesis by blast |
|
62 qed |
|
63 have h: "Max ((the_preced s \<circ> the_thread) ` |
|
64 ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) = |
|
65 Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)" |
|
66 (is "?L = ?R") |
|
67 proof - |
|
68 let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L |
|
69 let "Max (_ \<union> (?h ` ?B))" = ?R |
|
70 let ?L1 = "?f ` \<Union>(?g ` ?B)" |
|
71 have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" |
|
72 proof - |
|
73 have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp |
|
74 also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto |
|
75 finally have "Max ?L1 = Max ..." by simp |
|
76 also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)" |
|
77 by (subst Max_UNION, simp+) |
|
78 also have "... = Max (cp_gen s ` children (tRAG s) x)" |
|
79 by (unfold image_comp cp_gen_alt_def, simp) |
|
80 finally show ?thesis . |
|
81 qed |
|
82 show ?thesis |
|
83 proof - |
|
84 have "?L = Max (?f ` ?A \<union> ?L1)" by simp |
|
85 also have "... = max (the_preced s (the_thread x)) (Max ?L1)" |
|
86 by (subst Max_Un, simp+) |
|
87 also have "... = max (?f x) (Max (?h ` ?B))" |
|
88 by (unfold eq_Max_L1, simp) |
|
89 also have "... =?R" |
|
90 by (rule max_Max_eq, (simp)+, unfold assms, simp) |
|
91 finally show ?thesis . |
|
92 qed |
|
93 qed thus ?thesis |
|
94 by (fold h subtree_children, unfold cp_gen_def, simp) |
|
95 qed |
|
96 |
|
97 lemma cp_rec: |
|
98 "cp s th = Max ({the_preced s th} \<union> |
|
99 (cp s o the_thread) ` children (tRAG s) (Th th))" |
|
100 proof - |
|
101 have "Th th = Th th" by simp |
|
102 note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] |
|
103 show ?thesis |
|
104 proof - |
|
105 have "cp_gen s ` children (tRAG s) (Th th) = |
|
106 (cp s \<circ> the_thread) ` children (tRAG s) (Th th)" |
|
107 proof(rule cp_gen_over_set) |
|
108 show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th" |
|
109 by (unfold tRAG_alt_def, auto simp:children_def) |
|
110 qed |
|
111 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
|
112 qed |
|
113 qed |
|
114 |
|
115 end |
|
116 |
47 |
117 text {* (* ddd *) |
48 text {* (* ddd *) |
118 One beauty of our modelling is that we follow the definitional extension tradition of HOL. |
49 One beauty of our modelling is that we follow the definitional extension tradition of HOL. |
119 The benefit of such a concise and miniature model is that large number of intuitively |
50 The benefit of such a concise and miniature model is that large number of intuitively |
120 obvious facts are derived as lemmas, rather than asserted as axioms. |
51 obvious facts are derived as lemmas, rather than asserted as axioms. |