diff -r b620a2a0806a -r b4bcd1edbb6d Implementation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Implementation.thy Wed Jan 06 16:34:26 2016 +0000 @@ -0,0 +1,1640 @@ +section {* + This file contains lemmas used to guide the recalculation of current precedence + after every system call (or system operation) +*} +theory Implementation +imports PIPBasics Max RTree +begin + +text {* @{text "the_preced"} is also the same as @{text "preced"}, the only + difference is the order of arguemts. *} +definition "the_preced s th = preced th s" + +lemma inj_the_preced: + "inj_on (the_preced s) (threads s)" + by (metis inj_onI preced_unique the_preced_def) + +text {* @{term "the_thread"} extracts thread out of RAG node. *} +fun the_thread :: "node \ thread" where + "the_thread (Th th) = th" + +text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} +definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" + +text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} +definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" + +text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} +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) + +text {* + The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}. + It characterizes the dependency between threads when calculating current + precedences. It is defined as the composition of the above two sub-graphs, + names @{term "wRAG"} and @{term "hRAG"}. + *} +definition "tRAG s = wRAG s O hRAG s" + +(* ccc *) + +definition "cp_gen s x = + Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" + +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) + +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 eq_holding, unfolded cs_holding_def] + have " th \ set (wq s cs) \ th = hd (wq s cs)" . + 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) + interpret rtree: rtree "RAG s'" + proof + show "single_valued (RAG s')" + apply (intro_locales) + by (unfold single_valued_def, + auto intro:vt_s'.unique_RAG) + + show "acyclic (RAG s')" + by (rule vt_s'.acyclic_RAG) + qed + { 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] rtree.sgv + show ?thesis + by (unfold single_valued_def, 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 cp_alt_def: + "cp s th = + Max ((the_preced s) ` {th'. Th th' \ (subtree (RAG s) (Th th))})" +proof - + have "Max (the_preced s ` ({th} \ dependants (wq s) th)) = + Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})" + (is "Max (_ ` ?L) = Max (_ ` ?R)") + proof - + have "?L = ?R" + by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def) + thus ?thesis by simp + qed + thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp) +qed + +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[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_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[of s] 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, simp) + 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) + +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 count_eq_dependants dependants_alt_def eq_dependants by auto + +lemma count_eq_RAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" + using assms count_eq_dependants cs_dependants_def eq_RAG 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 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 RAG_threads: + assumes "(Th th) \ Field (RAG s)" + shows "th \ threads s" + using assms + by (metis Field_def UnE dm_RAG_threads range_in vt) + +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 range_in assms + show False by (unfold Field_def, blast) +qed + +lemma wf_RAG: "wf (RAG s)" +proof(rule finite_acyclic_wf) + from finite_RAG show "finite (RAG s)" . +next + from acyclic_RAG show "acyclic (RAG s)" . +qed + +lemma sgv_wRAG: "single_valued (wRAG s)" + using waiting_unique + by (unfold single_valued_def wRAG_def, auto) + +lemma sgv_hRAG: "single_valued (hRAG s)" + using holding_unique + by (unfold single_valued_def hRAG_def, auto) + +lemma sgv_tRAG: "single_valued (tRAG s)" + by (unfold tRAG_def, rule single_valued_relcomp, + insert sgv_wRAG sgv_hRAG, auto) + +lemma acyclic_tRAG: "acyclic (tRAG s)" +proof(unfold tRAG_def, rule acyclic_compose) + show "acyclic (RAG s)" using acyclic_RAG . +next + show "wRAG s \ RAG s" unfolding RAG_split by auto +next + show "hRAG s \ RAG s" unfolding RAG_split by auto +qed + +lemma sgv_RAG: "single_valued (RAG s)" + using unique_RAG by (auto simp:single_valued_def) + +lemma rtree_RAG: "rtree (RAG s)" + using sgv_RAG acyclic_RAG + by (unfold rtree_def rtree_axioms_def sgv_def, auto) + +end + + +sublocale valid_trace < rtree_RAG: rtree "RAG s" +proof + show "single_valued (RAG s)" + apply (intro_locales) + by (unfold single_valued_def, + auto intro:unique_RAG) + + show "acyclic (RAG s)" + by (rule acyclic_RAG) +qed + +sublocale valid_trace < rtree_s: rtree "tRAG s" +proof(unfold_locales) + from sgv_tRAG show "single_valued (tRAG s)" . +next + from acyclic_tRAG show "acyclic (tRAG s)" . +qed + +sublocale valid_trace < fsbtRAGs : fsubtree "RAG s" +proof - + show "fsubtree (RAG s)" + proof(intro_locales) + show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . + next + show "fsubtree_axioms (RAG s)" + proof(unfold fsubtree_axioms_def) + find_theorems wf RAG + from wf_RAG show "wf (RAG s)" . + qed + qed +qed + +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 + +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 + +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 + +end + +(* keep *) +lemma next_th_holding: + assumes vt: "vt s" + and 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 + +context valid_trace +begin + +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 + +-- {* A useless definition *} +definition cps:: "state \ (thread \ precedence) set" +where "cps s = {(th, cp s th) | th . th \ threads s}" + + +text {* (* ddd *) + One beauty of our modelling is that we follow the definitional extension tradition of HOL. + The benefit of such a concise and miniature model is that large number of intuitively + obvious facts are derived as lemmas, rather than asserted as axioms. +*} + +text {* + However, the lemmas in the forthcoming several locales are no longer + obvious. These lemmas show how the current precedences should be recalculated + after every execution step (in our model, every step is represented by an event, + which in turn, represents a system call, or operation). Each operation is + treated in a separate locale. + + The complication of current precedence recalculation comes + because the changing of RAG needs to be taken into account, + in addition to the changing of precedence. + The reason RAG changing affects current precedence is that, + according to the definition, current precedence + of a thread is the maximum of the precedences of its dependants, + where the dependants are defined in terms of RAG. + + Therefore, each operation, lemmas concerning the change of the precedences + and RAG are derived first, so that the lemmas about + current precedence recalculation can be based on. +*} + +text {* (* ddd *) + The following locale @{text "step_set_cps"} investigates the recalculation + after the @{text "Set"} operation. +*} +locale step_set_cps = + fixes s' th prio s + -- {* @{text "s'"} is the system state before the operation *} + -- {* @{text "s"} is the system state after the operation *} + defines s_def : "s \ (Set th prio#s')" + -- {* @{text "s"} is assumed to be a legitimate state, from which + the legitimacy of @{text "s"} can be derived. *} + assumes vt_s: "vt s" + +sublocale step_set_cps < vat_s : valid_trace "s" +proof + from vt_s show "vt s" . +qed + +sublocale step_set_cps < vat_s' : valid_trace "s'" +proof + from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . +qed + +context step_set_cps +begin + +text {* (* ddd *) + The following two lemmas confirm that @{text "Set"}-operating only changes the precedence + of the initiating thread. +*} + +lemma eq_preced: + assumes "th' \ th" + shows "preced th' s = preced th' s'" +proof - + from assms show ?thesis + by (unfold s_def, auto simp:preced_def) +qed + +lemma eq_the_preced: + fixes th' + assumes "th' \ th" + shows "the_preced s th' = the_preced s' th'" + using assms + by (unfold the_preced_def, intro eq_preced, simp) + +text {* + The following lemma assures that the resetting of priority does not change the RAG. +*} + +lemma eq_dep: "RAG s = RAG s'" + by (unfold s_def RAG_set_unchanged, auto) + +text {* (* ddd *) + Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"} + only affects those threads, which as @{text "Th th"} in their sub-trees. + + The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. +*} + +lemma eq_cp_pre: + fixes th' + assumes nd: "Th th \ subtree (RAG s') (Th th')" + shows "cp s th' = cp s' th'" +proof - + -- {* After unfolding using the alternative definition, elements + affecting the @{term "cp"}-value of threads become explicit. + We only need to prove the following: *} + have "Max (the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')}) = + Max (the_preced s' ` {th'a. Th th'a \ subtree (RAG s') (Th th')})" + (is "Max (?f ` ?S1) = Max (?g ` ?S2)") + proof - + -- {* The base sets are equal. *} + have "?S1 = ?S2" using eq_dep by simp + -- {* The function values on the base set are equal as well. *} + moreover have "\ e \ ?S2. ?f e = ?g e" + proof + fix th1 + assume "th1 \ ?S2" + with nd have "th1 \ th" by (auto) + from eq_the_preced[OF this] + show "the_preced s th1 = the_preced s' th1" . + qed + -- {* Therefore, the image of the functions are equal. *} + ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq) + thus ?thesis by simp + qed + thus ?thesis by (simp add:cp_alt_def) +qed + +text {* + The following lemma shows that @{term "th"} is not in the + sub-tree of any other thread. +*} +lemma th_in_no_subtree: + assumes "th' \ th" + shows "Th th \ subtree (RAG s') (Th th')" +proof - + have "th \ readys s'" + proof - + from step_back_step [OF vt_s[unfolded s_def]] + have "step s' (Set th prio)" . + hence "th \ runing s'" by (cases, simp) + thus ?thesis by (simp add:readys_def runing_def) + qed + find_theorems readys subtree + from vat_s'.readys_in_no_subtree[OF this assms(1)] + show ?thesis by blast +qed + +text {* + By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, + it is obvious that the change of priority only affects the @{text "cp"}-value + of the initiating thread @{text "th"}. +*} +lemma eq_cp: + fixes th' + assumes "th' \ th" + shows "cp s th' = cp s' th'" + by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) + +end + +text {* + The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. +*} + +locale step_v_cps = + -- {* @{text "th"} is the initiating thread *} + -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *} + fixes s' th cs s -- {* @{text "s'"} is the state before operation*} + defines s_def : "s \ (V th cs#s')" -- {* @{text "s"} is the state after operation*} + -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *} + assumes vt_s: "vt s" + +sublocale step_v_cps < vat_s : valid_trace "s" +proof + from vt_s show "vt s" . +qed + +sublocale step_v_cps < vat_s' : valid_trace "s'" +proof + from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . +qed + +context step_v_cps +begin + +lemma ready_th_s': "th \ readys s'" + using step_back_step[OF vt_s[unfolded s_def]] + by (cases, simp add:runing_def) + +lemma ancestors_th: "ancestors (RAG s') (Th th) = {}" +proof - + from vat_s'.readys_root[OF ready_th_s'] + show ?thesis + by (unfold root_def, simp) +qed + +lemma holding_th: "holding s' th cs" +proof - + from vt_s[unfolded s_def] + have " PIP s' (V th cs)" by (cases, simp) + thus ?thesis by (cases, auto) +qed + +lemma edge_of_th: + "(Cs cs, Th th) \ RAG s'" +proof - + from holding_th + show ?thesis + by (unfold s_RAG_def holding_eq, auto) +qed + +lemma ancestors_cs: + "ancestors (RAG s') (Cs cs) = {Th th}" +proof - + have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th) \ {Th th}" + proof(rule vat_s'.rtree_RAG.ancestors_accum) + from vt_s[unfolded s_def] + have " PIP s' (V th cs)" by (cases, simp) + thus "(Cs cs, Th th) \ RAG s'" + proof(cases) + assume "holding s' th cs" + from this[unfolded holding_eq] + show ?thesis by (unfold s_RAG_def, auto) + qed + qed + from this[unfolded ancestors_th] show ?thesis by simp +qed + +lemma preced_kept: "the_preced s = the_preced s'" + by (auto simp: s_def the_preced_def preced_def) + +end + +text {* + The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, + which represents the case when there is another thread @{text "th'"} + to take over the critical resource released by the initiating thread @{text "th"}. +*} +locale step_v_cps_nt = step_v_cps + + fixes th' + -- {* @{text "th'"} is assumed to take over @{text "cs"} *} + assumes nt: "next_th s' th cs th'" + +context step_v_cps_nt +begin + +text {* + Lemma @{text "RAG_s"} confirms the change of RAG: + two edges removed and one added, as shown by the following diagram. +*} + +(* + RAG before the V-operation + th1 ----| + | + th' ----| + |----> cs -----| + th2 ----| | + | | + th3 ----| | + |------> th + th4 ----| | + | | + th5 ----| | + |----> cs'-----| + th6 ----| + | + th7 ----| + + RAG after the V-operation + th1 ----| + | + |----> cs ----> th' + th2 ----| + | + th3 ----| + + th4 ----| + | + th5 ----| + |----> cs'----> th + th6 ----| + | + th7 ----| +*) + +lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s'" + using next_th_RAG[OF nt] . + +lemma ancestors_th': + "ancestors (RAG s') (Th th') = {Th th, Cs cs}" +proof - + have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \ {Cs cs}" + proof(rule vat_s'.rtree_RAG.ancestors_accum) + from sub_RAGs' show "(Th th', Cs cs) \ RAG s'" by auto + qed + thus ?thesis using ancestors_th ancestors_cs by auto +qed + +lemma RAG_s: + "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \ + {(Cs cs, Th th')}" +proof - + from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] + and nt show ?thesis by (auto intro:next_th_unique) +qed + +lemma subtree_kept: + assumes "th1 \ {th, th'}" + shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") +proof - + let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})" + let ?RAG'' = "?RAG' \ {(Cs cs, Th th')}" + have "subtree ?RAG' (Th th1) = ?R" + proof(rule subset_del_subtree_outside) + show "Range {(Cs cs, Th th), (Th th', Cs cs)} \ subtree (RAG s') (Th th1) = {}" + proof - + have "(Th th) \ subtree (RAG s') (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s') (Th th)" + by (unfold ancestors_th, simp) + next + from assms show "Th th1 \ Th th" by simp + qed + moreover have "(Cs cs) \ subtree (RAG s') (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s') (Cs cs)" + by (unfold ancestors_cs, insert assms, auto) + qed simp + ultimately have "{Th th, Cs cs} \ subtree (RAG s') (Th th1) = {}" by auto + thus ?thesis by simp + qed + qed + moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)" + proof(rule subtree_insert_next) + show "Th th' \ subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')" + (is "_ \ ?R") + proof - + have "?R \ ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto) + moreover have "Th th1 \ ..." using ancestors_th' assms by simp + ultimately show ?thesis by auto + qed + next + from assms show "Th th1 \ Th th'" by simp + qed + qed + ultimately show ?thesis by (unfold RAG_s, simp) +qed + +lemma cp_kept: + assumes "th1 \ {th, th'}" + shows "cp s th1 = cp s' th1" + by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp) + +end + +locale step_v_cps_nnt = step_v_cps + + assumes nnt: "\ th'. (\ next_th s' th cs th')" + +context step_v_cps_nnt +begin + +lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}" +proof - + from nnt and step_RAG_v[OF vt_s[unfolded s_def], folded s_def] + show ?thesis by auto +qed + +lemma subtree_kept: + assumes "th1 \ th" + shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" +proof(unfold RAG_s, rule subset_del_subtree_outside) + show "Range {(Cs cs, Th th)} \ subtree (RAG s') (Th th1) = {}" + proof - + have "(Th th) \ subtree (RAG s') (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s') (Th th)" + by (unfold ancestors_th, simp) + next + from assms show "Th th1 \ Th th" by simp + qed + thus ?thesis by auto + qed +qed + +lemma cp_kept_1: + assumes "th1 \ th" + shows "cp s th1 = cp s' th1" + by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp) + +lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}" +proof - + { fix n + have "(Cs cs) \ ancestors (RAG s') n" + proof + assume "Cs cs \ ancestors (RAG s') n" + hence "(n, Cs cs) \ (RAG s')^+" by (auto simp:ancestors_def) + from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \ RAG s'" by auto + then obtain th' where "nn = Th th'" + by (unfold s_RAG_def, auto) + from h[unfolded this] have "(Th th', Cs cs) \ RAG s'" . + from this[unfolded s_RAG_def] + have "waiting (wq s') th' cs" by auto + from this[unfolded cs_waiting_def] + have "1 < length (wq s' cs)" + by (cases "wq s' cs", auto) + from holding_next_thI[OF holding_th this] + obtain th' where "next_th s' th cs th'" by auto + with nnt show False by auto + qed + } note h = this + { fix n + assume "n \ subtree (RAG s') (Cs cs)" + hence "n = (Cs cs)" + by (elim subtreeE, insert h, auto) + } moreover have "(Cs cs) \ subtree (RAG s') (Cs cs)" + by (auto simp:subtree_def) + ultimately show ?thesis by auto +qed + +lemma subtree_th: + "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}" +find_theorems "subtree" "_ - _" RAG +proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside) + from edge_of_th + show "(Cs cs, Th th) \ edges_in (RAG s') (Th th)" + by (unfold edges_in_def, auto simp:subtree_def) +qed + +lemma cp_kept_2: + shows "cp s th = cp s' th" + by (unfold cp_alt_def subtree_th preced_kept, auto) + +lemma eq_cp: + fixes th' + shows "cp s th' = cp s' th'" + using cp_kept_1 cp_kept_2 + by (cases "th' = th", auto) +end + + +locale step_P_cps = + fixes s' th cs s + defines s_def : "s \ (P th cs#s')" + assumes vt_s: "vt s" + +sublocale step_P_cps < vat_s : valid_trace "s" +proof + from vt_s show "vt s" . +qed + +sublocale step_P_cps < vat_s' : valid_trace "s'" +proof + from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . +qed + +context step_P_cps +begin + +lemma readys_th: "th \ readys s'" +proof - + from step_back_step [OF vt_s[unfolded s_def]] + have "PIP s' (P th cs)" . + hence "th \ runing s'" by (cases, simp) + thus ?thesis by (simp add:readys_def runing_def) +qed + +lemma root_th: "root (RAG s') (Th th)" + using readys_root[OF readys_th] . + +lemma in_no_others_subtree: + assumes "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 root_th show ?thesis by (auto simp:root_def) + qed +qed + +lemma preced_kept: "the_preced s = the_preced s'" + by (auto simp: s_def the_preced_def preced_def) + +end + +locale step_P_cps_ne =step_P_cps + + fixes th' + assumes ne: "wq s' cs \ []" + defines th'_def: "th' \ hd (wq s' cs)" + +locale step_P_cps_e =step_P_cps + + assumes ee: "wq s' cs = []" + +context step_P_cps_e +begin + +lemma RAG_s: "RAG s = RAG s' \ {(Cs cs, Th th)}" +proof - + from ee and step_RAG_p[OF vt_s[unfolded s_def], folded s_def] + show ?thesis by auto +qed + +lemma subtree_kept: + assumes "th' \ th" + shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')" +proof(unfold RAG_s, rule subtree_insert_next) + from in_no_others_subtree[OF assms] + show "Th th \ subtree (RAG s') (Th th')" . +qed + +lemma cp_kept: + assumes "th' \ th" + shows "cp s th' = cp s' th'" +proof - + have "(the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')}) = + (the_preced s' ` {th'a. Th th'a \ subtree (RAG s') (Th th')})" + by (unfold preced_kept subtree_kept[OF assms], simp) + thus ?thesis by (unfold cp_alt_def, simp) +qed + +end + +context step_P_cps_ne +begin + +lemma RAG_s: "RAG s = RAG s' \ {(Th th, Cs cs)}" +proof - + from step_RAG_p[OF vt_s[unfolded s_def]] and ne + show ?thesis by (simp add:s_def) +qed + +lemma cs_held: "(Cs cs, Th th') \ RAG s'" +proof - + have "(Cs cs, Th th') \ hRAG s'" + proof - + from ne + have " holding s' th' cs" + by (unfold th'_def holding_eq cs_holding_def, auto) + thus ?thesis + by (unfold hRAG_def, auto) + qed + thus ?thesis by (unfold RAG_split, auto) +qed + +lemma tRAG_s: + "tRAG s = tRAG s' \ {(Th th, Th th')}" + using RAG_tRAG_transfer[OF RAG_s cs_held] . + +lemma cp_kept: + assumes "Th th'' \ ancestors (tRAG s) (Th th)" + shows "cp s th'' = cp s' th''" +proof - + have h: "subtree (tRAG s) (Th th'') = subtree (tRAG s') (Th th'')" + proof - + have "Th th' \ subtree (tRAG s') (Th th'')" + proof + assume "Th th' \ subtree (tRAG s') (Th th'')" + thus False + proof(rule subtreeE) + assume "Th th' = Th th''" + from assms[unfolded tRAG_s ancestors_def, folded this] + show ?thesis by auto + next + assume "Th th'' \ ancestors (tRAG s') (Th th')" + moreover have "... \ ancestors (tRAG s) (Th th')" + proof(rule ancestors_mono) + show "tRAG s' \ tRAG s" by (unfold tRAG_s, auto) + qed + ultimately have "Th th'' \ ancestors (tRAG s) (Th th')" by auto + moreover have "Th th' \ ancestors (tRAG s) (Th th)" + by (unfold tRAG_s, auto simp:ancestors_def) + ultimately have "Th th'' \ ancestors (tRAG s) (Th th)" + by (auto simp:ancestors_def) + with assms show ?thesis by auto + qed + qed + from subtree_insert_next[OF this] + have "subtree (tRAG s' \ {(Th th, Th th')}) (Th th'') = subtree (tRAG s') (Th th'')" . + from this[folded tRAG_s] show ?thesis . + qed + show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) +qed + +lemma cp_gen_update_stop: (* ddd *) + assumes "u \ ancestors (tRAG s) (Th th)" + and "cp_gen s u = cp_gen s' u" + and "y \ ancestors (tRAG s) u" + shows "cp_gen s y = cp_gen s' y" + using assms(3) +proof(induct rule:wf_induct[OF vat_s.fsbttRAGs.wf]) + case (1 x) + show ?case (is "?L = ?R") + proof - + from tRAG_ancestorsE[OF 1(2)] + obtain th2 where eq_x: "x = Th th2" by blast + from vat_s.cp_gen_rec[OF this] + have "?L = + Max ({the_preced s th2} \ cp_gen s ` RTree.children (tRAG s) x)" . + also have "... = + Max ({the_preced s' th2} \ cp_gen s' ` RTree.children (tRAG s') x)" + + proof - + from preced_kept have "the_preced s th2 = the_preced s' th2" by simp + moreover have "cp_gen s ` RTree.children (tRAG s) x = + cp_gen s' ` RTree.children (tRAG s') x" + proof - + have "RTree.children (tRAG s) x = RTree.children (tRAG s') x" + proof(unfold tRAG_s, rule children_union_kept) + have start: "(Th th, Th th') \ tRAG s" + by (unfold tRAG_s, auto) + note x_u = 1(2) + show "x \ Range {(Th th, Th th')}" + proof + assume "x \ Range {(Th th, Th th')}" + hence eq_x: "x = Th th'" using RangeE by auto + show False + proof(cases rule:vat_s.rtree_s.ancestors_headE[OF assms(1) start]) + case 1 + from x_u[folded this, unfolded eq_x] vat_s.acyclic_tRAG + show ?thesis by (auto simp:ancestors_def acyclic_def) + next + case 2 + with x_u[unfolded eq_x] + have "(Th th', Th th') \ (tRAG s)^+" by (auto simp:ancestors_def) + with vat_s.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) + qed + qed + qed + moreover have "cp_gen s ` RTree.children (tRAG s) x = + cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A") + proof(rule f_image_eq) + fix a + assume a_in: "a \ ?A" + from 1(2) + show "?f a = ?g a" + proof(cases rule:vat_s.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) + case in_ch + show ?thesis + proof(cases "a = u") + case True + from assms(2)[folded this] show ?thesis . + next + case False + have a_not_in: "a \ ancestors (tRAG s) (Th th)" + proof + assume a_in': "a \ ancestors (tRAG s) (Th th)" + have "a = u" + proof(rule vat_s.rtree_s.ancestors_children_unique) + from a_in' a_in show "a \ ancestors (tRAG s) (Th th) \ + RTree.children (tRAG s) x" by auto + next + from assms(1) in_ch show "u \ ancestors (tRAG s) (Th th) \ + RTree.children (tRAG s) x" by auto + qed + with False show False by simp + qed + from a_in obtain th_a where eq_a: "a = Th th_a" + by (unfold RTree.children_def tRAG_alt_def, auto) + from cp_kept[OF a_not_in[unfolded eq_a]] + have "cp s th_a = cp s' th_a" . + from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a] + show ?thesis . + qed + next + case (out_ch z) + hence h: "z \ ancestors (tRAG s) u" "z \ RTree.children (tRAG s) x" by auto + show ?thesis + proof(cases "a = z") + case True + from h(2) have zx_in: "(z, x) \ (tRAG s)" by (auto simp:RTree.children_def) + from 1(1)[rule_format, OF this h(1)] + have eq_cp_gen: "cp_gen s z = cp_gen s' z" . + with True show ?thesis by metis + next + case False + from a_in obtain th_a where eq_a: "a = Th th_a" + by (auto simp:RTree.children_def tRAG_alt_def) + have "a \ ancestors (tRAG s) (Th th)" + proof + assume a_in': "a \ ancestors (tRAG s) (Th th)" + have "a = z" + proof(rule vat_s.rtree_s.ancestors_children_unique) + from assms(1) h(1) have "z \ ancestors (tRAG s) (Th th)" + by (auto simp:ancestors_def) + with h(2) show " z \ ancestors (tRAG s) (Th th) \ + RTree.children (tRAG s) x" by auto + next + from a_in a_in' + show "a \ ancestors (tRAG s) (Th th) \ RTree.children (tRAG s) x" + by auto + qed + with False show False by auto + qed + from cp_kept[OF this[unfolded eq_a]] + have "cp s th_a = cp s' th_a" . + from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a] + show ?thesis . + qed + qed + qed + ultimately show ?thesis by metis + qed + ultimately show ?thesis by simp + qed + also have "... = ?R" + by (fold vat_s'.cp_gen_rec[OF eq_x], simp) + finally show ?thesis . + qed +qed + +lemma cp_up: + assumes "(Th th') \ ancestors (tRAG s) (Th th)" + and "cp s th' = cp s' th'" + and "(Th th'') \ ancestors (tRAG s) (Th th')" + shows "cp s th'' = cp s' th''" +proof - + have "cp_gen s (Th th'') = cp_gen s' (Th th'')" + proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)]) + from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]] + show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis + qed + with cp_gen_def_cond[OF refl[of "Th th''"]] + show ?thesis by metis +qed + +end + +locale step_create_cps = + fixes s' th prio s + defines s_def : "s \ (Create th prio#s')" + assumes vt_s: "vt s" + +sublocale step_create_cps < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +sublocale step_create_cps < vat_s': valid_trace "s'" + by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp) + +context step_create_cps +begin + +lemma RAG_kept: "RAG s = RAG s'" + by (unfold s_def RAG_create_unchanged, auto) + +lemma tRAG_kept: "tRAG s = tRAG s'" + by (unfold tRAG_alt_def RAG_kept, auto) + +lemma preced_kept: + assumes "th' \ th" + shows "the_preced s th' = the_preced s' th'" + by (unfold s_def the_preced_def preced_def, insert assms, auto) + +lemma th_not_in: "Th th \ Field (tRAG s')" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Create th prio)" by (cases, simp) + hence "th \ threads s'" by(cases, simp) + from vat_s'.not_in_thread_isolated[OF this] + have "Th th \ Field (RAG s')" . + with tRAG_Field show ?thesis by auto +qed + +lemma eq_cp: + assumes neq_th: "th' \ th" + shows "cp s th' = cp s' th'" +proof - + have "(the_preced s \ the_thread) ` subtree (tRAG s) (Th th') = + (the_preced s' \ the_thread) ` subtree (tRAG s') (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \ subtree (tRAG s') (Th th')" + then obtain th_a where eq_a: "a = Th th_a" + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF 2(2)] + and that show ?thesis by (unfold tRAG_alt_def, auto) + qed auto + have neq_th_a: "th_a \ th" + proof - + have "(Th th) \ subtree (tRAG s') (Th th')" + 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_not_in[unfolded Field_def] + show ?thesis by auto + qed (insert assms, auto) + qed + with a_in[unfolded eq_a] show ?thesis by auto + qed + from preced_kept[OF this] + show "(the_preced s \ the_thread) a = (the_preced s' \ the_thread) a" + by (unfold eq_a, simp) + qed + thus ?thesis by (unfold cp_alt_def1, simp) +qed + +lemma children_of_th: "RTree.children (tRAG s) (Th th) = {}" +proof - + { fix a + assume "a \ RTree.children (tRAG s) (Th th)" + hence "(a, Th th) \ tRAG s" by (auto simp:RTree.children_def) + with th_not_in have False + by (unfold Field_def tRAG_kept, auto) + } thus ?thesis by auto +qed + +lemma eq_cp_th: "cp s th = preced th s" + by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def) + +end + +locale step_exit_cps = + fixes s' th prio s + defines s_def : "s \ Exit th # s'" + assumes vt_s: "vt s" + +sublocale step_exit_cps < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +sublocale step_exit_cps < vat_s': valid_trace "s'" + by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp) + +context step_exit_cps +begin + +lemma preced_kept: + assumes "th' \ th" + shows "the_preced s th' = the_preced s' th'" + by (unfold s_def the_preced_def preced_def, insert assms, auto) + +lemma RAG_kept: "RAG s = RAG s'" + by (unfold s_def RAG_exit_unchanged, auto) + +lemma tRAG_kept: "tRAG s = tRAG s'" + by (unfold tRAG_alt_def RAG_kept, auto) + +lemma th_ready: "th \ readys s'" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Exit th)" by (cases, simp) + hence h: "th \ runing s' \ holdents s' th = {}" by (cases, metis) + thus ?thesis by (unfold runing_def, auto) +qed + +lemma th_holdents: "holdents s' th = {}" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Exit th)" by (cases, simp) + thus ?thesis by (cases, metis) +qed + +lemma th_RAG: "Th th \ Field (RAG s')" +proof - + have "Th th \ Range (RAG s')" + proof + assume "Th th \ Range (RAG s')" + then obtain cs where "holding (wq s') th cs" + by (unfold Range_iff s_RAG_def, auto) + with th_holdents[unfolded holdents_def] + show False by (unfold eq_holding, auto) + qed + moreover have "Th th \ Domain (RAG s')" + proof + assume "Th th \ Domain (RAG s')" + then obtain cs where "waiting (wq s') th cs" + by (unfold Domain_iff s_RAG_def, auto) + with th_ready show False by (unfold readys_def eq_waiting, auto) + qed + ultimately show ?thesis by (auto simp:Field_def) +qed + +lemma th_tRAG: "(Th th) \ Field (tRAG s')" + using th_RAG tRAG_Field[of s'] by auto + +lemma eq_cp: + assumes neq_th: "th' \ th" + shows "cp s th' = cp s' th'" +proof - + have "(the_preced s \ the_thread) ` subtree (tRAG s) (Th th') = + (the_preced s' \ the_thread) ` subtree (tRAG s') (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \ subtree (tRAG s') (Th th')" + then obtain th_a where eq_a: "a = Th th_a" + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF 2(2)] + and that show ?thesis by (unfold tRAG_alt_def, auto) + qed auto + have neq_th_a: "th_a \ th" + proof - + find_theorems readys subtree s' + from vat_s'.readys_in_no_subtree[OF th_ready assms] + have "(Th th) \ subtree (RAG s') (Th th')" . + 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] + show "(the_preced s \ the_thread) a = (the_preced s' \ the_thread) a" + by (unfold eq_a, simp) + qed + thus ?thesis by (unfold cp_alt_def1, simp) +qed + +end + +end +