diff -r ed938e2246b9 -r 0525670d8e6a Implementation.thy~ --- a/Implementation.thy~ Thu Jan 28 21:14:17 2016 +0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,913 +0,0 @@ -section {* - This file contains lemmas used to guide the recalculation of current precedence - after every system call (or system operation) -*} -theory Implementation -imports PIPBasics -begin - -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 - 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}" -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 - - 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 -