20 treated in a separate locale. |
20 treated in a separate locale. |
21 |
21 |
22 The complication of current precedence recalculation comes |
22 The complication of current precedence recalculation comes |
23 because the changing of RAG needs to be taken into account, |
23 because the changing of RAG needs to be taken into account, |
24 in addition to the changing of precedence. |
24 in addition to the changing of precedence. |
|
25 |
25 The reason RAG changing affects current precedence is that, |
26 The reason RAG changing affects current precedence is that, |
26 according to the definition, current precedence |
27 according to the definition, current precedence |
27 of a thread is the maximum of the precedences of its dependants, |
28 of a thread is the maximum of the precedences of every threads in its subtree, |
28 where the dependants are defined in terms of RAG. |
29 where the notion of sub-tree in RAG is defined in RTree.thy. |
29 |
30 |
30 Therefore, each operation, lemmas concerning the change of the precedences |
31 Therefore, for each operation, lemmas about the change of precedences |
31 and RAG are derived first, so that the lemmas about |
32 and RAG are derived first, on which lemmas about current precedence |
32 current precedence recalculation can be based on. |
33 recalculation are based on. |
33 *} |
34 *} |
|
35 |
|
36 section {* The @{term Set} operation *} |
34 |
37 |
35 text {* (* ddd *) |
38 text {* (* ddd *) |
36 The following locale @{text "step_set_cps"} investigates the recalculation |
39 The following locale @{text "step_set_cps"} investigates the recalculation |
37 after the @{text "Set"} operation. |
40 after the @{text "Set"} operation. |
38 *} |
41 *} |
57 |
60 |
58 context step_set_cps |
61 context step_set_cps |
59 begin |
62 begin |
60 |
63 |
61 text {* (* ddd *) |
64 text {* (* ddd *) |
62 The following two lemmas confirm that @{text "Set"}-operating only changes the precedence |
65 The following two lemmas confirm that @{text "Set"}-operation |
63 of the initiating thread. |
66 only changes the precedence of the initiating thread (or actor) |
|
67 of the operation (or event). |
64 *} |
68 *} |
65 |
69 |
66 lemma eq_preced: |
70 lemma eq_preced: |
67 assumes "th' \<noteq> th" |
71 assumes "th' \<noteq> th" |
68 shows "preced th' s = preced th' s'" |
72 shows "preced th' s = preced th' s'" |
70 from assms show ?thesis |
74 from assms show ?thesis |
71 by (unfold s_def, auto simp:preced_def) |
75 by (unfold s_def, auto simp:preced_def) |
72 qed |
76 qed |
73 |
77 |
74 lemma eq_the_preced: |
78 lemma eq_the_preced: |
75 fixes th' |
|
76 assumes "th' \<noteq> th" |
79 assumes "th' \<noteq> th" |
77 shows "the_preced s th' = the_preced s' th'" |
80 shows "the_preced s th' = the_preced s' th'" |
78 using assms |
81 using assms |
79 by (unfold the_preced_def, intro eq_preced, simp) |
82 by (unfold the_preced_def, intro eq_preced, simp) |
80 |
83 |
84 |
87 |
85 lemma eq_dep: "RAG s = RAG s'" |
88 lemma eq_dep: "RAG s = RAG s'" |
86 by (unfold s_def RAG_set_unchanged, auto) |
89 by (unfold s_def RAG_set_unchanged, auto) |
87 |
90 |
88 text {* (* ddd *) |
91 text {* (* ddd *) |
89 Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"} |
92 Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"} |
90 only affects those threads, which as @{text "Th th"} in their sub-trees. |
93 only affects those threads, which as @{text "Th th"} in their sub-trees. |
91 |
94 |
92 The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. |
95 The proof of this lemma is simplified by using the alternative definition |
|
96 of @{text "cp"}. |
93 *} |
97 *} |
94 |
98 |
95 lemma eq_cp_pre: |
99 lemma eq_cp_pre: |
96 fixes th' |
|
97 assumes nd: "Th th \<notin> subtree (RAG s') (Th th')" |
100 assumes nd: "Th th \<notin> subtree (RAG s') (Th th')" |
98 shows "cp s th' = cp s' th'" |
101 shows "cp s th' = cp s' th'" |
99 proof - |
102 proof - |
100 -- {* After unfolding using the alternative definition, elements |
103 -- {* After unfolding using the alternative definition, elements |
101 affecting the @{term "cp"}-value of threads become explicit. |
104 affecting the @{term "cp"}-value of threads become explicit. |
145 By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, |
148 By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, |
146 it is obvious that the change of priority only affects the @{text "cp"}-value |
149 it is obvious that the change of priority only affects the @{text "cp"}-value |
147 of the initiating thread @{text "th"}. |
150 of the initiating thread @{text "th"}. |
148 *} |
151 *} |
149 lemma eq_cp: |
152 lemma eq_cp: |
150 fixes th' |
|
151 assumes "th' \<noteq> th" |
153 assumes "th' \<noteq> th" |
152 shows "cp s th' = cp s' th'" |
154 shows "cp s th' = cp s' th'" |
153 by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) |
155 by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) |
154 |
156 |
155 end |
157 end |
|
158 |
|
159 section {* The @{term V} operation *} |
156 |
160 |
157 text {* |
161 text {* |
158 The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. |
162 The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. |
159 *} |
163 *} |
160 |
164 |
299 proof - |
303 proof - |
300 from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] |
304 from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] |
301 and nt show ?thesis by (auto intro:next_th_unique) |
305 and nt show ?thesis by (auto intro:next_th_unique) |
302 qed |
306 qed |
303 |
307 |
304 lemma subtree_kept: |
308 lemma subtree_kept: (* ddd *) |
305 assumes "th1 \<notin> {th, th'}" |
309 assumes "th1 \<notin> {th, th'}" |
306 shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") |
310 shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") |
307 proof - |
311 proof - |
308 let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})" |
312 let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})" |
309 let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}" |
313 let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}" |
427 lemma cp_kept_2: |
431 lemma cp_kept_2: |
428 shows "cp s th = cp s' th" |
432 shows "cp s th = cp s' th" |
429 by (unfold cp_alt_def subtree_th preced_kept, auto) |
433 by (unfold cp_alt_def subtree_th preced_kept, auto) |
430 |
434 |
431 lemma eq_cp: |
435 lemma eq_cp: |
432 fixes th' |
|
433 shows "cp s th' = cp s' th'" |
436 shows "cp s th' = cp s' th'" |
434 using cp_kept_1 cp_kept_2 |
437 using cp_kept_1 cp_kept_2 |
435 by (cases "th' = th", auto) |
438 by (cases "th' = th", auto) |
436 end |
439 end |
437 |
440 |