# HG changeset patch # User urbanc # Date 1334931336 0 # Node ID dae7501b26ac63118e1e13388f33b8a1b5d83356 # Parent bea94f1e6771015256d0769914bf13ffcb71e85c changes to get the files through for CU 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: diff -r bea94f1e6771 -r dae7501b26ac prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Fri Apr 20 11:45:06 2012 +0000 +++ b/prio/Paper/Paper.thy Fri Apr 20 14:15:36 2012 +0000 @@ -38,8 +38,9 @@ original_priority ("priority") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") -abbreviation +(*abbreviation "detached s th \ cntP s th = cntV s th" +*) (*>*) section {* Introduction *} @@ -375,6 +376,10 @@ {\bf ??? define detached} + \begin{isabelle}\ \ \ \ \ %%% + @{thm detached_def} + \end{isabelle} + Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a diff -r bea94f1e6771 -r dae7501b26ac prio/PrioG.thy --- a/prio/PrioG.thy Fri Apr 20 11:45:06 2012 +0000 +++ b/prio/PrioG.thy Fri Apr 20 14:15:36 2012 +0000 @@ -2776,6 +2776,8 @@ definition detached :: "state \ thread \ bool" where "detached s th \ (Th th \ Field (depend s))" +thm Field_def + lemma detached_intro: fixes s th assumes vt: "vt s" @@ -2803,12 +2805,14 @@ have "holdents s th = {}" by (simp add:cntCS_def) thus ?thesis - by (auto simp:holdents_def, case_tac x, - auto simp:holdents_def s_depend_def) + apply(auto simp:holdents_def) + apply(case_tac a) + apply(auto simp:holdents_def s_depend_def) + done qed ultimately show ?thesis apply (auto simp:detached_def Field_def Domain_def readys_def) - apply (case_tac y, auto simp:s_depend_def) + apply (case_tac b, auto simp:s_depend_def) by (erule_tac x = "nat" in allE, simp add: eq_waiting) qed qed diff -r bea94f1e6771 -r dae7501b26ac prio/paper.pdf Binary file prio/paper.pdf has changed