890 proof - |
890 proof - |
891 from runing_inversion_1[OF _ runing'] |
891 from runing_inversion_1[OF _ runing'] |
892 show ?thesis by auto |
892 show ?thesis by auto |
893 qed |
893 qed |
894 |
894 |
|
895 lemma runing_preced_inversion: |
|
896 assumes runing': "th' \<in> runing (t@s)" |
|
897 shows "cp (t@s) th' = preced th s" |
|
898 proof - |
|
899 from runing' have "cp (t@s) th' = Max (cp (t @ s) ` readys (t @ s))" |
|
900 by (unfold runing_def, auto) |
|
901 also have "\<dots> = preced th s" |
|
902 proof - |
|
903 from max_cp_readys_threads[OF vt_t] |
|
904 have "\<dots> = Max (cp (t @ s) ` threads (t @ s))" . |
|
905 also have "\<dots> = preced th s" |
|
906 proof - |
|
907 from max_kept |
|
908 and max_cp_eq [OF vt_t] |
|
909 show ?thesis by auto |
|
910 qed |
|
911 finally show ?thesis . |
|
912 qed |
|
913 finally show ?thesis . |
|
914 qed |
|
915 |
895 lemma runing_inversion_3: |
916 lemma runing_inversion_3: |
896 assumes runing': "th' \<in> runing (t@s)" |
917 assumes runing': "th' \<in> runing (t@s)" |
897 and neq_th: "th' \<noteq> th" |
918 and neq_th: "th' \<noteq> th" |
898 shows "th' \<in> threads s \<and> cntV s th' < cntP s th'" |
919 shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)" |
899 proof - |
920 proof - |
900 from runing_inversion_2 [OF runing'] and neq_th |
921 from runing_inversion_2 [OF runing'] |
|
922 and neq_th |
|
923 and runing_preced_inversion[OF runing'] |
901 show ?thesis by auto |
924 show ?thesis by auto |
902 qed |
925 qed |
|
926 |
903 |
927 |
904 lemma live: "runing (t@s) \<noteq> {}" |
928 lemma live: "runing (t@s) \<noteq> {}" |
905 proof(cases "th \<in> runing (t@s)") |
929 proof(cases "th \<in> runing (t@s)") |
906 case True thus ?thesis by auto |
930 case True thus ?thesis by auto |
907 next |
931 next |