544 qed |
544 qed |
545 ultimately show ?thesis using highest_preced_thread |
545 ultimately show ?thesis using highest_preced_thread |
546 by auto |
546 by auto |
547 qed |
547 qed |
548 |
548 |
549 lemma pv_blocked: |
549 lemma pv_blocked_pre: |
550 fixes th' |
550 fixes th' |
551 assumes th'_in: "th' \<in> threads (t@s)" |
551 assumes th'_in: "th' \<in> threads (t@s)" |
552 and neq_th': "th' \<noteq> th" |
552 and neq_th': "th' \<noteq> th" |
553 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
553 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
554 shows "th' \<notin> runing (t@s)" |
554 shows "th' \<notin> runing (t@s)" |
582 ultimately show ?thesis |
582 ultimately show ?thesis |
583 by (insert h, unfold cp_eq_cpreced cpreced_def, simp) |
583 by (insert h, unfold cp_eq_cpreced cpreced_def, simp) |
584 qed |
584 qed |
585 qed |
585 qed |
586 |
586 |
|
587 lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]] |
|
588 |
587 lemma runing_precond_pre: |
589 lemma runing_precond_pre: |
588 fixes th' |
590 fixes th' |
589 assumes th'_in: "th' \<in> threads s" |
591 assumes th'_in: "th' \<in> threads s" |
590 and eq_pv: "cntP s th' = cntV s th'" |
592 and eq_pv: "cntP s th' = cntV s th'" |
591 and neq_th': "th' \<noteq> th" |
593 and neq_th': "th' \<noteq> th" |
693 from pv_blocked[OF h1 neq_th' h2] |
695 from pv_blocked[OF h1 neq_th' h2] |
694 show ?thesis . |
696 show ?thesis . |
695 qed |
697 qed |
696 *) |
698 *) |
697 |
699 |
|
700 lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]] |
|
701 |
698 lemma runing_precond: |
702 lemma runing_precond: |
699 fixes th' |
703 fixes th' |
700 assumes th'_in: "th' \<in> threads s" |
704 assumes th'_in: "th' \<in> threads s" |
701 and neq_th': "th' \<noteq> th" |
705 and neq_th': "th' \<noteq> th" |
702 and is_runing: "th' \<in> runing (t@s)" |
706 and is_runing: "th' \<in> runing (t@s)" |
706 proof |
710 proof |
707 assume eq_pv: "cntP s th' = cntV s th'" |
711 assume eq_pv: "cntP s th' = cntV s th'" |
708 from runing_precond_pre[OF th'_in eq_pv neq_th'] |
712 from runing_precond_pre[OF th'_in eq_pv neq_th'] |
709 have h1: "th' \<in> threads (t @ s)" |
713 have h1: "th' \<in> threads (t @ s)" |
710 and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto |
714 and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto |
711 from pv_blocked[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" . |
715 from pv_blocked_pre[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" . |
712 with is_runing show "False" by simp |
716 with is_runing show "False" by simp |
713 qed |
717 qed |
714 moreover from cnp_cnv_cncs[OF vt_s, of th'] |
718 moreover from cnp_cnv_cncs[OF vt_s, of th'] |
715 have "cntV s th' \<le> cntP s th'" by auto |
719 have "cntV s th' \<le> cntP s th'" by auto |
716 ultimately show ?thesis by auto |
720 ultimately show ?thesis by auto |
810 next |
814 next |
811 case 0 |
815 case 0 |
812 from assms show ?case by auto |
816 from assms show ?case by auto |
813 qed |
817 qed |
814 |
818 |
815 lemma moment_blocked: |
819 lemma moment_blocked_eqpv: |
816 assumes neq_th': "th' \<noteq> th" |
820 assumes neq_th': "th' \<noteq> th" |
817 and th'_in: "th' \<in> threads ((moment i t)@s)" |
821 and th'_in: "th' \<in> threads ((moment i t)@s)" |
818 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
822 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
819 and le_ij: "i \<le> j" |
823 and le_ij: "i \<le> j" |
820 shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> |
824 shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> |
824 from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij |
828 from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij |
825 have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" |
829 have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" |
826 and h2: "th' \<in> threads ((moment j t)@s)" by auto |
830 and h2: "th' \<in> threads ((moment j t)@s)" by auto |
827 with extend_highest_gen.pv_blocked [OF red_moment [of j], OF h2 neq_th' h1] |
831 with extend_highest_gen.pv_blocked [OF red_moment [of j], OF h2 neq_th' h1] |
828 show ?thesis by auto |
832 show ?thesis by auto |
|
833 qed |
|
834 |
|
835 lemma moment_blocked: |
|
836 assumes neq_th': "th' \<noteq> th" |
|
837 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
838 and dtc: "detached (moment i t @ s) th'" |
|
839 and le_ij: "i \<le> j" |
|
840 shows "detached (moment j t @ s) th' \<and> |
|
841 th' \<in> threads ((moment j t)@s) \<and> |
|
842 th' \<notin> runing ((moment j t)@s)" |
|
843 proof - |
|
844 from vt_moment[OF vt_t, of "i+length s"] moment_prefix[of i t s] |
|
845 have vt_i: "vt (moment i t @ s)" by auto |
|
846 from vt_moment[OF vt_t, of "j+length s"] moment_prefix[of j t s] |
|
847 have vt_j: "vt (moment j t @ s)" by auto |
|
848 from moment_blocked_eqpv [OF neq_th' th'_in detached_elim [OF vt_i dtc] le_ij, |
|
849 folded detached_eq[OF vt_j]] |
|
850 show ?thesis . |
829 qed |
851 qed |
830 |
852 |
831 lemma runing_inversion_1: |
853 lemma runing_inversion_1: |
832 assumes neq_th': "th' \<noteq> th" |
854 assumes neq_th': "th' \<noteq> th" |
833 and runing': "th' \<in> runing (t@s)" |
855 and runing': "th' \<in> runing (t@s)" |
875 have h1: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" |
897 have h1: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" |
876 by simp |
898 by simp |
877 from eq_e have "th' \<in> threads ((e#moment i t)@s)" by simp |
899 from eq_e have "th' \<in> threads ((e#moment i t)@s)" by simp |
878 with eq_me [symmetric] |
900 with eq_me [symmetric] |
879 have h2: "th' \<in> threads (moment (Suc i) t @ s)" by simp |
901 have h2: "th' \<in> threads (moment (Suc i) t @ s)" by simp |
880 from moment_blocked [OF neq_th' h2 h1, of "length t"] and lt_its |
902 from moment_blocked_eqpv [OF neq_th' h2 h1, of "length t"] and lt_its |
881 and moment_ge |
903 and moment_ge |
882 have "th' \<notin> runing (t @ s)" by auto |
904 have "th' \<notin> runing (t @ s)" by auto |
883 with runing' |
905 with runing' |
884 show ?thesis by auto |
906 show ?thesis by auto |
885 qed |
907 qed |
921 from runing_inversion_2 [OF runing'] |
943 from runing_inversion_2 [OF runing'] |
922 and neq_th |
944 and neq_th |
923 and runing_preced_inversion[OF runing'] |
945 and runing_preced_inversion[OF runing'] |
924 show ?thesis by auto |
946 show ?thesis by auto |
925 qed |
947 qed |
926 |
|
927 |
948 |
928 lemma live: "runing (t@s) \<noteq> {}" |
949 lemma live: "runing (t@s) \<noteq> {}" |
929 proof(cases "th \<in> runing (t@s)") |
950 proof(cases "th \<in> runing (t@s)") |
930 case True thus ?thesis by auto |
951 case True thus ?thesis by auto |
931 next |
952 next |