414 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
413 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
415 and xy: "(x, y) \<in> r" |
414 and xy: "(x, y) \<in> r" |
416 and xz: "(x, z) \<in> r^+" |
415 and xz: "(x, z) \<in> r^+" |
417 and neq: "y \<noteq> z" |
416 and neq: "y \<noteq> z" |
418 shows "(y, z) \<in> r^+" |
417 shows "(y, z) \<in> r^+" |
419 by (metis neq rtranclD tranclD unique xy xz) |
418 proof - |
|
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 |
420 |
438 |
421 lemma unique_base: |
439 lemma unique_base: |
422 fixes r x y z |
440 fixes r x y z |
423 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
441 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
424 and xy: "(x, y) \<in> r" |
442 and xy: "(x, y) \<in> r" |
425 and xz: "(x, z) \<in> r^+" |
443 and xz: "(x, z) \<in> r^+" |
426 and neq_yz: "y \<noteq> z" |
444 and neq_yz: "y \<noteq> z" |
427 shows "(y, z) \<in> r^+" |
445 shows "(y, z) \<in> r^+" |
428 by (metis neq_yz unique unique_minus xy xz) |
446 proof - |
|
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 |
429 |
465 |
430 lemma unique_chain: |
466 lemma unique_chain: |
431 fixes r x y z |
467 fixes r x y z |
432 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
468 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
433 and xy: "(x, y) \<in> r^+" |
469 and xy: "(x, y) \<in> r^+" |
634 |
670 |
635 lemma step_v_get_hold: |
671 lemma step_v_get_hold: |
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" |
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" |
637 apply (unfold cs_holding_def next_th_def wq_def, |
673 apply (unfold cs_holding_def next_th_def wq_def, |
638 auto simp:Let_def) |
674 auto simp:Let_def) |
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) |
675 proof - |
|
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 |
640 |
694 |
641 lemma step_v_release_inv[elim_format]: |
695 lemma step_v_release_inv[elim_format]: |
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> |
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> |
643 c = cs \<and> t = th" |
697 c = cs \<and> t = th" |
644 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) |
698 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) |
662 qed |
716 qed |
663 qed |
717 qed |
664 |
718 |
665 lemma step_v_waiting_mono: |
719 lemma step_v_waiting_mono: |
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" |
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" |
667 by (metis abs2 block_pre cs_waiting_def event.simps(20)) |
721 proof - |
|
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 |
668 |
776 |
669 lemma step_depend_v: |
777 lemma step_depend_v: |
670 fixes th::thread |
778 fixes th::thread |
671 assumes vt: |
779 assumes vt: |
672 "vt (V th cs#s)" |
780 "vt (V th cs#s)" |
1081 assumes vt: "vt s" |
1201 assumes vt: "vt s" |
1082 and neq_th: "th \<noteq> thread" |
1202 and neq_th: "th \<noteq> thread" |
1083 and eq_wq: "wq s cs = thread#rest" |
1203 and eq_wq: "wq s cs = thread#rest" |
1084 and not_in: "th \<notin> set rest" |
1204 and not_in: "th \<notin> set rest" |
1085 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1205 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1086 using assms |
1206 proof - |
1087 apply (auto simp:readys_def) |
1207 from assms show ?thesis |
1088 apply(simp add:s_waiting_def[folded wq_def]) |
1208 apply (auto simp:readys_def) |
1089 apply (erule_tac x = csa in allE) |
1209 apply(simp add:s_waiting_def[folded wq_def]) |
1090 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
1210 apply (erule_tac x = csa in allE) |
1091 apply (case_tac "csa = cs", simp) |
1211 apply (simp add:s_waiting_def wq_def Let_def split:if_splits) |
1092 apply (erule_tac x = cs in allE) |
1212 apply (case_tac "csa = cs", simp) |
1093 apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) |
1213 apply (erule_tac x = cs in allE) |
1094 apply(auto simp add: wq_def) |
1214 apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) |
1095 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
1215 apply(auto simp add: wq_def) |
1096 by (metis (lifting, full_types) distinct.simps(2) someI_ex wq_def wq_distinct) |
1216 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
|
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 |
1097 |
1231 |
1098 lemma chain_building: |
1232 lemma chain_building: |
1099 assumes vt: "vt s" |
1233 assumes vt: "vt s" |
1100 shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)" |
1234 shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)" |
1101 proof - |
1235 proof - |
1268 moreover have cs_not_in: |
1402 moreover have cs_not_in: |
1269 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
1403 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" |
1270 apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) |
1404 apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) |
1271 apply (unfold holdents_def, unfold step_depend_v[OF vtv], |
1405 apply (unfold holdents_def, unfold step_depend_v[OF vtv], |
1272 auto simp:next_th_def) |
1406 auto simp:next_th_def) |
1273 apply (metis (lifting, full_types) hd_in_set hd_np_in someI_ex) |
1407 proof - |
1274 by (metis (lifting, full_types) hd_in_set hd_np_in someI_ex) |
1408 fix rest |
|
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 |
1275 ultimately |
1452 ultimately |
1276 have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" |
1453 have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" |
1277 by auto |
1454 by auto |
1278 moreover have "card \<dots> = |
1455 moreover have "card \<dots> = |
1279 Suc (card ((holdents (V thread cs#s) thread) - {cs}))" |
1456 Suc (card ((holdents (V thread cs#s) thread) - {cs}))" |
2050 next |
2227 next |
2051 assume "th2' \<in> dependents (wq s) th2" |
2228 assume "th2' \<in> dependents (wq s) th2" |
2052 with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp |
2229 with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp |
2053 hence "(Th th1, Th th2) \<in> (depend s)^+" |
2230 hence "(Th th1, Th th2) \<in> (depend s)^+" |
2054 by (unfold cs_dependents_def s_depend_def cs_depend_def, simp) |
2231 by (unfold cs_dependents_def s_depend_def cs_depend_def, simp) |
2055 hence "Th th1 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"] |
2232 hence "Th th1 \<in> Domain ((depend s)^+)" |
2056 by auto |
2233 apply (unfold cs_dependents_def cs_depend_def s_depend_def) |
|
2234 by (auto simp:Domain_def) |
2057 hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain) |
2235 hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain) |
2058 then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def) |
2236 then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def) |
2059 from depend_target_th [OF this] |
2237 from depend_target_th [OF this] |
2060 obtain cs' where "n = Cs cs'" by auto |
2238 obtain cs' where "n = Cs cs'" by auto |
2061 with d have "(Th th1, Cs cs') \<in> depend s" by simp |
2239 with d have "(Th th1, Cs cs') \<in> depend s" by simp |
2071 proof |
2249 proof |
2072 assume "th2' = th2" |
2250 assume "th2' = th2" |
2073 with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp |
2251 with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp |
2074 hence "(Th th2, Th th1) \<in> (depend s)^+" |
2252 hence "(Th th2, Th th1) \<in> (depend s)^+" |
2075 by (unfold cs_dependents_def s_depend_def cs_depend_def, simp) |
2253 by (unfold cs_dependents_def s_depend_def cs_depend_def, simp) |
2076 hence "Th th2 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"] |
2254 hence "Th th2 \<in> Domain ((depend s)^+)" |
2077 by auto |
2255 apply (unfold cs_dependents_def cs_depend_def s_depend_def) |
|
2256 by (auto simp:Domain_def) |
2078 hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain) |
2257 hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain) |
2079 then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def) |
2258 then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def) |
2080 from depend_target_th [OF this] |
2259 from depend_target_th [OF this] |
2081 obtain cs' where "n = Cs cs'" by auto |
2260 obtain cs' where "n = Cs cs'" by auto |
2082 with d have "(Th th2, Cs cs') \<in> depend s" by simp |
2261 with d have "(Th th2, Cs cs') \<in> depend s" by simp |
2129 |
2308 |
2130 lemma length_down_to_in: |
2309 lemma length_down_to_in: |
2131 assumes le_ij: "i \<le> j" |
2310 assumes le_ij: "i \<le> j" |
2132 and le_js: "j \<le> length s" |
2311 and le_js: "j \<le> length s" |
2133 shows "length (down_to j i s) = j - i" |
2312 shows "length (down_to j i s) = j - i" |
2134 by (metis down_to_def le_ij le_js length_from_to_in length_rev) |
2313 proof - |
|
2314 have "length (down_to j i s) = length (from_to i j (rev s))" |
|
2315 by (unfold down_to_def, auto) |
|
2316 also have "\<dots> = j - i" |
|
2317 proof(rule length_from_to_in[OF le_ij]) |
|
2318 from le_js show "j \<le> length (rev s)" by simp |
|
2319 qed |
|
2320 finally show ?thesis . |
|
2321 qed |
2135 |
2322 |
2136 |
2323 |
2137 lemma moment_head: |
2324 lemma moment_head: |
2138 assumes le_it: "Suc i \<le> length t" |
2325 assumes le_it: "Suc i \<le> length t" |
2139 obtains e where "moment (Suc i) t = e#moment i t" |
2326 obtains e where "moment (Suc i) t = e#moment i t" |
2140 by (metis assms moment_plus) |
2327 proof - |
|
2328 have "i \<le> Suc i" by simp |
|
2329 from length_down_to_in [OF this le_it] |
|
2330 have "length (down_to (Suc i) i t) = 1" by auto |
|
2331 then obtain e where "down_to (Suc i) i t = [e]" |
|
2332 apply (cases "(down_to (Suc i) i t)") by auto |
|
2333 moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" |
|
2334 by (rule down_to_conc[symmetric], auto) |
|
2335 ultimately have eq_me: "moment (Suc i) t = e#(moment i t)" |
|
2336 by (auto simp:down_to_moment) |
|
2337 from that [OF this] show ?thesis . |
|
2338 qed |
2141 |
2339 |
2142 lemma cnp_cnv_eq: |
2340 lemma cnp_cnv_eq: |
2143 fixes th s |
2341 fixes th s |
2144 assumes "vt s" |
2342 assumes "vt s" |
2145 and "th \<notin> threads s" |
2343 and "th \<notin> threads s" |
2146 shows "cntP s th = cntV s th" |
2344 shows "cntP s th = cntV s th" |
2147 by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs) |
2345 proof - |
|
2346 from assms show ?thesis |
|
2347 proof(induct) |
|
2348 case (vt_cons s e) |
|
2349 have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact |
|
2350 have not_in: "th \<notin> threads (e # s)" by fact |
|
2351 have "step s e" by fact |
|
2352 thus ?case proof(cases) |
|
2353 case (thread_create thread prio) |
|
2354 assume eq_e: "e = Create thread prio" |
|
2355 hence "thread \<in> threads (e#s)" by simp |
|
2356 with not_in and eq_e have "th \<notin> threads s" by auto |
|
2357 from ih [OF this] show ?thesis using eq_e |
|
2358 by (auto simp:cntP_def cntV_def count_def) |
|
2359 next |
|
2360 case (thread_exit thread) |
|
2361 assume eq_e: "e = Exit thread" |
|
2362 and not_holding: "holdents s thread = {}" |
|
2363 have vt_s: "vt s" by fact |
|
2364 from finite_holding[OF vt_s] have "finite (holdents s thread)" . |
|
2365 with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto) |
|
2366 moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def) |
|
2367 moreover note cnp_cnv_cncs[OF vt_s, of thread] |
|
2368 ultimately have eq_thread: "cntP s thread = cntV s thread" by auto |
|
2369 show ?thesis |
|
2370 proof(cases "th = thread") |
|
2371 case True |
|
2372 with eq_thread eq_e show ?thesis |
|
2373 by (auto simp:cntP_def cntV_def count_def) |
|
2374 next |
|
2375 case False |
|
2376 with not_in and eq_e have "th \<notin> threads s" by simp |
|
2377 from ih[OF this] and eq_e show ?thesis |
|
2378 by (auto simp:cntP_def cntV_def count_def) |
|
2379 qed |
|
2380 next |
|
2381 case (thread_P thread cs) |
|
2382 assume eq_e: "e = P thread cs" |
|
2383 have "thread \<in> runing s" by fact |
|
2384 with not_in eq_e have neq_th: "thread \<noteq> th" |
|
2385 by (auto simp:runing_def readys_def) |
|
2386 from not_in eq_e have "th \<notin> threads s" by simp |
|
2387 from ih[OF this] and neq_th and eq_e show ?thesis |
|
2388 by (auto simp:cntP_def cntV_def count_def) |
|
2389 next |
|
2390 case (thread_V thread cs) |
|
2391 assume eq_e: "e = V thread cs" |
|
2392 have "thread \<in> runing s" by fact |
|
2393 with not_in eq_e have neq_th: "thread \<noteq> th" |
|
2394 by (auto simp:runing_def readys_def) |
|
2395 from not_in eq_e have "th \<notin> threads s" by simp |
|
2396 from ih[OF this] and neq_th and eq_e show ?thesis |
|
2397 by (auto simp:cntP_def cntV_def count_def) |
|
2398 next |
|
2399 case (thread_set thread prio) |
|
2400 assume eq_e: "e = Set thread prio" |
|
2401 and "thread \<in> runing s" |
|
2402 hence "thread \<in> threads (e#s)" |
|
2403 by (simp add:runing_def readys_def) |
|
2404 with not_in and eq_e have "th \<notin> threads s" by auto |
|
2405 from ih [OF this] show ?thesis using eq_e |
|
2406 by (auto simp:cntP_def cntV_def count_def) |
|
2407 qed |
|
2408 next |
|
2409 case vt_nil |
|
2410 show ?case by (auto simp:cntP_def cntV_def count_def) |
|
2411 qed |
|
2412 qed |
2148 |
2413 |
2149 lemma eq_depend: |
2414 lemma eq_depend: |
2150 "depend (wq s) = depend s" |
2415 "depend (wq s) = depend s" |
2151 by (unfold cs_depend_def s_depend_def, auto) |
2416 by (unfold cs_depend_def s_depend_def, auto) |
2152 |
2417 |
2250 qed |
2515 qed |
2251 |
2516 |
2252 lemma le_cp: |
2517 lemma le_cp: |
2253 assumes vt: "vt s" |
2518 assumes vt: "vt s" |
2254 shows "preced th s \<le> cp s th" |
2519 shows "preced th s \<le> cp s th" |
2255 apply(unfold cp_eq_cpreced preced_def cpreced_def, simp) |
2520 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) |
2256 by (metis (mono_tags) Max_ge assms dependents_threads finite_imageI finite_insert finite_threads insertI1 preced_def rev_finite_subset) |
2521 show "Prc (original_priority th s) (birthtime th s) |
|
2522 \<le> Max (insert (Prc (original_priority th s) (birthtime th s)) |
|
2523 ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))" |
|
2524 (is "?l \<le> Max (insert ?l ?A)") |
|
2525 proof(cases "?A = {}") |
|
2526 case False |
|
2527 have "finite ?A" (is "finite (?f ` ?B)") |
|
2528 proof - |
|
2529 have "finite ?B" |
|
2530 proof- |
|
2531 have "finite {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}" |
|
2532 proof - |
|
2533 let ?F = "\<lambda> (x, y). the_th x" |
|
2534 have "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (wq s))\<^sup>+)" |
|
2535 apply (auto simp:image_def) |
|
2536 by (rule_tac x = "(Th x, Th th)" in bexI, auto) |
|
2537 moreover have "finite \<dots>" |
|
2538 proof - |
|
2539 from finite_depend[OF vt] have "finite (depend s)" . |
|
2540 hence "finite ((depend (wq s))\<^sup>+)" |
|
2541 apply (unfold finite_trancl) |
|
2542 by (auto simp: s_depend_def cs_depend_def wq_def) |
|
2543 thus ?thesis by auto |
|
2544 qed |
|
2545 ultimately show ?thesis by (auto intro:finite_subset) |
|
2546 qed |
|
2547 thus ?thesis by (simp add:cs_dependents_def) |
|
2548 qed |
|
2549 thus ?thesis by simp |
|
2550 qed |
|
2551 from Max_insert [OF this False, of ?l] show ?thesis by auto |
|
2552 next |
|
2553 case True |
|
2554 thus ?thesis by auto |
|
2555 qed |
|
2556 qed |
2257 |
2557 |
2258 lemma max_cp_eq: |
2558 lemma max_cp_eq: |
2259 assumes vt: "vt s" |
2559 assumes vt: "vt s" |
2260 shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)" |
2560 shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)" |
2261 (is "?l = ?r") |
2561 (is "?l = ?r") |