The overwriten original .thy files are working now. The ones in last revision aren't.
section {* This file contains lemmas used to guide the recalculation of current precedence after every system call (or system operation)*}theory ExtGGimports CpsGbegintext {* (* 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 *}context valid_trace_setbegintext {* (* 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' (e#s) = preced th' s"proof - from assms show ?thesis by (unfold is_set, auto simp:preced_def)qedlemma eq_the_preced: assumes "th' \<noteq> th" shows "the_preced (e#s) th' = the_preced s th'" using assms by (unfold the_preced_def, intro eq_preced, simp)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 (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 (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#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 RAG_unchanged 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 (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) 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 - from readys_in_no_subtree[OF th_ready_s 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 (e#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.*}context valid_trace_vbeginlemma ancestors_th: "ancestors (RAG s) (Th th) = {}"proof - from readys_root[OF th_ready_s] show ?thesis by (unfold root_def, simp)qedlemma edge_of_th: "(Cs cs, Th th) \<in> RAG s" proof - from holding_th_cs_s 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}" by (rule rtree_RAG.ancestors_accum[OF edge_of_th]) from this[unfolded ancestors_th] show ?thesis by simpqedendtext {* 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"}.*}context valid_trace_v_nbeginlemma sub_RAGs': "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s" using next_th_RAG[OF next_th_taker] .lemma ancestors_th': "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" proof - have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}" proof(rule rtree_RAG.ancestors_accum) from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto qed thus ?thesis using ancestors_th ancestors_cs by autoqedlemma RAG_s: "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union> {(Cs cs, Th taker)}" by (unfold RAG_es waiting_set_eq holding_set_eq, auto)lemma subtree_kept: (* ddd *) assumes "th1 \<notin> {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 taker, Cs cs)})" let ?RAG'' = "?RAG' \<union> {(Cs cs, Th taker)}" have "subtree ?RAG' (Th th1) = ?R" proof(rule subset_del_subtree_outside) show "Range {(Cs cs, Th th), (Th taker, 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 taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" proof(rule subtree_refute) show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" (is "_ \<notin> ?R") proof - have "?R \<subseteq> ancestors (RAG s) (Th taker)" 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 taker" by simp qed qed ultimately show ?thesis by (unfold RAG_s, simp)qedlemma cp_kept: assumes "th1 \<notin> {th, taker}" shows "cp (e#s) th1 = cp s th1" by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)endcontext valid_trace_v_ebeginfind_theorems RAG s elemma 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 \<noteq> th" 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)} \<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 (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}"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_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 \<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 (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) \<in> edges_in (RAG s) (Th th)" by (unfold edges_in_def, auto simp:subtree_def)qedlemma cp_kept_2: shows "cp (e#s) th = cp s th" by (unfold cp_alt_def subtree_th the_preced_es, auto)lemma eq_cp: shows "cp (e#s) th' = cp s th'" using cp_kept_1 cp_kept_2 by (cases "th' = th", auto)endsection {* The @{term P} operation *}context valid_trace_pbeginlemma root_th: "root (RAG s) (Th th)" by (simp add: ready_th_s readys_root)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 (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)qedendcontext valid_trace_p_hbeginlemma subtree_kept: assumes "th' \<noteq> th" 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 \<notin> subtree (RAG s) (Th th')" .qedlemma cp_kept: assumes "th' \<noteq> th" shows "cp (e#s) th' = cp s th'"proof - have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#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 valid_trace_p_wbegininterpretation vat_e: valid_trace "e#s" by (unfold_locales, insert vt_e, simp)lemma cs_held: "(Cs cs, Th holder) \<in> RAG s" using holding_s_holder by (unfold s_RAG_def, fold holding_eq, auto)lemma tRAG_s: "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}" using local.RAG_tRAG_transfer[OF RAG_es cs_held] .lemma cp_kept: assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)" shows "cp (e#s) th'' = cp s th''"proof - have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')" proof - have "Th holder \<notin> subtree (tRAG s) (Th th'')" proof assume "Th holder \<in> subtree (tRAG s) (Th th'')" thus False proof(rule subtreeE) assume "Th holder = Th th''" from assms[unfolded tRAG_s ancestors_def, folded this] show ?thesis by auto next assume "Th th'' \<in> ancestors (tRAG s) (Th holder)" moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)" proof(rule ancestors_mono) show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto) qed ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)" by (unfold tRAG_s, auto simp:ancestors_def) ultimately have "Th th'' \<in> 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 \<union> {(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)qedlemma cp_gen_update_stop: (* ddd *) assumes "u \<in> ancestors (tRAG (e#s)) (Th th)" and "cp_gen (e#s) u = cp_gen s u" and "y \<in> 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_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_e.cp_gen_rec[OF this] have "?L = Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#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 (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 (e#s)) x = RTree.children (tRAG s) x" proof(unfold tRAG_s, rule children_union_kept) have start: "(Th th, Th holder) \<in> tRAG (e#s)" by (unfold tRAG_s, auto) note x_u = 1(2) show "x \<notin> Range {(Th th, Th holder)}" proof assume "x \<in> Range {(Th th, Th holder)}" hence eq_x: "x = Th holder" using RangeE by auto show False proof(cases rule:vat_e.ancestors_headE[OF assms(1) start]) case 1 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 holder, Th holder) \<in> (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 (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 \<in> ?A" from 1(2) show "?f a = ?g a" proof(cases rule:vat_e.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 (e#s)) (Th th)" proof assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" have "a = u" proof(rule vat_e.rtree_s.ancestors_children_unique) from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x" by auto next from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 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 (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 \<in> ancestors (tRAG (e#s)) u" "z \<in> RTree.children (tRAG (e#s)) x" by auto show ?thesis proof(cases "a = z") case True from h(2) have zx_in: "(z, x) \<in> (tRAG (e#s))" by (auto simp:RTree.children_def) from 1(1)[rule_format, OF this h(1)] 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 \<notin> ancestors (tRAG (e#s)) (Th th)" proof assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" have "a = z" proof(rule vat_e.rtree_s.ancestors_children_unique) from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" by (auto simp:ancestors_def) with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x" by auto next from a_in a_in' show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 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 (e#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 cp_gen_rec[OF eq_x], simp) finally show ?thesis . qedqedlemma cp_up: assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)" and "cp (e#s) th' = cp s th'" and "(Th th'') \<in> ancestors (tRAG (e#s)) (Th th')" shows "cp (e#s) th'' = cp s th''"proof - 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 (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 metisqedendsection {* The @{term Create} operation *}context valid_trace_createbegin interpretation vat_e: valid_trace "e#s" by (unfold_locales, insert vt_e, simp)lemma tRAG_kept: "tRAG (e#s) = tRAG s" by (unfold tRAG_alt_def RAG_unchanged, auto)lemma preced_kept: assumes "th' \<noteq> th" 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 \<notin> Field (tRAG s)" by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)lemma eq_cp: assumes neq_th: "th' \<noteq> th" shows "cp (e#s) th' = cp s th'"proof - have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#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 (e#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 (e#s)) (Th th) = {}"proof - { fix a assume "a \<in> RTree.children (tRAG (e#s)) (Th th)" hence "(a, Th th) \<in> 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 autoqedlemma 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)endcontext valid_trace_exitbeginlemma preced_kept: assumes "th' \<noteq> th" shows "the_preced (e#s) th' = the_preced s th'" using assms by (unfold the_preced_def is_exit preced_def, simp)lemma tRAG_kept: "tRAG (e#s) = tRAG s" by (unfold tRAG_alt_def RAG_unchanged, auto)lemma 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 holdents_th_s[unfolded holdents_def] show False by (unfold holding_eq, 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_s show False by (unfold readys_def waiting_eq, auto) qed ultimately show ?thesis by (auto simp:Field_def)qedlemma th_tRAG: "(Th th) \<notin> Field (tRAG s)" using th_RAG tRAG_Field by autolemma eq_cp: assumes neq_th: "th' \<noteq> th" shows "cp (e#s) th' = cp s th'"proof - have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#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 readys_in_no_subtree[OF th_ready_s 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 (e#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=======theory ExtGGimports PrioG CpsGbegintext {* The following two auxiliary lemmas are used to reason about @{term Max}.*}lemma image_Max_eqI: assumes "finite B" and "b \<in> B" and "\<forall> x \<in> B. f x \<le> f b" shows "Max (f ` B) = f b" using assms using Max_eqI by blast lemma image_Max_subset: assumes "finite A" and "B \<subseteq> A" and "a \<in> 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 \<in> B" using assms by simpnext show "\<forall>x\<in>B. f x \<le> f a" by (metis Max_ge assms(1) assms(2) assms(4) finite_imageI image_eqI subsetCE) qedtext {* 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 \<in> 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_genbegintext {* @{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 \<le> ?R" by (unfold highest, rule Max_ge, auto simp:threads_s finite_threads) moreover have "?R \<le> ?L" by (unfold vat_s.cp_rec, rule Max_ge, auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) ultimately show ?thesis by autoqed(* ccc *)lemma highest_cp_preced: "cp s th = Max ((\<lambda> 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 ((\<lambda> 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 simpqedendlocale extend_highest_gen = highest_gen + fixes t assumes vt_t: "vt (t@s)" and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio" and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio" and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> 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) \<Longrightarrow> 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 qedqedlocale red_extend_highest_gen = extend_highest_gen + fixes i::natsublocale 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_genbegin lemma ind [consumes 0, case_names Nil Cons, induct type]: assumes h0: "R []" and h2: "\<And> e t. \<lbrakk>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\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> 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 qedqedlemma th_kept: "th \<in> threads (t @ s) \<and> 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 \<noteq> 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 \<noteq> 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 \<noteq> 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 qedqedtext {* 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 \<in> ?A" using h_e.th_kept by auto next show "\<forall>x\<in>?A. ?f x \<le> ?f th" proof fix x assume "x \<in> ?A" hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create) thus "?f x \<le> ?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 \<in> threads (t @ s)" from Cons(2)[unfolded Create] have "x \<noteq> 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 \<le> 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 \<in> ?A" using h_e.th_kept by auto next show "\<forall>x\<in>?A. ?f x \<le> ?f th" proof fix x assume "x \<in> ?A" hence "x \<in> threads (t@s)" by (simp add: Exit) hence "?f x \<le> Max (?f ` threads (t@s))" by (simp add: h_t.finite_threads) also have "... \<le> ?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 \<le> ?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 \<in> ?A" using h_e.th_kept by auto next show "\<forall>x\<in>?A. ?f x \<le> ?f th" proof fix x assume h: "x \<in> ?A" show "?f x \<le> ?f th" proof(cases "x = thread") case True moreover have "the_preced (Set thread prio' # t @ s) thread \<le> 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' \<le> 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 "... \<le> 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 qedqedlemma 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' \<in> subtree (RAG (t @ s)) (Th th)}" proof - have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and> (\<exists> 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 \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" by (auto simp:subtree_def) next show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}. the_preced (t @ s) x \<le> the_preced (t @ s) th" proof fix th' assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}" by (meson subtree_Field) ultimately have "Th th' \<in> ..." by auto hence "th' \<in> threads (t@s)" proof assume "Th th' \<in> {Th th}" thus ?thesis using th_kept by auto next assume "Th th' \<in> Field (RAG (t @ s))" thus ?thesis using vat_t.not_in_thread_isolated by blast qed thus "the_preced (t @ s) th' \<le> 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 .qedlemma 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 presburgerlemma 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' \<in> threads s" and neq_th': "th' \<noteq> th" shows "preced th' s < preced th s" using assmsby (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' \<in> threads (t@s)" and neq_th': "th' \<noteq> th" and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" shows "th' \<notin> runing (t@s)"proof assume otherwise: "th' \<in> 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' \<noteq> th" using neq_th' . ultimately show ?thesis by simp qedqedlemmas pv_blocked = pv_blocked_pre[folded detached_eq]lemma runing_precond_pre: fixes th' assumes th'_in: "th' \<in> threads s" and eq_pv: "cntP s th' = cntV s th'" and neq_th': "th' \<noteq> th" shows "th' \<in> threads (t@s) \<and> 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 \<noteq> th'" proof - have "step (t@s) (P thread cs)" using Cons P by auto thus ?thesis proof(cases) assume "thread \<in> runing (t@s)" moreover have "th' \<notin> 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' \<in> 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 \<noteq> th'" proof - have "step (t@s) (V thread cs)" using Cons V by auto thus ?thesis proof(cases) assume "thread \<in> runing (t@s)" moreover have "th' \<notin> 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' \<in> 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 \<noteq> 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' \<in> 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 \<noteq> 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' \<in> 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) qednext case Nil with assms show ?case by autoqedtext {* 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' \<in> threads s" and neq_th': "th' \<noteq> th" and is_runing: "th' \<in> runing (t@s)" shows "cntP s th' > cntV s th'" using assmsproof - have "cntP s th' \<noteq> cntV s th'" by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto ultimately show ?thesis by autoqedlemma moment_blocked_pre: assumes neq_th': "th' \<noteq> th" and th'_in: "th' \<in> 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' \<and> th' \<in> 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 \<in> 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' \<in> set (moment j (restm i t))" thus "prio' \<le> 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' \<in> set (moment j (restm i t))" thus "th' \<noteq> th \<and> prio' \<le> prio" by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) next fix th' assume "Exit th' \<in> set (moment j (restm i t))" thus "th' \<noteq> 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)qedlemma moment_blocked_eqpv: assumes neq_th': "th' \<noteq> th" and th'_in: "th' \<in> threads ((moment i t)@s)" and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" and le_ij: "i \<le> j" shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> th' \<in> threads ((moment j t)@s) \<and> th' \<notin> 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' \<in> threads ((moment j t)@s)" by auto moreover have "th' \<notin> 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 autoqed(* 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' \<noteq> th" and th'_in: "th' \<in> threads ((moment i t)@s)" and dtc: "detached (moment i t @ s) th'" and le_ij: "i \<le> j" shows "detached (moment j t @ s) th' \<and> th' \<in> threads ((moment j t)@s) \<and> th' \<notin> 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) qedlemma runing_preced_inversion: assumes runing': "th' \<in> 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 "\<dots> = ?R" by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) finally show ?thesis .qedtext {* 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' \<noteq> th" and runing': "th' \<in> runing (t@s)" shows "th' \<in> threads s"proof - -- {* The proof is by contradiction: *} { assume otherwise: "\<not> ?thesis" have "th' \<notin> runing (t @ s)" proof - -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} have th'_in: "th' \<in> 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' \<notin> 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 \<le> i" and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre") and post: "(\<forall>i'>i. th' \<in> 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 \<le> 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' \<in> 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' \<in> runing (t@s)` have False by simp } thus ?thesis by autoqedtext {* 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' \<noteq> th" and runing': "th' \<in> runing (t@s)" -- {* thread @{term "th'"} is a live on in state @{term "s"} and it has some unreleased resource. *} shows "th' \<in> threads s \<and> 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' \<in> 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 simpqedtext {* The following lemma is just a rephrasing of @{thm runing_inversion_1}:*}lemma runing_inversion_2: assumes runing': "th' \<in> runing (t@s)" shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"proof - from runing_inversion_1[OF _ runing'] show ?thesis by autoqedlemma runing_inversion_3: assumes runing': "th' \<in> runing (t@s)" and neq_th: "th' \<noteq> th" shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> 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' \<in> runing (t@s)" and neq_th: "th' \<noteq> th" shows "th' \<in> threads s" and "\<not>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 \<notin> runing (t@s)" obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" "th' \<in> 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 \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (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 \<notin> 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' \<in> readys (t@s)" and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto -- {* We are going to show that this @{term th'} is running. *} have "th' \<in> 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) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))" by (unfold cp_alt_def1, simp) also have "... = (the_preced (t @ s) \<circ> 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') \<subseteq> Th ` threads (t @ s)" by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) next show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp by (unfold tRAG_subtree_eq, auto simp:subtree_def) next show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) = (the_preced (t @ s) \<circ> 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' \<in> 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' \<in> ancestors (RAG (t @ s)) (Th th)" using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) ultimately show ?thesis using that by metisqedtext {* 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) \<noteq> {}"proof(cases "th \<in> runing (t@s)") case True thus ?thesis by autonext case False thus ?thesis using th_blockedE by autoqedendend