413 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
414 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
414 and xy: "(x, y) \<in> r" |
415 and xy: "(x, y) \<in> r" |
415 and xz: "(x, z) \<in> r^+" |
416 and xz: "(x, z) \<in> r^+" |
416 and neq: "y \<noteq> z" |
417 and neq: "y \<noteq> z" |
417 shows "(y, z) \<in> r^+" |
418 shows "(y, z) \<in> r^+" |
418 proof - |
419 by (metis neq rtranclD tranclD unique xy xz) |
419 from xz and neq show ?thesis |
|
420 proof(induct) |
|
421 case (base ya) |
|
422 have "(x, ya) \<in> r" by fact |
|
423 from unique [OF xy this] have "y = ya" . |
|
424 with base show ?case by auto |
|
425 next |
|
426 case (step ya z) |
|
427 show ?case |
|
428 proof(cases "y = ya") |
|
429 case True |
|
430 from step True show ?thesis by simp |
|
431 next |
|
432 case False |
|
433 from step False |
|
434 show ?thesis by auto |
|
435 qed |
|
436 qed |
|
437 qed |
|
438 |
420 |
439 lemma unique_base: |
421 lemma unique_base: |
440 fixes r x y z |
422 fixes r x y z |
441 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
423 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
442 and xy: "(x, y) \<in> r" |
424 and xy: "(x, y) \<in> r" |
443 and xz: "(x, z) \<in> r^+" |
425 and xz: "(x, z) \<in> r^+" |
444 and neq_yz: "y \<noteq> z" |
426 and neq_yz: "y \<noteq> z" |
445 shows "(y, z) \<in> r^+" |
427 shows "(y, z) \<in> r^+" |
446 proof - |
428 by (metis neq_yz unique unique_minus xy xz) |
447 from xz neq_yz show ?thesis |
|
448 proof(induct) |
|
449 case (base ya) |
|
450 from xy unique base show ?case by auto |
|
451 next |
|
452 case (step ya z) |
|
453 show ?case |
|
454 proof(cases "y = ya") |
|
455 case True |
|
456 from True step show ?thesis by auto |
|
457 next |
|
458 case False |
|
459 from False step |
|
460 have "(y, ya) \<in> r\<^sup>+" by auto |
|
461 with step show ?thesis by auto |
|
462 qed |
|
463 qed |
|
464 qed |
|
465 |
429 |
466 lemma unique_chain: |
430 lemma unique_chain: |
467 fixes r x y z |
431 fixes r x y z |
468 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
432 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
469 and xy: "(x, y) \<in> r^+" |
433 and xy: "(x, y) \<in> r^+" |
670 |
634 |
671 lemma step_v_get_hold: |
635 lemma step_v_get_hold: |
672 "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False" |
636 "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False" |
673 apply (unfold cs_holding_def next_th_def wq_def, |
637 apply (unfold cs_holding_def next_th_def wq_def, |
674 auto simp:Let_def) |
638 auto simp:Let_def) |
675 proof - |
639 by (metis (lifting, full_types) List.member_def distinct.simps(2) hd_in_set member_rec(2) someI_ex step_back_vt wq_def wq_distinct) |
676 fix rest |
|
677 assume vt: "vt (V th cs # s)" |
|
678 and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest" |
|
679 and nrest: "rest \<noteq> []" |
|
680 and ni: "hd (SOME q. distinct q \<and> set q = set rest) |
|
681 \<notin> set (SOME q. distinct q \<and> set q = set rest)" |
|
682 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
683 proof(rule someI2) |
|
684 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq |
|
685 show "distinct rest \<and> set rest = set rest" by auto |
|
686 next |
|
687 fix x assume "distinct x \<and> set x = set rest" |
|
688 hence "set x = set rest" by auto |
|
689 with nrest |
|
690 show "x \<noteq> []" by (case_tac x, auto) |
|
691 qed |
|
692 with ni show "False" by auto |
|
693 qed |
|
694 |
640 |
695 lemma step_v_release_inv[elim_format]: |
641 lemma step_v_release_inv[elim_format]: |
696 "\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> |
642 "\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> |
697 c = cs \<and> t = th" |
643 c = cs \<and> t = th" |
698 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) |
644 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) |
716 qed |
662 qed |
717 qed |
663 qed |
718 |
664 |
719 lemma step_v_waiting_mono: |
665 lemma step_v_waiting_mono: |
720 "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c" |
666 "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c" |
721 proof - |
667 by (metis abs2 block_pre cs_waiting_def event.simps(20)) |
722 fix t c |
|
723 let ?s' = "(V th cs # s)" |
|
724 assume vt: "vt ?s'" |
|
725 and wt: "waiting (wq ?s') t c" |
|
726 show "waiting (wq s) t c" |
|
727 proof(cases "c = cs") |
|
728 case False |
|
729 assume neq_cs: "c \<noteq> cs" |
|
730 hence "waiting (wq ?s') t c = waiting (wq s) t c" |
|
731 by (unfold cs_waiting_def wq_def, auto simp:Let_def) |
|
732 with wt show ?thesis by simp |
|
733 next |
|
734 case True |
|
735 with wt show ?thesis |
|
736 apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) |
|
737 proof - |
|
738 fix a list |
|
739 assume not_in: "t \<notin> set list" |
|
740 and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)" |
|
741 and eq_wq: "wq_fun (schs s) cs = a # list" |
|
742 have "set (SOME q. distinct q \<and> set q = set list) = set list" |
|
743 proof(rule someI2) |
|
744 from wq_distinct [OF step_back_vt[OF vt], of cs] |
|
745 and eq_wq[folded wq_def] |
|
746 show "distinct list \<and> set list = set list" by auto |
|
747 next |
|
748 fix x assume "distinct x \<and> set x = set list" |
|
749 thus "set x = set list" by auto |
|
750 qed |
|
751 with not_in is_in show "t = a" by auto |
|
752 next |
|
753 fix list |
|
754 assume is_waiting: "waiting (wq (V th cs # s)) t cs" |
|
755 and eq_wq: "wq_fun (schs s) cs = t # list" |
|
756 hence "t \<in> set list" |
|
757 apply (unfold wq_def, auto simp:Let_def cs_waiting_def) |
|
758 proof - |
|
759 assume " t \<in> set (SOME q. distinct q \<and> set q = set list)" |
|
760 moreover have "\<dots> = set list" |
|
761 proof(rule someI2) |
|
762 from wq_distinct [OF step_back_vt[OF vt], of cs] |
|
763 and eq_wq[folded wq_def] |
|
764 show "distinct list \<and> set list = set list" by auto |
|
765 next |
|
766 fix x assume "distinct x \<and> set x = set list" |
|
767 thus "set x = set list" by auto |
|
768 qed |
|
769 ultimately show "t \<in> set list" by simp |
|
770 qed |
|
771 with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def] |
|
772 show False by auto |
|
773 qed |
|
774 qed |
|
775 qed |
|
776 |
668 |
777 lemma step_depend_v: |
669 lemma step_depend_v: |
778 fixes th::thread |
670 fixes th::thread |
779 assumes vt: |
671 assumes vt: |
780 "vt (V th cs#s)" |
672 "vt (V th cs#s)" |
1201 assumes vt: "vt s" |
1081 assumes vt: "vt s" |
1202 and neq_th: "th \<noteq> thread" |
1082 and neq_th: "th \<noteq> thread" |
1203 and eq_wq: "wq s cs = thread#rest" |
1083 and eq_wq: "wq s cs = thread#rest" |
1204 and not_in: "th \<notin> set rest" |
1084 and not_in: "th \<notin> set rest" |
1205 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1085 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1206 proof - |
1086 using assms |
1207 from assms show ?thesis |
1087 apply (auto simp:readys_def) |
1208 apply (auto simp:readys_def) |
1088 apply(simp add:s_waiting_def[folded wq_def]) |
1209 apply(simp add:s_waiting_def[folded wq_def]) |
1089 apply (erule_tac x = csa in allE) |
1210 apply (erule_tac x = csa in allE) |
1090 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
1211 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
1091 apply (case_tac "csa = cs", simp) |
1212 apply (case_tac "csa = cs", simp) |
1092 apply (erule_tac x = cs in allE) |
1213 apply (erule_tac x = cs in allE) |
1093 apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) |
1214 apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) |
1094 apply(auto simp add: wq_def) |
1215 apply(auto simp add: wq_def) |
1095 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
1216 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
1096 by (metis (lifting, full_types) distinct.simps(2) someI_ex wq_def wq_distinct) |
1217 proof - |
|
1218 assume th_nin: "th \<notin> set rest" |
|
1219 and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
|
1220 and eq_wq: "wq_fun (schs s) cs = thread # rest" |
|
1221 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
1222 proof(rule someI2) |
|
1223 from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def] |
|
1224 show "distinct rest \<and> set rest = set rest" by auto |
|
1225 next |
|
1226 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
1227 qed |
|
1228 with th_nin th_in show False by auto |
|
1229 qed |
|
1230 qed |
|
1231 |
1097 |
1232 lemma chain_building: |
1098 lemma chain_building: |
1233 assumes vt: "vt s" |
1099 assumes vt: "vt s" |
1234 shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)" |
1100 shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)" |
1235 proof - |
1101 proof - |
1402 moreover have cs_not_in: |
1268 moreover have cs_not_in: |
1403 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
1269 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
1404 apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) |
1270 apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) |
1405 apply (unfold holdents_def, unfold step_depend_v[OF vtv], |
1271 apply (unfold holdents_def, unfold step_depend_v[OF vtv], |
1406 auto simp:next_th_def) |
1272 auto simp:next_th_def) |
1407 proof - |
1273 apply (metis (lifting, full_types) hd_in_set hd_np_in someI_ex) |
1408 fix rest |
1274 by (metis (lifting, full_types) hd_in_set hd_np_in someI_ex) |
1409 assume dst: "distinct (rest::thread list)" |
|
1410 and ne: "rest \<noteq> []" |
|
1411 and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
1412 moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
1413 proof(rule someI2) |
|
1414 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
1415 next |
|
1416 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
1417 qed |
|
1418 ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> |
|
1419 set (SOME q. distinct q \<and> set q = set rest)" by simp |
|
1420 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
1421 proof(rule someI2) |
|
1422 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
1423 next |
|
1424 fix x assume " distinct x \<and> set x = set rest" with ne |
|
1425 show "x \<noteq> []" by auto |
|
1426 qed |
|
1427 ultimately |
|
1428 show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> depend s" |
|
1429 by auto |
|
1430 next |
|
1431 fix rest |
|
1432 assume dst: "distinct (rest::thread list)" |
|
1433 and ne: "rest \<noteq> []" |
|
1434 and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" |
|
1435 moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
|
1436 proof(rule someI2) |
|
1437 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
1438 next |
|
1439 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto |
|
1440 qed |
|
1441 ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> |
|
1442 set (SOME q. distinct q \<and> set q = set rest)" by simp |
|
1443 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
|
1444 proof(rule someI2) |
|
1445 from dst show "distinct rest \<and> set rest = set rest" by auto |
|
1446 next |
|
1447 fix x assume " distinct x \<and> set x = set rest" with ne |
|
1448 show "x \<noteq> []" by auto |
|
1449 qed |
|
1450 ultimately show "False" by auto |
|
1451 qed |
|
1452 ultimately |
1275 ultimately |
1453 have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" |
1276 have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" |
1454 by auto |
1277 by auto |
1455 moreover have "card \<dots> = |
1278 moreover have "card \<dots> = |
1456 Suc (card ((holdents (V thread cs#s) thread) - {cs}))" |
1279 Suc (card ((holdents (V thread cs#s) thread) - {cs}))" |
2306 |
2129 |
2307 lemma length_down_to_in: |
2130 lemma length_down_to_in: |
2308 assumes le_ij: "i \<le> j" |
2131 assumes le_ij: "i \<le> j" |
2309 and le_js: "j \<le> length s" |
2132 and le_js: "j \<le> length s" |
2310 shows "length (down_to j i s) = j - i" |
2133 shows "length (down_to j i s) = j - i" |
2311 proof - |
2134 by (metis down_to_def le_ij le_js length_from_to_in length_rev) |
2312 have "length (down_to j i s) = length (from_to i j (rev s))" |
|
2313 by (unfold down_to_def, auto) |
|
2314 also have "\<dots> = j - i" |
|
2315 proof(rule length_from_to_in[OF le_ij]) |
|
2316 from le_js show "j \<le> length (rev s)" by simp |
|
2317 qed |
|
2318 finally show ?thesis . |
|
2319 qed |
|
2320 |
2135 |
2321 |
2136 |
2322 lemma moment_head: |
2137 lemma moment_head: |
2323 assumes le_it: "Suc i \<le> length t" |
2138 assumes le_it: "Suc i \<le> length t" |
2324 obtains e where "moment (Suc i) t = e#moment i t" |
2139 obtains e where "moment (Suc i) t = e#moment i t" |
2325 proof - |
2140 by (metis assms moment_plus) |
2326 have "i \<le> Suc i" by simp |
|
2327 from length_down_to_in [OF this le_it] |
|
2328 have "length (down_to (Suc i) i t) = 1" by auto |
|
2329 then obtain e where "down_to (Suc i) i t = [e]" |
|
2330 apply (cases "(down_to (Suc i) i t)") by auto |
|
2331 moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" |
|
2332 by (rule down_to_conc[symmetric], auto) |
|
2333 ultimately have eq_me: "moment (Suc i) t = e#(moment i t)" |
|
2334 by (auto simp:down_to_moment) |
|
2335 from that [OF this] show ?thesis . |
|
2336 qed |
|
2337 |
2141 |
2338 lemma cnp_cnv_eq: |
2142 lemma cnp_cnv_eq: |
2339 fixes th s |
2143 fixes th s |
2340 assumes "vt s" |
2144 assumes "vt s" |
2341 and "th \<notin> threads s" |
2145 and "th \<notin> threads s" |
2342 shows "cntP s th = cntV s th" |
2146 shows "cntP s th = cntV s th" |
2343 proof - |
2147 by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs) |
2344 from assms show ?thesis |
|
2345 proof(induct) |
|
2346 case (vt_cons s e) |
|
2347 have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact |
|
2348 have not_in: "th \<notin> threads (e # s)" by fact |
|
2349 have "step s e" by fact |
|
2350 thus ?case proof(cases) |
|
2351 case (thread_create thread prio) |
|
2352 assume eq_e: "e = Create thread prio" |
|
2353 hence "thread \<in> threads (e#s)" by simp |
|
2354 with not_in and eq_e have "th \<notin> threads s" by auto |
|
2355 from ih [OF this] show ?thesis using eq_e |
|
2356 by (auto simp:cntP_def cntV_def count_def) |
|
2357 next |
|
2358 case (thread_exit thread) |
|
2359 assume eq_e: "e = Exit thread" |
|
2360 and not_holding: "holdents s thread = {}" |
|
2361 have vt_s: "vt s" by fact |
|
2362 from finite_holding[OF vt_s] have "finite (holdents s thread)" . |
|
2363 with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto) |
|
2364 moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def) |
|
2365 moreover note cnp_cnv_cncs[OF vt_s, of thread] |
|
2366 ultimately have eq_thread: "cntP s thread = cntV s thread" by auto |
|
2367 show ?thesis |
|
2368 proof(cases "th = thread") |
|
2369 case True |
|
2370 with eq_thread eq_e show ?thesis |
|
2371 by (auto simp:cntP_def cntV_def count_def) |
|
2372 next |
|
2373 case False |
|
2374 with not_in and eq_e have "th \<notin> threads s" by simp |
|
2375 from ih[OF this] and eq_e show ?thesis |
|
2376 by (auto simp:cntP_def cntV_def count_def) |
|
2377 qed |
|
2378 next |
|
2379 case (thread_P thread cs) |
|
2380 assume eq_e: "e = P thread cs" |
|
2381 have "thread \<in> runing s" by fact |
|
2382 with not_in eq_e have neq_th: "thread \<noteq> th" |
|
2383 by (auto simp:runing_def readys_def) |
|
2384 from not_in eq_e have "th \<notin> threads s" by simp |
|
2385 from ih[OF this] and neq_th and eq_e show ?thesis |
|
2386 by (auto simp:cntP_def cntV_def count_def) |
|
2387 next |
|
2388 case (thread_V thread cs) |
|
2389 assume eq_e: "e = V thread cs" |
|
2390 have "thread \<in> runing s" by fact |
|
2391 with not_in eq_e have neq_th: "thread \<noteq> th" |
|
2392 by (auto simp:runing_def readys_def) |
|
2393 from not_in eq_e have "th \<notin> threads s" by simp |
|
2394 from ih[OF this] and neq_th and eq_e show ?thesis |
|
2395 by (auto simp:cntP_def cntV_def count_def) |
|
2396 next |
|
2397 case (thread_set thread prio) |
|
2398 assume eq_e: "e = Set thread prio" |
|
2399 and "thread \<in> runing s" |
|
2400 hence "thread \<in> threads (e#s)" |
|
2401 by (simp add:runing_def readys_def) |
|
2402 with not_in and eq_e have "th \<notin> threads s" by auto |
|
2403 from ih [OF this] show ?thesis using eq_e |
|
2404 by (auto simp:cntP_def cntV_def count_def) |
|
2405 qed |
|
2406 next |
|
2407 case vt_nil |
|
2408 show ?case by (auto simp:cntP_def cntV_def count_def) |
|
2409 qed |
|
2410 qed |
|
2411 |
2148 |
2412 lemma eq_depend: |
2149 lemma eq_depend: |
2413 "depend (wq s) = depend s" |
2150 "depend (wq s) = depend s" |
2414 by (unfold cs_depend_def s_depend_def, auto) |
2151 by (unfold cs_depend_def s_depend_def, auto) |
2415 |
2152 |
2513 qed |
2250 qed |
2514 |
2251 |
2515 lemma le_cp: |
2252 lemma le_cp: |
2516 assumes vt: "vt s" |
2253 assumes vt: "vt s" |
2517 shows "preced th s \<le> cp s th" |
2254 shows "preced th s \<le> cp s th" |
2518 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) |
2255 apply(unfold cp_eq_cpreced preced_def cpreced_def, simp) |
2519 show "Prc (original_priority th s) (birthtime th s) |
2256 by (metis (mono_tags) Max_ge assms dependents_threads finite_imageI finite_insert finite_threads insertI1 preced_def rev_finite_subset) |
2520 \<le> Max (insert (Prc (original_priority th s) (birthtime th s)) |
|
2521 ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))" |
|
2522 (is "?l \<le> Max (insert ?l ?A)") |
|
2523 proof(cases "?A = {}") |
|
2524 case False |
|
2525 have "finite ?A" (is "finite (?f ` ?B)") |
|
2526 proof - |
|
2527 have "finite ?B" |
|
2528 proof- |
|
2529 have "finite {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}" |
|
2530 proof - |
|
2531 let ?F = "\<lambda> (x, y). the_th x" |
|
2532 have "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (wq s))\<^sup>+)" |
|
2533 apply (auto simp:image_def) |
|
2534 by (rule_tac x = "(Th x, Th th)" in bexI, auto) |
|
2535 moreover have "finite \<dots>" |
|
2536 proof - |
|
2537 from finite_depend[OF vt] have "finite (depend s)" . |
|
2538 hence "finite ((depend (wq s))\<^sup>+)" |
|
2539 apply (unfold finite_trancl) |
|
2540 by (auto simp: s_depend_def cs_depend_def wq_def) |
|
2541 thus ?thesis by auto |
|
2542 qed |
|
2543 ultimately show ?thesis by (auto intro:finite_subset) |
|
2544 qed |
|
2545 thus ?thesis by (simp add:cs_dependents_def) |
|
2546 qed |
|
2547 thus ?thesis by simp |
|
2548 qed |
|
2549 from Max_insert [OF this False, of ?l] show ?thesis by auto |
|
2550 next |
|
2551 case True |
|
2552 thus ?thesis by auto |
|
2553 qed |
|
2554 qed |
|
2555 |
2257 |
2556 lemma max_cp_eq: |
2258 lemma max_cp_eq: |
2557 assumes vt: "vt s" |
2259 assumes vt: "vt s" |
2558 shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)" |
2260 shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)" |
2559 (is "?l = ?r") |
2261 (is "?l = ?r") |