diff -r 0525670d8e6a -r 4763aa246dbd Implementation.thy --- a/Implementation.thy Fri Jan 29 09:46:07 2016 +0800 +++ b/Implementation.thy Fri Jan 29 10:51:52 2016 +0800 @@ -2,8 +2,8 @@ This file contains lemmas used to guide the recalculation of current precedence after every system call (or system operation) *} -theory Implementation -imports PIPBasics +theory ExtGG +imports CpsG begin text {* (* ddd *) @@ -35,30 +35,7 @@ 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 \ (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 +context valid_trace_set begin text {* (* ddd *) @@ -67,26 +44,21 @@ of the operation (or event). *} + lemma eq_preced: assumes "th' \ th" - shows "preced th' s = preced th' s'" + shows "preced th' (e#s) = preced th' s" proof - from assms show ?thesis - by (unfold s_def, auto simp:preced_def) + by (unfold is_set, auto simp:preced_def) qed lemma eq_the_preced: assumes "th' \ th" - shows "the_preced s th' = the_preced s' th'" + shows "the_preced (e#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"} @@ -97,18 +69,18 @@ *} lemma eq_cp_pre: - assumes nd: "Th th \ subtree (RAG s') (Th th')" - shows "cp s th' = cp s' th'" + assumes nd: "Th th \ subtree (RAG s) (Th th')" + shows "cp (e#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')})" + have "Max (the_preced (e#s) ` {th'a. Th th'a \ subtree (RAG (e#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 + have "?S1 = ?S2" using RAG_unchanged by simp -- {* The function values on the base set are equal as well. *} moreover have "\ e \ ?S2. ?f e = ?g e" proof @@ -116,7 +88,7 @@ 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" . + show "the_preced (e#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) @@ -131,16 +103,9 @@ *} lemma th_in_no_subtree: assumes "th' \ th" - shows "Th th \ subtree (RAG s') (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)] + from readys_in_no_subtree[OF th_ready_s assms(1)] show ?thesis by blast qed @@ -151,7 +116,7 @@ *} lemma eq_cp: assumes "th' \ th" - shows "cp s th' = cp s' th'" + shows "cp (e#s) th' = cp s th'" by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) end @@ -162,73 +127,33 @@ 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 +context valid_trace_v 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) = {}" +lemma ancestors_th: "ancestors (RAG s) (Th th) = {}" proof - - from vat_s'.readys_root[OF ready_th_s'] + from readys_root[OF th_ready_s] show ?thesis by (unfold root_def, simp) qed -lemma holding_th: "holding s' th cs" +lemma edge_of_th: + "(Cs cs, Th th) \ RAG s" 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 + from holding_th_cs_s show ?thesis by (unfold s_RAG_def holding_eq, auto) qed lemma ancestors_cs: - "ancestors (RAG s') (Cs cs) = {Th th}" + "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 + have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \ {Th th}" + by (rule rtree_RAG.ancestors_accum[OF edge_of_th]) 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 {* @@ -236,147 +161,99 @@ 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 +context valid_trace_v_n 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 sub_RAGs': + "{(Cs cs, Th th), (Th taker, Cs cs)} \ RAG s" + using next_th_RAG[OF next_th_taker] . lemma ancestors_th': - "ancestors (RAG s') (Th th') = {Th th, Cs cs}" + "ancestors (RAG s) (Th taker) = {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 + have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \ {Cs cs}" + proof(rule rtree_RAG.ancestors_accum) + from sub_RAGs' show "(Th taker, 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 + "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \ + {(Cs cs, Th taker)}" + by (unfold RAG_es waiting_set_eq holding_set_eq, auto) lemma subtree_kept: (* ddd *) - assumes "th1 \ {th, th'}" - shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") + assumes "th1 \ {th, taker}" + shows "subtree (RAG (e#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')}" + let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})" + let ?RAG'' = "?RAG' \ {(Cs cs, Th taker)}" 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) = {}" + show "Range {(Cs cs, Th th), (Th taker, Cs cs)} \ subtree (RAG s) (Th th1) = {}" proof - - have "(Th th) \ subtree (RAG s') (Th th1)" + have "(Th th) \ subtree (RAG s) (Th th1)" proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s') (Th th)" + 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)" + moreover have "(Cs cs) \ subtree (RAG s) (Th th1)" proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s') (Cs cs)" + 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 + 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)" + show "Th taker \ subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')" + show "Th th1 \ ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" (is "_ \ ?R") proof - - have "?R \ ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto) + have "?R \ ancestors (RAG s) (Th taker)" 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 + from assms show "Th th1 \ Th taker" 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) + assumes "th1 \ {th, taker}" + shows "cp (e#s) th1 = cp s th1" + by (unfold cp_alt_def the_preced_es 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 +context valid_trace_v_e 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 +find_theorems RAG s e + +lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}" + by (unfold RAG_es waiting_set_eq holding_set_eq, simp) lemma subtree_kept: assumes "th1 \ th" - shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" + shows "subtree (RAG (e#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) = {}" + show "Range {(Cs cs, Th th)} \ subtree (RAG s) (Th th1) = {}" proof - - have "(Th th) \ subtree (RAG s') (Th th1)" + have "(Th th) \ subtree (RAG s) (Th th1)" proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s') (Th th)" + show "Th th1 \ ancestors (RAG s) (Th th)" by (unfold ancestors_th, simp) next from assms show "Th th1 \ Th th" by simp @@ -387,94 +264,72 @@ 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) + shows "cp (e#s) th1 = cp s th1" + by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) -lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}" +lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}" proof - { fix n - have "(Cs cs) \ ancestors (RAG s') 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 + 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 h[unfolded this] have "(Th th', Cs cs) \ RAG s" . from this[unfolded s_RAG_def] - have "waiting (wq s') th' cs" by auto + 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 + have "1 < length (wq s cs)" + by (cases "wq s cs", auto) + from holding_next_thI[OF holding_th_cs_s this] + obtain th' where "next_th s th cs th'" by auto + thus False using no_taker by blast qed } note h = this { fix n - assume "n \ subtree (RAG s') (Cs cs)" + 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)" + } 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) + "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" +proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside) from edge_of_th - show "(Cs cs, Th th) \ edges_in (RAG s') (Th 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) + shows "cp (e#s) th = cp s th" + by (unfold cp_alt_def subtree_th the_preced_es, auto) lemma eq_cp: - shows "cp s th' = cp s' th'" + shows "cp (e#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 - section {* 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'" . -qed - -context step_P_cps +context valid_trace_p 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 root_th: "root (RAG s) (Th th)" + by (simp add: ready_th_s readys_root) lemma in_no_others_subtree: assumes "th' \ th" - shows "Th th \ subtree (RAG s') (Th th')" + shows "Th th \ subtree (RAG s) (Th th')" proof - assume "Th th \ subtree (RAG s') (Th th')" + assume "Th th \ subtree (RAG s) (Th th')" thus False proof(cases rule:subtreeE) case 1 @@ -485,162 +340,140 @@ qed qed -lemma preced_kept: "the_preced s = the_preced s'" - by (auto simp: s_def the_preced_def preced_def) +lemma preced_kept: "the_preced (e#s) = the_preced s" +proof + fix th' + show "the_preced (e # s) th' = the_preced s th'" + by (unfold the_preced_def is_p preced_def, simp) +qed 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 +context valid_trace_p_h 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) + shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')" +proof(unfold RAG_es, rule subtree_insert_next) from in_no_others_subtree[OF assms] - show "Th th \ subtree (RAG s') (Th th')" . + show "Th th \ subtree (RAG s) (Th th')" . qed lemma cp_kept: assumes "th' \ th" - shows "cp s th' = cp s' th'" + shows "cp (e#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')})" + have "(the_preced (e#s) ` {th'a. Th th'a \ subtree (RAG (e#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 +context valid_trace_p_w 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 +interpretation vat_e: valid_trace "e#s" + by (unfold_locales, insert vt_e, simp) -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 cs_held: "(Cs cs, Th holder) \ RAG s" + using holding_s_holder + by (unfold s_RAG_def, fold holding_eq, auto) lemma tRAG_s: - "tRAG s = tRAG s' \ {(Th th, Th th')}" - using RAG_tRAG_transfer[OF RAG_s cs_held] . + "tRAG (e#s) = tRAG s \ {(Th th, Th holder)}" + using local.RAG_tRAG_transfer[OF RAG_es cs_held] . lemma cp_kept: - assumes "Th th'' \ ancestors (tRAG s) (Th th)" - shows "cp s th'' = cp s' th''" + assumes "Th th'' \ ancestors (tRAG (e#s)) (Th th)" + shows "cp (e#s) th'' = cp s th''" proof - - have h: "subtree (tRAG s) (Th th'') = subtree (tRAG s') (Th th'')" + have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')" proof - - have "Th th' \ subtree (tRAG s') (Th th'')" + have "Th holder \ subtree (tRAG s) (Th th'')" proof - assume "Th th' \ subtree (tRAG s') (Th th'')" + assume "Th holder \ subtree (tRAG s) (Th th'')" thus False proof(rule subtreeE) - assume "Th th' = Th th''" + assume "Th holder = 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')" + assume "Th th'' \ ancestors (tRAG s) (Th holder)" + moreover have "... \ ancestors (tRAG (e#s)) (Th holder)" proof(rule ancestors_mono) - show "tRAG s' \ tRAG s" by (unfold tRAG_s, auto) + show "tRAG s \ tRAG (e#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)" + ultimately have "Th th'' \ ancestors (tRAG (e#s)) (Th holder)" by auto + moreover have "Th holder \ ancestors (tRAG (e#s)) (Th th)" by (unfold tRAG_s, auto simp:ancestors_def) - ultimately have "Th th'' \ ancestors (tRAG s) (Th th)" + ultimately have "Th th'' \ ancestors (tRAG (e#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'')" . + have "subtree (tRAG s \ {(Th th, Th holder)}) (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" + assumes "u \ ancestors (tRAG (e#s)) (Th th)" + and "cp_gen (e#s) u = cp_gen s u" + and "y \ ancestors (tRAG (e#s)) u" + shows "cp_gen (e#s) y = cp_gen s y" using assms(3) -proof(induct rule:wf_induct[OF vat_s.fsbttRAGs.wf]) +proof(induct rule:wf_induct[OF vat_e.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] + from vat_e.cp_gen_rec[OF this] have "?L = - Max ({the_preced s th2} \ cp_gen s ` RTree.children (tRAG s) x)" . + Max ({the_preced (e#s) th2} \ cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . also have "... = - Max ({the_preced s' th2} \ cp_gen s' ` RTree.children (tRAG s') x)" - + 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" + from preced_kept have "the_preced (e#s) th2 = the_preced s th2" by simp + moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = + cp_gen s ` RTree.children (tRAG s) x" proof - - have "RTree.children (tRAG s) x = RTree.children (tRAG s') x" + have "RTree.children (tRAG (e#s)) x = RTree.children (tRAG s) x" proof(unfold tRAG_s, rule children_union_kept) - have start: "(Th th, Th th') \ tRAG s" + have start: "(Th th, Th holder) \ tRAG (e#s)" by (unfold tRAG_s, auto) note x_u = 1(2) - show "x \ Range {(Th th, Th th')}" + show "x \ Range {(Th th, Th holder)}" proof - assume "x \ Range {(Th th, Th th')}" - hence eq_x: "x = Th th'" using RangeE by auto + assume "x \ Range {(Th th, Th holder)}" + hence eq_x: "x = Th holder" using RangeE by auto show False - proof(cases rule:vat_s.rtree_s.ancestors_headE[OF assms(1) start]) + proof(cases rule:vat_e.ancestors_headE[OF assms(1) start]) case 1 - from x_u[folded this, unfolded eq_x] vat_s.acyclic_tRAG + from x_u[folded this, unfolded eq_x] vat_e.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) + have "(Th holder, Th holder) \ (tRAG (e#s))^+" by (auto simp:ancestors_def) + with vat_e.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") + moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = + cp_gen s ` RTree.children (tRAG (e#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]) + proof(cases rule:vat_e.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) case in_ch show ?thesis proof(cases "a = u") @@ -648,58 +481,58 @@ from assms(2)[folded this] show ?thesis . next case False - have a_not_in: "a \ ancestors (tRAG s) (Th th)" + have a_not_in: "a \ ancestors (tRAG (e#s)) (Th th)" proof - assume a_in': "a \ ancestors (tRAG s) (Th th)" + assume a_in': "a \ ancestors (tRAG (e#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 + proof(rule vat_e.rtree_s.ancestors_children_unique) + from a_in' a_in show "a \ ancestors (tRAG (e#s)) (Th th) \ + RTree.children (tRAG (e#s)) x" by auto next - from assms(1) in_ch show "u \ ancestors (tRAG s) (Th th) \ - RTree.children (tRAG s) x" by auto + from assms(1) in_ch show "u \ ancestors (tRAG (e#s)) (Th th) \ + RTree.children (tRAG (e#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" . + have "cp (e#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 + hence h: "z \ ancestors (tRAG (e#s)) u" "z \ RTree.children (tRAG (e#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 h(2) have zx_in: "(z, x) \ (tRAG (e#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" . + have eq_cp_gen: "cp_gen (e#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)" + have "a \ ancestors (tRAG (e#s)) (Th th)" proof - assume a_in': "a \ ancestors (tRAG s) (Th th)" + assume a_in': "a \ ancestors (tRAG (e#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)" + proof(rule vat_e.rtree_s.ancestors_children_unique) + from assms(1) h(1) have "z \ ancestors (tRAG (e#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 + with h(2) show " z \ ancestors (tRAG (e#s)) (Th th) \ + RTree.children (tRAG (e#s)) x" by auto next from a_in a_in' - show "a \ ancestors (tRAG s) (Th th) \ RTree.children (tRAG s) x" + show "a \ ancestors (tRAG (e#s)) (Th th) \ RTree.children (tRAG (e#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" . + have "cp (e#s) th_a = cp s th_a" . from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a] show ?thesis . qed @@ -710,21 +543,21 @@ ultimately show ?thesis by simp qed also have "... = ?R" - by (fold vat_s'.cp_gen_rec[OF eq_x], simp) + by (fold 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''" + assumes "(Th th') \ ancestors (tRAG (e#s)) (Th th)" + and "cp (e#s) th' = cp s th'" + and "(Th th'') \ ancestors (tRAG (e#s)) (Th th')" + shows "cp (e#s) th'' = cp s th''" proof - - have "cp_gen s (Th th'') = cp_gen s' (Th th'')" + have "cp_gen (e#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 + show "cp_gen (e#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 @@ -734,50 +567,32 @@ section {* The @{term Create} operation *} -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) +context valid_trace_create +begin -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 +interpretation vat_e: valid_trace "e#s" + by (unfold_locales, insert vt_e, simp) -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 tRAG_kept: "tRAG (e#s) = tRAG s" + by (unfold tRAG_alt_def RAG_unchanged, 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) + shows "the_preced (e#s) th' = the_preced s th'" + by (unfold the_preced_def preced_def is_create, 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 th_not_in: "Th th \ Field (tRAG s)" + by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s) lemma eq_cp: assumes neq_th: "th' \ th" - shows "cp s th' = cp s' th'" + shows "cp (e#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')" + have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#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')" + 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 @@ -786,9 +601,9 @@ qed auto have neq_th_a: "th_a \ th" proof - - have "(Th th) \ subtree (tRAG s') (Th th')" + have "(Th th) \ subtree (tRAG s) (Th th')" proof - assume "Th th \ subtree (tRAG s') (Th th')" + assume "Th th \ subtree (tRAG s) (Th th')" thus False proof(cases rule:subtreeE) case 2 @@ -800,99 +615,72 @@ 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" + show "(the_preced (e#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) = {}" +lemma children_of_th: "RTree.children (tRAG (e#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) + assume "a \ RTree.children (tRAG (e#s)) (Th th)" + hence "(a, Th th) \ tRAG (e#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) +lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" + by (unfold vat_e.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 +context valid_trace_exit 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) + shows "the_preced (e#s) th' = the_preced s th'" + using assms + by (unfold the_preced_def is_exit preced_def, simp) -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 tRAG_kept: "tRAG (e#s) = tRAG s" + by (unfold tRAG_alt_def RAG_unchanged, auto) -lemma th_holdents: "holdents s' th = {}" +lemma th_RAG: "Th th \ Field (RAG s)" 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')" + have "Th th \ Range (RAG s)" proof - assume "Th th \ Range (RAG s')" - then obtain cs where "holding (wq s') th cs" + 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) + with holdents_th_s[unfolded holdents_def] + show False by (unfold holding_eq, auto) qed - moreover have "Th th \ Domain (RAG s')" + moreover have "Th th \ Domain (RAG s)" proof - assume "Th th \ Domain (RAG s')" - then obtain cs where "waiting (wq s') th cs" + 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) + with th_ready_s show False by (unfold readys_def waiting_eq, 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 th_tRAG: "(Th th) \ Field (tRAG s)" + using th_RAG tRAG_Field by auto lemma eq_cp: assumes neq_th: "th' \ th" - shows "cp s th' = cp s' th'" + shows "cp (e#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')" + have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#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')" + 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 @@ -901,14 +689,14 @@ 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 + from readys_in_no_subtree[OF th_ready_s 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" + show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" by (unfold eq_a, simp) qed thus ?thesis by (unfold cp_alt_def1, simp) @@ -918,3 +706,924 @@ end +======= +theory ExtGG +imports PrioG CpsG +begin + +text {* + The following two auxiliary lemmas are used to reason about @{term Max}. +*} +lemma image_Max_eqI: + assumes "finite B" + and "b \ B" + and "\ x \ B. f x \ f b" + shows "Max (f ` B) = f b" + using assms + using Max_eqI by blast + +lemma image_Max_subset: + assumes "finite A" + and "B \ A" + and "a \ B" + and "Max (f ` A) = f a" + shows "Max (f ` B) = f a" +proof(rule image_Max_eqI) + show "finite B" + using assms(1) assms(2) finite_subset by auto +next + show "a \ B" using assms by simp +next + show "\x\B. f x \ f a" + by (metis Max_ge assms(1) assms(2) assms(4) + finite_imageI image_eqI subsetCE) +qed + +text {* + The following locale @{text "highest_gen"} sets the basic context for our + investigation: supposing thread @{text th} holds the highest @{term cp}-value + in state @{text s}, which means the task for @{text th} is the + most urgent. We want to show that + @{text th} is treated correctly by PIP, which means + @{text th} will not be blocked unreasonably by other less urgent + threads. +*} +locale highest_gen = + fixes s th prio tm + assumes vt_s: "vt s" + and threads_s: "th \ threads s" + and highest: "preced th s = Max ((cp s)`threads s)" + -- {* The internal structure of @{term th}'s precedence is exposed:*} + and preced_th: "preced th s = Prc prio tm" + +-- {* @{term s} is a valid trace, so it will inherit all results derived for + a valid trace: *} +sublocale highest_gen < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +context highest_gen +begin + +text {* + @{term tm} is the time when the precedence of @{term th} is set, so + @{term tm} must be a valid moment index into @{term s}. +*} +lemma lt_tm: "tm < length s" + by (insert preced_tm_lt[OF threads_s preced_th], simp) + +text {* + Since @{term th} holds the highest precedence and @{text "cp"} + is the highest precedence of all threads in the sub-tree of + @{text "th"} and @{text th} is among these threads, + its @{term cp} must equal to its precedence: +*} +lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") +proof - + have "?L \ ?R" + by (unfold highest, rule Max_ge, + auto simp:threads_s finite_threads) + moreover have "?R \ ?L" + by (unfold vat_s.cp_rec, rule Max_ge, + auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) + ultimately show ?thesis by auto +qed + +(* ccc *) +lemma highest_cp_preced: "cp s th = Max ((\ th'. preced th' s) ` threads s)" + by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) + +lemma highest_preced_thread: "preced th s = Max ((\ th'. preced th' s) ` threads s)" + by (fold eq_cp_s_th, unfold highest_cp_preced, simp) + +lemma highest': "cp s th = Max (cp s ` threads s)" +proof - + from highest_cp_preced max_cp_eq[symmetric] + show ?thesis by simp +qed + +end + +locale extend_highest_gen = highest_gen + + fixes t + assumes vt_t: "vt (t@s)" + and create_low: "Create th' prio' \ set t \ prio' \ prio" + and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" + and exit_diff: "Exit th' \ set t \ th' \ th" + +sublocale extend_highest_gen < vat_t: valid_trace "t@s" + by (unfold_locales, insert vt_t, simp) + +lemma step_back_vt_app: + assumes vt_ts: "vt (t@s)" + shows "vt s" +proof - + from vt_ts show ?thesis + proof(induct t) + case Nil + from Nil show ?case by auto + next + case (Cons e t) + assume ih: " vt (t @ s) \ vt s" + and vt_et: "vt ((e # t) @ s)" + show ?case + proof(rule ih) + show "vt (t @ s)" + proof(rule step_back_vt) + from vt_et show "vt (e # t @ s)" by simp + qed + qed + qed +qed + + +locale red_extend_highest_gen = extend_highest_gen + + fixes i::nat + +sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" + apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) + apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) + by (unfold highest_gen_def, auto dest:step_back_vt_app) + + +context extend_highest_gen +begin + + lemma ind [consumes 0, case_names Nil Cons, induct type]: + assumes + h0: "R []" + and h2: "\ e t. \vt (t@s); step (t@s) e; + extend_highest_gen s th prio tm t; + extend_highest_gen s th prio tm (e#t); R t\ \ R (e#t)" + shows "R t" +proof - + from vt_t extend_highest_gen_axioms show ?thesis + proof(induct t) + from h0 show "R []" . + next + case (Cons e t') + assume ih: "\vt (t' @ s); extend_highest_gen s th prio tm t'\ \ R t'" + and vt_e: "vt ((e # t') @ s)" + and et: "extend_highest_gen s th prio tm (e # t')" + from vt_e and step_back_step have stp: "step (t'@s) e" by auto + from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto + show ?case + proof(rule h2 [OF vt_ts stp _ _ _ ]) + show "R t'" + proof(rule ih) + from et show ext': "extend_highest_gen s th prio tm t'" + by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) + next + from vt_ts show "vt (t' @ s)" . + qed + next + from et show "extend_highest_gen s th prio tm (e # t')" . + next + from et show ext': "extend_highest_gen s th prio tm t'" + by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) + qed + qed +qed + + +lemma th_kept: "th \ threads (t @ s) \ + preced th (t@s) = preced th s" (is "?Q t") +proof - + show ?thesis + proof(induct rule:ind) + case Nil + from threads_s + show ?case + by auto + next + case (Cons e t) + interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto + interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto + show ?case + proof(cases e) + case (Create thread prio) + show ?thesis + proof - + from Cons and Create have "step (t@s) (Create thread prio)" by auto + hence "th \ thread" + proof(cases) + case thread_create + with Cons show ?thesis by auto + qed + hence "preced th ((e # t) @ s) = preced th (t @ s)" + by (unfold Create, auto simp:preced_def) + moreover note Cons + ultimately show ?thesis + by (auto simp:Create) + qed + next + case (Exit thread) + from h_e.exit_diff and Exit + have neq_th: "thread \ th" by auto + with Cons + show ?thesis + by (unfold Exit, auto simp:preced_def) + next + case (P thread cs) + with Cons + show ?thesis + by (auto simp:P preced_def) + next + case (V thread cs) + with Cons + show ?thesis + by (auto simp:V preced_def) + next + case (Set thread prio') + show ?thesis + proof - + from h_e.set_diff_low and Set + have "th \ thread" by auto + hence "preced th ((e # t) @ s) = preced th (t @ s)" + by (unfold Set, auto simp:preced_def) + moreover note Cons + ultimately show ?thesis + by (auto simp:Set) + qed + qed + qed +qed + +text {* + According to @{thm th_kept}, thread @{text "th"} has its living status + and precedence kept along the way of @{text "t"}. The following lemma + shows that this preserved precedence of @{text "th"} remains as the highest + along the way of @{text "t"}. + + The proof goes by induction over @{text "t"} using the specialized + induction rule @{thm ind}, followed by case analysis of each possible + operations of PIP. All cases follow the same pattern rendered by the + generalized introduction rule @{thm "image_Max_eqI"}. + + The very essence is to show that precedences, no matter whether they are newly introduced + or modified, are always lower than the one held by @{term "th"}, + which by @{thm th_kept} is preserved along the way. +*} +lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" +proof(induct rule:ind) + case Nil + from highest_preced_thread + show ?case + by (unfold the_preced_def, simp) +next + case (Cons e t) + interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto + interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto + show ?case + proof(cases e) + case (Create thread prio') + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + -- {* The following is the common pattern of each branch of the case analysis. *} + -- {* The major part is to show that @{text "th"} holds the highest precedence: *} + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) + thus "?f x \ ?f th" + proof + assume "x = thread" + thus ?thesis + apply (simp add:Create the_preced_def preced_def, fold preced_def) + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force + next + assume h: "x \ threads (t @ s)" + from Cons(2)[unfolded Create] + have "x \ thread" using h by (cases, auto) + hence "?f x = the_preced (t@s) x" + by (simp add:Create the_preced_def preced_def) + hence "?f x \ Max (the_preced (t@s) ` threads (t@s))" + by (simp add: h_t.finite_threads h) + also have "... = ?f th" + by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed + qed + -- {* The minor part is to show that the precedence of @{text "th"} + equals to preserved one, given by the foregoing lemma @{thm th_kept} *} + also have "... = ?t" using h_e.th_kept the_preced_def by auto + -- {* Then it follows trivially that the precedence preserved + for @{term "th"} remains the maximum of all living threads along the way. *} + finally show ?thesis . + qed + next + case (Exit thread) + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x \ threads (t@s)" by (simp add: Exit) + hence "?f x \ Max (?f ` threads (t@s))" + by (simp add: h_t.finite_threads) + also have "... \ ?f th" + apply (simp add:Exit the_preced_def preced_def, fold preced_def) + using Cons.hyps(5) h_t.th_kept the_preced_def by auto + finally show "?f x \ ?f th" . + qed + qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed + next + case (P thread cs) + with Cons + show ?thesis by (auto simp:preced_def the_preced_def) + next + case (V thread cs) + with Cons + show ?thesis by (auto simp:preced_def the_preced_def) + next + case (Set thread prio') + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume h: "x \ ?A" + show "?f x \ ?f th" + proof(cases "x = thread") + case True + moreover have "the_preced (Set thread prio' # t @ s) thread \ the_preced (t @ s) th" + proof - + have "the_preced (t @ s) th = Prc prio tm" + using h_t.th_kept preced_th by (simp add:the_preced_def) + moreover have "prio' \ prio" using Set h_e.set_diff_low by auto + ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) + qed + ultimately show ?thesis + by (unfold Set, simp add:the_preced_def preced_def) + next + case False + then have "?f x = the_preced (t@s) x" + by (simp add:the_preced_def preced_def Set) + also have "... \ Max (the_preced (t@s) ` threads (t@s))" + using Set h h_t.finite_threads by auto + also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed + qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed + qed +qed + +lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))" + by (insert th_kept max_kept, auto) + +text {* + The reason behind the following lemma is that: + Since @{term "cp"} is defined as the maximum precedence + of those threads contained in the sub-tree of node @{term "Th th"} + in @{term "RAG (t@s)"}, and all these threads are living threads, and + @{term "th"} is also among them, the maximum precedence of + them all must be the one for @{text "th"}. +*} +lemma th_cp_max_preced: + "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") +proof - + let ?f = "the_preced (t@s)" + have "?L = ?f th" + proof(unfold cp_alt_def, rule image_Max_eqI) + show "finite {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + proof - + have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = + the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ + (\ th'. n = Th th')}" + by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) + moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) + ultimately show ?thesis by simp + qed + next + show "th \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + by (auto simp:subtree_def) + next + show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. + the_preced (t @ s) x \ the_preced (t @ s) th" + proof + fix th' + assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto + moreover have "... \ Field (RAG (t @ s)) \ {Th th}" + by (meson subtree_Field) + ultimately have "Th th' \ ..." by auto + hence "th' \ threads (t@s)" + proof + assume "Th th' \ {Th th}" + thus ?thesis using th_kept by auto + next + assume "Th th' \ Field (RAG (t @ s))" + thus ?thesis using vat_t.not_in_thread_isolated by blast + qed + thus "the_preced (t @ s) th' \ the_preced (t @ s) th" + by (metis Max_ge finite_imageI finite_threads image_eqI + max_kept th_kept the_preced_def) + qed + qed + also have "... = ?R" by (simp add: max_preced the_preced_def) + finally show ?thesis . +qed + +lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" + using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger + +lemma th_cp_preced: "cp (t@s) th = preced th s" + by (fold max_kept, unfold th_cp_max_preced, simp) + +lemma preced_less: + assumes th'_in: "th' \ threads s" + and neq_th': "th' \ th" + shows "preced th' s < preced th s" + using assms +by (metis Max.coboundedI finite_imageI highest not_le order.trans + preced_linorder rev_image_eqI threads_s vat_s.finite_threads + vat_s.le_cp) + +text {* + Counting of the number of @{term "P"} and @{term "V"} operations + is the cornerstone of a large number of the following proofs. + The reason is that this counting is quite easy to calculate and + convenient to use in the reasoning. + + The following lemma shows that the counting controls whether + a thread is running or not. +*} + +lemma pv_blocked_pre: + assumes th'_in: "th' \ threads (t@s)" + and neq_th': "th' \ th" + and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" + shows "th' \ runing (t@s)" +proof + assume otherwise: "th' \ runing (t@s)" + show False + proof - + have "th' = th" + proof(rule preced_unique) + show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") + proof - + have "?L = cp (t@s) th'" + by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + also have "... = cp (t @ s) th" using otherwise + by (metis (mono_tags, lifting) mem_Collect_eq + runing_def th_cp_max vat_t.max_cp_readys_threads) + also have "... = ?R" by (metis th_cp_preced th_kept) + finally show ?thesis . + qed + qed (auto simp: th'_in th_kept) + moreover have "th' \ th" using neq_th' . + ultimately show ?thesis by simp + qed +qed + +lemmas pv_blocked = pv_blocked_pre[folded detached_eq] + +lemma runing_precond_pre: + fixes th' + assumes th'_in: "th' \ threads s" + and eq_pv: "cntP s th' = cntV s th'" + and neq_th': "th' \ th" + shows "th' \ threads (t@s) \ + cntP (t@s) th' = cntV (t@s) th'" +proof(induct rule:ind) + case (Cons e t) + interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp + interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp + show ?case + proof(cases e) + case (P thread cs) + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (P thread cs)" using Cons P by auto + thus ?thesis + proof(cases) + assume "thread \ runing (t@s)" + moreover have "th' \ runing (t@s)" using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + ultimately show ?thesis by auto + qed + qed with Cons show ?thesis + by (unfold P, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold P, simp) + ultimately show ?thesis by auto + qed + next + case (V thread cs) + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (V thread cs)" using Cons V by auto + thus ?thesis + proof(cases) + assume "thread \ runing (t@s)" + moreover have "th' \ runing (t@s)" using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + ultimately show ?thesis by auto + qed + qed with Cons show ?thesis + by (unfold V, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold V, simp) + ultimately show ?thesis by auto + qed + next + case (Create thread prio') + show ?thesis + proof - + have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" + proof - + have "thread \ th'" + proof - + have "step (t@s) (Create thread prio')" using Cons Create by auto + thus ?thesis using Cons(5) by (cases, auto) + qed with Cons show ?thesis + by (unfold Create, simp add:cntP_def cntV_def count_def) + qed + moreover have "th' \ threads ((e # t) @ s)" using Cons by (unfold Create, simp) + ultimately show ?thesis by auto + qed + next + case (Exit thread) + show ?thesis + proof - + have neq_thread: "thread \ th'" + proof - + have "step (t@s) (Exit thread)" using Cons Exit by auto + thus ?thesis apply (cases) using Cons(5) + by (metis neq_th' vat_t.pv_blocked_pre) + qed + hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons + by (unfold Exit, simp add:cntP_def cntV_def count_def) + moreover have "th' \ threads ((e # t) @ s)" using Cons neq_thread + by (unfold Exit, simp) + ultimately show ?thesis by auto + qed + next + case (Set thread prio') + with Cons + show ?thesis + by (auto simp:cntP_def cntV_def count_def) + qed +next + case Nil + with assms + show ?case by auto +qed + +text {* Changing counting balance to detachedness *} +lemmas runing_precond_pre_dtc = runing_precond_pre + [folded vat_t.detached_eq vat_s.detached_eq] + +lemma runing_precond: + fixes th' + assumes th'_in: "th' \ threads s" + and neq_th': "th' \ th" + and is_runing: "th' \ runing (t@s)" + shows "cntP s th' > cntV s th'" + using assms +proof - + have "cntP s th' \ cntV s th'" + by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) + moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto + ultimately show ?thesis by auto +qed + +lemma moment_blocked_pre: + assumes neq_th': "th' \ th" + and th'_in: "th' \ threads ((moment i t)@s)" + and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" + shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \ + th' \ threads ((moment (i+j) t)@s)" +proof - + interpret h_i: red_extend_highest_gen _ _ _ _ _ i + by (unfold_locales) + interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" + by (unfold_locales) + interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" + proof(unfold_locales) + show "vt (moment i t @ s)" by (metis h_i.vt_t) + next + show "th \ threads (moment i t @ s)" by (metis h_i.th_kept) + next + show "preced th (moment i t @ s) = + Max (cp (moment i t @ s) ` threads (moment i t @ s))" + by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) + next + show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) + next + show "vt (moment j (restm i t) @ moment i t @ s)" + using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) + next + fix th' prio' + assume "Create th' prio' \ set (moment j (restm i t))" + thus "prio' \ prio" using assms + by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) + next + fix th' prio' + assume "Set th' prio' \ set (moment j (restm i t))" + thus "th' \ th \ prio' \ prio" + by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) + next + fix th' + assume "Exit th' \ set (moment j (restm i t))" + thus "th' \ th" + by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) + qed + show ?thesis + by (metis add.commute append_assoc eq_pv h.runing_precond_pre + moment_plus_split neq_th' th'_in) +qed + +lemma moment_blocked_eqpv: + assumes neq_th': "th' \ th" + and th'_in: "th' \ threads ((moment i t)@s)" + and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" + and le_ij: "i \ j" + shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \ + th' \ threads ((moment j t)@s) \ + th' \ runing ((moment j t)@s)" +proof - + from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij + have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" + and h2: "th' \ threads ((moment j t)@s)" by auto + moreover have "th' \ runing ((moment j t)@s)" + proof - + interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) + show ?thesis + using h.pv_blocked_pre h1 h2 neq_th' by auto + qed + ultimately show ?thesis by auto +qed + +(* The foregoing two lemmas are preparation for this one, but + in long run can be combined. Maybe I am wrong. +*) +lemma moment_blocked: + assumes neq_th': "th' \ th" + and th'_in: "th' \ threads ((moment i t)@s)" + and dtc: "detached (moment i t @ s) th'" + and le_ij: "i \ j" + shows "detached (moment j t @ s) th' \ + th' \ threads ((moment j t)@s) \ + th' \ runing ((moment j t)@s)" +proof - + interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) + interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) + have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" + by (metis dtc h_i.detached_elim) + from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] + show ?thesis by (metis h_j.detached_intro) +qed + +lemma runing_preced_inversion: + assumes runing': "th' \ runing (t@s)" + shows "cp (t@s) th' = preced th s" (is "?L = ?R") +proof - + have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms + by (unfold runing_def, auto) + also have "\ = ?R" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) + finally show ?thesis . +qed + +text {* + The situation when @{term "th"} is blocked is analyzed by the following lemmas. +*} + +text {* + The following lemmas shows the running thread @{text "th'"}, if it is different from + @{term th}, must be live at the very beginning. By the term {\em the very beginning}, + we mean the moment where the formal investigation starts, i.e. the moment (or state) + @{term s}. +*} + +lemma runing_inversion_0: + assumes neq_th': "th' \ th" + and runing': "th' \ runing (t@s)" + shows "th' \ threads s" +proof - + -- {* The proof is by contradiction: *} + { assume otherwise: "\ ?thesis" + have "th' \ runing (t @ s)" + proof - + -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} + have th'_in: "th' \ threads (t@s)" using runing' by (simp add:runing_def readys_def) + -- {* However, @{text "th'"} does not exist at very beginning. *} + have th'_notin: "th' \ threads (moment 0 t @ s)" using otherwise + by (metis append.simps(1) moment_zero) + -- {* Therefore, there must be a moment during @{text "t"}, when + @{text "th'"} came into being. *} + -- {* Let us suppose the moment being @{text "i"}: *} + from p_split_gen[OF th'_in th'_notin] + obtain i where lt_its: "i < length t" + and le_i: "0 \ i" + and pre: " th' \ threads (moment i t @ s)" (is "th' \ threads ?pre") + and post: "(\i'>i. th' \ threads (moment i' t @ s))" by (auto) + interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) + interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) + from lt_its have "Suc i \ length t" by auto + -- {* Let us also suppose the event which makes this change is @{text e}: *} + from moment_head[OF this] obtain e where + eq_me: "moment (Suc i) t = e # moment i t" by blast + hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) + hence "PIP (moment i t @ s) e" by (cases, simp) + -- {* It can be derived that this event @{text "e"}, which + gives birth to @{term "th'"} must be a @{term "Create"}: *} + from create_pre[OF this, of th'] + obtain prio where eq_e: "e = Create th' prio" + by (metis append_Cons eq_me lessI post pre) + have h1: "th' \ threads (moment (Suc i) t @ s)" using post by auto + have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" + proof - + have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" + by (metis h_i.cnp_cnv_eq pre) + thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) + qed + show ?thesis + using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge + by auto + qed + with `th' \ runing (t@s)` + have False by simp + } thus ?thesis by auto +qed + +text {* + The second lemma says, if the running thread @{text th'} is different from + @{term th}, then this @{text th'} must in the possession of some resources + at the very beginning. + + To ease the reasoning of resource possession of one particular thread, + we used two auxiliary functions @{term cntV} and @{term cntP}, + which are the counters of @{term P}-operations and + @{term V}-operations respectively. + If the number of @{term V}-operation is less than the number of + @{term "P"}-operations, the thread must have some unreleased resource. +*} + +lemma runing_inversion_1: (* ddd *) + assumes neq_th': "th' \ th" + and runing': "th' \ runing (t@s)" + -- {* thread @{term "th'"} is a live on in state @{term "s"} and + it has some unreleased resource. *} + shows "th' \ threads s \ cntV s th' < cntP s th'" +proof - + -- {* The proof is a simple composition of @{thm runing_inversion_0} and + @{thm runing_precond}: *} + -- {* By applying @{thm runing_inversion_0} to assumptions, + it can be shown that @{term th'} is live in state @{term s}: *} + have "th' \ threads s" using runing_inversion_0[OF assms(1,2)] . + -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *} + with runing_precond [OF this neq_th' runing'] show ?thesis by simp +qed + +text {* + The following lemma is just a rephrasing of @{thm runing_inversion_1}: +*} +lemma runing_inversion_2: + assumes runing': "th' \ runing (t@s)" + shows "th' = th \ (th' \ th \ th' \ threads s \ cntV s th' < cntP s th')" +proof - + from runing_inversion_1[OF _ runing'] + show ?thesis by auto +qed + +lemma runing_inversion_3: + assumes runing': "th' \ runing (t@s)" + and neq_th: "th' \ th" + shows "th' \ threads s \ (cntV s th' < cntP s th' \ cp (t@s) th' = preced th s)" + by (metis neq_th runing' runing_inversion_2 runing_preced_inversion) + +lemma runing_inversion_4: + assumes runing': "th' \ runing (t@s)" + and neq_th: "th' \ th" + shows "th' \ threads s" + and "\detached s th'" + and "cp (t@s) th' = preced th s" + apply (metis neq_th runing' runing_inversion_2) + apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) + by (metis neq_th runing' runing_inversion_3) + + +text {* + Suppose @{term th} is not running, it is first shown that + there is a path in RAG leading from node @{term th} to another thread @{text "th'"} + in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). + + Now, since @{term readys}-set is non-empty, there must be + one in it which holds the highest @{term cp}-value, which, by definition, + is the @{term runing}-thread. However, we are going to show more: this running thread + is exactly @{term "th'"}. + *} +lemma th_blockedE: (* ddd *) + assumes "th \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" +proof - + -- {* According to @{thm vat_t.th_chain_to_ready}, either + @{term "th"} is in @{term "readys"} or there is path leading from it to + one thread in @{term "readys"}. *} + have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" + using th_kept vat_t.th_chain_to_ready by auto + -- {* However, @{term th} can not be in @{term readys}, because otherwise, since + @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} + moreover have "th \ readys (t@s)" + using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in + term @{term readys}: *} + ultimately obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} + have "th' \ runing (t@s)" + proof - + -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} + have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") + proof - + have "?L = Max ((the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" + by (unfold cp_alt_def1, simp) + also have "... = (the_preced (t @ s) \ the_thread) (Th th)" + proof(rule image_Max_subset) + show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) + next + show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" + by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) + next + show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp + by (unfold tRAG_subtree_eq, auto simp:subtree_def) + next + show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = + (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") + proof - + have "?L = the_preced (t @ s) ` threads (t @ s)" + by (unfold image_comp, rule image_cong, auto) + thus ?thesis using max_preced the_preced_def by auto + qed + qed + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + finally show ?thesis . + qed + -- {* Now, since @{term th'} holds the highest @{term cp} + and we have already show it is in @{term readys}, + it is @{term runing} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) + qed + -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} + moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" + using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) + ultimately show ?thesis using that by metis +qed + +text {* + Now it is easy to see there is always a thread to run by case analysis + on whether thread @{term th} is running: if the answer is Yes, the + the running thread is obviously @{term th} itself; otherwise, the running + thread is the @{text th'} given by lemma @{thm th_blockedE}. +*} +lemma live: "runing (t@s) \ {}" +proof(cases "th \ runing (t@s)") + case True thus ?thesis by auto +next + case False + thus ?thesis using th_blockedE by auto +qed + +end +end +