| changeset 63 | b620a2a0806a |
| parent 62 | 031d2ae9c9b8 |
| 62:031d2ae9c9b8 | 63:b620a2a0806a |
|---|---|
89 assumes "vt s'" |
89 assumes "vt s'" |
90 assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
90 assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
91 and "(Cs cs, Th th'') \<in> RAG s'" |
91 and "(Cs cs, Th th'') \<in> RAG s'" |
92 shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R") |
92 shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R") |
93 proof - |
93 proof - |
94 interpret vt_s': valid_trace "s'" using assms(1) |
|
95 by (unfold_locales, simp) |
|
94 interpret rtree: rtree "RAG s'" |
96 interpret rtree: rtree "RAG s'" |
95 proof |
97 proof |
96 show "single_valued (RAG s')" |
98 show "single_valued (RAG s')" |
97 apply (intro_locales) |
99 apply (intro_locales) |
98 by (unfold single_valued_def, |
100 by (unfold single_valued_def, |
99 auto intro:unique_RAG[OF assms(1)]) |
101 auto intro:vt_s'.unique_RAG) |
100 |
102 |
101 show "acyclic (RAG s')" |
103 show "acyclic (RAG s')" |
102 by (rule acyclic_RAG[OF assms(1)]) |
104 by (rule vt_s'.acyclic_RAG) |
103 qed |
105 qed |
104 { fix n1 n2 |
106 { fix n1 n2 |
105 assume "(n1, n2) \<in> ?L" |
107 assume "(n1, n2) \<in> ?L" |
106 from this[unfolded tRAG_alt_def] |
108 from this[unfolded tRAG_alt_def] |
107 obtain th1 th2 cs' where |
109 obtain th1 th2 cs' where |
150 by (unfold eq_n tRAG_alt_def, auto) |
152 by (unfold eq_n tRAG_alt_def, auto) |
151 qed |
153 qed |
152 } ultimately show ?thesis by auto |
154 } ultimately show ?thesis by auto |
153 qed |
155 qed |
154 |
156 |
157 context valid_trace |
|
158 begin |
|
159 |
|
160 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] |
|
161 |
|
162 end |
|
163 |
|
155 lemma cp_alt_def: |
164 lemma cp_alt_def: |
156 "cp s th = |
165 "cp s th = |
157 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
166 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
158 proof - |
167 proof - |
159 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = |
168 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = |
219 have "(a, x) \<in> (RAG s)^*" by auto |
228 have "(a, x) \<in> (RAG s)^*" by auto |
220 hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def) |
229 hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def) |
221 } thus ?thesis by auto |
230 } thus ?thesis by auto |
222 qed |
231 qed |
223 |
232 |
233 lemma tRAG_trancl_eq: |
|
234 "{th'. (Th th', Th th) \<in> (tRAG s)^+} = |
|
235 {th'. (Th th', Th th) \<in> (RAG s)^+}" |
|
236 (is "?L = ?R") |
|
237 proof - |
|
238 { fix th' |
|
239 assume "th' \<in> ?L" |
|
240 hence "(Th th', Th th) \<in> (tRAG s)^+" by auto |
|
241 from tranclD[OF this] |
|
242 obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto |
|
243 from tRAG_subtree_RAG[of s] and this(2) |
|
244 have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) |
|
245 moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto |
|
246 ultimately have "th' \<in> ?R" by auto |
|
247 } moreover |
|
248 { fix th' |
|
249 assume "th' \<in> ?R" |
|
250 hence "(Th th', Th th) \<in> (RAG s)^+" by (auto) |
|
251 from plus_rpath[OF this] |
|
252 obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto |
|
253 hence "(Th th', Th th) \<in> (tRAG s)^+" |
|
254 proof(induct xs arbitrary:th' th rule:length_induct) |
|
255 case (1 xs th' th) |
|
256 then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) |
|
257 show ?case |
|
258 proof(cases "xs1") |
|
259 case Nil |
|
260 from 1(2)[unfolded Cons1 Nil] |
|
261 have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . |
|
262 hence "(Th th', x1) \<in> (RAG s)" by (cases, simp) |
|
263 then obtain cs where "x1 = Cs cs" |
|
264 by (unfold s_RAG_def, auto) |
|
265 from rpath_nnl_lastE[OF rp[unfolded this]] |
|
266 show ?thesis by auto |
|
267 next |
|
268 case (Cons x2 xs2) |
|
269 from 1(2)[unfolded Cons1[unfolded this]] |
|
270 have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . |
|
271 from rpath_edges_on[OF this] |
|
272 have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" . |
|
273 have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
274 by (simp add: edges_on_unfold) |
|
275 with eds have rg1: "(Th th', x1) \<in> RAG s" by auto |
|
276 then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) |
|
277 have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
278 by (simp add: edges_on_unfold) |
|
279 from this eds |
|
280 have rg2: "(x1, x2) \<in> RAG s" by auto |
|
281 from this[unfolded eq_x1] |
|
282 obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) |
|
283 from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] |
|
284 have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto) |
|
285 from rp have "rpath (RAG s) x2 xs2 (Th th)" |
|
286 by (elim rpath_ConsE, simp) |
|
287 from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . |
|
288 show ?thesis |
|
289 proof(cases "xs2 = []") |
|
290 case True |
|
291 from rpath_nilE[OF rp'[unfolded this]] |
|
292 have "th1 = th" by auto |
|
293 from rt1[unfolded this] show ?thesis by auto |
|
294 next |
|
295 case False |
|
296 from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] |
|
297 have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp |
|
298 with rt1 show ?thesis by auto |
|
299 qed |
|
300 qed |
|
301 qed |
|
302 hence "th' \<in> ?L" by auto |
|
303 } ultimately show ?thesis by blast |
|
304 qed |
|
305 |
|
306 lemma tRAG_trancl_eq_Th: |
|
307 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
|
308 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
|
309 using tRAG_trancl_eq by auto |
|
310 |
|
311 lemma dependants_alt_def: |
|
312 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
|
313 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
|
314 |
|
315 context valid_trace |
|
316 begin |
|
317 |
|
318 lemma count_eq_tRAG_plus: |
|
319 assumes "cntP s th = cntV s th" |
|
320 shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
|
321 using assms count_eq_dependants dependants_alt_def eq_dependants by auto |
|
322 |
|
323 lemma count_eq_RAG_plus: |
|
324 assumes "cntP s th = cntV s th" |
|
325 shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
|
326 using assms count_eq_dependants cs_dependants_def eq_RAG by auto |
|
327 |
|
328 lemma count_eq_RAG_plus_Th: |
|
329 assumes "cntP s th = cntV s th" |
|
330 shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
|
331 using count_eq_RAG_plus[OF assms] by auto |
|
332 |
|
333 lemma count_eq_tRAG_plus_Th: |
|
334 assumes "cntP s th = cntV s th" |
|
335 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
|
336 using count_eq_tRAG_plus[OF assms] by auto |
|
337 |
|
338 end |
|
339 |
|
224 lemma tRAG_subtree_eq: |
340 lemma tRAG_subtree_eq: |
225 "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}" |
341 "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}" |
226 (is "?L = ?R") |
342 (is "?L = ?R") |
227 proof - |
343 proof - |
228 { fix n |
344 { fix n |
229 assume "n \<in> ?L" |
345 assume h: "n \<in> ?L" |
230 with subtree_nodeE[OF this] |
346 hence "n \<in> ?R" |
231 obtain th' where "n = Th th'" "Th th' \<in> subtree (tRAG s) (Th th)" by auto |
347 by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) |
232 with tRAG_subtree_RAG[of s "Th th"] |
|
233 have "n \<in> ?R" by auto |
|
234 } moreover { |
348 } moreover { |
235 fix n |
349 fix n |
236 assume "n \<in> ?R" |
350 assume "n \<in> ?R" |
237 then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" |
351 then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" |
238 by (auto simp:subtree_def) |
352 by (auto simp:subtree_def) |
239 from star_rpath[OF this(2)] |
353 from rtranclD[OF this(2)] |
240 obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto |
354 have "n \<in> ?L" |
241 hence "Th th' \<in> subtree (tRAG s) (Th th)" |
355 proof |
242 proof(induct xs arbitrary:th' th rule:length_induct) |
356 assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+" |
243 case (1 xs th' th) |
357 with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto |
244 show ?case |
358 thus ?thesis using subtree_def tRAG_trancl_eq by fastforce |
245 proof(cases xs) |
359 qed (insert h, auto simp:subtree_def) |
246 case Nil |
|
247 from rpath_nilE[OF 1(2)[unfolded this]] |
|
248 have "th' = th" by auto |
|
249 thus ?thesis by (auto simp:subtree_def) |
|
250 next |
|
251 case (Cons x1 xs1) note Cons1 = Cons |
|
252 show ?thesis |
|
253 proof(cases "xs1") |
|
254 case Nil |
|
255 from 1(2)[unfolded Cons[unfolded this]] |
|
256 have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . |
|
257 hence "(Th th', x1) \<in> (RAG s)" by (cases, simp) |
|
258 then obtain cs where "x1 = Cs cs" |
|
259 by (unfold s_RAG_def, auto) |
|
260 from rpath_nnl_lastE[OF rp[unfolded this]] |
|
261 show ?thesis by auto |
|
262 next |
|
263 case (Cons x2 xs2) |
|
264 from 1(2)[unfolded Cons1[unfolded this]] |
|
265 have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . |
|
266 from rpath_edges_on[OF this] |
|
267 have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" . |
|
268 have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
269 by (simp add: edges_on_unfold) |
|
270 with eds have rg1: "(Th th', x1) \<in> RAG s" by auto |
|
271 then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) |
|
272 have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)" |
|
273 by (simp add: edges_on_unfold) |
|
274 from this eds |
|
275 have rg2: "(x1, x2) \<in> RAG s" by auto |
|
276 from this[unfolded eq_x1] |
|
277 obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) |
|
278 from rp have "rpath (RAG s) x2 xs2 (Th th)" |
|
279 by (elim rpath_ConsE, simp) |
|
280 from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . |
|
281 from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons] |
|
282 have "Th th1 \<in> subtree (tRAG s) (Th th)" by simp |
|
283 moreover have "(Th th', Th th1) \<in> (tRAG s)^*" |
|
284 proof - |
|
285 from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] |
|
286 show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto) |
|
287 qed |
|
288 ultimately show ?thesis by (auto simp:subtree_def) |
|
289 qed |
|
290 qed |
|
291 qed |
|
292 from this[folded h(1)] |
|
293 have "n \<in> ?L" . |
|
294 } ultimately show ?thesis by auto |
360 } ultimately show ?thesis by auto |
295 qed |
361 qed |
296 |
362 |
297 lemma threads_set_eq: |
363 lemma threads_set_eq: |
298 "the_thread ` (subtree (tRAG s) (Th th)) = |
364 "the_thread ` (subtree (tRAG s) (Th th)) = |
323 obtain th where eq_a: "a = Th th" by auto |
389 obtain th where eq_a: "a = Th th" by auto |
324 show "cp_gen s a = (cp s \<circ> the_thread) a" |
390 show "cp_gen s a = (cp s \<circ> the_thread) a" |
325 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
391 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
326 qed |
392 qed |
327 |
393 |
328 locale valid_trace = |
|
329 fixes s |
|
330 assumes vt : "vt s" |
|
331 |
394 |
332 context valid_trace |
395 context valid_trace |
333 begin |
396 begin |
397 |
|
398 lemma RAG_threads: |
|
399 assumes "(Th th) \<in> Field (RAG s)" |
|
400 shows "th \<in> threads s" |
|
401 using assms |
|
402 by (metis Field_def UnE dm_RAG_threads range_in vt) |
|
403 |
|
404 lemma subtree_tRAG_thread: |
|
405 assumes "th \<in> threads s" |
|
406 shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R") |
|
407 proof - |
|
408 have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
409 by (unfold tRAG_subtree_eq, simp) |
|
410 also have "... \<subseteq> ?R" |
|
411 proof |
|
412 fix x |
|
413 assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
414 then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto |
|
415 from this(2) |
|
416 show "x \<in> ?R" |
|
417 proof(cases rule:subtreeE) |
|
418 case 1 |
|
419 thus ?thesis by (simp add: assms h(1)) |
|
420 next |
|
421 case 2 |
|
422 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) |
|
423 qed |
|
424 qed |
|
425 finally show ?thesis . |
|
426 qed |
|
334 |
427 |
335 lemma readys_root: |
428 lemma readys_root: |
336 assumes "th \<in> readys s" |
429 assumes "th \<in> readys s" |
337 shows "root (RAG s) (Th th)" |
430 shows "root (RAG s) (Th th)" |
338 proof - |
431 proof - |
367 lemma not_in_thread_isolated: |
460 lemma not_in_thread_isolated: |
368 assumes "th \<notin> threads s" |
461 assumes "th \<notin> threads s" |
369 shows "(Th th) \<notin> Field (RAG s)" |
462 shows "(Th th) \<notin> Field (RAG s)" |
370 proof |
463 proof |
371 assume "(Th th) \<in> Field (RAG s)" |
464 assume "(Th th) \<in> Field (RAG s)" |
372 with dm_RAG_threads[OF vt] and range_in[OF vt] assms |
465 with dm_RAG_threads and range_in assms |
373 show False by (unfold Field_def, blast) |
466 show False by (unfold Field_def, blast) |
374 qed |
467 qed |
375 |
468 |
376 lemma wf_RAG: "wf (RAG s)" |
469 lemma wf_RAG: "wf (RAG s)" |
377 proof(rule finite_acyclic_wf) |
470 proof(rule finite_acyclic_wf) |
378 from finite_RAG[OF vt] show "finite (RAG s)" . |
471 from finite_RAG show "finite (RAG s)" . |
379 next |
472 next |
380 from acyclic_RAG[OF vt] show "acyclic (RAG s)" . |
473 from acyclic_RAG show "acyclic (RAG s)" . |
381 qed |
474 qed |
382 |
475 |
383 lemma sgv_wRAG: "single_valued (wRAG s)" |
476 lemma sgv_wRAG: "single_valued (wRAG s)" |
384 using waiting_unique[OF vt] |
477 using waiting_unique |
385 by (unfold single_valued_def wRAG_def, auto) |
478 by (unfold single_valued_def wRAG_def, auto) |
386 |
479 |
387 lemma sgv_hRAG: "single_valued (hRAG s)" |
480 lemma sgv_hRAG: "single_valued (hRAG s)" |
388 using holding_unique |
481 using holding_unique |
389 by (unfold single_valued_def hRAG_def, auto) |
482 by (unfold single_valued_def hRAG_def, auto) |
392 by (unfold tRAG_def, rule single_valued_relcomp, |
485 by (unfold tRAG_def, rule single_valued_relcomp, |
393 insert sgv_wRAG sgv_hRAG, auto) |
486 insert sgv_wRAG sgv_hRAG, auto) |
394 |
487 |
395 lemma acyclic_tRAG: "acyclic (tRAG s)" |
488 lemma acyclic_tRAG: "acyclic (tRAG s)" |
396 proof(unfold tRAG_def, rule acyclic_compose) |
489 proof(unfold tRAG_def, rule acyclic_compose) |
397 show "acyclic (RAG s)" using acyclic_RAG[OF vt] . |
490 show "acyclic (RAG s)" using acyclic_RAG . |
398 next |
491 next |
399 show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
492 show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
400 next |
493 next |
401 show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
494 show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto |
402 qed |
495 qed |
403 |
496 |
404 lemma sgv_RAG: "single_valued (RAG s)" |
497 lemma sgv_RAG: "single_valued (RAG s)" |
405 using unique_RAG[OF vt] by (auto simp:single_valued_def) |
498 using unique_RAG by (auto simp:single_valued_def) |
406 |
499 |
407 lemma rtree_RAG: "rtree (RAG s)" |
500 lemma rtree_RAG: "rtree (RAG s)" |
408 using sgv_RAG acyclic_RAG[OF vt] |
501 using sgv_RAG acyclic_RAG |
409 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
502 by (unfold rtree_def rtree_axioms_def sgv_def, auto) |
503 |
|
410 end |
504 end |
411 |
505 |
412 |
506 |
413 sublocale valid_trace < rtree_RAG: rtree "RAG s" |
507 sublocale valid_trace < rtree_RAG: rtree "RAG s" |
414 proof |
508 proof |
415 show "single_valued (RAG s)" |
509 show "single_valued (RAG s)" |
416 apply (intro_locales) |
510 apply (intro_locales) |
417 by (unfold single_valued_def, |
511 by (unfold single_valued_def, |
418 auto intro:unique_RAG[OF vt]) |
512 auto intro:unique_RAG) |
419 |
513 |
420 show "acyclic (RAG s)" |
514 show "acyclic (RAG s)" |
421 by (rule acyclic_RAG[OF vt]) |
515 by (rule acyclic_RAG) |
422 qed |
516 qed |
423 |
517 |
424 sublocale valid_trace < rtree_s: rtree "tRAG s" |
518 sublocale valid_trace < rtree_s: rtree "tRAG s" |
425 proof(unfold_locales) |
519 proof(unfold_locales) |
426 from sgv_tRAG show "single_valued (tRAG s)" . |
520 from sgv_tRAG show "single_valued (tRAG s)" . |
430 |
524 |
431 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" |
525 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" |
432 proof - |
526 proof - |
433 show "fsubtree (RAG s)" |
527 show "fsubtree (RAG s)" |
434 proof(intro_locales) |
528 proof(intro_locales) |
435 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG[OF vt]] . |
529 show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . |
436 next |
530 next |
437 show "fsubtree_axioms (RAG s)" |
531 show "fsubtree_axioms (RAG s)" |
438 proof(unfold fsubtree_axioms_def) |
532 proof(unfold fsubtree_axioms_def) |
439 find_theorems wf RAG |
533 find_theorems wf RAG |
440 from wf_RAG show "wf (RAG s)" . |
534 from wf_RAG show "wf (RAG s)" . |
448 proof - |
542 proof - |
449 have "fbranch (tRAG s)" |
543 have "fbranch (tRAG s)" |
450 proof(unfold tRAG_def, rule fbranch_compose) |
544 proof(unfold tRAG_def, rule fbranch_compose) |
451 show "fbranch (wRAG s)" |
545 show "fbranch (wRAG s)" |
452 proof(rule finite_fbranchI) |
546 proof(rule finite_fbranchI) |
453 from finite_RAG[OF vt] show "finite (wRAG s)" |
547 from finite_RAG show "finite (wRAG s)" |
454 by (unfold RAG_split, auto) |
548 by (unfold RAG_split, auto) |
455 qed |
549 qed |
456 next |
550 next |
457 show "fbranch (hRAG s)" |
551 show "fbranch (hRAG s)" |
458 proof(rule finite_fbranchI) |
552 proof(rule finite_fbranchI) |
459 from finite_RAG[OF vt] |
553 from finite_RAG |
460 show "finite (hRAG s)" by (unfold RAG_split, auto) |
554 show "finite (hRAG s)" by (unfold RAG_split, auto) |
461 qed |
555 qed |
462 qed |
556 qed |
463 moreover have "wf (tRAG s)" |
557 moreover have "wf (tRAG s)" |
464 proof(rule wf_subset) |
558 proof(rule wf_subset) |
594 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
688 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
595 thus ?thesis |
689 thus ?thesis |
596 by (unfold cs_holding_def, auto) |
690 by (unfold cs_holding_def, auto) |
597 qed |
691 qed |
598 |
692 |
693 context valid_trace |
|
694 begin |
|
695 |
|
599 lemma next_th_waiting: |
696 lemma next_th_waiting: |
600 assumes vt: "vt s" |
697 assumes nxt: "next_th s th cs th'" |
601 and nxt: "next_th s th cs th'" |
|
602 shows "waiting (wq s) th' cs" |
698 shows "waiting (wq s) th' cs" |
603 proof - |
699 proof - |
604 from nxt[unfolded next_th_def] |
700 from nxt[unfolded next_th_def] |
605 obtain rest where h: "wq s cs = th # rest" |
701 obtain rest where h: "wq s cs = th # rest" |
606 "rest \<noteq> []" |
702 "rest \<noteq> []" |
607 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
703 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
608 from wq_distinct[OF vt, of cs, unfolded h] |
704 from wq_distinct[of cs, unfolded h] |
609 have dst: "distinct (th # rest)" . |
705 have dst: "distinct (th # rest)" . |
610 have in_rest: "th' \<in> set rest" |
706 have in_rest: "th' \<in> set rest" |
611 proof(unfold h, rule someI2) |
707 proof(unfold h, rule someI2) |
612 show "distinct rest \<and> set rest = set rest" using dst by auto |
708 show "distinct rest \<and> set rest = set rest" using dst by auto |
613 next |
709 next |
620 by (unfold h(1), insert in_rest dst, auto) |
716 by (unfold h(1), insert in_rest dst, auto) |
621 ultimately show ?thesis by (auto simp:cs_waiting_def) |
717 ultimately show ?thesis by (auto simp:cs_waiting_def) |
622 qed |
718 qed |
623 |
719 |
624 lemma next_th_RAG: |
720 lemma next_th_RAG: |
625 assumes vt: "vt s" |
721 assumes nxt: "next_th (s::event list) th cs th'" |
626 and nxt: "next_th s th cs th'" |
|
627 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
722 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
628 using assms next_th_holding next_th_waiting |
723 using vt assms next_th_holding next_th_waiting |
629 by (unfold s_RAG_def, simp) |
724 by (unfold s_RAG_def, simp) |
725 |
|
726 end |
|
630 |
727 |
631 -- {* A useless definition *} |
728 -- {* A useless definition *} |
632 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
729 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set" |
633 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
730 where "cps s = {(th, cp s th) | th . th \<in> threads s}" |
634 |
731 |
907 | |
1004 | |
908 th7 ----| |
1005 th7 ----| |
909 *) |
1006 *) |
910 |
1007 |
911 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'" |
1008 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'" |
912 using next_th_RAG[OF vat_s'.vt nt] . |
1009 using next_th_RAG[OF nt] . |
913 |
1010 |
914 lemma ancestors_th': |
1011 lemma ancestors_th': |
915 "ancestors (RAG s') (Th th') = {Th th, Cs cs}" |
1012 "ancestors (RAG s') (Th th') = {Th th, Cs cs}" |
916 proof - |
1013 proof - |
917 have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}" |
1014 have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}" |
1173 thus ?thesis by (unfold RAG_split, auto) |
1270 thus ?thesis by (unfold RAG_split, auto) |
1174 qed |
1271 qed |
1175 |
1272 |
1176 lemma tRAG_s: |
1273 lemma tRAG_s: |
1177 "tRAG s = tRAG s' \<union> {(Th th, Th th')}" |
1274 "tRAG s = tRAG s' \<union> {(Th th, Th th')}" |
1178 using RAG_tRAG_transfer[OF step_back_vt[OF vt_s[unfolded s_def]] RAG_s cs_held] . |
1275 using RAG_tRAG_transfer[OF RAG_s cs_held] . |
1179 |
1276 |
1180 lemma cp_kept: |
1277 lemma cp_kept: |
1181 assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)" |
1278 assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)" |
1182 shows "cp s th'' = cp s' th''" |
1279 shows "cp s th'' = cp s' th''" |
1183 proof - |
1280 proof - |