equal
deleted
inserted
replaced
599 case (Cons e t) |
599 case (Cons e t) |
600 from Cons |
600 from Cons |
601 have in_thread: "th' \<in> threads (t @ s)" |
601 have in_thread: "th' \<in> threads (t @ s)" |
602 and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto |
602 and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto |
603 from Cons have "extend_highest_gen s th prio tm t" by auto |
603 from Cons have "extend_highest_gen s th prio tm t" by auto |
604 from extend_highest_gen.pv_blocked |
604 then have not_runing: "th' \<notin> runing (t @ s)" |
605 [OF this, OF in_thread neq_th' not_holding] |
605 apply(rule extend_highest_gen.pv_blocked) |
606 have not_runing: "th' \<notin> runing (t @ s)" . |
606 using Cons(1) in_thread neq_th' not_holding |
|
607 apply(simp_all add: detached_eq) |
|
608 done |
607 show ?case |
609 show ?case |
608 proof(cases e) |
610 proof(cases e) |
609 case (V thread cs) |
611 case (V thread cs) |
610 from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto |
612 from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto |
611 |
613 |
749 next |
751 next |
750 from neq_th' show "th' \<noteq> th" . |
752 from neq_th' show "th' \<noteq> th" . |
751 next |
753 next |
752 from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" . |
754 from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" . |
753 next |
755 next |
754 from Suc show "cntP (moment (i + k) t @ s) th' = cntV (moment (i + k) t @ s) th'" |
756 from Suc vt_e show "detached (moment (i + k) t @ s) th'" |
755 by (auto) |
757 apply(subst detached_eq) |
|
758 apply(auto intro: vt_e evt_cons) |
|
759 done |
756 qed |
760 qed |
757 qed |
761 qed |
758 from step_back_step[OF vt_e] |
762 from step_back_step[OF vt_e] |
759 have "step ((moment (i + k) t)@s) e" . |
763 have "step ((moment (i + k) t)@s) e" . |
760 hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and> |
764 hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and> |
761 th' \<in> threads (e#(moment (i + k) t)@s) |
765 th' \<in> threads (e#(moment (i + k) t)@s)" |
762 " |
|
763 proof(cases) |
766 proof(cases) |
764 case (thread_create thread prio) |
767 case (thread_create thread prio) |
765 with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def) |
768 with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def) |
766 next |
769 next |
767 case (thread_exit thread) |
770 case (thread_exit thread) |
826 th' \<notin> runing ((moment j t)@s)" |
829 th' \<notin> runing ((moment j t)@s)" |
827 proof - |
830 proof - |
828 from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij |
831 from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij |
829 have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" |
832 have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" |
830 and h2: "th' \<in> threads ((moment j t)@s)" by auto |
833 and h2: "th' \<in> threads ((moment j t)@s)" by auto |
831 with extend_highest_gen.pv_blocked [OF red_moment [of j], OF h2 neq_th' h1] |
834 with extend_highest_gen.pv_blocked |
832 show ?thesis by auto |
835 show ?thesis |
|
836 using red_moment [of j] h2 neq_th' h1 |
|
837 apply(auto) |
|
838 by (metis extend_highest_gen.pv_blocked_pre) |
833 qed |
839 qed |
834 |
840 |
835 lemma moment_blocked: |
841 lemma moment_blocked: |
836 assumes neq_th': "th' \<noteq> th" |
842 assumes neq_th': "th' \<noteq> th" |
837 and th'_in: "th' \<in> threads ((moment i t)@s)" |
843 and th'_in: "th' \<in> threads ((moment i t)@s)" |