diff -r e7504bfdbd50 -r b3add51e2e0f prio/PrioG.thy --- a/prio/PrioG.thy Fri Apr 13 13:12:43 2012 +0000 +++ b/prio/PrioG.thy Sun Apr 15 21:53:12 2012 +0000 @@ -2,7 +2,6 @@ imports PrioGDef begin - lemma runing_ready: shows "runing s \ readys s" unfolding runing_def readys_def @@ -416,7 +415,26 @@ and xz: "(x, z) \ r^+" and neq: "y \ z" shows "(y, z) \ r^+" -by (metis neq rtranclD tranclD unique xy xz) +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 lemma unique_base: fixes r x y z @@ -425,7 +443,25 @@ and xz: "(x, z) \ r^+" and neq_yz: "y \ z" shows "(y, z) \ r^+" -by (metis neq_yz unique unique_minus xy xz) +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 lemma unique_chain: fixes r x y z @@ -636,7 +672,25 @@ "\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) -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) +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 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\ \ @@ -664,7 +718,61 @@ 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" -by (metis abs2 block_pre cs_waiting_def event.simps(20)) +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 lemma step_depend_v: fixes th::thread @@ -700,7 +808,13 @@ fixes A assumes h: "\ x y. \x \ A; y \ A\ \ x = y" shows "A = {} \ (\ a. A = {a})" -by (metis assms insertCI nonempty_iff) +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 lemma depend_target_th: "(Th th, x) \ depend (s::state) \ \ cs. x = Cs cs" by (unfold s_depend_def, auto) @@ -962,7 +1076,13 @@ fixes s assumes vt: "vt s" shows "wf ((depend s)^-1)" -by (metis acyclic_depend assms finite_acyclic_wf_converse finite_depend) +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 lemma hd_np_in: "x \ set l \ hd l \ set l" by (induct l, auto) @@ -1083,17 +1203,31 @@ and eq_wq: "wq s cs = thread#rest" and not_in: "th \ set rest" shows "(th \ readys (V thread cs#s)) = (th \ readys s)" -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) +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 lemma chain_building: assumes vt: "vt s" @@ -1270,8 +1404,51 @@ 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) - 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) + 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 ultimately have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" by auto @@ -1368,7 +1545,7 @@ assume eq_e: "e = P thread cs" and is_runing: "thread \ runing s" and no_dep: "(Cs cs, Th thread) \ (depend s)\<^sup>+" - from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto + from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto show ?thesis proof - { have hh: "\ A B C. (B = C) \ (A \ B) = (A \ C)" by blast @@ -2052,8 +2229,9 @@ with eq_th12 eq_th' have "th1 \ dependents (wq s) th2" by simp hence "(Th th1, Th th2) \ (depend s)^+" by (unfold cs_dependents_def s_depend_def cs_depend_def, simp) - hence "Th th1 \ Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"] - by auto + hence "Th th1 \ Domain ((depend s)^+)" + apply (unfold cs_dependents_def cs_depend_def s_depend_def) + by (auto simp:Domain_def) hence "Th th1 \ Domain (depend s)" by (simp add:trancl_domain) then obtain n where d: "(Th th1, n) \ depend s" by (auto simp:Domain_def) from depend_target_th [OF this] @@ -2073,8 +2251,9 @@ with th1'_in eq_th12 have "th2 \ dependents (wq s) th1" by simp hence "(Th th2, Th th1) \ (depend s)^+" by (unfold cs_dependents_def s_depend_def cs_depend_def, simp) - hence "Th th2 \ Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"] - by auto + hence "Th th2 \ Domain ((depend s)^+)" + apply (unfold cs_dependents_def cs_depend_def s_depend_def) + by (auto simp:Domain_def) hence "Th th2 \ Domain (depend s)" by (simp add:trancl_domain) then obtain n where d: "(Th th2, n) \ depend s" by (auto simp:Domain_def) from depend_target_th [OF this] @@ -2131,20 +2310,106 @@ assumes le_ij: "i \ j" and le_js: "j \ length s" shows "length (down_to j i s) = j - i" -by (metis down_to_def le_ij le_js length_from_to_in length_rev) +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 lemma moment_head: assumes le_it: "Suc i \ length t" obtains e where "moment (Suc i) t = e#moment i t" -by (metis assms moment_plus) +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 lemma cnp_cnv_eq: fixes th s assumes "vt s" and "th \ threads s" shows "cntP s th = cntV s th" -by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs) +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 lemma eq_depend: "depend (wq s) = depend s" @@ -2252,8 +2517,43 @@ lemma le_cp: assumes vt: "vt s" shows "preced th s \ cp s th" -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) +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 lemma max_cp_eq: assumes vt: "vt s"