diff -r 2056d9f481e2 -r ed938e2246b9 CpsG.thy~ --- a/CpsG.thy~ Thu Jan 28 16:36:46 2016 +0800 +++ b/CpsG.thy~ Thu Jan 28 21:14:17 2016 +0800 @@ -2,6 +2,17 @@ imports PIPDefs begin +lemma f_image_eq: + assumes h: "\ a. a \ A \ f a = g a" + shows "f ` A = g ` A" +proof + show "f ` A \ g ` A" + by(rule image_subsetI, auto intro:h) +next + show "g ` A \ f ` A" + by (rule image_subsetI, auto intro:h[symmetric]) +qed + lemma Max_fg_mono: assumes "finite A" and "\ a \ A. f a \ g a" @@ -46,6 +57,57 @@ from fnt and seq show "finite (f ` B)" by auto qed +lemma Max_UNION: + assumes "finite A" + and "A \ {}" + and "\ M \ f ` A. finite M" + and "\ M \ f ` A. M \ {}" + shows "Max (\x\ A. f x) = Max (Max ` f ` A)" (is "?L = ?R") + using assms[simp] +proof - + have "?L = Max (\(f ` A))" + by (fold Union_image_eq, simp) + also have "... = ?R" + by (subst Max_Union, simp+) + finally show ?thesis . +qed + +lemma max_Max_eq: + assumes "finite A" + and "A \ {}" + and "x = y" + shows "max x (Max A) = Max ({y} \ A)" (is "?L = ?R") +proof - + have "?R = Max (insert y A)" by simp + also from assms have "... = ?L" + by (subst Max.insert, simp+) + finally show ?thesis by simp +qed + +lemma birth_time_lt: + assumes "s \ []" + shows "last_set th s < length s" + using assms +proof(induct s) + case (Cons a s) + show ?case + proof(cases "s \ []") + case False + thus ?thesis + by (cases a, auto) + next + case True + show ?thesis using Cons(1)[OF True] + by (cases a, auto) + qed +qed simp + +lemma th_in_ne: "th \ threads s \ s \ []" + by (induct s, auto) + +lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" + by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt) + lemma eq_RAG: "RAG (wq s) = RAG s" by (unfold cs_RAG_def s_RAG_def, auto) @@ -1475,16 +1537,16 @@ by (unfold s_RAG_def cs_waiting_def cs_holding_def, auto intro:wq_threads) +lemma RAG_threads: + assumes "(Th th) \ Field (RAG s)" + shows "th \ threads s" + using assms + by (metis Field_def UnE dm_RAG_threads rg_RAG_threads) + end - - - -lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s" - by (unfold preced_def, simp) - lemma (in valid_trace_v) - preced_es: "preced th (e#s) = preced th s" + preced_es [simp]: "preced th (e#s) = preced th s" by (unfold is_v preced_def, simp) lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s" @@ -2105,6 +2167,44 @@ qed qed +lemma tRAG_alt_def: + "tRAG s = {(Th th1, Th th2) | th1 th2. + \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" + by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) + +sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" +proof - + have "fsubtree (tRAG s)" + proof - + have "fbranch (tRAG s)" + proof(unfold tRAG_def, rule fbranch_compose) + show "fbranch (wRAG s)" + proof(rule finite_fbranchI) + from finite_RAG show "finite (wRAG s)" + by (unfold RAG_split, auto) + qed + next + show "fbranch (hRAG s)" + proof(rule finite_fbranchI) + from finite_RAG + show "finite (hRAG s)" by (unfold RAG_split, auto) + qed + qed + moreover have "wf (tRAG s)" + proof(rule wf_subset) + show "wf (RAG s O RAG s)" using wf_RAG + by (fold wf_comp_self, simp) + next + show "tRAG s \ (RAG s O RAG s)" + by (unfold tRAG_alt_def, auto) + qed + ultimately show ?thesis + by (unfold fsubtree_def fsubtree_axioms_def,auto) + qed + from this[folded tRAG_def] show "fsubtree (tRAG s)" . +qed + + context valid_trace begin @@ -2119,7 +2219,7 @@ have "?B = (subtree (RAG s) (Th th)) \ {Th th' | th'. True}" by auto moreover have "... \ (subtree (RAG s) (Th th))" by auto - moreover have "finite ..." by (simp add: finite_subtree) + moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) ultimately show ?thesis by auto qed ultimately show ?thesis by auto @@ -2169,10 +2269,6 @@ ultimately show ?thesis by auto qed -lemma max_cp_eq_the_preced: - shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" - using max_cp_eq using the_preced_def by presburger - lemma wf_RAG_converse: shows "wf ((RAG s)^-1)" proof(rule finite_acyclic_wf_converse) @@ -2317,9 +2413,6 @@ "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}" by (unfold s_RAG_def, auto simp:children_def holding_eq) -fun the_cs :: "node \ cs" where - "the_cs (Cs cs) = cs" - lemma holdents_alt_def: "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))" by (unfold children_RAG_alt_def holdents_def, simp add: image_image) @@ -2333,7 +2426,7 @@ begin lemma finite_holdents: "finite (holdents s th)" - by (unfold holdents_alt_def, insert finite_children, auto) + by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto) end @@ -2577,7 +2670,7 @@ using readys_kept1[OF assms] readys_kept2[OF assms] by metis -lemma cnp_cnv_cncs_kept: +lemma cnp_cnv_cncs_kept: (* ddd *) assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" proof(cases "th' = th") @@ -3643,29 +3736,921 @@ from star_rpath[OF star2] obtain xs2 where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)" by auto + from rp1 rp2 show ?thesis - proof(cases rule:rtree_RAG.rpath_overlap[OF rp1 rp2]) - case (1 xs') + proof(cases) + case (less_1 xs') moreover have "xs' = []" proof(rule ccontr) assume otherwise: "xs' \ []" - find_theorems rpath "_@_" + from rpath_plus[OF less_1(3) this] + have "(Th th1, Th th2) \ (RAG s)\<^sup>+" . + from tranclD[OF this] + obtain cs where "waiting s th1 cs" + by (unfold s_RAG_def, fold waiting_eq, auto) + with runing_1 show False + by (unfold runing_def readys_def, auto) qed ultimately have "xs2 = xs1" by simp from rpath_dest_eq[OF rp1 rp2[unfolded this]] show ?thesis by simp next - case (2 xs') - moreover have "xs' = []" sorry + case (less_2 xs') + moreover have "xs' = []" + proof(rule ccontr) + assume otherwise: "xs' \ []" + from rpath_plus[OF less_2(3) this] + have "(Th th2, Th th1) \ (RAG s)\<^sup>+" . + from tranclD[OF this] + obtain cs where "waiting s th2 cs" + by (unfold s_RAG_def, fold waiting_eq, auto) + with runing_2 show False + by (unfold runing_def readys_def, auto) + qed ultimately have "xs2 = xs1" by simp from rpath_dest_eq[OF rp1 rp2[unfolded this]] show ?thesis by simp qed qed +lemma card_runing: "card (runing s) \ 1" +proof(cases "runing s = {}") + case True + thus ?thesis by auto +next + case False + then obtain th where [simp]: "th \ runing s" by auto + from runing_unique[OF this] + have "runing s = {th}" by auto + thus ?thesis by auto +qed + +lemma create_pre: + assumes stp: "step s e" + and not_in: "th \ threads s" + and is_in: "th \ threads (e#s)" + obtains prio where "e = Create th prio" +proof - + from assms + show ?thesis + proof(cases) + case (thread_create thread prio) + with is_in not_in have "e = Create th prio" by simp + from that[OF this] show ?thesis . + next + case (thread_exit thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_P thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_V thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_set thread) + with assms show ?thesis by (auto intro!:that) + qed +qed + +lemma eq_pv_children: + assumes eq_pv: "cntP s th = cntV s th" + shows "children (RAG s) (Th th) = {}" +proof - + from cnp_cnv_cncs and eq_pv + have "cntCS s th = 0" + by (auto split:if_splits) + from this[unfolded cntCS_def holdents_alt_def] + have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" . + have "finite (the_cs ` children (RAG s) (Th th))" + by (simp add: fsbtRAGs.finite_children) + from card_0[unfolded card_0_eq[OF this]] + show ?thesis by auto +qed + +lemma eq_pv_holdents: + assumes eq_pv: "cntP s th = cntV s th" + shows "holdents s th = {}" + by (unfold holdents_alt_def eq_pv_children[OF assms], simp) + +lemma eq_pv_subtree: + assumes eq_pv: "cntP s th = cntV s th" + shows "subtree (RAG s) (Th th) = {Th th}" + using eq_pv_children[OF assms] + by (unfold subtree_children, simp) + end - +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) + +lemma tRAG_nodeE: + assumes "(n1, n2) \ tRAG s" + obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" + using assms + by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) + +lemma subtree_nodeE: + assumes "n \ subtree (tRAG s) (Th th)" + obtains th1 where "n = Th th1" +proof - + show ?thesis + proof(rule subtreeE[OF assms]) + assume "n = Th th" + from that[OF this] show ?thesis . + next + assume "Th th \ ancestors (tRAG s) n" + hence "(n, Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) + hence "\ th1. n = Th th1" + proof(induct) + case (base y) + from tRAG_nodeE[OF this] show ?case by metis + next + case (step y z) + thus ?case by auto + qed + with that show ?thesis by auto + qed +qed + +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 a + assume "a \ subtree (tRAG s) x" + hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) + with tRAG_star_RAG + 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_trancl_eq: + "{th'. (Th th', Th th) \ (tRAG s)^+} = + {th'. (Th th', Th th) \ (RAG s)^+}" + (is "?L = ?R") +proof - + { fix th' + assume "th' \ ?L" + hence "(Th th', Th th) \ (tRAG s)^+" by auto + from tranclD[OF this] + obtain z where h: "(Th th', z) \ tRAG s" "(z, Th th) \ (tRAG s)\<^sup>*" by auto + from tRAG_subtree_RAG and this(2) + have "(z, Th th) \ (RAG s)^*" by (meson subsetCE tRAG_star_RAG) + moreover from h(1) have "(Th th', z) \ (RAG s)^+" using tRAG_alt_def by auto + ultimately have "th' \ ?R" by auto + } moreover + { fix th' + assume "th' \ ?R" + hence "(Th th', Th th) \ (RAG s)^+" by (auto) + from plus_rpath[OF this] + obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \ []" by auto + hence "(Th th', Th th) \ (tRAG s)^+" + proof(induct xs arbitrary:th' th rule:length_induct) + case (1 xs th' th) + then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) + show ?case + proof(cases "xs1") + case Nil + from 1(2)[unfolded Cons1 Nil] + have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . + hence "(Th th', x1) \ (RAG s)" + by (cases, auto) + then obtain cs where "x1 = Cs cs" + by (unfold s_RAG_def, auto) + from rpath_nnl_lastE[OF rp[unfolded this]] + show ?thesis by auto + next + case (Cons x2 xs2) + from 1(2)[unfolded Cons1[unfolded this]] + have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . + from rpath_edges_on[OF this] + have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . + have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + with eds have rg1: "(Th th', x1) \ RAG s" by auto + then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) + have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + from this eds + have rg2: "(x1, x2) \ RAG s" by auto + from this[unfolded eq_x1] + obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) + from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] + have rt1: "(Th th', Th th1) \ tRAG s" by (unfold tRAG_alt_def, auto) + from rp have "rpath (RAG s) x2 xs2 (Th th)" + by (elim rpath_ConsE, simp) + from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . + show ?thesis + proof(cases "xs2 = []") + case True + from rpath_nilE[OF rp'[unfolded this]] + have "th1 = th" by auto + from rt1[unfolded this] show ?thesis by auto + next + case False + from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] + have "(Th th1, Th th) \ (tRAG s)\<^sup>+" by simp + with rt1 show ?thesis by auto + qed + qed + qed + hence "th' \ ?L" by auto + } ultimately show ?thesis by blast +qed + +lemma tRAG_trancl_eq_Th: + "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = + {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" + using tRAG_trancl_eq by auto + +lemma dependants_alt_def: + "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" + by (metis eq_RAG s_dependants_def tRAG_trancl_eq) + +lemma dependants_alt_def1: + "dependants (s::state) th = {th'. (Th th', Th th) \ (RAG s)^+}" + using dependants_alt_def tRAG_trancl_eq by auto + +context valid_trace +begin +lemma count_eq_RAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" +proof(rule ccontr) + assume otherwise: "{th'. (Th th', Th th) \ (RAG s)\<^sup>+} \ {}" + then obtain th' where "(Th th', Th th) \ (RAG s)^+" by auto + from tranclD2[OF this] + obtain z where "z \ children (RAG s) (Th th)" + by (auto simp:children_def) + with eq_pv_children[OF assms] + show False by simp +qed + +lemma eq_pv_dependants: + assumes eq_pv: "cntP s th = cntV s th" + shows "dependants s th = {}" +proof - + from count_eq_RAG_plus[OF assms, folded dependants_alt_def1] + show ?thesis . +qed + +end + +lemma eq_dependants: "dependants (wq s) = dependants s" + by (simp add: s_dependants_abv wq_def) + +context valid_trace +begin + +lemma count_eq_tRAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" + using assms eq_pv_dependants dependants_alt_def eq_dependants by auto + +lemma count_eq_RAG_plus_Th: + assumes "cntP s th = cntV s th" + shows "{Th th' | th'. (Th th', Th th) \ (RAG s)^+} = {}" + using count_eq_RAG_plus[OF assms] by auto + +lemma count_eq_tRAG_plus_Th: + assumes "cntP s th = cntV s th" + shows "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = {}" + using count_eq_tRAG_plus[OF assms] by auto +end + +lemma inj_the_preced: + "inj_on (the_preced s) (threads s)" + by (metis inj_onI preced_unique the_preced_def) + +lemma tRAG_Field: + "Field (tRAG s) \ Field (RAG s)" + by (unfold tRAG_alt_def Field_def, auto) + +lemma tRAG_ancestorsE: + assumes "x \ ancestors (tRAG s) u" + obtains th where "x = Th th" +proof - + from assms have "(u, x) \ (tRAG s)^+" + by (unfold ancestors_def, auto) + from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto + then obtain th where "x = Th th" + by (unfold tRAG_alt_def, auto) + from that[OF this] show ?thesis . +qed + +lemma tRAG_mono: + assumes "RAG s' \ RAG s" + shows "tRAG s' \ tRAG s" + using assms + by (unfold tRAG_alt_def, auto) + +lemma holding_next_thI: + assumes "holding s th cs" + and "length (wq s cs) > 1" + obtains th' where "next_th s th cs th'" +proof - + from assms(1)[folded holding_eq, unfolded cs_holding_def] + have " th \ set (wq s cs) \ th = hd (wq s cs)" + by (unfold s_holding_def, fold wq_def, auto) + then obtain rest where h1: "wq s cs = th#rest" + by (cases "wq s cs", auto) + with assms(2) have h2: "rest \ []" by auto + let ?th' = "hd (SOME q. distinct q \ set q = set rest)" + have "next_th s th cs ?th'" using h1(1) h2 + by (unfold next_th_def, auto) + from that[OF this] show ?thesis . +qed + +lemma RAG_tRAG_transfer: + assumes "vt s'" + assumes "RAG s = RAG s' \ {(Th th, Cs cs)}" + and "(Cs cs, Th th'') \ RAG s'" + shows "tRAG s = tRAG s' \ {(Th th, Th th'')}" (is "?L = ?R") +proof - + interpret vt_s': valid_trace "s'" using assms(1) + by (unfold_locales, simp) + { fix n1 n2 + assume "(n1, n2) \ ?L" + from this[unfolded tRAG_alt_def] + obtain th1 th2 cs' where + h: "n1 = Th th1" "n2 = Th th2" + "(Th th1, Cs cs') \ RAG s" + "(Cs cs', Th th2) \ RAG s" by auto + from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \ RAG s'" by auto + from h(3) and assms(2) + have "(Th th1, Cs cs') = (Th th, Cs cs) \ + (Th th1, Cs cs') \ RAG s'" by auto + hence "(n1, n2) \ ?R" + proof + assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" + hence eq_th1: "th1 = th" by simp + moreover have "th2 = th''" + proof - + from h1 have "cs' = cs" by simp + from assms(3) cs_in[unfolded this] + show ?thesis using vt_s'.unique_RAG by auto + qed + ultimately show ?thesis using h(1,2) by auto + next + assume "(Th th1, Cs cs') \ RAG s'" + with cs_in have "(Th th1, Th th2) \ tRAG s'" + by (unfold tRAG_alt_def, auto) + from this[folded h(1, 2)] show ?thesis by auto + qed + } moreover { + fix n1 n2 + assume "(n1, n2) \ ?R" + hence "(n1, n2) \tRAG s' \ (n1, n2) = (Th th, Th th'')" by auto + hence "(n1, n2) \ ?L" + proof + assume "(n1, n2) \ tRAG s'" + moreover have "... \ ?L" + proof(rule tRAG_mono) + show "RAG s' \ RAG s" by (unfold assms(2), auto) + qed + ultimately show ?thesis by auto + next + assume eq_n: "(n1, n2) = (Th th, Th th'')" + from assms(2, 3) have "(Cs cs, Th th'') \ RAG s" by auto + moreover have "(Th th, Cs cs) \ RAG s" using assms(2) by auto + ultimately show ?thesis + by (unfold eq_n tRAG_alt_def, auto) + qed + } ultimately show ?thesis by auto +qed + +context valid_trace +begin + +lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] end +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 h: "n \ ?L" + hence "n \ ?R" + by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) + } moreover { + 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 rtranclD[OF this(2)] + have "n \ ?L" + proof + assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" + with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto + thus ?thesis using subtree_def tRAG_trancl_eq by fastforce + qed (insert h, auto simp:subtree_def) + } 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 - + have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = + ((the_preced s \ the_thread) ` subtree (tRAG s) (Th th))" + by auto + thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) +qed + +lemma cp_gen_def_cond: + assumes "x = Th th" + shows "cp s th = cp_gen s (Th th)" +by (unfold cp_alt_def1 cp_gen_def, simp) + +lemma cp_gen_over_set: + assumes "\ x \ A. \ th. x = Th th" + shows "cp_gen s ` A = (cp s \ the_thread) ` A" +proof(rule f_image_eq) + fix a + assume "a \ A" + from assms[rule_format, OF this] + obtain th where eq_a: "a = Th th" by auto + show "cp_gen s a = (cp s \ the_thread) a" + by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) +qed + +context valid_trace +begin + +lemma subtree_tRAG_thread: + assumes "th \ threads s" + shows "subtree (tRAG s) (Th th) \ Th ` threads s" (is "?L \ ?R") +proof - + have "?L = {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" + by (unfold tRAG_subtree_eq, simp) + also have "... \ ?R" + proof + fix x + assume "x \ {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" + then obtain th' where h: "x = Th th'" "Th th' \ subtree (RAG s) (Th th)" by auto + from this(2) + show "x \ ?R" + proof(cases rule:subtreeE) + case 1 + thus ?thesis by (simp add: assms h(1)) + next + case 2 + thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) + qed + qed + finally show ?thesis . +qed + +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)" +proof + assume "(Th th) \ Field (RAG s)" + with dm_RAG_threads and rg_RAG_threads assms + show False by (unfold Field_def, blast) +qed + +end + +definition detached :: "state \ thread \ bool" + where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\cs. waiting s th cs))" + + +lemma detached_test: + shows "detached s th = (Th th \ Field (RAG s))" +apply(simp add: detached_def Field_def) +apply(simp add: s_RAG_def) +apply(simp add: s_holding_abv s_waiting_abv) +apply(simp add: Domain_iff Range_iff) +apply(simp add: wq_def) +apply(auto) +done + +context valid_trace +begin + +lemma detached_intro: + assumes eq_pv: "cntP s th = cntV s th" + shows "detached s th" +proof - + from eq_pv cnp_cnv_cncs + have "th \ readys s \ th \ threads s" by (auto simp:pvD_def) + thus ?thesis + proof + assume "th \ threads s" + with rg_RAG_threads dm_RAG_threads + show ?thesis + by (auto simp add: detached_def s_RAG_def s_waiting_abv + s_holding_abv wq_def Domain_iff Range_iff) + next + assume "th \ readys s" + moreover have "Th th \ Range (RAG s)" + proof - + from eq_pv_children[OF assms] + have "children (RAG s) (Th th) = {}" . + thus ?thesis + by (unfold children_def, auto) + qed + ultimately show ?thesis + by (auto simp add: detached_def s_RAG_def s_waiting_abv + s_holding_abv wq_def readys_def) + qed +qed + +lemma detached_elim: + assumes dtc: "detached s th" + shows "cntP s th = cntV s th" +proof - + have cncs_z: "cntCS s th = 0" + proof - + from dtc have "holdents s th = {}" + unfolding detached_def holdents_test s_RAG_def + by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) + thus ?thesis by (auto simp:cntCS_def) + qed + show ?thesis + proof(cases "th \ threads s") + case True + with dtc + have "th \ readys s" + by (unfold readys_def detached_def Field_def Domain_def Range_def, + auto simp:waiting_eq s_RAG_def) + with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def) + next + case False + with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def) + qed +qed + +lemma detached_eq: + shows "(detached s th) = (cntP s th = cntV s th)" + by (insert vt, auto intro:detached_intro detached_elim) + +end + +context valid_trace +begin +(* ddd *) +lemma cp_gen_rec: + assumes "x = Th th" + shows "cp_gen s x = Max ({the_preced s th} \ (cp_gen s) ` children (tRAG s) x)" +proof(cases "children (tRAG s) x = {}") + case True + show ?thesis + by (unfold True cp_gen_def subtree_children, simp add:assms) +next + case False + hence [simp]: "children (tRAG s) x \ {}" by auto + note fsbttRAGs.finite_subtree[simp] + have [simp]: "finite (children (tRAG s) x)" + by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], + rule children_subtree) + { fix r x + have "subtree r x \ {}" by (auto simp:subtree_def) + } note this[simp] + have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" + proof - + from False obtain q where "q \ children (tRAG s) x" by blast + moreover have "subtree (tRAG s) q \ {}" by simp + ultimately show ?thesis by blast + qed + have h: "Max ((the_preced s \ the_thread) ` + ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = + Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" + (is "?L = ?R") + proof - + let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L + let "Max (_ \ (?h ` ?B))" = ?R + let ?L1 = "?f ` \(?g ` ?B)" + have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" + proof - + have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp + also have "... = (\ x \ ?B. ?f ` (?g x))" by auto + finally have "Max ?L1 = Max ..." by simp + also have "... = Max (Max ` (\x. ?f ` subtree (tRAG s) x) ` ?B)" + by (subst Max_UNION, simp+) + also have "... = Max (cp_gen s ` children (tRAG s) x)" + by (unfold image_comp cp_gen_alt_def, simp) + finally show ?thesis . + qed + show ?thesis + proof - + have "?L = Max (?f ` ?A \ ?L1)" by simp + also have "... = max (the_preced s (the_thread x)) (Max ?L1)" + by (subst Max_Un, simp+) + also have "... = max (?f x) (Max (?h ` ?B))" + by (unfold eq_Max_L1, simp) + also have "... =?R" + by (rule max_Max_eq, (simp)+, unfold assms, simp) + finally show ?thesis . + qed + qed thus ?thesis + by (fold h subtree_children, unfold cp_gen_def, simp) +qed + +lemma cp_rec: + "cp s th = Max ({the_preced s th} \ + (cp s o the_thread) ` children (tRAG s) (Th th))" +proof - + have "Th th = Th th" by simp + note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] + show ?thesis + proof - + have "cp_gen s ` children (tRAG s) (Th th) = + (cp s \ the_thread) ` children (tRAG s) (Th th)" + proof(rule cp_gen_over_set) + show " \x\children (tRAG s) (Th th). \th. x = Th th" + by (unfold tRAG_alt_def, auto simp:children_def) + qed + thus ?thesis by (subst (1) h(1), unfold h(2), simp) + qed +qed + +lemma next_th_holding: + assumes nxt: "next_th s th cs th'" + shows "holding (wq s) th cs" +proof - + from nxt[unfolded next_th_def] + obtain rest where h: "wq s cs = th # rest" + "rest \ []" + "th' = hd (SOME q. distinct q \ set q = set rest)" by auto + thus ?thesis + by (unfold cs_holding_def, auto) +qed + +lemma next_th_waiting: + assumes nxt: "next_th s th cs th'" + shows "waiting (wq s) th' cs" +proof - + from nxt[unfolded next_th_def] + obtain rest where h: "wq s cs = th # rest" + "rest \ []" + "th' = hd (SOME q. distinct q \ set q = set rest)" by auto + from wq_distinct[of cs, unfolded h] + have dst: "distinct (th # rest)" . + have in_rest: "th' \ set rest" + proof(unfold h, rule someI2) + show "distinct rest \ set rest = set rest" using dst by auto + next + fix x assume "distinct x \ set x = set rest" + with h(2) + show "hd x \ set (rest)" by (cases x, auto) + qed + hence "th' \ set (wq s cs)" by (unfold h(1), auto) + moreover have "th' \ hd (wq s cs)" + by (unfold h(1), insert in_rest dst, auto) + ultimately show ?thesis by (auto simp:cs_waiting_def) +qed + +lemma next_th_RAG: + assumes nxt: "next_th (s::event list) th cs th'" + shows "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s" + using vt assms next_th_holding next_th_waiting + by (unfold s_RAG_def, simp) + +end + +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) + +context valid_trace +begin + +thm th_chain_to_ready + +find_theorems subtree Th RAG + +lemma "(threads s) = (\ th \ readys s. {th'. Th th' \ subtree (RAG s) (Th th)})" + (is "?L = ?R") +proof - + { fix th1 + assume "th1 \ ?L" + from th_chain_to_ready[OF this] + have "th1 \ readys s \ (\th'a. th'a \ readys s \ (Th th1, Th th'a) \ (RAG s)\<^sup>+)" . + hence "th1 \ ?R" + proof + assume "th1 \ readys s" + thus ?thesis by (auto simp:subtree_def) + next + assume "\th'a. th'a \ readys s \ (Th th1, Th th'a) \ (RAG s)\<^sup>+" + thus ?thesis + qed + } moreover + { fix th' + assume "th' \ ?R" + have "th' \ ?L" sorry + } ultimately show ?thesis by auto +qed + +lemma max_cp_readys_threads_pre: (* ccc *) + assumes np: "threads s \ {}" + shows "Max (cp s ` readys s) = Max (cp s ` threads s)" +proof(unfold max_cp_eq) + show "Max (cp s ` readys s) = Max (the_preced s ` threads s)" + proof - + let ?p = "Max (the_preced s ` threads s)" + let ?f = "the_preced s" + have "?p \ (?f ` threads s)" + proof(rule Max_in) + from finite_threads show "finite (?f ` threads s)" by simp + next + from np show "?f ` threads s \ {}" by simp + qed + then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \ threads s" + by (auto simp:Image_def) + from th_chain_to_ready [OF tm_in] + have "tm \ readys s \ (\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+)" . + thus ?thesis + proof + assume "\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+ " + then obtain th' where th'_in: "th' \ readys s" + and tm_chain:"(Th tm, Th th') \ (RAG s)\<^sup>+" by auto + have "cp s th' = ?f tm" + proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) + from dependants_threads finite_threads + show "finite ((\th. preced th s) ` ({th'} \ dependants (wq s) th'))" + by (auto intro:finite_subset) + next + fix p assume p_in: "p \ (\th. preced th s) ` ({th'} \ dependants (wq s) th')" + from tm_max have " preced tm s = Max ((\th. preced th s) ` threads s)" . + moreover have "p \ \" + proof(rule Max_ge) + from finite_threads + show "finite ((\th. preced th s) ` threads s)" by simp + next + from p_in and th'_in and dependants_threads[of th'] + show "p \ (\th. preced th s) ` threads s" + by (auto simp:readys_def) + qed + ultimately show "p \ preced tm s" by auto + next + show "preced tm s \ (\th. preced th s) ` ({th'} \ dependants (wq s) th')" + proof - + from tm_chain + have "tm \ dependants (wq s) th'" + by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto) + thus ?thesis by auto + qed + qed + with tm_max + have h: "cp s th' = Max ((\th. preced th s) ` threads s)" by simp + show ?thesis + proof (fold h, rule Max_eqI) + fix q + assume "q \ cp s ` readys s" + then obtain th1 where th1_in: "th1 \ readys s" + and eq_q: "q = cp s th1" by auto + show "q \ cp s th'" + apply (unfold h eq_q) + apply (unfold cp_eq_cpreced cpreced_def) + apply (rule Max_mono) + proof - + from dependants_threads [of th1] th1_in + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ + (\th. preced th s) ` threads s" + by (auto simp:readys_def) + next + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp + next + from finite_threads + show " finite ((\th. preced th s) ` threads s)" by simp + qed + next + from finite_threads + show "finite (cp s ` readys s)" by (auto simp:readys_def) + next + from th'_in + show "cp s th' \ cp s ` readys s" by simp + qed + next + assume tm_ready: "tm \ readys s" + show ?thesis + proof(fold tm_max) + have cp_eq_p: "cp s tm = preced tm s" + proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) + fix y + assume hy: "y \ (\th. preced th s) ` ({tm} \ dependants (wq s) tm)" + show "y \ preced tm s" + proof - + { fix y' + assume hy' : "y' \ ((\th. preced th s) ` dependants (wq s) tm)" + have "y' \ preced tm s" + proof(unfold tm_max, rule Max_ge) + from hy' dependants_threads[of tm] + show "y' \ (\th. preced th s) ` threads s" by auto + next + from finite_threads + show "finite ((\th. preced th s) ` threads s)" by simp + qed + } with hy show ?thesis by auto + qed + next + from dependants_threads[of tm] finite_threads + show "finite ((\th. preced th s) ` ({tm} \ dependants (wq s) tm))" + by (auto intro:finite_subset) + next + show "preced tm s \ (\th. preced th s) ` ({tm} \ dependants (wq s) tm)" + by simp + qed + moreover have "Max (cp s ` readys s) = cp s tm" + proof(rule Max_eqI) + from tm_ready show "cp s tm \ cp s ` readys s" by simp + next + from finite_threads + show "finite (cp s ` readys s)" by (auto simp:readys_def) + next + fix y assume "y \ cp s ` readys s" + then obtain th1 where th1_readys: "th1 \ readys s" + and h: "y = cp s th1" by auto + show "y \ cp s tm" + apply(unfold cp_eq_p h) + apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) + proof - + from finite_threads + show "finite ((\th. preced th s) ` threads s)" by simp + next + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" + by simp + next + from dependants_threads[of th1] th1_readys + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) + \ (\th. preced th s) ` threads s" + by (auto simp:readys_def) + qed + qed + ultimately show " Max (cp s ` readys s) = preced tm s" by simp + qed + qed + qed +qed + +text {* (* ccc *) \noindent + Since the current precedence of the threads in ready queue will always be boosted, + there must be one inside it has the maximum precedence of the whole system. +*} +lemma max_cp_readys_threads: + shows "Max (cp s ` readys s) = Max (cp s ` threads s)" +proof(cases "threads s = {}") + case True + thus ?thesis + by (auto simp:readys_def) +next + case False + show ?thesis by (rule max_cp_readys_threads_pre[OF False]) +qed + +end + +end +