--- a/prio/ExtGG.thy Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/ExtGG.thy Fri Apr 20 14:15:36 2012 +0000
@@ -601,9 +601,11 @@
have in_thread: "th' \<in> threads (t @ s)"
and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
from Cons have "extend_highest_gen s th prio tm t" by auto
- from extend_highest_gen.pv_blocked
- [OF this, OF in_thread neq_th' not_holding]
- have not_runing: "th' \<notin> runing (t @ s)" .
+ then have not_runing: "th' \<notin> runing (t @ s)"
+ apply(rule extend_highest_gen.pv_blocked)
+ using Cons(1) in_thread neq_th' not_holding
+ apply(simp_all add: detached_eq)
+ done
show ?case
proof(cases e)
case (V thread cs)
@@ -751,15 +753,16 @@
next
from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" .
next
- from Suc show "cntP (moment (i + k) t @ s) th' = cntV (moment (i + k) t @ s) th'"
- by (auto)
+ from Suc vt_e show "detached (moment (i + k) t @ s) th'"
+ apply(subst detached_eq)
+ apply(auto intro: vt_e evt_cons)
+ done
qed
qed
from step_back_step[OF vt_e]
have "step ((moment (i + k) t)@s) e" .
hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and>
- th' \<in> threads (e#(moment (i + k) t)@s)
- "
+ th' \<in> threads (e#(moment (i + k) t)@s)"
proof(cases)
case (thread_create thread prio)
with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def)
@@ -828,8 +831,11 @@
from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij
have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"
and h2: "th' \<in> threads ((moment j t)@s)" by auto
- with extend_highest_gen.pv_blocked [OF red_moment [of j], OF h2 neq_th' h1]
- show ?thesis by auto
+ with extend_highest_gen.pv_blocked
+ show ?thesis
+ using red_moment [of j] h2 neq_th' h1
+ apply(auto)
+ by (metis extend_highest_gen.pv_blocked_pre)
qed
lemma moment_blocked: