242 RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}" |
242 RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}" |
243 unfolding RAG2_def RAG_def waits_def holds_def |
243 unfolding RAG2_def RAG_def waits_def holds_def |
244 using assms wq_distinct[OF vt(1), of"cs"] |
244 using assms wq_distinct[OF vt(1), of"cs"] |
245 by (auto simp add: Let_def wq_def) |
245 by (auto simp add: Let_def wq_def) |
246 |
246 |
247 lemma waiting_unique: |
247 (* |
|
248 lemma single_valued_waits2: |
|
249 assumes "vt s" |
|
250 shows "single_valuedP (waits2 s)" |
|
251 using assms |
|
252 apply(induct) |
|
253 apply(simp add: waits2_def waits_def) |
|
254 apply(erule step.cases) |
|
255 apply(auto simp add: Let_def waits2_def) |
|
256 unfolding single_valued_def waits2_def waits_def |
|
257 apply(auto) |
|
258 *) |
|
259 |
|
260 |
|
261 lemma waits2_unique: |
248 assumes "vt s" |
262 assumes "vt s" |
249 and "waits2 s th cs1" |
263 and "waits2 s th cs1" |
250 and "waits2 s th cs2" |
264 and "waits2 s th cs2" |
251 shows "cs1 = cs2" |
265 shows "cs1 = cs2" |
252 using assms |
266 using assms |
258 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
272 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
259 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
273 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
260 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
274 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
261 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
275 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
262 |
276 |
263 |
277 lemma single_valued_holds2: |
264 lemma rtrancl_eq_trancl [simp]: |
278 assumes "vt s" |
265 assumes "x \<noteq> y" |
279 shows "single_valuedP (\<lambda>cs th. holds2 s th cs)" |
266 shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+" |
280 unfolding single_valued_def holds2_def holds_def by simp |
267 using assms by (metis rtrancl_eq_or_trancl) |
281 |
|
282 |
|
283 lemma holds2_unique: |
|
284 assumes "holds2 s th1 cs" |
|
285 and "holds2 s th2 cs" |
|
286 shows "th1 = th2" |
|
287 using assms |
|
288 unfolding holds2_def holds_def by auto |
|
289 |
|
290 lemma single_valued_waits2: |
|
291 assumes "vt s" |
|
292 shows "single_valuedP (waits2 s)" |
|
293 by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique) |
|
294 |
|
295 |
|
296 (* was unique_RAG2 *) |
|
297 lemma single_valued_RAG2: |
|
298 assumes "vt s" |
|
299 shows "single_valued (RAG2 s)" |
|
300 using single_valued_waits2[OF assms] single_valued_holds2[OF assms] |
|
301 unfolding RAG2_def RAG_def |
|
302 unfolding single_valued_def |
|
303 unfolding holds2_def waits2_def |
|
304 by auto |
268 |
305 |
269 lemma acyclic_RAG_step: |
306 lemma acyclic_RAG_step: |
270 assumes vt: "vt s" |
307 assumes vt: "vt s" |
271 and stp: "step s e" |
308 and stp: "step s e" |
272 and ac: "acyclic (RAG2 s)" |
309 and ac: "acyclic (RAG2 s)" |
335 unfolding RAG2_def RAG_def by auto |
372 unfolding RAG2_def RAG_def by auto |
336 moreover |
373 moreover |
337 have "waits2 s nth cs'" |
374 have "waits2 s nth cs'" |
338 using b(2) unfolding RAG2_def RAG_def waits2_def by simp |
375 using b(2) unfolding RAG2_def RAG_def waits2_def by simp |
339 ultimately have "cs = cs'" |
376 ultimately have "cs = cs'" |
340 by (rule_tac waiting_unique[OF vt waits2_cs]) |
377 by (rule_tac waits2_unique[OF vt waits2_cs]) |
341 then show "False" using a b(1) by simp |
378 then show "False" using a b(1) by simp |
342 qed |
379 qed |
343 ultimately |
380 ultimately |
344 show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp |
381 show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp |
345 qed |
382 qed |
414 defer |
451 defer |
415 defer |
452 defer |
416 oops |
453 oops |
417 |
454 |
418 |
455 |
|
456 |
|
457 |
|
458 |
|
459 |
|
460 lemma dchain_unique: |
|
461 assumes vt: "vt s" |
|
462 and th1_d: "(n, Th th1) \<in> (RAG2 s)^+" |
|
463 and th1_r: "th1 \<in> readys s" |
|
464 and th2_d: "(n, Th th2) \<in> (RAG2 s)^+" |
|
465 and th2_r: "th2 \<in> readys s" |
|
466 shows "th1 = th2" |
|
467 proof(rule ccontr) |
|
468 assume neq: "th1 \<noteq> th2" |
|
469 hence "Th th1 \<noteq> Th th2" by simp |
|
470 from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt] |
|
471 have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" |
|
472 unfolding single_valued_def by auto |
|
473 then show "False" |
|
474 proof |
|
475 assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+" |
|
476 from trancl_split [OF this] |
|
477 obtain n where dd: "(Th th1, n) \<in> RAG2 s" by auto |
|
478 then obtain cs where eq_n: "n = Cs cs" |
|
479 unfolding RAG2_def RAG_def by (case_tac n) (auto) |
|
480 from dd eq_n have "th1 \<notin> readys s" |
|
481 unfolding RAG2_def RAG_def waits2_def readys_def by (auto) |
|
482 with th1_r show ?thesis by auto |
|
483 next |
|
484 assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" |
|
485 from trancl_split [OF this] |
|
486 obtain n where dd: "(Th th2, n) \<in> RAG2 s" by auto |
|
487 then obtain cs where eq_n: "n = Cs cs" |
|
488 unfolding RAG2_def RAG_def by (case_tac n) (auto) |
|
489 from dd eq_n have "th2 \<notin> readys s" |
|
490 unfolding RAG2_def RAG_def waits2_def readys_def by (auto) |
|
491 with th2_r show ?thesis by auto |
|
492 qed |
|
493 qed |
|
494 |
|
495 |
|
496 |
419 end |
497 end |