diff -r f98a95f3deae -r f8194fd6214f CpsG.thy~ --- a/CpsG.thy~ Fri Dec 18 19:13:19 2015 +0800 +++ b/CpsG.thy~ Fri Dec 18 22:47:32 2015 +0800 @@ -6,12 +6,21 @@ imports PrioG Max RTree begin +definition "the_preced s th = preced th s" + +fun the_thread :: "node \ thread" where + "the_thread (Th th) = th" + definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" definition "tRAG s = wRAG s O hRAG s" +definition "cp_gen s x = + Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" +(* ccc *) + lemma RAG_split: "RAG s = (wRAG s \ hRAG s)" by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv s_holding_abv cs_RAG_def, auto) @@ -126,47 +135,6 @@ } ultimately show ?thesis by auto qed -lemma readys_root: - assumes "vt s" - and "th \ readys s" - shows "root (RAG s) (Th th)" -proof - - { fix x - assume "x \ ancestors (RAG s) (Th th)" - hence h: "(Th th, x) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - obtain z where "(Th th, z) \ RAG s" by auto - with assms(2) have False - apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) - by (fold wq_def, blast) - } thus ?thesis by (unfold root_def, auto) -qed - -lemma readys_in_no_subtree: - assumes "vt s" - and "th \ readys s" - and "th' \ th" - shows "Th th \ subtree (RAG s) (Th th')" -proof - assume "Th th \ subtree (RAG s) (Th th')" - thus False - proof(cases rule:subtreeE) - case 1 - with assms show ?thesis by auto - next - case 2 - with readys_root[OF assms(1,2)] - show ?thesis by (auto simp:root_def) - qed -qed - -lemma image_id: - assumes "\ x. x \ A \ f x = x" - shows "f ` A = A" - using assms by (auto simp:image_def) - -definition "the_preced s th = preced th s" - lemma cp_alt_def: "cp s th = Max ((the_preced s) ` {th'. Th th' \ (subtree (RAG s) (Th th))})" @@ -182,12 +150,6 @@ thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) qed -fun the_thread :: "node \ thread" where - "the_thread (Th th) = th" - -definition "cp_gen s x = - Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" - lemma cp_gen_alt_def: "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" by (auto simp:cp_gen_def) @@ -221,45 +183,43 @@ qed qed -lemma threads_set_eq: - "the_thread ` (subtree (tRAG s) (Th th)) = - {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") +lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" +proof - + have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" + by (rule rtrancl_mono, auto simp:RAG_split) + also have "... \ ((RAG s)^*)^*" + by (rule rtrancl_mono, auto) + also have "... = (RAG s)^*" by simp + finally show ?thesis by (unfold tRAG_def, simp) +qed + +lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" proof - - { fix th' - assume "th' \ ?L" - then obtain n where h: "th' = the_thread n" "n \ subtree (tRAG s) (Th th)" by auto - from subtree_nodeE[OF this(2)] - obtain th1 where "n = Th th1" by auto - with h have "Th th' \ subtree (tRAG s) (Th th)" by auto - hence "Th th' \ subtree (RAG s) (Th th)" - proof(cases rule:subtreeE[consumes 1]) - case 1 - thus ?thesis by (auto simp:subtree_def) - next - case 2 - hence "(Th th', Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) - thus ?thesis - proof(induct) - case (step y z) - from this(2)[unfolded tRAG_alt_def] - obtain u where - h: "(y, u) \ RAG s" "(u, z) \ RAG s" - by auto - hence "y \ subtree (RAG s) z" by (auto simp:subtree_def) - with step(3) - show ?case by (auto simp:subtree_def) - next - case (base y) - from this[unfolded tRAG_alt_def] - show ?case by (auto simp:subtree_def) - qed - qed - hence "th' \ ?R" by auto + { fix a + assume "a \ subtree (tRAG s) x" + hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) + with tRAG_star_RAG[of s] + have "(a, x) \ (RAG s)^*" by auto + hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) + } thus ?thesis by auto +qed + +lemma tRAG_subtree_eq: + "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \ (subtree (RAG s) (Th th))}" + (is "?L = ?R") +proof - + { fix n + assume "n \ ?L" + with subtree_nodeE[OF this] + obtain th' where "n = Th th'" "Th th' \ subtree (tRAG s) (Th th)" by auto + with tRAG_subtree_RAG[of s "Th th"] + have "n \ ?R" by auto } moreover { - fix th' - assume "th' \ ?R" - hence "(Th th', Th th) \ (RAG s)^*" by (auto simp:subtree_def) - from star_rpath[OF this] + fix n + assume "n \ ?R" + then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" + by (auto simp:subtree_def) + from star_rpath[OF this(2)] obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto hence "Th th' \ subtree (tRAG s) (Th th)" proof(induct xs arbitrary:th' th rule:length_induct) @@ -280,7 +240,6 @@ hence "(Th th', x1) \ (RAG s)" by (cases, simp) then obtain cs where "x1 = Cs cs" by (unfold s_RAG_def, auto) - find_theorems rpath "_ = _@[_]" from rpath_nnl_lastE[OF rp[unfolded this]] show ?thesis by auto next @@ -313,11 +272,16 @@ qed qed qed - from imageI[OF this, of the_thread] - have "th' \ ?L" by simp + from this[folded h(1)] + have "n \ ?L" . } ultimately show ?thesis by auto qed - + +lemma threads_set_eq: + "the_thread ` (subtree (tRAG s) (Th th)) = + {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") + by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) + lemma cp_alt_def1: "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" proof - @@ -344,8 +308,6 @@ by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) qed - - locale valid_trace = fixes s assumes vt : "vt s" @@ -353,6 +315,38 @@ context valid_trace begin +lemma readys_root: + assumes "th \ readys s" + shows "root (RAG s) (Th th)" +proof - + { fix x + assume "x \ ancestors (RAG s) (Th th)" + hence h: "(Th th, x) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + obtain z where "(Th th, z) \ RAG s" by auto + with assms(1) have False + apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) + by (fold wq_def, blast) + } thus ?thesis by (unfold root_def, auto) +qed + +lemma readys_in_no_subtree: + assumes "th \ readys s" + and "th' \ th" + shows "Th th \ subtree (RAG s) (Th th')" +proof + assume "Th th \ subtree (RAG s) (Th th')" + thus False + proof(cases rule:subtreeE) + case 1 + with assms show ?thesis by auto + next + case 2 + with readys_root[OF assms(1)] + show ?thesis by (auto simp:root_def) + qed +qed + lemma not_in_thread_isolated: assumes "th \ threads s" shows "(Th th) \ Field (RAG s)" @@ -566,169 +560,11 @@ end +(* ccc *) -lemma eq_dependants: "dependants (wq s) = dependants s" - by (simp add: s_dependants_abv wq_def) - + (* obvious lemma *) -lemma not_thread_holdents: - fixes th s - assumes vt: "vt s" - and not_in: "th \ threads s" - shows "holdents s th = {}" -proof - - from vt not_in show ?thesis - proof(induct arbitrary:th) - case (vt_cons s e th) - assume vt: "vt s" - and ih: "\th. th \ threads s \ holdents s th = {}" - and stp: "step s e" - and not_in: "th \ threads (e # s)" - from stp show ?case - proof(cases) - case (thread_create thread prio) - assume eq_e: "e = Create thread prio" - and not_in': "thread \ threads s" - have "holdents (e # s) th = holdents s th" - apply (unfold eq_e holdents_test) - by (simp add:RAG_create_unchanged) - moreover have "th \ threads s" - proof - - from not_in eq_e show ?thesis by simp - qed - moreover note ih ultimately show ?thesis by auto - next - case (thread_exit thread) - assume eq_e: "e = Exit thread" - and nh: "holdents s thread = {}" - show ?thesis - proof(cases "th = thread") - case True - with nh eq_e - show ?thesis - by (auto simp:holdents_test RAG_exit_unchanged) - next - case False - with not_in and eq_e - have "th \ threads s" by simp - from ih[OF this] False eq_e show ?thesis - by (auto simp:holdents_test RAG_exit_unchanged) - qed - next - case (thread_P thread cs) - assume eq_e: "e = P thread cs" - and is_runing: "thread \ runing s" - from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto - have neq_th: "th \ thread" - proof - - from not_in eq_e have "th \ threads s" by simp - moreover from is_runing have "thread \ threads s" - by (simp add:runing_def readys_def) - ultimately show ?thesis by auto - qed - hence "holdents (e # s) th = holdents s th " - apply (unfold cntCS_def holdents_test eq_e) - by (unfold step_RAG_p[OF vtp], auto) - moreover have "holdents s th = {}" - proof(rule ih) - from not_in eq_e show "th \ threads s" by simp - qed - ultimately show ?thesis by simp - next - case (thread_V thread cs) - assume eq_e: "e = V thread cs" - and is_runing: "thread \ runing s" - and hold: "holding s thread cs" - have neq_th: "th \ thread" - proof - - from not_in eq_e have "th \ threads s" by simp - moreover from is_runing have "thread \ threads s" - by (simp add:runing_def readys_def) - ultimately show ?thesis by auto - qed - from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto - from hold obtain rest - where eq_wq: "wq s cs = thread # rest" - by (case_tac "wq s cs", auto simp: wq_def s_holding_def) - from not_in eq_e eq_wq - have "\ next_th s thread cs th" - apply (auto simp:next_th_def) - proof - - assume ne: "rest \ []" - and ni: "hd (SOME q. distinct q \ set q = set rest) \ threads s" (is "?t \ threads s") - have "?t \ set rest" - proof(rule someI2) - from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x assume "distinct x \ set x = set rest" with ne - show "hd x \ set rest" by (cases x, auto) - qed - with eq_wq have "?t \ set (wq s cs)" by simp - from wq_threads[OF step_back_vt[OF vtv], OF this] and ni - show False by auto - qed - moreover note neq_th eq_wq - ultimately have "holdents (e # s) th = holdents s th" - by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) - moreover have "holdents s th = {}" - proof(rule ih) - from not_in eq_e show "th \ threads s" by simp - qed - ultimately show ?thesis by simp - next - case (thread_set thread prio) - print_facts - assume eq_e: "e = Set thread prio" - and is_runing: "thread \ runing s" - from not_in and eq_e have "th \ threads s" by auto - from ih [OF this] and eq_e - show ?thesis - apply (unfold eq_e cntCS_def holdents_test) - by (simp add:RAG_set_unchanged) - qed - next - case vt_nil - show ?case - by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) - qed -qed - -(* obvious lemma *) -lemma next_th_neq: - assumes vt: "vt s" - and nt: "next_th s th cs th'" - shows "th' \ th" -proof - - from nt show ?thesis - apply (auto simp:next_th_def) - proof - - fix rest - assume eq_wq: "wq s cs = hd (SOME q. distinct q \ set q = set rest) # rest" - and ne: "rest \ []" - have "hd (SOME q. distinct q \ set q = set rest) \ set rest" - proof(rule someI2) - from wq_distinct[OF vt, of cs] eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x - assume "distinct x \ set x = set rest" - hence eq_set: "set x = set rest" by auto - with ne have "x \ []" by auto - hence "hd x \ set x" by auto - with eq_set show "hd x \ set rest" by auto - qed - with wq_distinct[OF vt, of cs] eq_wq show False by auto - qed -qed - -(* obvious lemma *) -lemma next_th_unique: - assumes nt1: "next_th s th cs th1" - and nt2: "next_th s th cs th2" - shows "th1 = th2" -using assms by (unfold next_th_def, auto) lemma wf_RAG: assumes vt: "vt s" @@ -2039,17 +1875,8 @@ proof - from readys_in_no_subtree[OF vat_s'.vt th_ready assms] have "(Th th) \ subtree (RAG s') (Th th')" . - find_theorems subtree tRAG RAG (* ccc *) - proof - assume "Th th \ subtree (tRAG s') (Th th')" - thus False - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF this(2)] - and th_tRAG[unfolded Field_def] - show ?thesis by auto - qed (insert assms, auto) - qed + with tRAG_subtree_RAG[of s' "Th th'"] + have "(Th th) \ subtree (tRAG s') (Th th')" by auto with a_in[unfolded eq_a] show ?thesis by auto qed from preced_kept[OF this]