equal
deleted
inserted
replaced
949 from runing_inversion_2 [OF runing'] |
949 from runing_inversion_2 [OF runing'] |
950 and neq_th |
950 and neq_th |
951 and runing_preced_inversion[OF runing'] |
951 and runing_preced_inversion[OF runing'] |
952 show ?thesis by auto |
952 show ?thesis by auto |
953 qed |
953 qed |
|
954 |
|
955 lemma runing_inversion_4: |
|
956 assumes runing': "th' \<in> runing (t@s)" |
|
957 and neq_th: "th' \<noteq> th" |
|
958 shows "th' \<in> threads s" |
|
959 and "\<not>detached s th'" |
|
960 and "cp (t@s) th' = preced th s" |
|
961 using runing_inversion_3 [OF runing'] |
|
962 and neq_th |
|
963 and runing_preced_inversion[OF runing'] |
|
964 apply(auto simp add: detached_eq[OF vt_s]) |
|
965 done |
|
966 |
|
967 |
954 |
968 |
955 lemma live: "runing (t@s) \<noteq> {}" |
969 lemma live: "runing (t@s) \<noteq> {}" |
956 proof(cases "th \<in> runing (t@s)") |
970 proof(cases "th \<in> runing (t@s)") |
957 case True thus ?thesis by auto |
971 case True thus ?thesis by auto |
958 next |
972 next |