diff -r cab43c4a96d2 -r bc5bf9e9ada2 prio/PrioG.thy --- a/prio/PrioG.thy Sat Feb 11 09:14:14 2012 +0000 +++ b/prio/PrioG.thy Sat Feb 11 09:34:46 2012 +0000 @@ -18,14 +18,14 @@ proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) fix thread s assume h1: "(Cs cs, Th thread) \ (depend s)\<^sup>+" - and h2: "thread \ set (waiting_queue (schs s) cs)" + and h2: "thread \ set (wq_fun (schs s) cs)" and h3: "thread \ runing s" show "False" proof - - from h3 have "\ cs. thread \ set (waiting_queue (schs s) cs) \ - thread = hd ((waiting_queue (schs s) cs))" + from h3 have "\ cs. thread \ set (wq_fun (schs s) cs) \ + thread = hd ((wq_fun (schs s) cs))" by (simp add:runing_def readys_def s_waiting_def wq_def) - from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" . + from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" . with h2 have "(Cs cs, Th thread) \ (depend s)" by (simp add:s_depend_def s_holding_def wq_def cs_holding_def) @@ -81,8 +81,8 @@ apply (auto simp:wq_def Let_def split:if_splits) proof - fix q qs - assume h1: "thread \ set (waiting_queue (schs s) cs)" - and h2: "q # qs = waiting_queue (schs s) cs" + assume h1: "thread \ set (wq_fun (schs s) cs)" + and h2: "q # qs = wq_fun (schs s) cs" and h3: "thread \ set (SOME q. distinct q \ set q = set qs)" and vt: "vt step (V th cs # s)" from h1 and h2[symmetric] have "thread \ set (q # qs)" by simp @@ -143,7 +143,7 @@ fix th qs assume vt: "vt step (V th cs # s)" and th_in: "thread \ set (SOME q. distinct q \ set q = set qs)" - and eq_wq: "waiting_queue (schs s) cs = thread # qs" + and eq_wq: "wq_fun (schs s) cs = thread # qs" show "False" proof - from wq_distinct[OF step_back_vt[OF vt], of cs] @@ -193,7 +193,7 @@ qed (* Wrong: - lemma \thread \ set (waiting_queue cs1 s); thread \ set (waiting_queue cs2 s)\ \ cs1 = cs2" + lemma \thread \ set (wq_fun cs1 s); thread \ set (wq_fun cs2 s)\ \ cs1 = cs2" *) lemma waiting_unique_pre: @@ -583,7 +583,7 @@ fix a list assume t_in: "t \ set list" and t_ni: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "waiting_queue (schs s) cs = a # list" + and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] @@ -597,7 +597,7 @@ fix a list assume t_in: "t \ set list" and t_ni: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "waiting_queue (schs s) cs = a # list" + and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] @@ -609,7 +609,7 @@ with t_ni and t_in show "t = hd (SOME q. distinct q \ set q = set list)" by auto next fix a list - assume eq_wq: "waiting_queue (schs s) cs = a # list" + assume eq_wq: "wq_fun (schs s) cs = a # list" from step_back_step[OF vt] show "a = th" proof(cases) @@ -641,7 +641,7 @@ proof - fix list assume eq_wq[folded wq_def]: - "waiting_queue (schs s) cs = hd (SOME q. distinct q \ set q = set list) # list" + "wq_fun (schs s) cs = hd (SOME q. distinct q \ set q = set list) # list" and hd_in: "hd (SOME q. distinct q \ set q = set list) \ set (SOME q. distinct q \ set q = set list)" have "set (SOME q. distinct q \ set q = set list) = set list" @@ -670,7 +670,7 @@ proof - fix rest assume vt: "vt step (V th cs # s)" - and eq_wq[folded wq_def]: " waiting_queue (schs s) cs = th # rest" + and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest" and nrest: "rest \ []" and ni: "hd (SOME q. distinct q \ set q = set rest) \ set (SOME q. distinct q \ set q = set rest)" @@ -693,7 +693,7 @@ apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) proof - fix a list - assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list" + assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" from step_back_step [OF vt] show "a = th" proof(cases) assume "holding s th cs" with eq_wq @@ -702,7 +702,7 @@ qed next fix a list - assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list" + assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" from step_back_step [OF vt] show "a = th" proof(cases) assume "holding s th cs" with eq_wq @@ -733,7 +733,7 @@ fix a list assume not_in: "t \ set list" and is_in: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "waiting_queue (schs s) cs = a # list" + and eq_wq: "wq_fun (schs s) cs = a # list" have "set (SOME q. distinct q \ set q = set list) = set list" proof(rule someI2) from wq_distinct [OF step_back_vt[OF vt], of cs] @@ -747,7 +747,7 @@ next fix list assume is_waiting: "waiting (wq (V th cs # s)) t cs" - and eq_wq: "waiting_queue (schs s) cs = t # list" + and eq_wq: "wq_fun (schs s) cs = t # list" hence "t \ set list" apply (unfold wq_def, auto simp:Let_def cs_waiting_def) proof - @@ -1125,25 +1125,25 @@ from h show ?thesis proof(unfold V wq_def) - assume th_in: "th \ set (waiting_queue (schs (V th' cs' # s)) cs)" (is "th \ set ?l") + assume th_in: "th \ set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \ set ?l") show "th \ threads (V th' cs' # s)" proof(cases "cs = cs'") case False - hence "?l = waiting_queue (schs s) cs" by (simp add:Let_def) + hence "?l = wq_fun (schs s) cs" by (simp add:Let_def) with th_in have " th \ set (wq s cs)" by (fold wq_def, simp) from ih [OF this] show ?thesis by simp next case True show ?thesis - proof(cases "waiting_queue (schs s) cs'") + proof(cases "wq_fun (schs s) cs'") case Nil with h V show ?thesis apply (auto simp:wq_def Let_def split:if_splits) by (fold wq_def, drule_tac ih, simp) next case (Cons a rest) - assume eq_wq: "waiting_queue (schs s) cs' = a # rest" + assume eq_wq: "wq_fun (schs s) cs' = a # rest" with h V show ?thesis apply (auto simp:Let_def wq_def split:if_splits) proof - @@ -1156,10 +1156,10 @@ show "\x. distinct x \ set x = set rest \ set x = set rest" by auto qed - with eq_wq th_in have "th \ set (waiting_queue (schs s) cs')" by auto + with eq_wq th_in have "th \ set (wq_fun (schs s) cs')" by auto from ih[OF this[folded wq_def]] show "th \ threads s" . next - assume th_in: "th \ set (waiting_queue (schs s) cs)" + assume th_in: "th \ set (wq_fun (schs s) cs)" from ih[OF this[folded wq_def]] show "th \ threads s" . qed @@ -1210,7 +1210,7 @@ proof - assume th_nin: "th \ set rest" and th_in: "th \ set (SOME q. distinct q \ set q = set rest)" - and eq_wq: "waiting_queue (schs s) cs = thread # rest" + and eq_wq: "wq_fun (schs s) cs = thread # rest" have "set (SOME q. distinct q \ set q = set rest) = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs] and eq_wq[folded wq_def] @@ -1550,9 +1550,9 @@ apply (rule_tac hh, clarify) apply (intro iffI allI, clarify) apply (erule_tac x = csa in allE, auto) - apply (subgoal_tac "waiting_queue (schs s) cs \ []", auto) + apply (subgoal_tac "wq_fun (schs s) cs \ []", auto) apply (erule_tac x = cs in allE, auto) - by (case_tac "(waiting_queue (schs s) cs)", auto) + by (case_tac "(wq_fun (schs s) cs)", auto) moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" apply (simp add:cntCS_def holdents_def) by (unfold step_depend_p [OF vtp], auto) @@ -1807,7 +1807,7 @@ apply (auto simp:eq_e readys_def s_waiting_def wq_def Let_def next_th_def) proof - - assume eq_wq: "waiting_queue (schs s) cs = thread # rest" + assume eq_wq: "wq_fun (schs s) cs = thread # rest" and t_in: "?t \ set rest" show "?t \ threads s" proof(rule wq_threads[OF step_back_vt[OF vtv]]) @@ -1816,13 +1816,13 @@ qed next fix csa - assume eq_wq: "waiting_queue (schs s) cs = thread # rest" + assume eq_wq: "wq_fun (schs s) cs = thread # rest" and t_in: "?t \ set rest" and neq_cs: "csa \ cs" - and t_in': "?t \ set (waiting_queue (schs s) csa)" - show "?t = hd (waiting_queue (schs s) csa)" + and t_in': "?t \ set (wq_fun (schs s) csa)" + show "?t = hd (wq_fun (schs s) csa)" proof - - { assume neq_hd': "?t \ hd (waiting_queue (schs s) csa)" + { assume neq_hd': "?t \ hd (wq_fun (schs s) csa)" from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq[folded wq_def] and t_in eq_wq have "?t \ thread" by auto