section {* This file contains lemmas used to guide the recalculation of current precedence after every system call (or system operation)*}theory Implementationimports PIPBasicsbegintext {* (* 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 every threads in its subtree, where the notion of sub-tree in RAG is defined in RTree.thy. Therefore, for each operation, lemmas about the change of precedences and RAG are derived first, on which lemmas about current precedence recalculation are based on.*}section {* The @{term Set} operation *}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 \<equiv> (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" .qedsublocale step_set_cps < vat_s' : valid_trace "s'"proof from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .qedcontext step_set_cps begintext {* (* ddd *) The following two lemmas confirm that @{text "Set"}-operation only changes the precedence of the initiating thread (or actor) of the operation (or event).*}lemma eq_preced: assumes "th' \<noteq> th" shows "preced th' s = preced th' s'"proof - from assms show ?thesis by (unfold s_def, auto simp:preced_def)qedlemma eq_the_preced: assumes "th' \<noteq> 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 that 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: assumes nd: "Th th \<notin> 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 \<in> subtree (RAG s) (Th th')}) = Max (the_preced s' ` {th'a. Th th'a \<in> 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 "\<forall> e \<in> ?S2. ?f e = ?g e" proof fix th1 assume "th1 \<in> ?S2" with nd have "th1 \<noteq> 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)qedtext {* The following lemma shows that @{term "th"} is not in the sub-tree of any other thread. *}lemma th_in_no_subtree: assumes "th' \<noteq> th" shows "Th th \<notin> subtree (RAG s') (Th th')"proof - have "th \<in> readys s'" proof - from step_back_step [OF vt_s[unfolded s_def]] have "step s' (Set th prio)" . hence "th \<in> runing s'" by (cases, simp) thus ?thesis by (simp add:readys_def runing_def) qed from vat_s'.readys_in_no_subtree[OF this assms(1)] show ?thesis by blastqedtext {* 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: assumes "th' \<noteq> th" shows "cp s th' = cp s' th'" by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])endsection {* The @{term V} operation *}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 \<equiv> (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" .qedsublocale step_v_cps < vat_s' : valid_trace "s'"proof from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .qedcontext step_v_cpsbeginlemma ready_th_s': "th \<in> 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)qedlemma 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)qedlemma edge_of_th: "(Cs cs, Th th) \<in> RAG s'" proof - from holding_th show ?thesis by (unfold s_RAG_def holding_eq, auto)qedlemma ancestors_cs: "ancestors (RAG s') (Cs cs) = {Th th}"proof - have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th) \<union> {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) \<in> 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 simpqedlemma preced_kept: "the_preced s = the_preced s'" by (auto simp: s_def the_preced_def preced_def)endtext {* 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_ntbegintext {* 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)} \<subseteq> 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) \<union> {Cs cs}" proof(rule vat_s'.rtree_RAG.ancestors_accum) from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto qed thus ?thesis using ancestors_th ancestors_cs by autoqedlemma RAG_s: "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> {(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)qedlemma subtree_kept: (* ddd *) assumes "th1 \<notin> {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' \<union> {(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)} \<inter> subtree (RAG s') (Th th1) = {}" proof - have "(Th th) \<notin> subtree (RAG s') (Th th1)" proof(rule subtree_refute) show "Th th1 \<notin> ancestors (RAG s') (Th th)" by (unfold ancestors_th, simp) next from assms show "Th th1 \<noteq> Th th" by simp qed moreover have "(Cs cs) \<notin> subtree (RAG s') (Th th1)" proof(rule subtree_refute) show "Th th1 \<notin> ancestors (RAG s') (Cs cs)" by (unfold ancestors_cs, insert assms, auto) qed simp ultimately have "{Th th, Cs cs} \<inter> 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' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)" proof(rule subtree_refute) show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')" (is "_ \<notin> ?R") proof - have "?R \<subseteq> ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto) moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp ultimately show ?thesis by auto qed next from assms show "Th th1 \<noteq> Th th'" by simp qed qed ultimately show ?thesis by (unfold RAG_s, simp)qedlemma cp_kept: assumes "th1 \<notin> {th, th'}" shows "cp s th1 = cp s' th1" by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)endlocale step_v_cps_nnt = step_v_cps + assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"context step_v_cps_nntbeginlemma 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 autoqedlemma subtree_kept: assumes "th1 \<noteq> 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)} \<inter> subtree (RAG s') (Th th1) = {}" proof - have "(Th th) \<notin> subtree (RAG s') (Th th1)" proof(rule subtree_refute) show "Th th1 \<notin> ancestors (RAG s') (Th th)" by (unfold ancestors_th, simp) next from assms show "Th th1 \<noteq> Th th" by simp qed thus ?thesis by auto qedqedlemma cp_kept_1: assumes "th1 \<noteq> 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) \<notin> ancestors (RAG s') n" proof assume "Cs cs \<in> ancestors (RAG s') n" hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def) from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> 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) \<in> 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 \<in> subtree (RAG s') (Cs cs)" hence "n = (Cs cs)" by (elim subtreeE, insert h, auto) } moreover have "(Cs cs) \<in> subtree (RAG s') (Cs cs)" by (auto simp:subtree_def) ultimately show ?thesis by auto qedlemma subtree_th: "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside) from edge_of_th show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)" by (unfold edges_in_def, auto simp:subtree_def)qedlemma cp_kept_2: shows "cp s th = cp s' th" by (unfold cp_alt_def subtree_th preced_kept, auto)lemma eq_cp: shows "cp s th' = cp s' th'" using cp_kept_1 cp_kept_2 by (cases "th' = th", auto)endlocale step_P_cps = fixes s' th cs s defines s_def : "s \<equiv> (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" .qedsection {* The @{term P} operation *}sublocale step_P_cps < vat_s' : valid_trace "s'"proof from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .qedcontext step_P_cpsbeginlemma readys_th: "th \<in> readys s'"proof - from step_back_step [OF vt_s[unfolded s_def]] have "PIP s' (P th cs)" . hence "th \<in> runing s'" by (cases, simp) thus ?thesis by (simp add:readys_def runing_def)qedlemma root_th: "root (RAG s') (Th th)" using readys_root[OF readys_th] .lemma in_no_others_subtree: assumes "th' \<noteq> th" shows "Th th \<notin> subtree (RAG s') (Th th')"proof assume "Th th \<in> 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) qedqedlemma preced_kept: "the_preced s = the_preced s'" by (auto simp: s_def the_preced_def preced_def)endlocale step_P_cps_ne =step_P_cps + fixes th' assumes ne: "wq s' cs \<noteq> []" defines th'_def: "th' \<equiv> hd (wq s' cs)"locale step_P_cps_e =step_P_cps + assumes ee: "wq s' cs = []"context step_P_cps_ebeginlemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"proof - from ee and step_RAG_p[OF vt_s[unfolded s_def], folded s_def] show ?thesis by autoqedlemma subtree_kept: assumes "th' \<noteq> 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 \<notin> subtree (RAG s') (Th th')" .qedlemma cp_kept: assumes "th' \<noteq> th" shows "cp s th' = cp s' th'"proof - have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) = (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})" by (unfold preced_kept subtree_kept[OF assms], simp) thus ?thesis by (unfold cp_alt_def, simp)qedendcontext step_P_cps_ne beginlemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"proof - from step_RAG_p[OF vt_s[unfolded s_def]] and ne show ?thesis by (simp add:s_def)qedlemma cs_held: "(Cs cs, Th th') \<in> RAG s'"proof - have "(Cs cs, Th th') \<in> 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)qedlemma tRAG_s: "tRAG s = tRAG s' \<union> {(Th th, Th th')}" using RAG_tRAG_transfer[OF RAG_s cs_held] .lemma cp_kept: assumes "Th th'' \<notin> 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' \<notin> subtree (tRAG s') (Th th'')" proof assume "Th th' \<in> 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'' \<in> ancestors (tRAG s') (Th th')" moreover have "... \<subseteq> ancestors (tRAG s) (Th th')" proof(rule ancestors_mono) show "tRAG s' \<subseteq> tRAG s" by (unfold tRAG_s, auto) qed ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th')" by auto moreover have "Th th' \<in> ancestors (tRAG s) (Th th)" by (unfold tRAG_s, auto simp:ancestors_def) ultimately have "Th th'' \<in> 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' \<union> {(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)qedlemma cp_gen_update_stop: (* ddd *) assumes "u \<in> ancestors (tRAG s) (Th th)" and "cp_gen s u = cp_gen s' u" and "y \<in> 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} \<union> cp_gen s ` RTree.children (tRAG s) x)" . also have "... = Max ({the_preced s' th2} \<union> 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') \<in> tRAG s" by (unfold tRAG_s, auto) note x_u = 1(2) show "x \<notin> Range {(Th th, Th th')}" proof assume "x \<in> 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') \<in> (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 \<in> ?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 \<notin> ancestors (tRAG s) (Th th)" proof assume a_in': "a \<in> ancestors (tRAG s) (Th th)" have "a = u" proof(rule vat_s.rtree_s.ancestors_children_unique) from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x" by auto next from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter> 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 \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto show ?thesis proof(cases "a = z") case True from h(2) have zx_in: "(z, x) \<in> (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 \<notin> ancestors (tRAG s) (Th th)" proof assume a_in': "a \<in> ancestors (tRAG s) (Th th)" have "a = z" proof(rule vat_s.rtree_s.ancestors_children_unique) from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)" by (auto simp:ancestors_def) with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x" by auto next from a_in a_in' show "a \<in> ancestors (tRAG s) (Th th) \<inter> 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 . qedqedlemma cp_up: assumes "(Th th') \<in> ancestors (tRAG s) (Th th)" and "cp s th' = cp s' th'" and "(Th th'') \<in> 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 metisqedendsection {* The @{term Create} operation *}locale step_create_cps = fixes s' th prio s defines s_def : "s \<equiv> (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_cpsbeginlemma 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' \<noteq> 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 \<notin> Field (tRAG s')"proof - from vt_s[unfolded s_def] have "PIP s' (Create th prio)" by (cases, simp) hence "th \<notin> threads s'" by(cases, simp) from vat_s'.not_in_thread_isolated[OF this] have "Th th \<notin> Field (RAG s')" . with tRAG_Field show ?thesis by autoqedlemma eq_cp: assumes neq_th: "th' \<noteq> th" shows "cp s th' = cp s' th'"proof - have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') = (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')" proof(unfold tRAG_kept, rule f_image_eq) fix a assume a_in: "a \<in> 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 \<noteq> th" proof - have "(Th th) \<notin> subtree (tRAG s') (Th th')" proof assume "Th th \<in> 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 \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a" by (unfold eq_a, simp) qed thus ?thesis by (unfold cp_alt_def1, simp)qedlemma children_of_th: "RTree.children (tRAG s) (Th th) = {}"proof - { fix a assume "a \<in> RTree.children (tRAG s) (Th th)" hence "(a, Th th) \<in> tRAG s" by (auto simp:RTree.children_def) with th_not_in have False by (unfold Field_def tRAG_kept, auto) } thus ?thesis by autoqedlemma eq_cp_th: "cp s th = preced th s" by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def)endlocale step_exit_cps = fixes s' th prio s defines s_def : "s \<equiv> 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_cpsbeginlemma preced_kept: assumes "th' \<noteq> 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 \<in> readys s'"proof - from vt_s[unfolded s_def] have "PIP s' (Exit th)" by (cases, simp) hence h: "th \<in> runing s' \<and> holdents s' th = {}" by (cases, metis) thus ?thesis by (unfold runing_def, auto)qedlemma 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)qedlemma th_RAG: "Th th \<notin> Field (RAG s')"proof - have "Th th \<notin> Range (RAG s')" proof assume "Th th \<in> 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 \<notin> Domain (RAG s')" proof assume "Th th \<in> 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)qedlemma th_tRAG: "(Th th) \<notin> Field (tRAG s')" using th_RAG tRAG_Field[of s'] by autolemma eq_cp: assumes neq_th: "th' \<noteq> th" shows "cp s th' = cp s' th'"proof - have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') = (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')" proof(unfold tRAG_kept, rule f_image_eq) fix a assume a_in: "a \<in> 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 \<noteq> th" proof - from vat_s'.readys_in_no_subtree[OF th_ready assms] have "(Th th) \<notin> subtree (RAG s') (Th th')" . with tRAG_subtree_RAG[of s' "Th th'"] have "(Th th) \<notin> 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 \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a" by (unfold eq_a, simp) qed thus ?thesis by (unfold cp_alt_def1, simp)qedendend