|
1 section {* |
|
2 This file contains lemmas used to guide the recalculation of current precedence |
|
3 after every system call (or system operation) |
|
4 *} |
|
5 theory CpsG |
|
6 imports PrioG Max RTree |
|
7 begin |
|
8 |
|
9 |
|
10 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" |
|
11 |
|
12 definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" |
|
13 |
|
14 definition "tRAG s = wRAG s O hRAG s" |
|
15 |
|
16 definition "pairself f = (\<lambda>(a, b). (f a, f b))" |
|
17 |
|
18 definition "rel_map f r = (pairself f ` r)" |
|
19 |
|
20 fun the_thread :: "node \<Rightarrow> thread" where |
|
21 "the_thread (Th th) = th" |
|
22 |
|
23 definition "tG s = rel_map the_thread (tRAG s)" |
|
24 |
|
25 locale pip = |
|
26 fixes s |
|
27 assumes vt: "vt s" |
|
28 |
|
29 |
|
30 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" |
|
31 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv |
|
32 s_holding_abv cs_RAG_def, auto) |
|
33 |
|
34 lemma relpow_mult: |
|
35 "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)" |
|
36 proof(induct n arbitrary:m) |
|
37 case (Suc k m) |
|
38 thus ?case (is "?L = ?R") |
|
39 proof - |
|
40 have h: "(m * k + m) = (m + m * k)" by auto |
|
41 show ?thesis |
|
42 apply (simp add:Suc relpow_add[symmetric]) |
|
43 by (unfold h, simp) |
|
44 qed |
|
45 qed simp |
|
46 |
|
47 lemma compose_relpow_2: |
|
48 assumes "r1 \<subseteq> r" |
|
49 and "r2 \<subseteq> r" |
|
50 shows "r1 O r2 \<subseteq> r ^^ (2::nat)" |
|
51 proof - |
|
52 { fix a b |
|
53 assume "(a, b) \<in> r1 O r2" |
|
54 then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2" |
|
55 by auto |
|
56 with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto |
|
57 hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto |
|
58 } thus ?thesis by (auto simp:numeral_2_eq_2) |
|
59 qed |
|
60 |
|
61 |
|
62 lemma acyclic_compose: |
|
63 assumes "acyclic r" |
|
64 and "r1 \<subseteq> r" |
|
65 and "r2 \<subseteq> r" |
|
66 shows "acyclic (r1 O r2)" |
|
67 proof - |
|
68 { fix a |
|
69 assume "(a, a) \<in> (r1 O r2)^+" |
|
70 from trancl_mono[OF this compose_relpow_2[OF assms(2, 3)]] |
|
71 have "(a, a) \<in> (r ^^ 2) ^+" . |
|
72 from trancl_power[THEN iffD1, OF this] |
|
73 obtain n where h: "(a, a) \<in> (r ^^ 2) ^^ n" "n > 0" by blast |
|
74 from this(1)[unfolded relpow_mult] have h2: "(a, a) \<in> r ^^ (2 * n)" . |
|
75 have "(a, a) \<in> r^+" |
|
76 proof(cases rule:trancl_power[THEN iffD2]) |
|
77 from h(2) h2 show "\<exists>n>0. (a, a) \<in> r ^^ n" |
|
78 by (rule_tac x = "2*n" in exI, auto) |
|
79 qed |
|
80 with assms have "False" by (auto simp:acyclic_def) |
|
81 } thus ?thesis by (auto simp:acyclic_def) |
|
82 qed |
|
83 |
|
84 lemma range_tRAG: "Range (tRAG s) \<subseteq> {Th th | th. True}" |
|
85 proof - |
|
86 have "Range (wRAG s O hRAG s) \<subseteq> {Th th |th. True}" (is "?L \<subseteq> ?R") |
|
87 proof - |
|
88 have "?L \<subseteq> Range (hRAG s)" by auto |
|
89 also have "... \<subseteq> ?R" |
|
90 by (unfold hRAG_def, auto) |
|
91 finally show ?thesis by auto |
|
92 qed |
|
93 thus ?thesis by (simp add:tRAG_def) |
|
94 qed |
|
95 |
|
96 lemma domain_tRAG: "Domain (tRAG s) \<subseteq> {Th th | th. True}" |
|
97 proof - |
|
98 have "Domain (wRAG s O hRAG s) \<subseteq> {Th th |th. True}" (is "?L \<subseteq> ?R") |
|
99 proof - |
|
100 have "?L \<subseteq> Domain (wRAG s)" by auto |
|
101 also have "... \<subseteq> ?R" |
|
102 by (unfold wRAG_def, auto) |
|
103 finally show ?thesis by auto |
|
104 qed |
|
105 thus ?thesis by (simp add:tRAG_def) |
|
106 qed |
|
107 |
|
108 lemma rel_mapE: |
|
109 assumes "(a, b) \<in> rel_map f r" |
|
110 obtains c d |
|
111 where "(c, d) \<in> r" "(a, b) = (f c, f d)" |
|
112 using assms |
|
113 by (unfold rel_map_def pairself_def, auto) |
|
114 |
|
115 lemma rel_mapI: |
|
116 assumes "(a, b) \<in> r" |
|
117 and "c = f a" |
|
118 and "d = f b" |
|
119 shows "(c, d) \<in> rel_map f r" |
|
120 using assms |
|
121 by (unfold rel_map_def pairself_def, auto) |
|
122 |
|
123 lemma map_appendE: |
|
124 assumes "map f zs = xs @ ys" |
|
125 obtains xs' ys' |
|
126 where "zs = xs' @ ys'" "xs = map f xs'" "ys = map f ys'" |
|
127 proof - |
|
128 have "\<exists> xs' ys'. zs = xs' @ ys' \<and> xs = map f xs' \<and> ys = map f ys'" |
|
129 using assms |
|
130 proof(induct xs arbitrary:zs ys) |
|
131 case (Nil zs ys) |
|
132 thus ?case by auto |
|
133 next |
|
134 case (Cons x xs zs ys) |
|
135 note h = this |
|
136 show ?case |
|
137 proof(cases zs) |
|
138 case (Cons e es) |
|
139 with h have eq_x: "map f es = xs @ ys" "x = f e" by auto |
|
140 from h(1)[OF this(1)] |
|
141 obtain xs' ys' where "es = xs' @ ys'" "xs = map f xs'" "ys = map f ys'" |
|
142 by blast |
|
143 with Cons eq_x |
|
144 have "zs = (e#xs') @ ys' \<and> x # xs = map f (e#xs') \<and> ys = map f ys'" by auto |
|
145 thus ?thesis by metis |
|
146 qed (insert h, auto) |
|
147 qed |
|
148 thus ?thesis by (auto intro!:that) |
|
149 qed |
|
150 |
|
151 lemma rel_map_mono: |
|
152 assumes "r1 \<subseteq> r2" |
|
153 shows "rel_map f r1 \<subseteq> rel_map f r2" |
|
154 using assms |
|
155 by (auto simp:rel_map_def pairself_def) |
|
156 |
|
157 lemma rel_map_compose [simp]: |
|
158 shows "rel_map f1 (rel_map f2 r) = rel_map (f1 o f2) r" |
|
159 by (auto simp:rel_map_def pairself_def) |
|
160 |
|
161 lemma edges_on_map: "edges_on (map f xs) = rel_map f (edges_on xs)" |
|
162 proof - |
|
163 { fix a b |
|
164 assume "(a, b) \<in> edges_on (map f xs)" |
|
165 then obtain l1 l2 where eq_map: "map f xs = l1 @ [a, b] @ l2" |
|
166 by (unfold edges_on_def, auto) |
|
167 hence "(a, b) \<in> rel_map f (edges_on xs)" |
|
168 by (auto elim!:map_appendE intro!:rel_mapI simp:edges_on_def) |
|
169 } moreover { |
|
170 fix a b |
|
171 assume "(a, b) \<in> rel_map f (edges_on xs)" |
|
172 then obtain c d where |
|
173 h: "(c, d) \<in> edges_on xs" "(a, b) = (f c, f d)" |
|
174 by (elim rel_mapE, auto) |
|
175 then obtain l1 l2 where |
|
176 eq_xs: "xs = l1 @ [c, d] @ l2" |
|
177 by (auto simp:edges_on_def) |
|
178 hence eq_map: "map f xs = map f l1 @ [f c, f d] @ map f l2" by auto |
|
179 have "(a, b) \<in> edges_on (map f xs)" |
|
180 proof - |
|
181 from h(2) have "[f c, f d] = [a, b]" by simp |
|
182 from eq_map[unfolded this] show ?thesis by (auto simp:edges_on_def) |
|
183 qed |
|
184 } ultimately show ?thesis by auto |
|
185 qed |
|
186 |
|
187 lemma plus_rpath: |
|
188 assumes "(a, b) \<in> r^+" |
|
189 obtains xs where "rpath r a xs b" "xs \<noteq> []" |
|
190 proof - |
|
191 from assms obtain m where h: "(a, m) \<in> r" "(m, b) \<in> r^*" |
|
192 by (auto dest!:tranclD) |
|
193 from star_rpath[OF this(2)] obtain xs where "rpath r m xs b" by auto |
|
194 from rstepI[OF h(1) this] have "rpath r a (m # xs) b" . |
|
195 from that[OF this] show ?thesis by auto |
|
196 qed |
|
197 |
|
198 lemma edges_on_unfold: |
|
199 "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R") |
|
200 proof - |
|
201 { fix c d |
|
202 assume "(c, d) \<in> ?L" |
|
203 then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2" |
|
204 by (auto simp:edges_on_def) |
|
205 have "(c, d) \<in> ?R" |
|
206 proof(cases "l1") |
|
207 case Nil |
|
208 with h have "(c, d) = (a, b)" by auto |
|
209 thus ?thesis by auto |
|
210 next |
|
211 case (Cons e es) |
|
212 from h[unfolded this] have "b#xs = es@[c, d]@l2" by auto |
|
213 thus ?thesis by (auto simp:edges_on_def) |
|
214 qed |
|
215 } moreover |
|
216 { fix c d |
|
217 assume "(c, d) \<in> ?R" |
|
218 moreover have "(a, b) \<in> ?L" |
|
219 proof - |
|
220 have "(a # b # xs) = []@[a,b]@xs" by simp |
|
221 hence "\<exists> l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto |
|
222 thus ?thesis by (unfold edges_on_def, simp) |
|
223 qed |
|
224 moreover { |
|
225 assume "(c, d) \<in> edges_on (b#xs)" |
|
226 then obtain l1 l2 where "b#xs = l1@[c, d]@l2" by (unfold edges_on_def, auto) |
|
227 hence "a#b#xs = (a#l1)@[c,d]@l2" by simp |
|
228 hence "\<exists> l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis |
|
229 hence "(c,d) \<in> ?L" by (unfold edges_on_def, simp) |
|
230 } |
|
231 ultimately have "(c, d) \<in> ?L" by auto |
|
232 } ultimately show ?thesis by auto |
|
233 qed |
|
234 |
|
235 lemma edges_on_rpathI: |
|
236 assumes "edges_on (a#xs@[b]) \<subseteq> r" |
|
237 shows "rpath r a (xs@[b]) b" |
|
238 using assms |
|
239 proof(induct xs arbitrary: a b) |
|
240 case Nil |
|
241 moreover have "(a, b) \<in> edges_on (a # [] @ [b])" |
|
242 by (unfold edges_on_def, auto) |
|
243 ultimately have "(a, b) \<in> r" by auto |
|
244 thus ?case by auto |
|
245 next |
|
246 case (Cons x xs a b) |
|
247 from this(2) have "edges_on (x # xs @ [b]) \<subseteq> r" by (simp add:edges_on_unfold) |
|
248 from Cons(1)[OF this] have " rpath r x (xs @ [b]) b" . |
|
249 moreover from Cons(2) have "(a, x) \<in> r" by (auto simp:edges_on_unfold) |
|
250 ultimately show ?case by (auto intro!:rstepI) |
|
251 qed |
|
252 |
|
253 lemma image_id: |
|
254 assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x" |
|
255 shows "f ` A = A" |
|
256 using assms by (auto simp:image_def) |
|
257 |
|
258 lemma rel_map_inv_id: |
|
259 assumes "inj_on f ((Domain r) \<union> (Range r))" |
|
260 shows "(rel_map (inv_into ((Domain r) \<union> (Range r)) f \<circ> f) r) = r" |
|
261 proof - |
|
262 let ?f = "(inv_into (Domain r \<union> Range r) f \<circ> f)" |
|
263 { |
|
264 fix a b |
|
265 assume h0: "(a, b) \<in> r" |
|
266 have "pairself ?f (a, b) = (a, b)" |
|
267 proof - |
|
268 from assms h0 have "?f a = a" by (auto intro:inv_into_f_f) |
|
269 moreover have "?f b = b" |
|
270 by (insert h0, simp, intro inv_into_f_f[OF assms], auto intro!:RangeI) |
|
271 ultimately show ?thesis by (auto simp:pairself_def) |
|
272 qed |
|
273 } thus ?thesis by (unfold rel_map_def, intro image_id, case_tac x, auto) |
|
274 qed |
|
275 |
|
276 lemma rel_map_acyclic: |
|
277 assumes "acyclic r" |
|
278 and "inj_on f ((Domain r) \<union> (Range r))" |
|
279 shows "acyclic (rel_map f r)" |
|
280 proof - |
|
281 let ?D = "Domain r \<union> Range r" |
|
282 { fix a |
|
283 assume "(a, a) \<in> (rel_map f r)^+" |
|
284 from plus_rpath[OF this] |
|
285 obtain xs where rp: "rpath (rel_map f r) a xs a" "xs \<noteq> []" by auto |
|
286 from rpath_nnl_lastE[OF this] obtain xs' where eq_xs: "xs = xs'@[a]" by auto |
|
287 from rpath_edges_on[OF rp(1)] |
|
288 have h: "edges_on (a # xs) \<subseteq> rel_map f r" . |
|
289 from edges_on_map[of "inv_into ?D f" "a#xs"] |
|
290 have "edges_on (map (inv_into ?D f) (a # xs)) = rel_map (inv_into ?D f) (edges_on (a # xs))" . |
|
291 with rel_map_mono[OF h, of "inv_into ?D f"] |
|
292 have "edges_on (map (inv_into ?D f) (a # xs)) \<subseteq> rel_map ((inv_into ?D f) o f) r" by simp |
|
293 from this[unfolded eq_xs] |
|
294 have subr: "edges_on (map (inv_into ?D f) (a # xs' @ [a])) \<subseteq> rel_map (inv_into ?D f \<circ> f) r" . |
|
295 have "(map (inv_into ?D f) (a # xs' @ [a])) = (inv_into ?D f a) # map (inv_into ?D f) xs' @ [inv_into ?D f a]" |
|
296 by simp |
|
297 from edges_on_rpathI[OF subr[unfolded this]] |
|
298 have "rpath (rel_map (inv_into ?D f \<circ> f) r) |
|
299 (inv_into ?D f a) (map (inv_into ?D f) xs' @ [inv_into ?D f a]) (inv_into ?D f a)" . |
|
300 hence "(inv_into ?D f a, inv_into ?D f a) \<in> (rel_map (inv_into ?D f \<circ> f) r)^+" |
|
301 by (rule rpath_plus, simp) |
|
302 moreover have "(rel_map (inv_into ?D f \<circ> f) r) = r" by (rule rel_map_inv_id[OF assms(2)]) |
|
303 moreover note assms(1) |
|
304 ultimately have False by (unfold acyclic_def, auto) |
|
305 } thus ?thesis by (auto simp:acyclic_def) |
|
306 qed |
|
307 |
|
308 context pip |
|
309 begin |
|
310 |
|
311 interpretation rtree_RAG: rtree "RAG s" |
|
312 proof |
|
313 show "single_valued (RAG s)" |
|
314 by (unfold single_valued_def, auto intro: unique_RAG[OF vt]) |
|
315 |
|
316 show "acyclic (RAG s)" |
|
317 by (rule acyclic_RAG[OF vt]) |
|
318 qed |
|
319 |
|
320 lemma sgv_wRAG: |
|
321 shows "single_valued (wRAG s)" |
|
322 using waiting_unique[OF vt] |
|
323 by (unfold single_valued_def wRAG_def, auto) |
|
324 |
|
325 lemma sgv_hRAG: |
|
326 shows "single_valued (hRAG s)" |
|
327 using held_unique |
|
328 by (unfold single_valued_def hRAG_def, auto) |
|
329 |
|
330 lemma sgv_tRAG: shows "single_valued (tRAG s)" |
|
331 by (unfold tRAG_def, rule Relation.single_valued_relcomp, |
|
332 insert sgv_hRAG sgv_wRAG, auto) |
|
333 |
|
334 lemma acyclic_hRAG: |
|
335 shows "acyclic (hRAG s)" |
|
336 by (rule acyclic_subset[OF acyclic_RAG[OF vt]], insert RAG_split, auto) |
|
337 |
|
338 lemma acyclic_wRAG: |
|
339 shows "acyclic (wRAG s)" |
|
340 by (rule acyclic_subset[OF acyclic_RAG[OF vt]], insert RAG_split, auto) |
|
341 |
|
342 lemma acyclic_tRAG: |
|
343 shows "acyclic (tRAG s)" |
|
344 by (unfold tRAG_def, rule acyclic_compose[OF acyclic_RAG[OF vt]], |
|
345 unfold RAG_split, auto) |
|
346 |
|
347 lemma acyclic_tG: |
|
348 shows "acyclic (tG s)" |
|
349 proof(unfold tG_def, rule rel_map_acyclic[OF acyclic_tRAG]) |
|
350 show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))" |
|
351 proof(rule subset_inj_on) |
|
352 show " inj_on the_thread {Th th |th. True}" by (unfold inj_on_def, auto) |
|
353 next |
|
354 from domain_tRAG range_tRAG |
|
355 show " Domain (tRAG s) \<union> Range (tRAG s) \<subseteq> {Th th |th. True}" by auto |
|
356 qed |
|
357 qed |
|
358 |
|
359 end |