diff -r bea94f1e6771 -r dae7501b26ac prio/ExtGG.thy --- 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' \ 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' \ runing (t @ s)" . + then have not_runing: "th' \ 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' \ - th' \ threads (e#(moment (i + k) t)@s) - " + th' \ 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' \ 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: