equal
deleted
inserted
replaced
30 locale highest_gen = |
30 locale highest_gen = |
31 fixes s th prio tm |
31 fixes s th prio tm |
32 assumes vt_s: "vt step s" |
32 assumes vt_s: "vt step s" |
33 and threads_s: "th \<in> threads s" |
33 and threads_s: "th \<in> threads s" |
34 and highest: "preced th s = Max ((cp s)`threads s)" |
34 and highest: "preced th s = Max ((cp s)`threads s)" |
35 and nh: "preced th s' \<noteq> Max ((cp s)`threads s')" |
|
36 and preced_th: "preced th s = Prc prio tm" |
35 and preced_th: "preced th s = Prc prio tm" |
37 |
36 |
38 context highest_gen |
37 context highest_gen |
39 begin |
38 begin |
40 |
39 |
116 qed |
115 qed |
117 qed |
116 qed |
118 |
117 |
119 context extend_highest_gen |
118 context extend_highest_gen |
120 begin |
119 begin |
121 |
|
122 thm extend_highest_gen.axioms |
|
123 |
120 |
124 lemma red_moment: |
121 lemma red_moment: |
125 "extend_highest_gen s th prio tm (moment i t)" |
122 "extend_highest_gen s th prio tm (moment i t)" |
126 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) |
123 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) |
127 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) |
124 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) |
162 qed |
159 qed |
163 qed |
160 qed |
164 qed |
161 qed |
165 |
162 |
166 lemma th_kept: "th \<in> threads (t @ s) \<and> |
163 lemma th_kept: "th \<in> threads (t @ s) \<and> |
167 preced th (t@s) = preced th s" (is "?Q t") |
164 preced th (t@s) = preced th s" (is "?Q t") |
168 proof - |
165 proof - |
169 show ?thesis |
166 show ?thesis |
170 proof(induct rule:ind) |
167 proof(induct rule:ind) |
171 case Nil |
168 case Nil |
172 from threads_s |
169 from threads_s |
519 by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp) |
516 by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp) |
520 |
517 |
521 lemma th_cp_preced: "cp (t@s) th = preced th s" |
518 lemma th_cp_preced: "cp (t@s) th = preced th s" |
522 by (fold max_kept, unfold th_cp_max_preced, simp) |
519 by (fold max_kept, unfold th_cp_max_preced, simp) |
523 |
520 |
524 lemma preced_less': |
521 lemma preced_less: |
525 fixes th' |
522 fixes th' |
526 assumes th'_in: "th' \<in> threads s" |
523 assumes th'_in: "th' \<in> threads s" |
527 and neq_th': "th' \<noteq> th" |
524 and neq_th': "th' \<noteq> th" |
528 shows "preced th' s < preced th s" |
525 shows "preced th' s < preced th s" |
529 proof - |
526 proof - |