4 *} |
4 *} |
5 theory CpsG |
5 theory CpsG |
6 imports PrioG Max RTree |
6 imports PrioG Max RTree |
7 begin |
7 begin |
8 |
8 |
9 locale pip = |
9 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" |
10 fixes s |
10 |
11 assumes vt: "vt s" |
11 definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" |
12 |
12 |
13 context pip |
13 definition "tRAG s = wRAG s O hRAG s" |
14 begin |
14 |
15 |
15 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" |
16 interpretation rtree_RAG: rtree "RAG s" |
16 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv |
|
17 s_holding_abv cs_RAG_def, auto) |
|
18 |
|
19 lemma tRAG_alt_def: |
|
20 "tRAG s = {(Th th1, Th th2) | th1 th2. |
|
21 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" |
|
22 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
|
23 |
|
24 lemma tRAG_mono: |
|
25 assumes "RAG s' \<subseteq> RAG s" |
|
26 shows "tRAG s' \<subseteq> tRAG s" |
|
27 using assms |
|
28 by (unfold tRAG_alt_def, auto) |
|
29 |
|
30 lemma holding_next_thI: |
|
31 assumes "holding s th cs" |
|
32 and "length (wq s cs) > 1" |
|
33 obtains th' where "next_th s th cs th'" |
|
34 proof - |
|
35 from assms(1)[folded eq_holding, unfolded cs_holding_def] |
|
36 have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" . |
|
37 then obtain rest where h1: "wq s cs = th#rest" |
|
38 by (cases "wq s cs", auto) |
|
39 with assms(2) have h2: "rest \<noteq> []" by auto |
|
40 let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" |
|
41 have "next_th s th cs ?th'" using h1(1) h2 |
|
42 by (unfold next_th_def, auto) |
|
43 from that[OF this] show ?thesis . |
|
44 qed |
|
45 |
|
46 lemma RAG_tRAG_transfer: |
|
47 assumes "vt s'" |
|
48 assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
|
49 and "(Cs cs, Th th'') \<in> RAG s'" |
|
50 shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R") |
|
51 proof - |
|
52 interpret rtree: rtree "RAG s'" |
|
53 proof |
|
54 show "single_valued (RAG s')" |
|
55 apply (intro_locales) |
|
56 by (unfold single_valued_def, |
|
57 auto intro:unique_RAG[OF assms(1)]) |
|
58 |
|
59 show "acyclic (RAG s')" |
|
60 by (rule acyclic_RAG[OF assms(1)]) |
|
61 qed |
|
62 { fix n1 n2 |
|
63 assume "(n1, n2) \<in> ?L" |
|
64 from this[unfolded tRAG_alt_def] |
|
65 obtain th1 th2 cs' where |
|
66 h: "n1 = Th th1" "n2 = Th th2" |
|
67 "(Th th1, Cs cs') \<in> RAG s" |
|
68 "(Cs cs', Th th2) \<in> RAG s" by auto |
|
69 from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto |
|
70 from h(3) and assms(2) |
|
71 have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> |
|
72 (Th th1, Cs cs') \<in> RAG s'" by auto |
|
73 hence "(n1, n2) \<in> ?R" |
|
74 proof |
|
75 assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" |
|
76 hence eq_th1: "th1 = th" by simp |
|
77 moreover have "th2 = th''" |
|
78 proof - |
|
79 from h1 have "cs' = cs" by simp |
|
80 from assms(3) cs_in[unfolded this] rtree.sgv |
|
81 show ?thesis |
|
82 by (unfold single_valued_def, auto) |
|
83 qed |
|
84 ultimately show ?thesis using h(1,2) by auto |
|
85 next |
|
86 assume "(Th th1, Cs cs') \<in> RAG s'" |
|
87 with cs_in have "(Th th1, Th th2) \<in> tRAG s'" |
|
88 by (unfold tRAG_alt_def, auto) |
|
89 from this[folded h(1, 2)] show ?thesis by auto |
|
90 qed |
|
91 } moreover { |
|
92 fix n1 n2 |
|
93 assume "(n1, n2) \<in> ?R" |
|
94 hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto |
|
95 hence "(n1, n2) \<in> ?L" |
|
96 proof |
|
97 assume "(n1, n2) \<in> tRAG s'" |
|
98 moreover have "... \<subseteq> ?L" |
|
99 proof(rule tRAG_mono) |
|
100 show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto) |
|
101 qed |
|
102 ultimately show ?thesis by auto |
|
103 next |
|
104 assume eq_n: "(n1, n2) = (Th th, Th th'')" |
|
105 from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto |
|
106 moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto |
|
107 ultimately show ?thesis |
|
108 by (unfold eq_n tRAG_alt_def, auto) |
|
109 qed |
|
110 } ultimately show ?thesis by auto |
|
111 qed |
|
112 |
|
113 lemma readys_root: |
|
114 assumes "vt s" |
|
115 and "th \<in> readys s" |
|
116 shows "root (RAG s) (Th th)" |
|
117 proof - |
|
118 { fix x |
|
119 assume "x \<in> ancestors (RAG s) (Th th)" |
|
120 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
121 from tranclD[OF this] |
|
122 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
123 with assms(2) have False |
|
124 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
125 by (fold wq_def, blast) |
|
126 } thus ?thesis by (unfold root_def, auto) |
|
127 qed |
|
128 |
|
129 lemma readys_in_no_subtree: |
|
130 assumes "vt s" |
|
131 and "th \<in> readys s" |
|
132 and "th' \<noteq> th" |
|
133 shows "Th th \<notin> subtree (RAG s) (Th th')" |
17 proof |
134 proof |
18 show "single_valued (RAG s)" |
135 assume "Th th \<in> subtree (RAG s) (Th th')" |
19 by (unfold single_valued_def, auto intro: unique_RAG[OF vt]) |
136 thus False |
20 |
137 proof(cases rule:subtreeE) |
21 show "acyclic (RAG s)" |
138 case 1 |
22 by (rule acyclic_RAG[OF vt]) |
139 with assms show ?thesis by auto |
23 qed |
140 next |
24 |
141 case 2 |
25 thm rtree_RAG.rpath_overlap_oneside |
142 with readys_root[OF assms(1,2)] |
26 |
143 show ?thesis by (auto simp:root_def) |
27 end |
144 qed |
28 |
145 qed |
29 |
146 |
|
147 lemma image_id: |
|
148 assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x" |
|
149 shows "f ` A = A" |
|
150 using assms by (auto simp:image_def) |
30 |
151 |
31 definition "the_preced s th = preced th s" |
152 definition "the_preced s th = preced th s" |
32 |
153 |
33 lemma cp_alt_def: |
154 lemma cp_alt_def: |
34 "cp s th = |
155 "cp s th = |
43 thus ?thesis by simp |
164 thus ?thesis by simp |
44 qed |
165 qed |
45 thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) |
166 thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) |
46 qed |
167 qed |
47 |
168 |
|
169 fun the_thread :: "node \<Rightarrow> thread" where |
|
170 "the_thread (Th th) = th" |
|
171 |
|
172 definition "cp_gen s x = |
|
173 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
|
174 |
|
175 lemma cp_gen_alt_def: |
|
176 "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" |
|
177 by (auto simp:cp_gen_def) |
|
178 |
|
179 lemma tRAG_nodeE: |
|
180 assumes "(n1, n2) \<in> tRAG s" |
|
181 obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" |
|
182 using assms |
|
183 by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) |
|
184 |
|
185 lemma subtree_nodeE: |
|
186 assumes "n \<in> subtree (tRAG s) (Th th)" |
|
187 obtains th1 where "n = Th th1" |
|
188 proof - |
|
189 show ?thesis |
|
190 proof(rule subtreeE[OF assms]) |
|
191 assume "n = Th th" |
|
192 from that[OF this] show ?thesis . |
|
193 next |
|
194 assume "Th th \<in> ancestors (tRAG s) n" |
|
195 hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
|
196 hence "\<exists> th1. n = Th th1" |
|
197 proof(induct) |
|
198 case (base y) |
|
199 from tRAG_nodeE[OF this] show ?case by metis |
|
200 next |
|
201 case (step y z) |
|
202 thus ?case by auto |
|
203 qed |
|
204 with that show ?thesis by auto |
|
205 qed |
|
206 qed |
|
207 |
|
208 lemma threads_set_eq: |
|
209 "the_thread ` (subtree (tRAG s) (Th th)) = |
|
210 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") |
|
211 proof - |
|
212 { fix th' |
|
213 assume "th' \<in> ?L" |
|
214 then obtain n where h: "th' = the_thread n" "n \<in> subtree (tRAG s) (Th th)" by auto |
|
215 from subtree_nodeE[OF this(2)] |
|
216 obtain th1 where "n = Th th1" by auto |
|
217 with h have "Th th' \<in> subtree (tRAG s) (Th th)" by auto |
|
218 hence "Th th' \<in> subtree (RAG s) (Th th)" |
|
219 proof(cases rule:subtreeE[consumes 1]) |
|
220 case 1 |
|
221 thus ?thesis by (auto simp:subtree_def) |
|
222 next |
|
223 case 2 |
|
224 hence "(Th th', Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
|
225 thus ?thesis |
|
226 proof(induct) |
|
227 case (step y z) |
|
228 from this(2)[unfolded tRAG_alt_def] |
|
229 obtain u where |
|
230 h: "(y, u) \<in> RAG s" "(u, z) \<in> RAG s" |
|
231 by auto |
|
232 hence "y \<in> subtree (RAG s) z" by (auto simp:subtree_def) |
|
233 with step(3) |
|
234 show ?case by (auto simp:subtree_def) |
|
235 next |
|
236 case (base y) |
|
237 from this[unfolded tRAG_alt_def] |
|
238 show ?case by (auto simp:subtree_def) |
|
239 qed |
|
240 qed |
|
241 hence "th' \<in> ?R" by auto |
|
242 } moreover { |
|
243 fix th' |
|
244 assume "th' \<in> ?R" |
|
245 hence "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def) |
|
246 from star_rpath[OF this] |
|
247 obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto |
|
248 hence "Th th' \<in> subtree (tRAG s) (Th th)" |
|
249 proof(induct xs arbitrary:th' th rule:length_induct) |
|
250 case (1 xs th' th) |
|
251 show ?case |
|
252 proof(cases xs) |
|
253 case Nil |
|
254 from rpath_nilE[OF 1(2)[unfolded this]] |
|
255 have "th' = th" by auto |
|
256 thus ?thesis by (auto simp:subtree_def) |
|
257 next |
|
258 case (Cons x1 xs1) note Cons1 = Cons |
|
259 show ?thesis |
|
260 proof(cases "xs1") |
|
261 case Nil |
|
262 from 1(2)[unfolded Cons[unfolded this]] |
|
263 have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . |
|
264 hence "(Th th', x1) \<in> (RAG s)" by (cases, simp) |
|
265 then obtain cs where "x1 = Cs cs" |
|
266 by (unfold s_RAG_def, auto) |
|
267 find_theorems rpath "_ = _@[_]" |
|
268 from rpath_nnl_lastE[OF rp[unfolded this]] |
|
269 show ?thesis by auto |
|
270 next |
|
271 case (Cons x2 xs2) |
|
272 from 1(2)[unfolded Cons1[unfolded this]] |
|
273 have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . |
|
274 from rpath_edges_on[OF this] |
|
275 have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" . |
|
276 have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
277 by (simp add: edges_on_unfold) |
|
278 with eds have rg1: "(Th th', x1) \<in> RAG s" by auto |
|
279 then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) |
|
280 have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
281 by (simp add: edges_on_unfold) |
|
282 from this eds |
|
283 have rg2: "(x1, x2) \<in> RAG s" by auto |
|
284 from this[unfolded eq_x1] |
|
285 obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) |
|
286 from rp have "rpath (RAG s) x2 xs2 (Th th)" |
|
287 by (elim rpath_ConsE, simp) |
|
288 from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . |
|
289 from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons] |
|
290 have "Th th1 \<in> subtree (tRAG s) (Th th)" by simp |
|
291 moreover have "(Th th', Th th1) \<in> (tRAG s)^*" |
|
292 proof - |
|
293 from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] |
|
294 show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto) |
|
295 qed |
|
296 ultimately show ?thesis by (auto simp:subtree_def) |
|
297 qed |
|
298 qed |
|
299 qed |
|
300 from imageI[OF this, of the_thread] |
|
301 have "th' \<in> ?L" by simp |
|
302 } ultimately show ?thesis by auto |
|
303 qed |
|
304 |
|
305 lemma cp_alt_def1: |
|
306 "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" |
|
307 proof - |
|
308 have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = |
|
309 ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))" |
|
310 by auto |
|
311 thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) |
|
312 qed |
|
313 |
|
314 lemma cp_gen_def_cond: |
|
315 assumes "x = Th th" |
|
316 shows "cp s th = cp_gen s (Th th)" |
|
317 by (unfold cp_alt_def1 cp_gen_def, simp) |
|
318 |
|
319 lemma cp_gen_over_set: |
|
320 assumes "\<forall> x \<in> A. \<exists> th. x = Th th" |
|
321 shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A" |
|
322 proof(rule f_image_eq) |
|
323 fix a |
|
324 assume "a \<in> A" |
|
325 from assms[rule_format, OF this] |
|
326 obtain th where eq_a: "a = Th th" by auto |
|
327 show "cp_gen s a = (cp s \<circ> the_thread) a" |
|
328 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
|
329 qed |
|
330 |
|
331 |
|
332 |
|
333 locale valid_trace = |
|
334 fixes s |
|
335 assumes vt : "vt s" |
|
336 |
|
337 context valid_trace |
|
338 begin |
|
339 |
|
340 lemma wf_RAG: "wf (RAG s)" |
|
341 proof(rule finite_acyclic_wf) |
|
342 from finite_RAG[OF vt] show "finite (RAG s)" . |
|
343 next |
|
344 from acyclic_RAG[OF vt] show "acyclic (RAG s)" . |
|
345 qed |
|
346 |
|
347 end |
|
348 |
|
349 context valid_trace |
|
350 begin |
|
351 |
|
352 lemma sgv_wRAG: "single_valued (wRAG s)" |
|
353 using waiting_unique[OF vt] |
|
354 by (unfold single_valued_def wRAG_def, auto) |
|
355 |
|
356 lemma sgv_hRAG: "single_valued (hRAG s)" |
|
357 using holding_unique |
|
358 by (unfold single_valued_def hRAG_def, auto) |
|
359 |
|
360 lemma sgv_tRAG: "single_valued (tRAG s)" |
|
361 by (unfold tRAG_def, rule single_valued_relcomp, |
|
362 insert sgv_wRAG sgv_hRAG, auto) |
|
363 |
|
364 lemma acyclic_tRAG: "acyclic (tRAG s)" |
|
365 proof(unfold tRAG_def, rule acyclic_compose) |
|
366 show "acyclic (RAG s)" using acyclic_RAG[OF vt] . |
|
367 next |
|
368 show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
|
369 next |
|
370 show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
|
371 qed |
|
372 |
|
373 lemma sgv_RAG: "single_valued (RAG s)" |
|
374 using unique_RAG[OF vt] by (auto simp:single_valued_def) |
|
375 |
|
376 lemma rtree_RAG: "rtree (RAG s)" |
|
377 using sgv_RAG acyclic_RAG[OF vt] |
|
378 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
|
379 |
|
380 end |
|
381 |
|
382 sublocale valid_trace < rtree_s: rtree "tRAG s" |
|
383 proof(unfold_locales) |
|
384 from sgv_tRAG show "single_valued (tRAG s)" . |
|
385 next |
|
386 from acyclic_tRAG show "acyclic (tRAG s)" . |
|
387 qed |
|
388 |
|
389 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" |
|
390 proof - |
|
391 show "fsubtree (RAG s)" |
|
392 proof(intro_locales) |
|
393 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG[OF vt]] . |
|
394 next |
|
395 show "fsubtree_axioms (RAG s)" |
|
396 proof(unfold fsubtree_axioms_def) |
|
397 find_theorems wf RAG |
|
398 from wf_RAG show "wf (RAG s)" . |
|
399 qed |
|
400 qed |
|
401 qed |
|
402 |
|
403 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" |
|
404 proof - |
|
405 have "fsubtree (tRAG s)" |
|
406 proof - |
|
407 have "fbranch (tRAG s)" |
|
408 proof(unfold tRAG_def, rule fbranch_compose) |
|
409 show "fbranch (wRAG s)" |
|
410 proof(rule finite_fbranchI) |
|
411 from finite_RAG[OF vt] show "finite (wRAG s)" |
|
412 by (unfold RAG_split, auto) |
|
413 qed |
|
414 next |
|
415 show "fbranch (hRAG s)" |
|
416 proof(rule finite_fbranchI) |
|
417 from finite_RAG[OF vt] |
|
418 show "finite (hRAG s)" by (unfold RAG_split, auto) |
|
419 qed |
|
420 qed |
|
421 moreover have "wf (tRAG s)" |
|
422 proof(rule wf_subset) |
|
423 show "wf (RAG s O RAG s)" using wf_RAG |
|
424 by (fold wf_comp_self, simp) |
|
425 next |
|
426 show "tRAG s \<subseteq> (RAG s O RAG s)" |
|
427 by (unfold tRAG_alt_def, auto) |
|
428 qed |
|
429 ultimately show ?thesis |
|
430 by (unfold fsubtree_def fsubtree_axioms_def,auto) |
|
431 qed |
|
432 from this[folded tRAG_def] show "fsubtree (tRAG s)" . |
|
433 qed |
|
434 |
|
435 lemma Max_UNION: |
|
436 assumes "finite A" |
|
437 and "A \<noteq> {}" |
|
438 and "\<forall> M \<in> f ` A. finite M" |
|
439 and "\<forall> M \<in> f ` A. M \<noteq> {}" |
|
440 shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") |
|
441 using assms[simp] |
|
442 proof - |
|
443 have "?L = Max (\<Union>(f ` A))" |
|
444 by (fold Union_image_eq, simp) |
|
445 also have "... = ?R" |
|
446 by (subst Max_Union, simp+) |
|
447 finally show ?thesis . |
|
448 qed |
|
449 |
|
450 lemma max_Max_eq: |
|
451 assumes "finite A" |
|
452 and "A \<noteq> {}" |
|
453 and "x = y" |
|
454 shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R") |
|
455 proof - |
|
456 have "?R = Max (insert y A)" by simp |
|
457 also from assms have "... = ?L" |
|
458 by (subst Max.insert, simp+) |
|
459 finally show ?thesis by simp |
|
460 qed |
|
461 |
|
462 |
|
463 context valid_trace |
|
464 begin |
|
465 |
|
466 (* ddd *) |
|
467 lemma cp_gen_rec: |
|
468 assumes "x = Th th" |
|
469 shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)" |
|
470 proof(cases "children (tRAG s) x = {}") |
|
471 case True |
|
472 show ?thesis |
|
473 by (unfold True cp_gen_def subtree_children, simp add:assms) |
|
474 next |
|
475 case False |
|
476 hence [simp]: "children (tRAG s) x \<noteq> {}" by auto |
|
477 note fsbttRAGs.finite_subtree[simp] |
|
478 have [simp]: "finite (children (tRAG s) x)" |
|
479 by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], |
|
480 rule children_subtree) |
|
481 { fix r x |
|
482 have "subtree r x \<noteq> {}" by (auto simp:subtree_def) |
|
483 } note this[simp] |
|
484 have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}" |
|
485 proof - |
|
486 from False obtain q where "q \<in> children (tRAG s) x" by blast |
|
487 moreover have "subtree (tRAG s) q \<noteq> {}" by simp |
|
488 ultimately show ?thesis by blast |
|
489 qed |
|
490 have h: "Max ((the_preced s \<circ> the_thread) ` |
|
491 ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) = |
|
492 Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)" |
|
493 (is "?L = ?R") |
|
494 proof - |
|
495 let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L |
|
496 let "Max (_ \<union> (?h ` ?B))" = ?R |
|
497 let ?L1 = "?f ` \<Union>(?g ` ?B)" |
|
498 have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" |
|
499 proof - |
|
500 have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp |
|
501 also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto |
|
502 finally have "Max ?L1 = Max ..." by simp |
|
503 also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)" |
|
504 by (subst Max_UNION, simp+) |
|
505 also have "... = Max (cp_gen s ` children (tRAG s) x)" |
|
506 by (unfold image_comp cp_gen_alt_def, simp) |
|
507 finally show ?thesis . |
|
508 qed |
|
509 show ?thesis |
|
510 proof - |
|
511 have "?L = Max (?f ` ?A \<union> ?L1)" by simp |
|
512 also have "... = max (the_preced s (the_thread x)) (Max ?L1)" |
|
513 by (subst Max_Un, simp+) |
|
514 also have "... = max (?f x) (Max (?h ` ?B))" |
|
515 by (unfold eq_Max_L1, simp) |
|
516 also have "... =?R" |
|
517 by (rule max_Max_eq, (simp)+, unfold assms, simp) |
|
518 finally show ?thesis . |
|
519 qed |
|
520 qed thus ?thesis |
|
521 by (fold h subtree_children, unfold cp_gen_def, simp) |
|
522 qed |
|
523 |
|
524 lemma cp_rec: |
|
525 "cp s th = Max ({the_preced s th} \<union> |
|
526 (cp s o the_thread) ` children (tRAG s) (Th th))" |
|
527 proof - |
|
528 have "Th th = Th th" by simp |
|
529 note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] |
|
530 show ?thesis |
|
531 proof - |
|
532 have "cp_gen s ` children (tRAG s) (Th th) = |
|
533 (cp s \<circ> the_thread) ` children (tRAG s) (Th th)" |
|
534 proof(rule cp_gen_over_set) |
|
535 show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th" |
|
536 by (unfold tRAG_alt_def, auto simp:children_def) |
|
537 qed |
|
538 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
|
539 qed |
|
540 qed |
|
541 |
|
542 end |
|
543 |
|
544 |
48 lemma eq_dependants: "dependants (wq s) = dependants s" |
545 lemma eq_dependants: "dependants (wq s) = dependants s" |
49 by (simp add: s_dependants_abv wq_def) |
546 by (simp add: s_dependants_abv wq_def) |
50 |
547 |
|
548 |
51 (* obvious lemma *) |
549 (* obvious lemma *) |
52 lemma not_thread_holdents: |
550 lemma not_thread_holdents: |
53 fixes th s |
551 fixes th s |
54 assumes vt: "vt s" |
552 assumes vt: "vt s" |
55 and not_in: "th \<notin> threads s" |
553 and not_in: "th \<notin> threads s" |
546 by (simp add: UN_exists) |
1044 by (simp add: UN_exists) |
547 |
1045 |
548 (* moving in Max *) |
1046 (* moving in Max *) |
549 also have "\<dots> = max (Max {preced th s}) |
1047 also have "\<dots> = max (Max {preced th s}) |
550 (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" |
1048 (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" |
551 by (subst Max_Union) (auto simp add: image_image) |
1049 by (subst Max_Union) (auto simp add: image_image) |
552 |
1050 |
553 (* folding cp + moving out Max *) |
1051 (* folding cp + moving out Max *) |
554 also have "\<dots> = ?RHS" |
1052 also have "\<dots> = ?RHS" |
555 unfolding eq_cp by (simp add: Max_insert) |
1053 unfolding eq_cp by (simp add: Max_insert) |
556 |
1054 |
557 finally show "?LHS = ?RHS" . |
1055 finally show "?LHS = ?RHS" . |
558 qed |
1056 qed |
559 qed |
1057 qed |
560 |
1058 |
561 lemma next_waiting: |
1059 lemma next_th_holding: |
562 assumes vt: "vt s" |
1060 assumes vt: "vt s" |
563 and nxt: "next_th s th cs th'" |
1061 and nxt: "next_th s th cs th'" |
564 shows "waiting s th' cs" |
1062 shows "holding (wq s) th cs" |
565 proof - |
1063 proof - |
566 from assms show ?thesis |
1064 from nxt[unfolded next_th_def] |
567 apply (auto simp:next_th_def s_waiting_def[folded wq_def]) |
1065 obtain rest where h: "wq s cs = th # rest" |
568 proof - |
1066 "rest \<noteq> []" |
569 fix rest |
1067 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
570 assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
1068 thus ?thesis |
571 and eq_wq: "wq s cs = th # rest" |
1069 by (unfold cs_holding_def, auto) |
572 and ne: "rest \<noteq> []" |
1070 qed |
573 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
1071 |
574 proof(rule someI2) |
1072 lemma next_th_waiting: |
575 from wq_distinct[OF vt, of cs] eq_wq |
1073 assumes vt: "vt s" |
576 show "distinct rest \<and> set rest = set rest" by auto |
1074 and nxt: "next_th s th cs th'" |
577 next |
1075 shows "waiting (wq s) th' cs" |
578 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
1076 proof - |
579 qed |
1077 from nxt[unfolded next_th_def] |
580 with ni |
1078 obtain rest where h: "wq s cs = th # rest" |
581 have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)" |
1079 "rest \<noteq> []" |
582 by simp |
1080 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
583 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
1081 from wq_distinct[OF vt, of cs, unfolded h] |
584 proof(rule someI2) |
1082 have dst: "distinct (th # rest)" . |
585 from wq_distinct[OF vt, of cs] eq_wq |
1083 have in_rest: "th' \<in> set rest" |
586 show "distinct rest \<and> set rest = set rest" by auto |
1084 proof(unfold h, rule someI2) |
587 next |
1085 show "distinct rest \<and> set rest = set rest" using dst by auto |
588 from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto |
|
589 qed |
|
590 ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto |
|
591 next |
1086 next |
592 fix rest |
1087 fix x assume "distinct x \<and> set x = set rest" |
593 assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest" |
1088 with h(2) |
594 and ne: "rest \<noteq> []" |
1089 show "hd x \<in> set (rest)" by (cases x, auto) |
595 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
1090 qed |
596 proof(rule someI2) |
1091 hence "th' \<in> set (wq s cs)" by (unfold h(1), auto) |
597 from wq_distinct[OF vt, of cs] eq_wq |
1092 moreover have "th' \<noteq> hd (wq s cs)" |
598 show "distinct rest \<and> set rest = set rest" by auto |
1093 by (unfold h(1), insert in_rest dst, auto) |
599 next |
1094 ultimately show ?thesis by (auto simp:cs_waiting_def) |
600 from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto |
1095 qed |
601 qed |
1096 |
602 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)" |
1097 lemma next_th_RAG: |
603 by auto |
1098 assumes vt: "vt s" |
604 moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
1099 and nxt: "next_th s th cs th'" |
605 proof(rule someI2) |
1100 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
606 from wq_distinct[OF vt, of cs] eq_wq |
1101 using assms next_th_holding next_th_waiting |
607 show "distinct rest \<and> set rest = set rest" by auto |
1102 by (unfold s_RAG_def, simp) |
608 next |
|
609 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
610 qed |
|
611 ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp |
|
612 with eq_wq and wq_distinct[OF vt, of cs] |
|
613 show False by auto |
|
614 qed |
|
615 qed |
|
616 |
1103 |
617 -- {* A useless definition *} |
1104 -- {* A useless definition *} |
618 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
1105 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
619 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
1106 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
620 |
1107 |
680 proof - |
1160 proof - |
681 from assms show ?thesis |
1161 from assms show ?thesis |
682 by (unfold s_def, auto simp:preced_def) |
1162 by (unfold s_def, auto simp:preced_def) |
683 qed |
1163 qed |
684 |
1164 |
685 text {* (* ddd *) |
1165 lemma eq_the_preced: |
|
1166 fixes th' |
|
1167 assumes "th' \<noteq> th" |
|
1168 shows "the_preced s th' = the_preced s' th'" |
|
1169 using assms |
|
1170 by (unfold the_preced_def, intro eq_preced, simp) |
|
1171 |
|
1172 text {* |
686 The following lemma assures that the resetting of priority does not change the RAG. |
1173 The following lemma assures that the resetting of priority does not change the RAG. |
687 *} |
1174 *} |
688 |
1175 |
689 lemma eq_dep: "RAG s = RAG s'" |
1176 lemma eq_dep: "RAG s = RAG s'" |
690 by (unfold s_def RAG_set_unchanged, auto) |
1177 by (unfold s_def RAG_set_unchanged, auto) |
691 |
1178 |
692 text {* |
1179 text {* (* ddd *) |
693 Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation. |
1180 Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"} |
694 It says, thread other than the initiating thread @{text "th"} does not need recalculation |
1181 only affects those threads, which as @{text "Th th"} in their sub-trees. |
695 unless it lies upstream of @{text "th"} in the RAG. |
1182 |
696 |
1183 The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. |
697 The reason behind this lemma is that: |
|
698 the change of precedence of one thread can only affect it's upstream threads, according to |
|
699 lemma @{text "eq_preced"}. Since the only thread which might change precedence is |
|
700 @{text "th"}, so only @{text "th"} and its upstream threads need recalculation. |
|
701 (* ccc *) |
|
702 *} |
1184 *} |
703 |
1185 |
704 lemma eq_cp_pre: |
1186 lemma eq_cp_pre: |
705 fixes th' |
1187 fixes th' |
706 assumes neq_th: "th' \<noteq> th" |
1188 assumes nd: "Th th \<notin> subtree (RAG s') (Th th')" |
707 and nd: "th \<notin> dependants s th'" |
|
708 shows "cp s th' = cp s' th'" |
1189 shows "cp s th' = cp s' th'" |
709 proof - |
1190 proof - |
710 -- {* This is what we need to prove after expanding the definition of @{text "cp"} *} |
1191 -- {* After unfolding using the alternative definition, elements |
711 have "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = |
1192 affecting the @{term "cp"}-value of threads become explicit. |
712 Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" |
1193 We only need to prove the following: *} |
713 (is "Max (?f1 ` ({th'} \<union> ?A)) = Max (?f2 ` ({th'} \<union> ?B))") |
1194 have "Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) = |
|
1195 Max (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})" |
|
1196 (is "Max (?f ` ?S1) = Max (?g ` ?S2)") |
714 proof - |
1197 proof - |
715 -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of |
1198 -- {* The base sets are equal. *} |
716 any threads are not changed, this is one of key facts underpinning this |
1199 have "?S1 = ?S2" using eq_dep by simp |
717 lemma *} |
1200 -- {* The function values on the base set are equal as well. *} |
718 have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) |
1201 moreover have "\<forall> e \<in> ?S2. ?f e = ?g e" |
719 have "(?f1 ` ({th'} \<union> ?A)) = (?f2 ` ({th'} \<union> ?B))" |
1202 proof |
720 proof(rule image_cong) |
1203 fix th1 |
721 show "{th'} \<union> ?A = {th'} \<union> ?B" by (simp only:eq_ab) |
1204 assume "th1 \<in> ?S2" |
722 next |
1205 with nd have "th1 \<noteq> th" by (auto) |
723 fix x |
1206 from eq_the_preced[OF this] |
724 assume x_in: "x \<in> {th'} \<union> ?B" |
1207 show "the_preced s th1 = the_preced s' th1" . |
725 show "?f1 x = ?f2 x" |
1208 qed |
726 proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *} |
1209 -- {* Therefore, the image of the functions are equal. *} |
727 from x_in[folded eq_ab, unfolded eq_dependants] |
1210 ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq) |
728 have "x \<in> {th'} \<union> dependants s th'" . |
1211 thus ?thesis by simp |
729 thus "x \<noteq> th" |
1212 qed |
730 proof |
1213 thus ?thesis by (simp add:cp_alt_def) |
731 assume "x \<in> {th'}" |
|
732 with `th' \<noteq> th` show ?thesis by simp |
|
733 next |
|
734 assume "x \<in> dependants s th'" |
|
735 with `th \<notin> dependants s th'` show ?thesis by auto |
|
736 qed |
|
737 qed |
|
738 qed |
|
739 thus ?thesis by simp |
|
740 qed |
|
741 thus ?thesis by (unfold cp_eq_cpreced cpreced_def) |
|
742 qed |
1214 qed |
743 |
1215 |
744 text {* |
1216 text {* |
745 The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}. |
1217 The following lemma shows that @{term "th"} is not in the |
746 The reason for this is that only no-blocked thread can initiate |
1218 sub-tree of any other thread. |
747 a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any |
|
748 critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG. |
|
749 Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}. |
|
750 *} |
1219 *} |
751 lemma no_dependants: |
1220 lemma th_in_no_subtree: |
752 shows "th \<notin> dependants s th'" |
1221 assumes "th' \<noteq> th" |
753 proof |
1222 shows "Th th \<notin> subtree (RAG s') (Th th')" |
754 assume "th \<in> dependants s th'" |
1223 proof - |
755 from `th \<in> dependants s th'` have "(Th th, Th th') \<in> (RAG s')\<^sup>+" |
1224 have "th \<in> readys s'" |
756 by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto) |
|
757 from tranclD[OF this] |
|
758 obtain z where "(Th th, z) \<in> RAG s'" by auto |
|
759 moreover have "th \<in> readys s'" |
|
760 proof - |
1225 proof - |
761 from step_back_step [OF vt_s[unfolded s_def]] |
1226 from step_back_step [OF vt_s[unfolded s_def]] |
762 have "step s' (Set th prio)" . |
1227 have "step s' (Set th prio)" . |
763 hence "th \<in> runing s'" by (cases, simp) |
1228 hence "th \<in> runing s'" by (cases, simp) |
764 thus ?thesis by (simp add:readys_def runing_def) |
1229 thus ?thesis by (simp add:readys_def runing_def) |
765 qed |
1230 qed |
766 ultimately show "False" |
1231 from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] this assms(1)] |
767 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
1232 show ?thesis by blast |
768 by (fold wq_def, blast) |
1233 qed |
769 qed |
1234 |
770 |
|
771 (* Result improved *) |
|
772 text {* |
1235 text {* |
773 A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"} |
1236 By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, |
774 gives the main lemma of this locale, which shows that |
1237 it is obvious that the change of priority only affects the @{text "cp"}-value |
775 only the initiating thread needs a recalculation of current precedence. |
1238 of the initiating thread @{text "th"}. |
776 *} |
1239 *} |
777 lemma eq_cp: |
1240 lemma eq_cp: |
778 fixes th' |
1241 fixes th' |
779 assumes "th' \<noteq> th" |
1242 assumes "th' \<noteq> th" |
780 shows "cp s th' = cp s' th'" |
1243 shows "cp s th' = cp s' th'" |
781 by (rule eq_cp_pre[OF assms no_dependants]) |
1244 by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) |
782 |
1245 |
783 end |
1246 end |
784 |
1247 |
785 text {* |
1248 text {* |
786 The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. |
1249 The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. |
845 th6 ----| |
1385 th6 ----| |
846 | |
1386 | |
847 th7 ----| |
1387 th7 ----| |
848 *) |
1388 *) |
849 |
1389 |
|
1390 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'" |
|
1391 using next_th_RAG[OF vt_s' nt] . |
|
1392 |
|
1393 lemma ancestors_th': |
|
1394 "ancestors (RAG s') (Th th') = {Th th, Cs cs}" |
|
1395 proof - |
|
1396 have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}" |
|
1397 proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs']) |
|
1398 from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto |
|
1399 qed |
|
1400 thus ?thesis using ancestors_th ancestors_cs by auto |
|
1401 qed |
|
1402 |
850 lemma RAG_s: |
1403 lemma RAG_s: |
851 "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> |
1404 "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> |
852 {(Cs cs, Th th')}" |
1405 {(Cs cs, Th th')}" |
853 proof - |
1406 proof - |
854 from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] |
1407 from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] |
855 and nt show ?thesis by (auto intro:next_th_unique) |
1408 and nt show ?thesis by (auto intro:next_th_unique) |
856 qed |
1409 qed |
857 |
1410 |
858 text {* |
1411 lemma subtree_kept: |
859 Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"} |
1412 assumes "th1 \<notin> {th, th'}" |
860 have their dependants changed. |
1413 shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") |
861 *} |
1414 proof - |
862 lemma dependants_kept: |
1415 let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})" |
863 fixes th'' |
1416 let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}" |
864 assumes neq1: "th'' \<noteq> th" |
1417 have "subtree ?RAG' (Th th1) = ?R" |
865 and neq2: "th'' \<noteq> th'" |
1418 proof(rule subset_del_subtree_outside) |
866 shows "dependants (wq s) th'' = dependants (wq s') th''" |
1419 show "Range {(Cs cs, Th th), (Th th', Cs cs)} \<inter> subtree (RAG s') (Th th1) = {}" |
867 proof(auto) (* ccc *) |
1420 proof - |
868 fix x |
1421 have "(Th th) \<notin> subtree (RAG s') (Th th1)" |
869 assume "x \<in> dependants (wq s) th''" |
1422 proof(rule subtree_refute) |
870 hence dp: "(Th x, Th th'') \<in> (RAG s)^+" |
1423 show "Th th1 \<notin> ancestors (RAG s') (Th th)" |
871 by (auto simp:cs_dependants_def eq_RAG) |
1424 by (unfold ancestors_th, simp) |
872 { fix n |
1425 next |
873 have "(n, Th th'') \<in> (RAG s)^+ \<Longrightarrow> (n, Th th'') \<in> (RAG s')^+" |
1426 from assms show "Th th1 \<noteq> Th th" by simp |
874 proof(induct rule:converse_trancl_induct) |
1427 qed |
875 fix y |
1428 moreover have "(Cs cs) \<notin> subtree (RAG s') (Th th1)" |
876 assume "(y, Th th'') \<in> RAG s" |
1429 proof(rule subtree_refute) |
877 with RAG_s neq1 neq2 |
1430 show "Th th1 \<notin> ancestors (RAG s') (Cs cs)" |
878 have "(y, Th th'') \<in> RAG s'" by auto |
1431 by (unfold ancestors_cs, insert assms, auto) |
879 thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto |
1432 qed simp |
|
1433 ultimately have "{Th th, Cs cs} \<inter> subtree (RAG s') (Th th1) = {}" by auto |
|
1434 thus ?thesis by simp |
|
1435 qed |
|
1436 qed |
|
1437 moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)" |
|
1438 proof(rule subtree_insert_next) |
|
1439 show "Th th' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)" |
|
1440 proof(rule subtree_refute) |
|
1441 show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')" |
|
1442 (is "_ \<notin> ?R") |
|
1443 proof - |
|
1444 have "?R \<subseteq> ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto) |
|
1445 moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp |
|
1446 ultimately show ?thesis by auto |
|
1447 qed |
880 next |
1448 next |
881 fix y z |
1449 from assms show "Th th1 \<noteq> Th th'" by simp |
882 assume yz: "(y, z) \<in> RAG s" |
1450 qed |
883 and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+" |
1451 qed |
884 and ztp': "(z, Th th'') \<in> (RAG s')\<^sup>+" |
1452 ultimately show ?thesis by (unfold RAG_s, simp) |
885 have "y \<noteq> Cs cs \<and> y \<noteq> Th th'" |
|
886 proof |
|
887 show "y \<noteq> Cs cs" |
|
888 proof |
|
889 assume eq_y: "y = Cs cs" |
|
890 with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp |
|
891 from RAG_s |
|
892 have cst': "(Cs cs, Th th') \<in> RAG s" by simp |
|
893 from unique_RAG[OF vt_s this dp_yz] |
|
894 have eq_z: "z = Th th'" by simp |
|
895 with ztp have "(Th th', Th th'') \<in> (RAG s)^+" by simp |
|
896 from converse_tranclE[OF this] |
|
897 obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s" |
|
898 by (auto simp:s_RAG_def) |
|
899 with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto |
|
900 from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (RAG s)^+" by auto |
|
901 moreover have "cs' = cs" |
|
902 proof - |
|
903 from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt] |
|
904 have "(Th th', Cs cs) \<in> RAG s'" |
|
905 by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def) |
|
906 from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp'] |
|
907 show ?thesis by simp |
|
908 qed |
|
909 ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp |
|
910 moreover note wf_trancl[OF wf_RAG[OF vt_s]] |
|
911 ultimately show False by auto |
|
912 qed |
|
913 next |
|
914 show "y \<noteq> Th th'" |
|
915 proof |
|
916 assume eq_y: "y = Th th'" |
|
917 with yz have dps: "(Th th', z) \<in> RAG s" by simp |
|
918 with RAG_s have dps': "(Th th', z) \<in> RAG s'" by auto |
|
919 have "z = Cs cs" |
|
920 proof - |
|
921 from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt] |
|
922 have "(Th th', Cs cs) \<in> RAG s'" |
|
923 by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def) |
|
924 from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this] |
|
925 show ?thesis . |
|
926 qed |
|
927 with dps RAG_s show False by auto |
|
928 qed |
|
929 qed |
|
930 with RAG_s yz have "(y, z) \<in> RAG s'" by auto |
|
931 with ztp' |
|
932 show "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto |
|
933 qed |
|
934 } |
|
935 from this[OF dp] |
|
936 show "x \<in> dependants (wq s') th''" |
|
937 by (auto simp:cs_dependants_def eq_RAG) |
|
938 next |
|
939 fix x |
|
940 assume "x \<in> dependants (wq s') th''" |
|
941 hence dp: "(Th x, Th th'') \<in> (RAG s')^+" |
|
942 by (auto simp:cs_dependants_def eq_RAG) |
|
943 { fix n |
|
944 have "(n, Th th'') \<in> (RAG s')^+ \<Longrightarrow> (n, Th th'') \<in> (RAG s)^+" |
|
945 proof(induct rule:converse_trancl_induct) |
|
946 fix y |
|
947 assume "(y, Th th'') \<in> RAG s'" |
|
948 with RAG_s neq1 neq2 |
|
949 have "(y, Th th'') \<in> RAG s" by auto |
|
950 thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto |
|
951 next |
|
952 fix y z |
|
953 assume yz: "(y, z) \<in> RAG s'" |
|
954 and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+" |
|
955 and ztp': "(z, Th th'') \<in> (RAG s)\<^sup>+" |
|
956 have "y \<noteq> Cs cs \<and> y \<noteq> Th th'" |
|
957 proof |
|
958 show "y \<noteq> Cs cs" |
|
959 proof |
|
960 assume eq_y: "y = Cs cs" |
|
961 with yz have dp_yz: "(Cs cs, z) \<in> RAG s'" by simp |
|
962 from this have eq_z: "z = Th th" |
|
963 proof - |
|
964 from step_back_step[OF vt_s[unfolded s_def]] |
|
965 have "(Cs cs, Th th) \<in> RAG s'" |
|
966 by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def) |
|
967 from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz] |
|
968 show ?thesis by simp |
|
969 qed |
|
970 from converse_tranclE[OF ztp] |
|
971 obtain u where "(z, u) \<in> RAG s'" by auto |
|
972 moreover |
|
973 from step_back_step[OF vt_s[unfolded s_def]] |
|
974 have "th \<in> readys s'" by (cases, simp add:runing_def) |
|
975 moreover note eq_z |
|
976 ultimately show False |
|
977 by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) |
|
978 qed |
|
979 next |
|
980 show "y \<noteq> Th th'" |
|
981 proof |
|
982 assume eq_y: "y = Th th'" |
|
983 with yz have dps: "(Th th', z) \<in> RAG s'" by simp |
|
984 have "z = Cs cs" |
|
985 proof - |
|
986 from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt] |
|
987 have "(Th th', Cs cs) \<in> RAG s'" |
|
988 by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def) |
|
989 from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps this] |
|
990 show ?thesis . |
|
991 qed |
|
992 with ztp have cs_i: "(Cs cs, Th th'') \<in> (RAG s')\<^sup>+" by simp |
|
993 from step_back_step[OF vt_s[unfolded s_def]] |
|
994 have cs_th: "(Cs cs, Th th) \<in> RAG s'" |
|
995 by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def) |
|
996 have "(Cs cs, Th th'') \<notin> RAG s'" |
|
997 proof |
|
998 assume "(Cs cs, Th th'') \<in> RAG s'" |
|
999 from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th] |
|
1000 and neq1 show "False" by simp |
|
1001 qed |
|
1002 with converse_tranclE[OF cs_i] |
|
1003 obtain u where cu: "(Cs cs, u) \<in> RAG s'" |
|
1004 and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto |
|
1005 have "u = Th th" |
|
1006 proof - |
|
1007 from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th] |
|
1008 show ?thesis . |
|
1009 qed |
|
1010 with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp |
|
1011 from converse_tranclE[OF this] |
|
1012 obtain v where "(Th th, v) \<in> (RAG s')" by auto |
|
1013 moreover from step_back_step[OF vt_s[unfolded s_def]] |
|
1014 have "th \<in> readys s'" by (cases, simp add:runing_def) |
|
1015 ultimately show False |
|
1016 by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) |
|
1017 qed |
|
1018 qed |
|
1019 with RAG_s yz have "(y, z) \<in> RAG s" by auto |
|
1020 with ztp' |
|
1021 show "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto |
|
1022 qed |
|
1023 } |
|
1024 from this[OF dp] |
|
1025 show "x \<in> dependants (wq s) th''" |
|
1026 by (auto simp:cs_dependants_def eq_RAG) |
|
1027 qed |
1453 qed |
1028 |
1454 |
1029 lemma cp_kept: |
1455 lemma cp_kept: |
1030 fixes th'' |
1456 assumes "th1 \<notin> {th, th'}" |
1031 assumes neq1: "th'' \<noteq> th" |
1457 shows "cp s th1 = cp s' th1" |
1032 and neq2: "th'' \<noteq> th'" |
1458 by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp) |
1033 shows "cp s th'' = cp s' th''" |
|
1034 proof - |
|
1035 from dependants_kept[OF neq1 neq2] |
|
1036 have "dependants (wq s) th'' = dependants (wq s') th''" . |
|
1037 moreover { |
|
1038 fix th1 |
|
1039 assume "th1 \<in> dependants (wq s) th''" |
|
1040 have "preced th1 s = preced th1 s'" |
|
1041 by (unfold s_def, auto simp:preced_def) |
|
1042 } |
|
1043 moreover have "preced th'' s = preced th'' s'" |
|
1044 by (unfold s_def, auto simp:preced_def) |
|
1045 ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) = |
|
1046 ((\<lambda>th. preced th s') ` ({th''} \<union> dependants (wq s') th''))" |
|
1047 by (auto simp:image_def) |
|
1048 thus ?thesis |
|
1049 by (unfold cp_eq_cpreced cpreced_def, simp) |
|
1050 qed |
|
1051 |
1459 |
1052 end |
1460 end |
1053 |
1461 |
1054 locale step_v_cps_nnt = step_v_cps + |
1462 locale step_v_cps_nnt = step_v_cps + |
1055 assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')" |
1463 assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')" |
1056 |
1464 |
1057 context step_v_cps_nnt |
1465 context step_v_cps_nnt |
1058 begin |
1466 begin |
1059 |
1467 |
1060 lemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'" |
|
1061 proof |
|
1062 assume "(Th th1, Cs cs) \<in> RAG s'" |
|
1063 thus "False" |
|
1064 apply (auto simp:s_RAG_def cs_waiting_def) |
|
1065 proof - |
|
1066 assume h1: "th1 \<in> set (wq s' cs)" |
|
1067 and h2: "th1 \<noteq> hd (wq s' cs)" |
|
1068 from step_back_step[OF vt_s[unfolded s_def]] |
|
1069 show "False" |
|
1070 proof(cases) |
|
1071 assume "holding s' th cs" |
|
1072 then obtain rest where |
|
1073 eq_wq: "wq s' cs = th#rest" |
|
1074 apply (unfold s_holding_def wq_def[symmetric]) |
|
1075 by (case_tac "(wq s' cs)", auto) |
|
1076 with h1 h2 have ne: "rest \<noteq> []" by auto |
|
1077 with eq_wq |
|
1078 have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))" |
|
1079 by(unfold next_th_def, rule_tac x = "rest" in exI, auto) |
|
1080 with nnt show ?thesis by auto |
|
1081 qed |
|
1082 qed |
|
1083 qed |
|
1084 |
|
1085 lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}" |
1468 lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}" |
1086 proof - |
1469 proof - |
1087 from nnt and step_RAG_v[OF vt_s[unfolded s_def], folded s_def] |
1470 from nnt and step_RAG_v[OF vt_s[unfolded s_def], folded s_def] |
1088 show ?thesis by auto |
1471 show ?thesis by auto |
1089 qed |
1472 qed |
1090 |
1473 |
1091 lemma child_kept_left: |
1474 lemma subtree_kept: |
1092 assumes |
1475 assumes "th1 \<noteq> th" |
1093 "(n1, n2) \<in> (child s')^+" |
1476 shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" |
1094 shows "(n1, n2) \<in> (child s)^+" |
1477 proof(unfold RAG_s, rule subset_del_subtree_outside) |
1095 proof - |
1478 show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s') (Th th1) = {}" |
1096 from assms show ?thesis |
1479 proof - |
1097 proof(induct rule: converse_trancl_induct) |
1480 have "(Th th) \<notin> subtree (RAG s') (Th th1)" |
1098 case (base y) |
1481 proof(rule subtree_refute) |
1099 from base obtain th1 cs1 th2 |
1482 show "Th th1 \<notin> ancestors (RAG s') (Th th)" |
1100 where h1: "(Th th1, Cs cs1) \<in> RAG s'" |
1483 by (unfold ancestors_th, simp) |
1101 and h2: "(Cs cs1, Th th2) \<in> RAG s'" |
1484 next |
1102 and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def) |
1485 from assms show "Th th1 \<noteq> Th th" by simp |
1103 have "cs1 \<noteq> cs" |
1486 qed |
|
1487 thus ?thesis by auto |
|
1488 qed |
|
1489 qed |
|
1490 |
|
1491 lemma cp_kept_1: |
|
1492 assumes "th1 \<noteq> th" |
|
1493 shows "cp s th1 = cp s' th1" |
|
1494 by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp) |
|
1495 |
|
1496 lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}" |
|
1497 proof - |
|
1498 { fix n |
|
1499 have "(Cs cs) \<notin> ancestors (RAG s') n" |
1104 proof |
1500 proof |
1105 assume eq_cs: "cs1 = cs" |
1501 assume "Cs cs \<in> ancestors (RAG s') n" |
1106 with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp |
1502 hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def) |
1107 with nw_cs eq_cs show False by auto |
1503 from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s'" by auto |
1108 qed |
1504 then obtain th' where "nn = Th th'" |
1109 with h1 h2 RAG_s have |
1505 by (unfold s_RAG_def, auto) |
1110 h1': "(Th th1, Cs cs1) \<in> RAG s" and |
1506 from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s'" . |
1111 h2': "(Cs cs1, Th th2) \<in> RAG s" by auto |
1507 from this[unfolded s_RAG_def] |
1112 hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def) |
1508 have "waiting (wq s') th' cs" by auto |
1113 with eq_y eq_n2 have "(y, n2) \<in> child s" by simp |
1509 from this[unfolded cs_waiting_def] |
1114 thus ?case by auto |
1510 have "1 < length (wq s' cs)" |
1115 next |
1511 by (cases "wq s' cs", auto) |
1116 case (step y z) |
1512 from holding_next_thI[OF holding_th this] |
1117 have "(y, z) \<in> child s'" by fact |
1513 obtain th' where "next_th s' th cs th'" by auto |
1118 then obtain th1 cs1 th2 |
1514 with nnt show False by auto |
1119 where h1: "(Th th1, Cs cs1) \<in> RAG s'" |
1515 qed |
1120 and h2: "(Cs cs1, Th th2) \<in> RAG s'" |
1516 } note h = this |
1121 and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) |
1517 { fix n |
1122 have "cs1 \<noteq> cs" |
1518 assume "n \<in> subtree (RAG s') (Cs cs)" |
1123 proof |
1519 hence "n = (Cs cs)" |
1124 assume eq_cs: "cs1 = cs" |
1520 by (elim subtreeE, insert h, auto) |
1125 with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp |
1521 } moreover have "(Cs cs) \<in> subtree (RAG s') (Cs cs)" |
1126 with nw_cs eq_cs show False by auto |
1522 by (auto simp:subtree_def) |
1127 qed |
1523 ultimately show ?thesis by auto |
1128 with h1 h2 RAG_s have |
1524 qed |
1129 h1': "(Th th1, Cs cs1) \<in> RAG s" and |
1525 |
1130 h2': "(Cs cs1, Th th2) \<in> RAG s" by auto |
1526 lemma subtree_th: |
1131 hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def) |
1527 "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}" |
1132 with eq_y eq_z have "(y, z) \<in> child s" by simp |
1528 proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs']) |
1133 moreover have "(z, n2) \<in> (child s)^+" by fact |
1529 from edge_of_th |
1134 ultimately show ?case by auto |
1530 show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)" |
1135 qed |
1531 by (unfold edges_in_def, auto simp:subtree_def) |
1136 qed |
1532 qed |
1137 |
1533 |
1138 lemma child_kept_right: |
1534 lemma cp_kept_2: |
1139 assumes |
1535 shows "cp s th = cp s' th" |
1140 "(n1, n2) \<in> (child s)^+" |
1536 by (unfold cp_alt_def subtree_th preced_kept, auto) |
1141 shows "(n1, n2) \<in> (child s')^+" |
|
1142 proof - |
|
1143 from assms show ?thesis |
|
1144 proof(induct) |
|
1145 case (base y) |
|
1146 from base and RAG_s |
|
1147 have "(n1, y) \<in> child s'" |
|
1148 by (auto simp:child_def) |
|
1149 thus ?case by auto |
|
1150 next |
|
1151 case (step y z) |
|
1152 have "(y, z) \<in> child s" by fact |
|
1153 with RAG_s have "(y, z) \<in> child s'" |
|
1154 by (auto simp:child_def) |
|
1155 moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact |
|
1156 ultimately show ?case by auto |
|
1157 qed |
|
1158 qed |
|
1159 |
|
1160 lemma eq_child: "(child s)^+ = (child s')^+" |
|
1161 by (insert child_kept_left child_kept_right, auto) |
|
1162 |
1537 |
1163 lemma eq_cp: |
1538 lemma eq_cp: |
1164 fixes th' |
1539 fixes th' |
1165 shows "cp s th' = cp s' th'" |
1540 shows "cp s th' = cp s' th'" |
1166 apply (unfold cp_eq_cpreced cpreced_def) |
1541 using cp_kept_1 cp_kept_2 |
1167 proof - |
1542 by (cases "th' = th", auto) |
1168 have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th" |
1543 |
1169 apply (unfold cs_dependants_def, unfold eq_RAG) |
|
1170 proof - |
|
1171 from eq_child |
|
1172 have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}" |
|
1173 by simp |
|
1174 with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] |
|
1175 show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}" |
|
1176 by simp |
|
1177 qed |
|
1178 moreover { |
|
1179 fix th1 |
|
1180 assume "th1 \<in> {th'} \<union> dependants (wq s') th'" |
|
1181 hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto |
|
1182 hence "preced th1 s = preced th1 s'" |
|
1183 proof |
|
1184 assume "th1 = th'" |
|
1185 show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) |
|
1186 next |
|
1187 assume "th1 \<in> dependants (wq s') th'" |
|
1188 show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) |
|
1189 qed |
|
1190 } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = |
|
1191 ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" |
|
1192 by (auto simp:image_def) |
|
1193 thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = |
|
1194 Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp |
|
1195 qed |
|
1196 |
|
1197 end |
1544 end |
|
1545 |
|
1546 find_theorems "_`_" "\<Union> _" |
|
1547 |
|
1548 find_theorems "Max" "\<Union> _" |
|
1549 |
|
1550 find_theorems wf RAG |
|
1551 |
|
1552 thm wf_def |
|
1553 |
|
1554 thm image_Union |
1198 |
1555 |
1199 locale step_P_cps = |
1556 locale step_P_cps = |
1200 fixes s' th cs s |
1557 fixes s' th cs s |
1201 defines s_def : "s \<equiv> (P th cs#s')" |
1558 defines s_def : "s \<equiv> (P th cs#s')" |
1202 assumes vt_s: "vt s" |
1559 assumes vt_s: "vt s" |
1203 |
1560 |
|
1561 sublocale step_P_cps < vat_s : valid_trace "s" |
|
1562 proof |
|
1563 from vt_s show "vt s" . |
|
1564 qed |
|
1565 |
|
1566 sublocale step_P_cps < vat_s' : valid_trace "s'" |
|
1567 proof |
|
1568 from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . |
|
1569 qed |
|
1570 |
|
1571 |
|
1572 context step_P_cps |
|
1573 begin |
|
1574 |
|
1575 lemma rtree_RAGs: "rtree (RAG s)" |
|
1576 proof |
|
1577 show "single_valued (RAG s)" |
|
1578 apply (intro_locales) |
|
1579 by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s]) |
|
1580 |
|
1581 show "acyclic (RAG s)" |
|
1582 by (rule acyclic_RAG[OF vt_s]) |
|
1583 qed |
|
1584 |
|
1585 lemma rtree_RAGs': "rtree (RAG s')" |
|
1586 proof |
|
1587 show "single_valued (RAG s')" |
|
1588 apply (intro_locales) |
|
1589 by (unfold single_valued_def, |
|
1590 auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]]) |
|
1591 |
|
1592 show "acyclic (RAG s')" |
|
1593 by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]]) |
|
1594 qed |
|
1595 |
|
1596 lemma preced_kept: "the_preced s = the_preced s'" |
|
1597 by (auto simp: s_def the_preced_def preced_def) |
|
1598 |
|
1599 end |
|
1600 |
1204 locale step_P_cps_ne =step_P_cps + |
1601 locale step_P_cps_ne =step_P_cps + |
|
1602 fixes th' |
1205 assumes ne: "wq s' cs \<noteq> []" |
1603 assumes ne: "wq s' cs \<noteq> []" |
|
1604 defines th'_def: "th' \<equiv> hd (wq s' cs)" |
1206 |
1605 |
1207 locale step_P_cps_e =step_P_cps + |
1606 locale step_P_cps_e =step_P_cps + |
1208 assumes ee: "wq s' cs = []" |
1607 assumes ee: "wq s' cs = []" |
1209 |
1608 |
1210 context step_P_cps_e |
1609 context step_P_cps_e |
1338 Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp |
1737 Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp |
1339 qed |
1738 qed |
1340 |
1739 |
1341 end |
1740 end |
1342 |
1741 |
1343 context step_P_cps_ne |
1742 lemma tRAG_ancestorsE: |
|
1743 assumes "x \<in> ancestors (tRAG s) u" |
|
1744 obtains th where "x = Th th" |
|
1745 proof - |
|
1746 from assms have "(u, x) \<in> (tRAG s)^+" |
|
1747 by (unfold ancestors_def, auto) |
|
1748 from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto |
|
1749 then obtain th where "x = Th th" |
|
1750 by (unfold tRAG_alt_def, auto) |
|
1751 from that[OF this] show ?thesis . |
|
1752 qed |
|
1753 |
|
1754 |
|
1755 context step_P_cps_ne |
1344 begin |
1756 begin |
1345 |
1757 |
1346 lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
1758 lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
1347 proof - |
1759 proof - |
1348 from step_RAG_p[OF vt_s[unfolded s_def]] and ne |
1760 from step_RAG_p[OF vt_s[unfolded s_def]] and ne |
1349 show ?thesis by (simp add:s_def) |
1761 show ?thesis by (simp add:s_def) |
1350 qed |
1762 qed |
1351 |
1763 |
|
1764 lemma cs_held: "(Cs cs, Th th') \<in> RAG s'" |
|
1765 proof - |
|
1766 have "(Cs cs, Th th') \<in> hRAG s'" |
|
1767 proof - |
|
1768 from ne |
|
1769 have " holding s' th' cs" |
|
1770 by (unfold th'_def holding_eq cs_holding_def, auto) |
|
1771 thus ?thesis |
|
1772 by (unfold hRAG_def, auto) |
|
1773 qed |
|
1774 thus ?thesis by (unfold RAG_split, auto) |
|
1775 qed |
|
1776 |
|
1777 lemma tRAG_s: |
|
1778 "tRAG s = tRAG s' \<union> {(Th th, Th th')}" |
|
1779 using RAG_tRAG_transfer[OF step_back_vt[OF vt_s[unfolded s_def]] RAG_s cs_held] . |
|
1780 |
|
1781 lemma cp_kept: |
|
1782 assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)" |
|
1783 shows "cp s th'' = cp s' th''" |
|
1784 proof - |
|
1785 have h: "subtree (tRAG s) (Th th'') = subtree (tRAG s') (Th th'')" |
|
1786 proof - |
|
1787 have "Th th' \<notin> subtree (tRAG s') (Th th'')" |
|
1788 proof |
|
1789 assume "Th th' \<in> subtree (tRAG s') (Th th'')" |
|
1790 thus False |
|
1791 proof(rule subtreeE) |
|
1792 assume "Th th' = Th th''" |
|
1793 from assms[unfolded tRAG_s ancestors_def, folded this] |
|
1794 show ?thesis by auto |
|
1795 next |
|
1796 assume "Th th'' \<in> ancestors (tRAG s') (Th th')" |
|
1797 moreover have "... \<subseteq> ancestors (tRAG s) (Th th')" |
|
1798 proof(rule ancestors_mono) |
|
1799 show "tRAG s' \<subseteq> tRAG s" by (unfold tRAG_s, auto) |
|
1800 qed |
|
1801 ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th')" by auto |
|
1802 moreover have "Th th' \<in> ancestors (tRAG s) (Th th)" |
|
1803 by (unfold tRAG_s, auto simp:ancestors_def) |
|
1804 ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th)" |
|
1805 by (auto simp:ancestors_def) |
|
1806 with assms show ?thesis by auto |
|
1807 qed |
|
1808 qed |
|
1809 from subtree_insert_next[OF this] |
|
1810 have "subtree (tRAG s' \<union> {(Th th, Th th')}) (Th th'') = subtree (tRAG s') (Th th'')" . |
|
1811 from this[folded tRAG_s] show ?thesis . |
|
1812 qed |
|
1813 show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) |
|
1814 qed |
|
1815 |
|
1816 lemma set_prop_split: |
|
1817 "A = {x. x \<in> A \<and> PP x} \<union> {x. x \<in> A \<and> \<not> PP x}" |
|
1818 by auto |
|
1819 |
|
1820 lemma f_image_union_eq: |
|
1821 assumes "f ` A = g ` A" |
|
1822 and "f ` B = g ` B" |
|
1823 shows "f ` (A \<union> B) = g ` (A \<union> B)" |
|
1824 using assms by auto |
|
1825 |
|
1826 (* ccc *) |
|
1827 |
|
1828 lemma cp_gen_update_stop: |
|
1829 assumes "u \<in> ancestors (tRAG s) (Th th)" |
|
1830 and "cp_gen s u = cp_gen s' u" |
|
1831 and "y \<in> ancestors (tRAG s) u" |
|
1832 shows "cp_gen s y = cp_gen s' y" |
|
1833 using assms(3) |
|
1834 proof(induct rule:wf_induct[OF vat_s.fsbttRAGs.wf]) |
|
1835 case (1 x) |
|
1836 show ?case (is "?L = ?R") |
|
1837 proof - |
|
1838 from tRAG_ancestorsE[OF 1(2)] |
|
1839 obtain th2 where eq_x: "x = Th th2" by blast |
|
1840 from vat_s.cp_gen_rec[OF this] |
|
1841 have "?L = |
|
1842 Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" . |
|
1843 also have "... = |
|
1844 Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)" |
|
1845 proof - |
|
1846 have "the_preced s th2 = the_preced s' th2" sorry |
|
1847 moreover have "cp_gen s ` RTree.children (tRAG s) x = |
|
1848 cp_gen s' ` RTree.children (tRAG s') x" |
|
1849 proof - |
|
1850 have "RTree.children (tRAG s) x = RTree.children (tRAG s') x" |
|
1851 proof(unfold tRAG_s, rule children_union_kept) |
|
1852 have start: "(Th th, Th th') \<in> tRAG s" |
|
1853 by (unfold tRAG_s, auto) |
|
1854 note x_u = 1(2) |
|
1855 show "x \<notin> Range {(Th th, Th th')}" |
|
1856 proof |
|
1857 assume "x \<in> Range {(Th th, Th th')}" |
|
1858 hence eq_x: "x = Th th'" using RangeE by auto |
|
1859 show False |
|
1860 proof(cases rule:vat_s.rtree_s.ancestors_headE[OF assms(1) start]) |
|
1861 case 1 |
|
1862 from x_u[folded this, unfolded eq_x] vat_s.acyclic_tRAG |
|
1863 show ?thesis by (auto simp:ancestors_def acyclic_def) |
|
1864 next |
|
1865 case 2 |
|
1866 with x_u[unfolded eq_x] |
|
1867 have "(Th th', Th th') \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
|
1868 with vat_s.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) |
|
1869 qed |
|
1870 qed |
|
1871 qed |
|
1872 moreover have "cp_gen s ` RTree.children (tRAG s) x = |
|
1873 cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A") |
|
1874 proof - |
|
1875 have h: "?A = ({y. y \<in> ?A \<and> y \<in> ancestors (tRAG s) u} \<union> |
|
1876 {y. y \<in> ?A \<and> \<not> (y \<in> ancestors (tRAG s) u)})" (is "_ = ?B \<union> ?C") |
|
1877 by (rule set_prop_split) |
|
1878 show ?thesis |
|
1879 proof(subst h, subst (3) h, rule f_image_union_eq) |
|
1880 show "?f ` ?B = ?g ` ?B" |
|
1881 proof(rule f_image_eq) |
|
1882 fix a |
|
1883 assume "a \<in> ?B" |
|
1884 hence h: "a \<in> RTree.children (tRAG s) x" "a \<in> ancestors (tRAG s) u" by auto |
|
1885 show "?f a = ?g a" |
|
1886 proof(rule 1(1)[rule_format]) |
|
1887 from h(2) show "a \<in> ancestors (tRAG s) u" . |
|
1888 next |
|
1889 from h(1) show "(a, x) \<in> tRAG s" |
|
1890 unfolding RTree.children_def by auto |
|
1891 qed |
|
1892 qed |
|
1893 next |
|
1894 show "?f ` ?C = ?g ` ?C" |
|
1895 proof(rule f_image_eq) |
|
1896 fix a |
|
1897 assume "a \<in> ?C" |
|
1898 hence h: "a \<in> RTree.children (tRAG s) x" "a \<notin> ancestors (tRAG s) u" by auto |
|
1899 from h(1) obtain th3 where eq_a: "a = Th th3" |
|
1900 by (unfold RTree.children_def tRAG_alt_def, auto) |
|
1901 thm cp_gen_def_cond[OF eq_a, folded eq_a] |
|
1902 show "?f a = ?g a" |
|
1903 proof(fold cp_gen_def_cond[OF eq_a, folded eq_a], rule cp_kept) |
|
1904 show "Th th3 \<notin> ancestors (tRAG s) (Th th)" |
|
1905 proof |
|
1906 assume "Th th3 \<in> ancestors (tRAG s) (Th th)" |
|
1907 from this[folded eq_a] have "(Th th, a) \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
|
1908 from plus_rpath[OF this] obtain xs1 |
|
1909 where h_a: "rpath (tRAG s) (Th th) xs1 a" "xs1 \<noteq> []" by auto |
|
1910 from assms(1) have "(Th th, u) \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
|
1911 from plus_rpath[OF this] obtain xs2 |
|
1912 where h_u: "rpath (tRAG s) (Th th) xs2 u" "xs2 \<noteq> []" by auto |
|
1913 show False |
|
1914 proof(cases rule:vat_s.rtree_s.rpath_overlap[OF h_a(1) h_u(1)]) |
|
1915 case (1 xs3) |
|
1916 (* ccc *) |
|
1917 qed |
|
1918 qed |
|
1919 qed |
|
1920 qed |
|
1921 qed |
|
1922 qed |
|
1923 ultimately show ?thesis by metis |
|
1924 qed |
|
1925 ultimately show ?thesis by simp |
|
1926 qed |
|
1927 also have "... = ?R" |
|
1928 by (fold vat_s'.cp_gen_rec[OF eq_x], simp) |
|
1929 finally show ?thesis . |
|
1930 qed |
|
1931 qed |
|
1932 |
|
1933 |
|
1934 |
|
1935 (* ccc *) |
1352 |
1936 |
1353 lemma eq_child_left: |
1937 lemma eq_child_left: |
1354 assumes nd: "(Th th, Th th') \<notin> (child s)^+" |
1938 assumes nd: "(Th th, Th th') \<notin> (child s)^+" |
1355 shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+" |
1939 shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+" |
1356 proof(induct rule:converse_trancl_induct) |
1940 proof(induct rule:converse_trancl_induct) |