equal
deleted
inserted
replaced
35 and preced_th: "preced th s = Prc prio tm" |
35 and preced_th: "preced th s = Prc prio tm" |
36 |
36 |
37 context highest_gen |
37 context highest_gen |
38 begin |
38 begin |
39 |
39 |
|
40 |
|
41 |
40 lemma lt_tm: "tm < length s" |
42 lemma lt_tm: "tm < length s" |
41 by (insert preced_tm_lt[OF threads_s preced_th], simp) |
43 by (insert preced_tm_lt[OF threads_s preced_th], simp) |
42 |
44 |
43 lemma eq_cp_s_th: "cp s th = preced th s" |
45 lemma eq_cp_s_th: "cp s th = preced th s" |
44 proof - |
46 proof - |
115 qed |
117 qed |
116 qed |
118 qed |
117 |
119 |
118 context extend_highest_gen |
120 context extend_highest_gen |
119 begin |
121 begin |
|
122 |
|
123 thm extend_highest_gen_axioms_def |
120 |
124 |
121 lemma red_moment: |
125 lemma red_moment: |
122 "extend_highest_gen s th prio tm (moment i t)" |
126 "extend_highest_gen s th prio tm (moment i t)" |
123 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) |
127 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) |
124 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) |
128 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) |
883 lemma runing_inversion_2: |
887 lemma runing_inversion_2: |
884 assumes runing': "th' \<in> runing (t@s)" |
888 assumes runing': "th' \<in> runing (t@s)" |
885 shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')" |
889 shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')" |
886 proof - |
890 proof - |
887 from runing_inversion_1[OF _ runing'] |
891 from runing_inversion_1[OF _ runing'] |
|
892 show ?thesis by auto |
|
893 qed |
|
894 |
|
895 lemma runing_inversion_3: |
|
896 assumes runing': "th' \<in> runing (t@s)" |
|
897 and neq_th: "th' \<noteq> th" |
|
898 shows "(th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')" |
|
899 proof - |
|
900 from runing_inversion_2 [OF runing'] and neq_th |
888 show ?thesis by auto |
901 show ?thesis by auto |
889 qed |
902 qed |
890 |
903 |
891 lemma live: "runing (t@s) \<noteq> {}" |
904 lemma live: "runing (t@s) \<noteq> {}" |
892 proof(cases "th \<in> runing (t@s)") |
905 proof(cases "th \<in> runing (t@s)") |