diff -r 7fe2a20017c0 -r f9e0d3274c14 prio/PrioG.thy --- a/prio/PrioG.thy Mon Feb 27 18:53:53 2012 +0000 +++ b/prio/PrioG.thy Tue Feb 28 13:13:32 2012 +0000 @@ -2,6 +2,7 @@ imports PrioGDef begin + lemma runing_ready: shows "runing s \ readys s" unfolding runing_def readys_def @@ -415,26 +416,7 @@ and xz: "(x, z) \ r^+" and neq: "y \ z" shows "(y, z) \ r^+" -proof - - from xz and neq show ?thesis - proof(induct) - case (base ya) - have "(x, ya) \ r" by fact - from unique [OF xy this] have "y = ya" . - with base show ?case by auto - next - case (step ya z) - show ?case - proof(cases "y = ya") - case True - from step True show ?thesis by simp - next - case False - from step False - show ?thesis by auto - qed - qed -qed +by (metis neq rtranclD tranclD unique xy xz) lemma unique_base: fixes r x y z @@ -443,25 +425,7 @@ and xz: "(x, z) \ r^+" and neq_yz: "y \ z" shows "(y, z) \ r^+" -proof - - from xz neq_yz show ?thesis - proof(induct) - case (base ya) - from xy unique base show ?case by auto - next - case (step ya z) - show ?case - proof(cases "y = ya") - case True - from True step show ?thesis by auto - next - case False - from False step - have "(y, ya) \ r\<^sup>+" by auto - with step show ?thesis by auto - qed - qed -qed +by (metis neq_yz unique unique_minus xy xz) lemma unique_chain: fixes r x y z @@ -672,25 +636,7 @@ "\th'. \vt (V th cs # s); \ holding (wq (V th cs # s)) th' cs; next_th s th cs th'\ \ False" apply (unfold cs_holding_def next_th_def wq_def, auto simp:Let_def) -proof - - fix rest - assume vt: "vt (V th cs # s)" - 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)" - have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x assume "distinct x \ set x = set rest" - hence "set x = set rest" by auto - with nrest - show "x \ []" by (case_tac x, auto) - qed - with ni show "False" by auto -qed +by (metis (lifting, full_types) List.member_def distinct.simps(2) hd_in_set member_rec(2) someI_ex step_back_vt wq_def wq_distinct) lemma step_v_release_inv[elim_format]: "\c t. \vt (V th cs # s); \ holding (wq (V th cs # s)) t c; holding (wq s) t c\ \ @@ -718,61 +664,7 @@ lemma step_v_waiting_mono: "\t c. \vt (V th cs # s); waiting (wq (V th cs # s)) t c\ \ waiting (wq s) t c" -proof - - fix t c - let ?s' = "(V th cs # s)" - assume vt: "vt ?s'" - and wt: "waiting (wq ?s') t c" - show "waiting (wq s) t c" - proof(cases "c = cs") - case False - assume neq_cs: "c \ cs" - hence "waiting (wq ?s') t c = waiting (wq s) t c" - by (unfold cs_waiting_def wq_def, auto simp:Let_def) - with wt show ?thesis by simp - next - case True - with wt show ?thesis - apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) - proof - - 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: "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] - show "distinct list \ set list = set list" by auto - next - fix x assume "distinct x \ set x = set list" - thus "set x = set list" by auto - qed - with not_in is_in show "t = a" by auto - next - fix list - assume is_waiting: "waiting (wq (V th cs # s)) t cs" - 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 - - assume " t \ set (SOME q. distinct q \ set q = set list)" - moreover have "\ = set list" - proof(rule someI2) - from wq_distinct [OF step_back_vt[OF vt], of cs] - and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - fix x assume "distinct x \ set x = set list" - thus "set x = set list" by auto - qed - ultimately show "t \ set list" by simp - qed - with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def] - show False by auto - qed - qed -qed +by (metis abs2 block_pre cs_waiting_def event.simps(20)) lemma step_depend_v: fixes th::thread @@ -808,13 +700,7 @@ fixes A assumes h: "\ x y. \x \ A; y \ A\ \ x = y" shows "A = {} \ (\ a. A = {a})" -proof(cases "A = {}") - case True thus ?thesis by simp -next - case False then obtain a where "a \ A" by auto - with h have "A = {a}" by auto - thus ?thesis by simp -qed +by (metis assms insertCI nonempty_iff) lemma depend_target_th: "(Th th, x) \ depend (s::state) \ \ cs. x = Cs cs" by (unfold s_depend_def, auto) @@ -1076,13 +962,7 @@ fixes s assumes vt: "vt s" shows "wf ((depend s)^-1)" -proof(rule finite_acyclic_wf_converse) - from finite_depend [OF vt] - show "finite (depend s)" . -next - from acyclic_depend[OF vt] - show "acyclic (depend s)" . -qed +by (metis acyclic_depend assms finite_acyclic_wf_converse finite_depend) lemma hd_np_in: "x \ set l \ hd l \ set l" by (induct l, auto) @@ -1203,31 +1083,17 @@ and eq_wq: "wq s cs = thread#rest" and not_in: "th \ set rest" shows "(th \ readys (V thread cs#s)) = (th \ readys s)" -proof - - from assms show ?thesis - apply (auto simp:readys_def) - apply(simp add:s_waiting_def[folded wq_def]) - apply (erule_tac x = csa in allE) - apply (simp add:s_waiting_def wq_def Let_def split:if_splits) - apply (case_tac "csa = cs", simp) - apply (erule_tac x = cs in allE) - apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) - apply(auto simp add: wq_def) - apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) - proof - - assume th_nin: "th \ set rest" - and th_in: "th \ set (SOME q. distinct q \ set q = set 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, unfolded wq_def] and eq_wq[unfolded wq_def] - show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - with th_nin th_in show False by auto - qed -qed +using assms +apply (auto simp:readys_def) +apply(simp add:s_waiting_def[folded wq_def]) +apply (erule_tac x = csa in allE) +apply (simp add:s_waiting_def wq_def Let_def split:if_splits) +apply (case_tac "csa = cs", simp) +apply (erule_tac x = cs in allE) +apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) +apply(auto simp add: wq_def) +apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) +by (metis (lifting, full_types) distinct.simps(2) someI_ex wq_def wq_distinct) lemma chain_building: assumes vt: "vt s" @@ -1404,51 +1270,8 @@ apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) apply (unfold holdents_def, unfold step_depend_v[OF vtv], auto simp:next_th_def) - proof - - fix rest - assume dst: "distinct (rest::thread list)" - and ne: "rest \ []" - and hd_ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - moreover have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - ultimately have "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)" by simp - moreover have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - fix x assume " distinct x \ set x = set rest" with ne - show "x \ []" by auto - qed - ultimately - show "(Cs cs, Th (hd (SOME q. distinct q \ set q = set rest))) \ depend s" - by auto - next - fix rest - assume dst: "distinct (rest::thread list)" - and ne: "rest \ []" - and hd_ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - moreover have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - ultimately have "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)" by simp - moreover have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - fix x assume " distinct x \ set x = set rest" with ne - show "x \ []" by auto - qed - ultimately show "False" by auto - qed + apply (metis (lifting, full_types) hd_in_set hd_np_in someI_ex) + by (metis (lifting, full_types) hd_in_set hd_np_in someI_ex) ultimately have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" by auto @@ -2308,106 +2131,20 @@ assumes le_ij: "i \ j" and le_js: "j \ length s" shows "length (down_to j i s) = j - i" -proof - - have "length (down_to j i s) = length (from_to i j (rev s))" - by (unfold down_to_def, auto) - also have "\ = j - i" - proof(rule length_from_to_in[OF le_ij]) - from le_js show "j \ length (rev s)" by simp - qed - finally show ?thesis . -qed +by (metis down_to_def le_ij le_js length_from_to_in length_rev) lemma moment_head: assumes le_it: "Suc i \ length t" obtains e where "moment (Suc i) t = e#moment i t" -proof - - have "i \ Suc i" by simp - from length_down_to_in [OF this le_it] - have "length (down_to (Suc i) i t) = 1" by auto - then obtain e where "down_to (Suc i) i t = [e]" - apply (cases "(down_to (Suc i) i t)") by auto - moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" - by (rule down_to_conc[symmetric], auto) - ultimately have eq_me: "moment (Suc i) t = e#(moment i t)" - by (auto simp:down_to_moment) - from that [OF this] show ?thesis . -qed +by (metis assms moment_plus) lemma cnp_cnv_eq: fixes th s assumes "vt s" and "th \ threads s" shows "cntP s th = cntV s th" -proof - - from assms show ?thesis - proof(induct) - case (vt_cons s e) - have ih: "th \ threads s \ cntP s th = cntV s th" by fact - have not_in: "th \ threads (e # s)" by fact - have "step s e" by fact - thus ?case proof(cases) - case (thread_create thread prio) - assume eq_e: "e = Create thread prio" - hence "thread \ threads (e#s)" by simp - with not_in and eq_e have "th \ threads s" by auto - from ih [OF this] show ?thesis using eq_e - by (auto simp:cntP_def cntV_def count_def) - next - case (thread_exit thread) - assume eq_e: "e = Exit thread" - and not_holding: "holdents s thread = {}" - have vt_s: "vt s" by fact - from finite_holding[OF vt_s] have "finite (holdents s thread)" . - with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto) - moreover have "thread \ readys s" using thread_exit by (auto simp:runing_def) - moreover note cnp_cnv_cncs[OF vt_s, of thread] - ultimately have eq_thread: "cntP s thread = cntV s thread" by auto - show ?thesis - proof(cases "th = thread") - case True - with eq_thread eq_e show ?thesis - by (auto simp:cntP_def cntV_def count_def) - next - case False - with not_in and eq_e have "th \ threads s" by simp - from ih[OF this] and eq_e show ?thesis - by (auto simp:cntP_def cntV_def count_def) - qed - next - case (thread_P thread cs) - assume eq_e: "e = P thread cs" - have "thread \ runing s" by fact - with not_in eq_e have neq_th: "thread \ th" - by (auto simp:runing_def readys_def) - from not_in eq_e have "th \ threads s" by simp - from ih[OF this] and neq_th and eq_e show ?thesis - by (auto simp:cntP_def cntV_def count_def) - next - case (thread_V thread cs) - assume eq_e: "e = V thread cs" - have "thread \ runing s" by fact - with not_in eq_e have neq_th: "thread \ th" - by (auto simp:runing_def readys_def) - from not_in eq_e have "th \ threads s" by simp - from ih[OF this] and neq_th and eq_e show ?thesis - by (auto simp:cntP_def cntV_def count_def) - next - case (thread_set thread prio) - assume eq_e: "e = Set thread prio" - and "thread \ runing s" - hence "thread \ threads (e#s)" - by (simp add:runing_def readys_def) - with not_in and eq_e have "th \ threads s" by auto - from ih [OF this] show ?thesis using eq_e - by (auto simp:cntP_def cntV_def count_def) - qed - next - case vt_nil - show ?case by (auto simp:cntP_def cntV_def count_def) - qed -qed +by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs) lemma eq_depend: "depend (wq s) = depend s" @@ -2515,43 +2252,8 @@ lemma le_cp: assumes vt: "vt s" shows "preced th s \ cp s th" -proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) - show "Prc (original_priority th s) (birthtime th s) - \ Max (insert (Prc (original_priority th s) (birthtime th s)) - ((\th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))" - (is "?l \ Max (insert ?l ?A)") - proof(cases "?A = {}") - case False - have "finite ?A" (is "finite (?f ` ?B)") - proof - - have "finite ?B" - proof- - have "finite {th'. (Th th', Th th) \ (depend (wq s))\<^sup>+}" - proof - - let ?F = "\ (x, y). the_th x" - have "{th'. (Th th', Th th) \ (depend (wq s))\<^sup>+} \ ?F ` ((depend (wq s))\<^sup>+)" - apply (auto simp:image_def) - by (rule_tac x = "(Th x, Th th)" in bexI, auto) - moreover have "finite \" - proof - - from finite_depend[OF vt] have "finite (depend s)" . - hence "finite ((depend (wq s))\<^sup>+)" - apply (unfold finite_trancl) - by (auto simp: s_depend_def cs_depend_def wq_def) - thus ?thesis by auto - qed - ultimately show ?thesis by (auto intro:finite_subset) - qed - thus ?thesis by (simp add:cs_dependents_def) - qed - thus ?thesis by simp - qed - from Max_insert [OF this False, of ?l] show ?thesis by auto - next - case True - thus ?thesis by auto - qed -qed +apply(unfold cp_eq_cpreced preced_def cpreced_def, simp) +by (metis (mono_tags) Max_ge assms dependents_threads finite_imageI finite_insert finite_threads insertI1 preced_def rev_finite_subset) lemma max_cp_eq: assumes vt: "vt s"