theory PrioGimports PrioGDef beginlemma runing_ready: shows "runing s \<subseteq> readys s" unfolding runing_def readys_def by auto lemma readys_threads: shows "readys s \<subseteq> threads s" unfolding readys_def by autolemma wq_v_neq: "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'" by (auto simp:wq_def Let_def cp_def split:list.splits)lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"proof(erule_tac vt.induct, simp add:wq_def) fix s e assume h1: "step s e" and h2: "distinct (wq s cs)" thus "distinct (wq (e # s) cs)" proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) fix thread s assume h1: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+" and h2: "thread \<in> set (wq_fun (schs s) cs)" and h3: "thread \<in> runing s" show "False" proof - from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow> thread = hd ((wq_fun (schs s) cs))" by (simp add:runing_def readys_def s_waiting_def wq_def) from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" . with h2 have "(Cs cs, Th thread) \<in> (RAG s)" by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def) with h1 show False by auto qed next fix thread s a list assume dst: "distinct list" show "distinct (SOME q. distinct q \<and> set q = set list)" proof(rule someI2) from dst show "distinct list \<and> set list = set list" by auto next fix q assume "distinct q \<and> set q = set list" thus "distinct q" by auto qed qedqedtext {* The following lemma shows that only the @{text "P"} operation can add new thread into waiting queues. Such kind of lemmas are very obvious, but need to be checked formally. This is a kind of confirmation that our modelling is correct.*}lemma block_pre: fixes thread cs s assumes vt_e: "vt (e#s)" and s_ni: "thread \<notin> set (wq s cs)" and s_i: "thread \<in> set (wq (e#s) cs)" shows "e = P thread cs"proof - show ?thesis proof(cases e) case (P th cs) with assms show ?thesis by (auto simp:wq_def Let_def split:if_splits) next case (Create th prio) with assms show ?thesis by (auto simp:wq_def Let_def split:if_splits) next case (Exit th) with assms show ?thesis by (auto simp:wq_def Let_def split:if_splits) next case (Set th prio) with assms show ?thesis by (auto simp:wq_def Let_def split:if_splits) next case (V th cs) with assms show ?thesis apply (auto simp:wq_def Let_def split:if_splits) proof - fix q qs assume h1: "thread \<notin> set (wq_fun (schs s) cs)" and h2: "q # qs = wq_fun (schs s) cs" and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" and vt: "vt (V th cs # s)" from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp moreover have "thread \<in> set qs" proof - have "set (SOME q. distinct q \<and> set q = set qs) = set qs" proof(rule someI2) from wq_distinct [OF step_back_vt[OF vt], of cs] and h2[symmetric, folded wq_def] show "distinct qs \<and> set qs = set qs" by auto next fix x assume "distinct x \<and> set x = set qs" thus "set x = set qs" by auto qed with h3 show ?thesis by simp qed ultimately show "False" by auto qed qedqedtext {* The following lemmas is also obvious and shallow. It says that only running thread can request for a critical resource and that the requested resource must be one which is not current held by the thread.*}lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (RAG s)^+"apply (ind_cases "vt ((P thread cs)#s)")apply (ind_cases "step s (P thread cs)")by autolemma abs1: fixes e es assumes ein: "e \<in> set es" and neq: "hd es \<noteq> hd (es @ [x])" shows "False"proof - from ein have "es \<noteq> []" by auto then obtain e ess where "es = e # ess" by (cases es, auto) with neq show ?thesis by autoqedlemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]" by (cases es, auto)inductive_cases evt_cons: "vt (a#s)"lemma abs2: assumes vt: "vt (e#s)" and inq: "thread \<in> set (wq s cs)" and nh: "thread = hd (wq s cs)" and qt: "thread \<noteq> hd (wq (e#s) cs)" and inq': "thread \<in> set (wq (e#s) cs)" shows "False"proof - from assms show "False" apply (cases e) apply ((simp split:if_splits add:Let_def wq_def)[1])+ apply (insert abs1, fast)[1] apply (auto simp:wq_def simp:Let_def split:if_splits list.splits) proof - fix th qs assume vt: "vt (V th cs # s)" and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" and eq_wq: "wq_fun (schs s) cs = thread # qs" show "False" proof - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp moreover have "thread \<in> set qs" proof - have "set (SOME q. distinct q \<and> set q = set qs) = set qs" proof(rule someI2) from wq_distinct [OF step_back_vt[OF vt], of cs] and eq_wq [folded wq_def] show "distinct qs \<and> set qs = set qs" by auto next fix x assume "distinct x \<and> set x = set qs" thus "set x = set qs" by auto qed with th_in show ?thesis by auto qed ultimately show ?thesis by auto qed qedqedlemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"proof(induct s, simp) fix a s t assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)" and vt_a: "vt (a # s)" show "vt (moment t (a # s))" proof(cases "t \<ge> length (a#s)") case True from True have "moment t (a#s) = a#s" by simp with vt_a show ?thesis by simp next case False hence le_t1: "t \<le> length s" by simp from vt_a have "vt s" by (erule_tac evt_cons, simp) from h [OF this] have "vt (moment t s)" . moreover have "moment t (a#s) = moment t s" proof - from moment_app [OF le_t1, of "[a]"] show ?thesis by simp qed ultimately show ?thesis by auto qedqed(* Wrong: lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"*)text {* (* ddd *) The nature of the work is like this: since it starts from a very simple and basic model, even intuitively very `basic` and `obvious` properties need to derived from scratch. For instance, the fact that one thread can not be blocked by two critical resources at the same time is obvious, because only running threads can make new requests, if one is waiting for a critical resource and get blocked, it can not make another resource request and get blocked the second time (because it is not running). To derive this fact, one needs to prove by contraction and reason about time (or @{text "moement"}). The reasoning is based on a generic theorem named @{text "p_split"}, which is about status changing along the time axis. It says if a condition @{text "Q"} is @{text "True"} at a state @{text "s"}, but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history of events leading to it), such that @{text "Q"} switched from being @{text "False"} to @{text "True"} and kept being @{text "True"} till the last moment of @{text "s"}. Suppose a thread @{text "th"} is blocked on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, since no thread is blocked at the very beginning, by applying @{text "p_split"} to these two blocking facts, there exist two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} and kept on blocked on them respectively ever since. Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}. However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still in blocked state at moment @{text "t2"} and could not make any request and get blocked the second time: Contradiction.*}lemma waiting_unique_pre: fixes cs1 cs2 s thread assumes vt: "vt s" and h11: "thread \<in> set (wq s cs1)" and h12: "thread \<noteq> hd (wq s cs1)" assumes h21: "thread \<in> set (wq s cs2)" and h22: "thread \<noteq> hd (wq s cs2)" and neq12: "cs1 \<noteq> cs2" shows "False"proof - let "?Q cs s" = "thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)" from h11 and h12 have q1: "?Q cs1 s" by simp from h21 and h22 have q2: "?Q cs2 s" by simp have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def) have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def) from p_split [of "?Q cs1", OF q1 nq1] obtain t1 where lt1: "t1 < length s" and np1: "\<not>(thread \<in> set (wq (moment t1 s) cs1) \<and> thread \<noteq> hd (wq (moment t1 s) cs1))" and nn1: "(\<forall>i'>t1. thread \<in> set (wq (moment i' s) cs1) \<and> thread \<noteq> hd (wq (moment i' s) cs1))" by auto from p_split [of "?Q cs2", OF q2 nq2] obtain t2 where lt2: "t2 < length s" and np2: "\<not>(thread \<in> set (wq (moment t2 s) cs2) \<and> thread \<noteq> hd (wq (moment t2 s) cs2))" and nn2: "(\<forall>i'>t2. thread \<in> set (wq (moment i' s) cs2) \<and> thread \<noteq> hd (wq (moment i' s) cs2))" by auto show ?thesis proof - { assume lt12: "t1 < t2" let ?t3 = "Suc t2" from lt2 have le_t3: "?t3 \<le> length s" by auto from moment_plus [OF this] obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto have "t2 < ?t3" by simp from nn2 [rule_format, OF this] and eq_m have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto have vt_e: "vt (e#moment t2 s)" proof - from vt_moment [OF vt] have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed have ?thesis proof(cases "thread \<in> set (wq (moment t2 s) cs2)") case True from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" by auto thm abs2 from abs2 [OF vt_e True eq_th h2 h1] show ?thesis by auto next case False from block_pre [OF vt_e False h1] have "e = P thread cs2" . with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp with runing_ready have "thread \<in> readys (moment t2 s)" by auto with nn1 [rule_format, OF lt12] show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) qed } moreover { assume lt12: "t2 < t1" let ?t3 = "Suc t1" from lt1 have le_t3: "?t3 \<le> length s" by auto from moment_plus [OF this] obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto have lt_t3: "t1 < ?t3" by simp from nn1 [rule_format, OF this] and eq_m have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto have vt_e: "vt (e#moment t1 s)" proof - from vt_moment [OF vt] have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed have ?thesis proof(cases "thread \<in> set (wq (moment t1 s) cs1)") case True from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" by auto from abs2 [OF vt_e True eq_th h2 h1] show ?thesis by auto next case False from block_pre [OF vt_e False h1] have "e = P thread cs1" . with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp with runing_ready have "thread \<in> readys (moment t1 s)" by auto with nn2 [rule_format, OF lt12] show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) qed } moreover { assume eqt12: "t1 = t2" let ?t3 = "Suc t1" from lt1 have le_t3: "?t3 \<le> length s" by auto from moment_plus [OF this] obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto have lt_t3: "t1 < ?t3" by simp from nn1 [rule_format, OF this] and eq_m have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto have vt_e: "vt (e#moment t1 s)" proof - from vt_moment [OF vt] have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed have ?thesis proof(cases "thread \<in> set (wq (moment t1 s) cs1)") case True from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" by auto from abs2 [OF vt_e True eq_th h2 h1] show ?thesis by auto next case False from block_pre [OF vt_e False h1] have eq_e1: "e = P thread cs1" . have lt_t3: "t1 < ?t3" by simp with eqt12 have "t2 < ?t3" by simp from nn2 [rule_format, OF this] and eq_m and eqt12 have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto show ?thesis proof(cases "thread \<in> set (wq (moment t2 s) cs2)") case True from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" by auto from vt_e and eqt12 have "vt (e#moment t2 s)" by simp from abs2 [OF this True eq_th h2 h1] show ?thesis . next case False have vt_e: "vt (e#moment t2 s)" proof - from vt_moment [OF vt] eqt12 have "vt (moment (Suc t2) s)" by auto with eq_m eqt12 show ?thesis by simp qed from block_pre [OF vt_e False h1] have "e = P thread cs2" . with eq_e1 neq12 show ?thesis by auto qed qed } ultimately show ?thesis by arith qedqedtext {* This lemma is a simple corrolary of @{text "waiting_unique_pre"}.*}lemma waiting_unique: fixes s cs1 cs2 assumes "vt s" and "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2"using waiting_unique_pre assmsunfolding wq_def s_waiting_defby auto(* not used *)text {* Every thread can only be blocked on one critical resource, symmetrically, every critical resource can only be held by one thread. This fact is much more easier according to our definition. *}lemma held_unique: fixes s::"state" assumes "holding s th1 cs" and "holding s th2 cs" shows "th1 = th2"using assmsunfolding s_holding_defby autolemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s" apply (induct s, auto) by (case_tac a, auto split:if_splits)lemma last_set_unique: "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk> \<Longrightarrow> th1 = th2" apply (induct s, auto) by (case_tac a, auto split:if_splits dest:last_set_lt)lemma preced_unique : assumes pcd_eq: "preced th1 s = preced th2 s" and th_in1: "th1 \<in> threads s" and th_in2: " th2 \<in> threads s" shows "th1 = th2"proof - from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def) from last_set_unique [OF this th_in1 th_in2] show ?thesis .qedlemma preced_linorder: assumes neq_12: "th1 \<noteq> th2" and th_in1: "th1 \<in> threads s" and th_in2: " th2 \<in> threads s" shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"proof - from preced_unique [OF _ th_in1 th_in2] and neq_12 have "preced th1 s \<noteq> preced th2 s" by auto thus ?thesis by autoqed(* An aux lemma used later *)lemma unique_minus: fixes x y z r assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" and xy: "(x, y) \<in> r" and xz: "(x, z) \<in> r^+" and neq: "y \<noteq> z" shows "(y, z) \<in> r^+"proof - from xz and neq show ?thesis proof(induct) case (base ya) have "(x, ya) \<in> r" by fact from unique [OF xy this] have "y = ya" . with base show ?case by auto next case (step ya z) show ?case proof(cases "y = ya") case True from step True show ?thesis by simp next case False from step False show ?thesis by auto qed qedqedlemma unique_base: fixes r x y z assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" and xy: "(x, y) \<in> r" and xz: "(x, z) \<in> r^+" and neq_yz: "y \<noteq> z" shows "(y, z) \<in> r^+"proof - from xz neq_yz show ?thesis proof(induct) case (base ya) from xy unique base show ?case by auto next case (step ya z) show ?case proof(cases "y = ya") case True from True step show ?thesis by auto next case False from False step have "(y, ya) \<in> r\<^sup>+" by auto with step show ?thesis by auto qed qedqedlemma unique_chain: fixes r x y z assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" and xy: "(x, y) \<in> r^+" and xz: "(x, z) \<in> r^+" and neq_yz: "y \<noteq> z" shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"proof - from xy xz neq_yz show ?thesis proof(induct) case (base y) have h1: "(x, y) \<in> r" and h2: "(x, z) \<in> r\<^sup>+" and h3: "y \<noteq> z" using base by auto from unique_base [OF _ h1 h2 h3] and unique show ?case by auto next case (step y za) show ?case proof(cases "y = z") case True from True step show ?thesis by auto next case False from False step have "(y, z) \<in> r\<^sup>+ \<or> (z, y) \<in> r\<^sup>+" by auto thus ?thesis proof assume "(z, y) \<in> r\<^sup>+" with step have "(z, za) \<in> r\<^sup>+" by auto thus ?thesis by auto next assume h: "(y, z) \<in> r\<^sup>+" from step have yza: "(y, za) \<in> r" by simp from step have "za \<noteq> z" by simp from unique_minus [OF _ yza h this] and unique have "(za, z) \<in> r\<^sup>+" by auto thus ?thesis by auto qed qed qedqedtext {* The following three lemmas show that @{text "RAG"} does not change by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"} events, respectively.*}lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"apply (unfold s_RAG_def s_waiting_def wq_def)by (simp add:Let_def)lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"apply (unfold s_RAG_def s_waiting_def wq_def)by (simp add:Let_def)lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"apply (unfold s_RAG_def s_waiting_def wq_def)by (simp add:Let_def)text {* The following lemmas are used in the proof of lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed by @{text "V"}-events. However, since our model is very concise, such seemingly obvious lemmas need to be derived from scratch, starting from the model definitions.*}lemma step_v_hold_inv[elim_format]: "\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"proof - fix c t assume vt: "vt (V th cs # s)" and nhd: "\<not> holding (wq s) t c" and hd: "holding (wq (V th cs # s)) t c" show "next_th s th cs t \<and> c = cs" proof(cases "c = cs") case False with nhd hd show ?thesis by (unfold cs_holding_def wq_def, auto simp:Let_def) next case True with step_back_step [OF vt] have "step s (V th c)" by simp hence "next_th s th cs t" proof(cases) assume "holding s th c" with nhd hd show ?thesis apply (unfold s_holding_def cs_holding_def wq_def next_th_def, auto simp:Let_def split:list.splits if_splits) proof - assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])" moreover have "\<dots> = set []" proof(rule someI2) show "distinct [] \<and> [] = []" by auto next fix x assume "distinct x \<and> x = []" thus "set x = set []" by auto qed ultimately show False by auto next assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])" moreover have "\<dots> = set []" proof(rule someI2) show "distinct [] \<and> [] = []" by auto next fix x assume "distinct x \<and> x = []" thus "set x = set []" by auto qed ultimately show False by auto qed qed with True show ?thesis by auto qedqedtext {* The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.*}lemma step_v_wait_inv[elim_format]: "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c \<rbrakk> \<Longrightarrow> (next_th s th cs t \<and> cs = c)"proof - fix t c assume vt: "vt (V th cs # s)" and nw: "\<not> waiting (wq (V th cs # s)) t c" and wt: "waiting (wq s) t c" show "next_th s th cs t \<and> cs = c" proof(cases "cs = c") case False with nw wt show ?thesis by (auto simp:cs_waiting_def wq_def Let_def) next case True from nw[folded True] wt[folded True] have "next_th s th cs t" apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits) proof - fix a list assume t_in: "t \<in> set list" and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)" and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \<and> set q = set list) = set list" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] show "distinct list \<and> set list = set list" by auto next show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list" by auto qed with t_ni and t_in show "a = th" by auto next fix a list assume t_in: "t \<in> set list" and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)" and eq_wq: "wq_fun (schs s) cs = a # list" have " set (SOME q. distinct q \<and> set q = set list) = set list" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] show "distinct list \<and> set list = set list" by auto next show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list" by auto qed with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto next fix a list assume eq_wq: "wq_fun (schs s) cs = a # list" from step_back_step[OF vt] show "a = th" proof(cases) assume "holding s th cs" with eq_wq show ?thesis by (unfold s_holding_def wq_def, auto) qed qed with True show ?thesis by simp qedqedlemma step_v_not_wait[consumes 3]: "\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False" by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)lemma step_v_release: "\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"proof - assume vt: "vt (V th cs # s)" and hd: "holding (wq (V th cs # s)) th cs" from step_back_step [OF vt] and hd show "False" proof(cases) assume "holding (wq (V th cs # s)) th cs" and "holding s th cs" thus ?thesis apply (unfold s_holding_def wq_def cs_holding_def) apply (auto simp:Let_def split:list.splits) proof - fix list assume eq_wq[folded wq_def]: "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list" and hd_in: "hd (SOME q. distinct q \<and> set q = set list) \<in> set (SOME q. distinct q \<and> set q = set list)" have "set (SOME q. distinct q \<and> set q = set list) = set list" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq show "distinct list \<and> set list = set list" by auto next show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list" by auto qed moreover have "distinct (hd (SOME q. distinct q \<and> set q = set list) # list)" proof - from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq show ?thesis by auto qed moreover note eq_wq and hd_in ultimately show "False" by auto qed qedqedlemma step_v_get_hold: "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False" apply (unfold cs_holding_def next_th_def wq_def, auto simp:Let_def)proof - fix rest assume vt: "vt (V th cs # s)" and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest" and nrest: "rest \<noteq> []" and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)" have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next fix x assume "distinct x \<and> set x = set rest" hence "set x = set rest" by auto with nrest show "x \<noteq> []" by (case_tac x, auto) qed with ni show "False" by autoqedlemma step_v_release_inv[elim_format]:"\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> c = cs \<and> t = th" apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) proof - fix a list assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" from step_back_step [OF vt] show "a = th" proof(cases) assume "holding s th cs" with eq_wq show ?thesis by (unfold s_holding_def wq_def, auto) qed next fix a list assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" from step_back_step [OF vt] show "a = th" proof(cases) assume "holding s th cs" with eq_wq show ?thesis by (unfold s_holding_def wq_def, auto) qed qedlemma step_v_waiting_mono: "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"proof - fix t c let ?s' = "(V th cs # s)" assume vt: "vt ?s'" and wt: "waiting (wq ?s') t c" show "waiting (wq s) t c" proof(cases "c = cs") case False assume neq_cs: "c \<noteq> cs" hence "waiting (wq ?s') t c = waiting (wq s) t c" by (unfold cs_waiting_def wq_def, auto simp:Let_def) with wt show ?thesis by simp next case True with wt show ?thesis apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) proof - fix a list assume not_in: "t \<notin> set list" and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)" and eq_wq: "wq_fun (schs s) cs = a # list" have "set (SOME q. distinct q \<and> set q = set list) = set list" proof(rule someI2) from wq_distinct [OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] show "distinct list \<and> set list = set list" by auto next fix x assume "distinct x \<and> set x = set list" thus "set x = set list" by auto qed with not_in is_in show "t = a" by auto next fix list assume is_waiting: "waiting (wq (V th cs # s)) t cs" and eq_wq: "wq_fun (schs s) cs = t # list" hence "t \<in> set list" apply (unfold wq_def, auto simp:Let_def cs_waiting_def) proof - assume " t \<in> set (SOME q. distinct q \<and> set q = set list)" moreover have "\<dots> = set list" proof(rule someI2) from wq_distinct [OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] show "distinct list \<and> set list = set list" by auto next fix x assume "distinct x \<and> set x = set list" thus "set x = set list" by auto qed ultimately show "t \<in> set list" by simp qed with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def] show False by auto qed qedqedtext {* (* ddd *) The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed with the happening of @{text "V"}-events:*}lemma step_RAG_v:fixes th::threadassumes vt: "vt (V th cs#s)"shows " RAG (V th cs # s) = RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> {(Cs cs, Th th') |th'. next_th s th cs th'}" apply (insert vt, unfold s_RAG_def) apply (auto split:if_splits list.splits simp:Let_def) apply (auto elim: step_v_waiting_mono step_v_hold_inv step_v_release step_v_wait_inv step_v_get_hold step_v_release_inv) apply (erule_tac step_v_not_wait, auto) donetext {* The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed with the happening of @{text "P"}-events:*}lemma step_RAG_p: "vt (P th cs#s) \<Longrightarrow> RAG (P th cs # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)} else RAG s \<union> {(Th th, Cs cs)})" apply(simp only: s_RAG_def wq_def) apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def) apply(case_tac "csa = cs", auto) apply(fold wq_def) apply(drule_tac step_back_step) apply(ind_cases " step s (P (hd (wq s cs)) cs)") apply(simp add:s_RAG_def wq_def cs_holding_def) apply(auto) donelemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs" by (unfold s_RAG_def, auto)text {* The following lemma shows that @{text "RAG"} is acyclic. The overall structure is by induction on the formation of @{text "vt s"} and then case analysis on event @{text "e"}, where the non-trivial cases for those for @{text "V"} and @{text "P"} events.*}lemma acyclic_RAG: fixes s assumes vt: "vt s" shows "acyclic (RAG s)"using assmsproof(induct) case (vt_cons s e) assume ih: "acyclic (RAG s)" and stp: "step s e" and vt: "vt s" show ?case proof(cases e) case (Create th prio) with ih show ?thesis by (simp add:RAG_create_unchanged) next case (Exit th) with ih show ?thesis by (simp add:RAG_exit_unchanged) next case (V th cs) from V vt stp have vtt: "vt (V th cs#s)" by auto from step_RAG_v [OF this] have eq_de: "RAG (e # s) = RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V) from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset) from step_back_step [OF vtt] have "step s (V th cs)" . thus ?thesis proof(cases) assume "holding s th cs" hence th_in: "th \<in> set (wq s cs)" and eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto then obtain rest where eq_wq: "wq s cs = th#rest" by (cases "wq s cs", auto) show ?thesis proof(cases "rest = []") case False let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}" by (unfold next_th_def, auto) let ?E = "(?A - ?B - ?C)" have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*" proof assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*" hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl) from tranclD [OF this] obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast hence th_d: "(Th ?th', x) \<in> ?A" by simp from RAG_target_th [OF this] obtain cs' where eq_x: "x = Cs cs'" by auto with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp hence wt_th': "waiting s ?th' cs'" unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp hence "cs' = cs" proof(rule waiting_unique [OF vt]) from eq_wq wq_distinct[OF vt, of cs] show "waiting s ?th' cs" apply (unfold s_waiting_def wq_def, auto) proof - assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" and eq_wq: "wq_fun (schs s) cs = th # rest" have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from wq_distinct[OF vt, of cs] and eq_wq show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto next fix x assume "distinct x \<and> set x = set rest" with False show "x \<noteq> []" by auto qed hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)" by auto moreover have "\<dots> = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs] and eq_wq show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed moreover note hd_in ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto next assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest" have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from wq_distinct[OF vt, of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next fix x assume "distinct x \<and> set x = set rest" with False show "x \<noteq> []" by auto qed hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)" by auto moreover have "\<dots> = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed moreover note hd_in ultimately show False by auto qed qed with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp with False show "False" by (auto simp: next_th_def eq_wq) qed with acyclic_insert[symmetric] and ac and eq_de eq_D show ?thesis by auto next case True with eq_wq have eq_D: "?D = {}" by (unfold next_th_def, auto) with eq_de ac show ?thesis by auto qed qed next case (P th cs) from P vt stp have vtt: "vt (P th cs#s)" by auto from step_RAG_p [OF this] P have "RAG (e # s) = (if wq s cs = [] then RAG s \<union> {(Cs cs, Th th)} else RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R") by simp moreover have "acyclic ?R" proof(cases "wq s cs = []") case True hence eq_r: "?R = RAG s \<union> {(Cs cs, Th th)}" by simp have "(Th th, Cs cs) \<notin> (RAG s)\<^sup>*" proof assume "(Th th, Cs cs) \<in> (RAG s)\<^sup>*" hence "(Th th, Cs cs) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) from tranclD2 [OF this] obtain x where "(x, Cs cs) \<in> RAG s" by auto with True show False by (auto simp:s_RAG_def cs_waiting_def) qed with acyclic_insert ih eq_r show ?thesis by auto next case False hence eq_r: "?R = RAG s \<union> {(Th th, Cs cs)}" by simp have "(Cs cs, Th th) \<notin> (RAG s)\<^sup>*" proof assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*" hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) moreover from step_back_step [OF vtt] have "step s (P th cs)" . ultimately show False proof - show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False" by (ind_cases "step s (P th cs)", simp) qed qed with acyclic_insert ih eq_r show ?thesis by auto qed ultimately show ?thesis by simp next case (Set thread prio) with ih thm RAG_set_unchanged show ?thesis by (simp add:RAG_set_unchanged) qed next case vt_nil show "acyclic (RAG ([]::state))" by (auto simp: s_RAG_def cs_waiting_def cs_holding_def wq_def acyclic_def)qedlemma finite_RAG: fixes s assumes vt: "vt s" shows "finite (RAG s)"proof - from vt show ?thesis proof(induct) case (vt_cons s e) assume ih: "finite (RAG s)" and stp: "step s e" and vt: "vt s" show ?case proof(cases e) case (Create th prio) with ih show ?thesis by (simp add:RAG_create_unchanged) next case (Exit th) with ih show ?thesis by (simp add:RAG_exit_unchanged) next case (V th cs) from V vt stp have vtt: "vt (V th cs#s)" by auto from step_RAG_v [OF this] have eq_de: "RAG (e # s) = RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V) moreover from ih have ac: "finite (?A - ?B - ?C)" by simp moreover have "finite ?D" proof - have "?D = {} \<or> (\<exists> a. ?D = {a})" by (unfold next_th_def, auto) thus ?thesis proof assume h: "?D = {}" show ?thesis by (unfold h, simp) next assume "\<exists> a. ?D = {a}" thus ?thesis by (metis finite.simps) qed qed ultimately show ?thesis by simp next case (P th cs) from P vt stp have vtt: "vt (P th cs#s)" by auto from step_RAG_p [OF this] P have "RAG (e # s) = (if wq s cs = [] then RAG s \<union> {(Cs cs, Th th)} else RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R") by simp moreover have "finite ?R" proof(cases "wq s cs = []") case True hence eq_r: "?R = RAG s \<union> {(Cs cs, Th th)}" by simp with True and ih show ?thesis by auto next case False hence "?R = RAG s \<union> {(Th th, Cs cs)}" by simp with False and ih show ?thesis by auto qed ultimately show ?thesis by auto next case (Set thread prio) with ih show ?thesis by (simp add:RAG_set_unchanged) qed next case vt_nil show "finite (RAG ([]::state))" by (auto simp: s_RAG_def cs_waiting_def cs_holding_def wq_def acyclic_def) qedqedtext {* Several useful lemmas *}lemma wf_dep_converse: fixes s assumes vt: "vt s" shows "wf ((RAG s)^-1)"proof(rule finite_acyclic_wf_converse) from finite_RAG [OF vt] show "finite (RAG s)" .next from acyclic_RAG[OF vt] show "acyclic (RAG s)" .qedlemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"by (induct l, auto)lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s" by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)lemma wq_threads: fixes s cs assumes vt: "vt s" and h: "th \<in> set (wq s cs)" shows "th \<in> threads s"proof - from vt and h show ?thesis proof(induct arbitrary: th cs) case (vt_cons s e) assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s" and stp: "step s e" and vt: "vt s" and h: "th \<in> set (wq (e # s) cs)" show ?case proof(cases e) case (Create th' prio) with ih h show ?thesis by (auto simp:wq_def Let_def) next case (Exit th') with stp ih h show ?thesis apply (auto simp:wq_def Let_def) apply (ind_cases "step s (Exit th')") apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def s_RAG_def s_holding_def cs_holding_def) done next case (V th' cs') show ?thesis proof(cases "cs' = cs") case False with h show ?thesis apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def) by (drule_tac ih, simp) next case True from h show ?thesis proof(unfold V wq_def) assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l") show "th \<in> threads (V th' cs' # s)" proof(cases "cs = cs'") case False hence "?l = wq_fun (schs s) cs" by (simp add:Let_def) with th_in have " th \<in> set (wq s cs)" by (fold wq_def, simp) from ih [OF this] show ?thesis by simp next case True show ?thesis proof(cases "wq_fun (schs s) cs'") case Nil with h V show ?thesis apply (auto simp:wq_def Let_def split:if_splits) by (fold wq_def, drule_tac ih, simp) next case (Cons a rest) assume eq_wq: "wq_fun (schs s) cs' = a # rest" with h V show ?thesis apply (auto simp:Let_def wq_def split:if_splits) proof - assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" have "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def] show "distinct rest \<and> set rest = set rest" by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto from ih[OF this[folded wq_def]] show "th \<in> threads s" . next assume th_in: "th \<in> set (wq_fun (schs s) cs)" from ih[OF this[folded wq_def]] show "th \<in> threads s" . qed qed qed qed qed next case (P th' cs') from h stp show ?thesis apply (unfold P wq_def) apply (auto simp:Let_def split:if_splits, fold wq_def) apply (auto intro:ih) apply(ind_cases "step s (P th' cs')") by (unfold runing_def readys_def, auto) next case (Set thread prio) with ih h show ?thesis by (auto simp:wq_def Let_def) qed next case vt_nil thus ?case by (auto simp:wq_def) qedqedlemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s" apply(unfold s_RAG_def cs_waiting_def cs_holding_def) by (auto intro:wq_threads)lemma readys_v_eq: fixes th thread cs rest assumes vt: "vt s" and neq_th: "th \<noteq> thread" and eq_wq: "wq s cs = thread#rest" and not_in: "th \<notin> set rest" shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"proof - from assms show ?thesis apply (auto simp:readys_def) apply(simp add:s_waiting_def[folded wq_def]) apply (erule_tac x = csa in allE) apply (simp add:s_waiting_def wq_def Let_def split:if_splits) apply (case_tac "csa = cs", simp) apply (erule_tac x = cs in allE) apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) apply(auto simp add: wq_def) apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) proof - assume th_nin: "th \<notin> set rest" and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" and eq_wq: "wq_fun (schs s) cs = thread # rest" have "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def] show "distinct rest \<and> set rest = set rest" by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed with th_nin th_in show False by auto qedqedtext {* \noindent The following lemmas shows that: starting from any node in @{text "RAG"}, by chasing out-going edges, it is always possible to reach a node representing a ready thread. In this lemma, it is the @{text "th'"}.*}lemma chain_building: assumes vt: "vt s" shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"proof - from wf_dep_converse [OF vt] have h: "wf ((RAG s)\<inverse>)" . show ?thesis proof(induct rule:wf_induct [OF h]) fix x assume ih [rule_format]: "\<forall>y. (y, x) \<in> (RAG s)\<inverse> \<longrightarrow> y \<in> Domain (RAG s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (y, Th th') \<in> (RAG s)\<^sup>+)" show "x \<in> Domain (RAG s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (RAG s)\<^sup>+)" proof assume x_d: "x \<in> Domain (RAG s)" show "\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (RAG s)\<^sup>+" proof(cases x) case (Th th) from x_d Th obtain cs where x_in: "(Th th, Cs cs) \<in> RAG s" by (auto simp:s_RAG_def) with Th have x_in_r: "(Cs cs, x) \<in> (RAG s)^-1" by simp from th_chasing [OF x_in] obtain th' where "(Cs cs, Th th') \<in> RAG s" by blast hence "Cs cs \<in> Domain (RAG s)" by auto from ih [OF x_in_r this] obtain th' where th'_ready: " th' \<in> readys s" and cs_in: "(Cs cs, Th th') \<in> (RAG s)\<^sup>+" by auto have "(x, Th th') \<in> (RAG s)\<^sup>+" using Th x_in cs_in by auto with th'_ready show ?thesis by auto next case (Cs cs) from x_d Cs obtain th' where th'_d: "(Th th', x) \<in> (RAG s)^-1" by (auto simp:s_RAG_def) show ?thesis proof(cases "th' \<in> readys s") case True from True and th'_d show ?thesis by auto next case False from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto with False have "Th th' \<in> Domain (RAG s)" by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def) from ih [OF th'_d this] obtain th'' where th''_r: "th'' \<in> readys s" and th''_in: "(Th th', Th th'') \<in> (RAG s)\<^sup>+" by auto from th'_d and th''_in have "(x, Th th'') \<in> (RAG s)\<^sup>+" by auto with th''_r show ?thesis by auto qed qed qed qedqedtext {* \noindent The following is just an instance of @{text "chain_building"}.*}lemma th_chain_to_ready: fixes s th assumes vt: "vt s" and th_in: "th \<in> threads s" shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"proof(cases "th \<in> readys s") case True thus ?thesis by autonext case False from False and th_in have "Th th \<in> Domain (RAG s)" by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) from chain_building [rule_format, OF vt this] show ?thesis by autoqedlemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" by (unfold s_waiting_def cs_waiting_def wq_def, auto)lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs" by (unfold s_holding_def wq_def cs_holding_def, simp)lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2" by (unfold s_holding_def cs_holding_def, auto)lemma unique_RAG: "\<lbrakk>vt s; (n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2" apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq) by(auto elim:waiting_unique holding_unique)lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"by (induct rule:trancl_induct, auto)lemma dchain_unique: assumes vt: "vt s" and th1_d: "(n, Th th1) \<in> (RAG s)^+" and th1_r: "th1 \<in> readys s" and th2_d: "(n, Th th2) \<in> (RAG s)^+" and th2_r: "th2 \<in> readys s" shows "th1 = th2"proof - { assume neq: "th1 \<noteq> th2" hence "Th th1 \<noteq> Th th2" by simp from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt] have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto hence "False" proof assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" from trancl_split [OF this] obtain n where dd: "(Th th1, n) \<in> RAG s" by auto then obtain cs where eq_n: "n = Cs cs" by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) from dd eq_n have "th1 \<notin> readys s" by (auto simp:readys_def s_RAG_def wq_def s_waiting_def cs_waiting_def) with th1_r show ?thesis by auto next assume "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" from trancl_split [OF this] obtain n where dd: "(Th th2, n) \<in> RAG s" by auto then obtain cs where eq_n: "n = Cs cs" by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) from dd eq_n have "th2 \<notin> readys s" by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) with th2_r show ?thesis by auto qed } thus ?thesis by autoqedlemma step_holdents_p_add: fixes th cs s assumes vt: "vt (P th cs#s)" and "wq s cs = []" shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"proof - from assms show ?thesis unfolding holdents_test step_RAG_p[OF vt] by (auto)qedlemma step_holdents_p_eq: fixes th cs s assumes vt: "vt (P th cs#s)" and "wq s cs \<noteq> []" shows "holdents (P th cs#s) th = holdents s th"proof - from assms show ?thesis unfolding holdents_test step_RAG_p[OF vt] by autoqedlemma finite_holding: fixes s th cs assumes vt: "vt s" shows "finite (holdents s th)"proof - let ?F = "\<lambda> (x, y). the_cs x" from finite_RAG [OF vt] have "finite (RAG s)" . hence "finite (?F `(RAG s))" by simp moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>" proof - { have h: "\<And> a A f. a \<in> A \<Longrightarrow> f a \<in> f ` A" by auto fix x assume "(Cs x, Th th) \<in> RAG s" hence "?F (Cs x, Th th) \<in> ?F `(RAG s)" by (rule h) moreover have "?F (Cs x, Th th) = x" by simp ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` RAG s" by simp } thus ?thesis by auto qed ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset)qedlemma cntCS_v_dec: fixes s thread cs assumes vtv: "vt (V thread cs#s)" shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"proof - from step_back_step[OF vtv] have cs_in: "cs \<in> holdents s thread" apply (cases, unfold holdents_test s_RAG_def, simp) by (unfold cs_holding_def s_holding_def wq_def, auto) moreover have cs_not_in: "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) apply (unfold holdents_test, unfold step_RAG_v[OF vtv], auto simp:next_th_def) proof - fix rest assume dst: "distinct (rest::thread list)" and ne: "rest \<noteq> []" and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from dst show "distinct rest \<and> set rest = set rest" by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)" by simp moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from dst show "distinct rest \<and> set rest = set rest" by auto next fix x assume " distinct x \<and> set x = set rest" with ne show "x \<noteq> []" by auto qed ultimately show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> RAG s" by auto next fix rest assume dst: "distinct (rest::thread list)" and ne: "rest \<noteq> []" and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from dst show "distinct rest \<and> set rest = set rest" by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)" by simp moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from dst show "distinct rest \<and> set rest = set rest" by auto next fix x assume " distinct x \<and> set x = set rest" with ne show "x \<noteq> []" by auto qed ultimately show "False" by auto qed ultimately have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" by auto moreover have "card \<dots> = Suc (card ((holdents (V thread cs#s) thread) - {cs}))" proof(rule card_insert) from finite_holding [OF vtv] show " finite (holdents (V thread cs # s) thread)" . qed moreover from cs_not_in have "cs \<notin> (holdents (V thread cs#s) thread)" by auto ultimately show ?thesis by (simp add:cntCS_def)qed text {* (* ddd *) \noindent The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} of one particular thread. *} lemma cnp_cnv_cncs: fixes s th assumes vt: "vt s" shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"proof - from vt show ?thesis proof(induct arbitrary:th) case (vt_cons s e) assume vt: "vt s" and ih: "\<And>th. cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)" and stp: "step s e" from stp show ?case proof(cases) case (thread_create thread prio) assume eq_e: "e = Create thread prio" and not_in: "thread \<notin> threads s" show ?thesis proof - { fix cs assume "thread \<in> set (wq s cs)" from wq_threads [OF vt this] have "thread \<in> threads s" . with not_in have "False" by simp } with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}" by (auto simp:readys_def threads.simps s_waiting_def wq_def cs_waiting_def Let_def) from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" unfolding cntCS_def holdents_test by (simp add:RAG_create_unchanged eq_e) { assume "th \<noteq> thread" with eq_readys eq_e have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = (th \<in> readys (s) \<or> th \<notin> threads (s))" by (simp add:threads.simps) with eq_cnp eq_cnv eq_cncs ih not_in have ?thesis by simp } moreover { assume eq_th: "th = thread" with not_in ih have " cntP s th = cntV s th + cntCS s th" by simp moreover from eq_th and eq_readys have "th \<in> readys (e#s)" by simp moreover note eq_cnp eq_cnv eq_cncs ultimately have ?thesis by auto } ultimately show ?thesis by blast qed next case (thread_exit thread) assume eq_e: "e = Exit thread" and is_runing: "thread \<in> runing s" and no_hold: "holdents s thread = {}" from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" unfolding cntCS_def holdents_test by (simp add:RAG_exit_unchanged eq_e) { assume "th \<noteq> thread" with eq_e have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = (th \<in> readys (s) \<or> th \<notin> threads (s))" apply (simp add:threads.simps readys_def) apply (subst s_waiting_def) apply (simp add:Let_def) apply (subst s_waiting_def, simp) done with eq_cnp eq_cnv eq_cncs ih have ?thesis by simp } moreover { assume eq_th: "th = thread" with ih is_runing have " cntP s th = cntV s th + cntCS s th" by (simp add:runing_def) moreover from eq_th eq_e have "th \<notin> threads (e#s)" by simp moreover note eq_cnp eq_cnv eq_cncs ultimately have ?thesis by auto } ultimately show ?thesis by blast next case (thread_P thread cs) assume eq_e: "e = P thread cs" and is_runing: "thread \<in> runing s" and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+" from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto show ?thesis proof - { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast assume neq_th: "th \<noteq> thread" with eq_e have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))" apply (simp add:readys_def s_waiting_def wq_def Let_def) apply (rule_tac hh) apply (intro iffI allI, clarify) apply (erule_tac x = csa in allE, auto) apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) apply (erule_tac x = cs in allE, auto) by (case_tac "(wq_fun (schs s) cs)", auto) moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" apply (simp add:cntCS_def holdents_test) by (unfold step_RAG_p [OF vtp], auto) moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" by (simp add:cntP_def count_def) moreover from eq_e neq_th have "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) moreover from eq_e neq_th have "threads (e#s) = threads s" by simp moreover note ih [of th] ultimately have ?thesis by simp } moreover { assume eq_th: "th = thread" have ?thesis proof - from eq_e eq_th have eq_cnp: "cntP (e # s) th = 1 + (cntP s th)" by (simp add:cntP_def count_def) from eq_e eq_th have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) show ?thesis proof (cases "wq s cs = []") case True with is_runing have "th \<in> readys (e#s)" apply (unfold eq_e wq_def, unfold readys_def s_RAG_def) apply (simp add: wq_def[symmetric] runing_def eq_th s_waiting_def) by (auto simp:readys_def wq_def Let_def s_waiting_def wq_def) moreover have "cntCS (e # s) th = 1 + cntCS s th" proof - have "card {csa. csa = cs \<or> (Cs csa, Th thread) \<in> RAG s} = Suc (card {cs. (Cs cs, Th thread) \<in> RAG s})" (is "card ?L = Suc (card ?R)") proof - have "?L = insert cs ?R" by auto moreover have "card \<dots> = Suc (card (?R - {cs}))" proof(rule card_insert) from finite_holding [OF vt, of thread] show " finite {cs. (Cs cs, Th thread) \<in> RAG s}" by (unfold holdents_test, simp) qed moreover have "?R - {cs} = ?R" proof - have "cs \<notin> ?R" proof assume "cs \<in> {cs. (Cs cs, Th thread) \<in> RAG s}" with no_dep show False by auto qed thus ?thesis by auto qed ultimately show ?thesis by auto qed thus ?thesis apply (unfold eq_e eq_th cntCS_def) apply (simp add: holdents_test) by (unfold step_RAG_p [OF vtp], auto simp:True) qed moreover from is_runing have "th \<in> readys s" by (simp add:runing_def eq_th) moreover note eq_cnp eq_cnv ih [of th] ultimately show ?thesis by auto next case False have eq_wq: "wq (e#s) cs = wq s cs @ [th]" by (unfold eq_th eq_e wq_def, auto simp:Let_def) have "th \<notin> readys (e#s)" proof assume "th \<in> readys (e#s)" hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def) from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" . hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)" by (simp add:s_waiting_def wq_def) moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto ultimately have "th = hd (wq (e#s) cs)" by blast with eq_wq have "th = hd (wq s cs @ [th])" by simp hence "th = hd (wq s cs)" using False by auto with False eq_wq wq_distinct [OF vtp, of cs] show False by (fold eq_e, auto) qed moreover from is_runing have "th \<in> threads (e#s)" by (unfold eq_e, auto simp:runing_def readys_def eq_th) moreover have "cntCS (e # s) th = cntCS s th" apply (unfold cntCS_def holdents_test eq_e step_RAG_p[OF vtp]) by (auto simp:False) moreover note eq_cnp eq_cnv ih[of th] moreover from is_runing have "th \<in> readys s" by (simp add:runing_def eq_th) ultimately show ?thesis by auto qed qed } ultimately show ?thesis by blast qed next case (thread_V thread cs) from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto assume eq_e: "e = V thread cs" and is_runing: "thread \<in> runing s" and hold: "holding s thread cs" from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e) have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto qed show ?thesis proof - { assume eq_th: "th = thread" from eq_th have eq_cnp: "cntP (e # s) th = cntP s th" by (unfold eq_e, simp add:cntP_def count_def) moreover from eq_th have eq_cnv: "cntV (e#s) th = 1 + cntV s th" by (unfold eq_e, simp add:cntV_def count_def) moreover from cntCS_v_dec [OF vtv] have "cntCS (e # s) thread + 1 = cntCS s thread" by (simp add:eq_e) moreover from is_runing have rd_before: "thread \<in> readys s" by (unfold runing_def, simp) moreover have "thread \<in> readys (e # s)" proof - from is_runing have "thread \<in> threads (e#s)" by (unfold eq_e, auto simp:runing_def readys_def) moreover have "\<forall> cs1. \<not> waiting (e#s) thread cs1" proof fix cs1 { assume eq_cs: "cs1 = cs" have "\<not> waiting (e # s) thread cs1" proof - from eq_wq have "thread \<notin> set (wq (e#s) cs1)" apply(unfold eq_e wq_def eq_cs s_holding_def) apply (auto simp:Let_def) proof - assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)" with eq_set have "thread \<in> set rest" by simp with wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq show False by auto qed thus ?thesis by (simp add:wq_def s_waiting_def) qed } moreover { assume neq_cs: "cs1 \<noteq> cs" have "\<not> waiting (e # s) thread cs1" proof - from wq_v_neq [OF neq_cs[symmetric]] have "wq (V thread cs # s) cs1 = wq s cs1" . moreover have "\<not> waiting s thread cs1" proof - from runing_ready and is_runing have "thread \<in> readys s" by auto thus ?thesis by (simp add:readys_def) qed ultimately show ?thesis by (auto simp:wq_def s_waiting_def eq_e) qed } ultimately show "\<not> waiting (e # s) thread cs1" by blast qed ultimately show ?thesis by (simp add:readys_def) qed moreover note eq_th ih ultimately have ?thesis by auto } moreover { assume neq_th: "th \<noteq> thread" from neq_th eq_e have eq_cnp: "cntP (e # s) th = cntP s th" by (simp add:cntP_def count_def) from neq_th eq_e have eq_cnv: "cntV (e # s) th = cntV s th" by (simp add:cntV_def count_def) have ?thesis proof(cases "th \<in> set rest") case False have "(th \<in> readys (e # s)) = (th \<in> readys s)" apply (insert step_back_vt[OF vtv]) by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) moreover have "cntCS (e#s) th = cntCS s th" apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) proof - have "{csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} = {cs. (Cs cs, Th th) \<in> RAG s}" proof - from False eq_wq have " next_th s thread cs th \<Longrightarrow> (Cs cs, Th th) \<in> RAG s" apply (unfold next_th_def, auto) proof - assume ne: "rest \<noteq> []" and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" and eq_wq: "wq s cs = thread # rest" from eq_set ni have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest) " by simp moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next fix x assume "distinct x \<and> set x = set rest" with ne show "x \<noteq> []" by auto qed ultimately show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> RAG s" by auto qed thus ?thesis by auto qed thus "card {csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} = card {cs. (Cs cs, Th th) \<in> RAG s}" by simp qed moreover note ih eq_cnp eq_cnv eq_threads ultimately show ?thesis by auto next case True assume th_in: "th \<in> set rest" show ?thesis proof(cases "next_th s thread cs th") case False with eq_wq and th_in have neq_hd: "th \<noteq> hd (SOME q. distinct q \<and> set q = set rest)" (is "th \<noteq> hd ?rest") by (auto simp:next_th_def) have "(th \<in> readys (e # s)) = (th \<in> readys s)" proof - from eq_wq and th_in have "\<not> th \<in> readys s" apply (auto simp:readys_def s_waiting_def) apply (rule_tac x = cs in exI, auto) by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def) moreover from eq_wq and th_in and neq_hd have "\<not> (th \<in> readys (e # s))" apply (auto simp:readys_def s_waiting_def eq_e wq_def Let_def split:list.splits) by (rule_tac x = cs in exI, auto simp:eq_set) ultimately show ?thesis by auto qed moreover have "cntCS (e#s) th = cntCS s th" proof - from eq_wq and th_in and neq_hd have "(holdents (e # s) th) = (holdents s th)" apply (unfold eq_e step_RAG_v[OF vtv], auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def Let_def cs_holding_def) by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) thus ?thesis by (simp add:cntCS_def) qed moreover note ih eq_cnp eq_cnv eq_threads ultimately show ?thesis by auto next case True let ?rest = " (SOME q. distinct q \<and> set q = set rest)" let ?t = "hd ?rest" from True eq_wq th_in neq_th have "th \<in> readys (e # s)" apply (auto simp:eq_e readys_def s_waiting_def wq_def Let_def next_th_def) proof - assume eq_wq: "wq_fun (schs s) cs = thread # rest" and t_in: "?t \<in> set rest" show "?t \<in> threads s" proof(rule wq_threads[OF step_back_vt[OF vtv]]) from eq_wq and t_in show "?t \<in> set (wq s cs)" by (auto simp:wq_def) qed next fix csa assume eq_wq: "wq_fun (schs s) cs = thread # rest" and t_in: "?t \<in> set rest" and neq_cs: "csa \<noteq> cs" and t_in': "?t \<in> set (wq_fun (schs s) csa)" show "?t = hd (wq_fun (schs s) csa)" proof - { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)" from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq[folded wq_def] and t_in eq_wq have "?t \<noteq> thread" by auto with eq_wq and t_in have w1: "waiting s ?t cs" by (auto simp:s_waiting_def wq_def) from t_in' neq_hd' have w2: "waiting s ?t csa" by (auto simp:s_waiting_def wq_def) from waiting_unique[OF step_back_vt[OF vtv] w1 w2] and neq_cs have "False" by auto } thus ?thesis by auto qed qed moreover have "cntP s th = cntV s th + cntCS s th + 1" proof - have "th \<notin> readys s" proof - from True eq_wq neq_th th_in show ?thesis apply (unfold readys_def s_waiting_def, auto) by (rule_tac x = cs in exI, auto simp add: wq_def) qed moreover have "th \<in> threads s" proof - from th_in eq_wq have "th \<in> set (wq s cs)" by simp from wq_threads [OF step_back_vt[OF vtv] this] show ?thesis . qed ultimately show ?thesis using ih by auto qed moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" apply (unfold cntCS_def holdents_test eq_e step_RAG_v[OF vtv], auto) proof - show "card {csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs} = Suc (card {cs. (Cs cs, Th th) \<in> RAG s})" (is "card ?A = Suc (card ?B)") proof - have "?A = insert cs ?B" by auto hence "card ?A = card (insert cs ?B)" by simp also have "\<dots> = Suc (card ?B)" proof(rule card_insert_disjoint) have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)" apply (auto simp:image_def) by (rule_tac x = "(Cs x, Th th)" in bexI, auto) with finite_RAG[OF step_back_vt[OF vtv]] show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset) next show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}" proof assume "cs \<in> {cs. (Cs cs, Th th) \<in> RAG s}" hence "(Cs cs, Th th) \<in> RAG s" by simp with True neq_th eq_wq show False by (auto simp:next_th_def s_RAG_def cs_holding_def) qed qed finally show ?thesis . qed qed moreover note eq_cnp eq_cnv ultimately show ?thesis by simp qed qed } ultimately show ?thesis by blast qed next case (thread_set thread prio) assume eq_e: "e = Set thread prio" and is_runing: "thread \<in> runing s" show ?thesis proof - from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" unfolding cntCS_def holdents_test by (simp add:RAG_set_unchanged eq_e) from eq_e have eq_readys: "readys (e#s) = readys s" by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, auto simp:Let_def) { assume "th \<noteq> thread" with eq_readys eq_e have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) = (th \<in> readys (s) \<or> th \<notin> threads (s))" by (simp add:threads.simps) with eq_cnp eq_cnv eq_cncs ih is_runing have ?thesis by simp } moreover { assume eq_th: "th = thread" with is_runing ih have " cntP s th = cntV s th + cntCS s th" by (unfold runing_def, auto) moreover from eq_th and eq_readys is_runing have "th \<in> readys (e#s)" by (simp add:runing_def) moreover note eq_cnp eq_cnv eq_cncs ultimately have ?thesis by auto } ultimately show ?thesis by blast qed qed next case vt_nil show ?case by (unfold cntP_def cntV_def cntCS_def, auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) qedqedlemma not_thread_cncs: fixes th s assumes vt: "vt s" and not_in: "th \<notin> threads s" shows "cntCS s th = 0"proof - from vt not_in show ?thesis proof(induct arbitrary:th) case (vt_cons s e th) assume vt: "vt s" and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0" and stp: "step s e" and not_in: "th \<notin> threads (e # s)" from stp show ?case proof(cases) case (thread_create thread prio) assume eq_e: "e = Create thread prio" and not_in': "thread \<notin> threads s" have "cntCS (e # s) th = cntCS s th" apply (unfold eq_e cntCS_def holdents_test) by (simp add:RAG_create_unchanged) moreover have "th \<notin> threads s" proof - from not_in eq_e show ?thesis by simp qed moreover note ih ultimately show ?thesis by auto next case (thread_exit thread) assume eq_e: "e = Exit thread" and nh: "holdents s thread = {}" have eq_cns: "cntCS (e # s) th = cntCS s th" apply (unfold eq_e cntCS_def holdents_test) by (simp add:RAG_exit_unchanged) show ?thesis proof(cases "th = thread") case True have "cntCS s th = 0" by (unfold cntCS_def, auto simp:nh True) with eq_cns show ?thesis by simp next case False with not_in and eq_e have "th \<notin> threads s" by simp from ih[OF this] and eq_cns show ?thesis by simp qed next case (thread_P thread cs) assume eq_e: "e = P thread cs" and is_runing: "thread \<in> runing s" from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto have neq_th: "th \<noteq> thread" proof - from not_in eq_e have "th \<notin> threads s" by simp moreover from is_runing have "thread \<in> threads s" by (simp add:runing_def readys_def) ultimately show ?thesis by auto qed hence "cntCS (e # s) th = cntCS s th " apply (unfold cntCS_def holdents_test eq_e) by (unfold step_RAG_p[OF vtp], auto) moreover have "cntCS s th = 0" proof(rule ih) from not_in eq_e show "th \<notin> threads s" by simp qed ultimately show ?thesis by simp next case (thread_V thread cs) assume eq_e: "e = V thread cs" and is_runing: "thread \<in> runing s" and hold: "holding s thread cs" have neq_th: "th \<noteq> thread" proof - from not_in eq_e have "th \<notin> threads s" by simp moreover from is_runing have "thread \<in> threads s" by (simp add:runing_def readys_def) ultimately show ?thesis by auto qed from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) from not_in eq_e eq_wq have "\<not> next_th s thread cs th" apply (auto simp:next_th_def) proof - assume ne: "rest \<noteq> []" and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s") have "?t \<in> set rest" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next fix x assume "distinct x \<and> set x = set rest" with ne show "hd x \<in> set rest" by (cases x, auto) qed with eq_wq have "?t \<in> set (wq s cs)" by simp from wq_threads[OF step_back_vt[OF vtv], OF this] and ni show False by auto qed moreover note neq_th eq_wq ultimately have "cntCS (e # s) th = cntCS s th" by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) moreover have "cntCS s th = 0" proof(rule ih) from not_in eq_e show "th \<notin> threads s" by simp qed ultimately show ?thesis by simp next case (thread_set thread prio) print_facts assume eq_e: "e = Set thread prio" and is_runing: "thread \<in> runing s" from not_in and eq_e have "th \<notin> threads s" by auto from ih [OF this] and eq_e show ?thesis apply (unfold eq_e cntCS_def holdents_test) by (simp add:RAG_set_unchanged) qed next case vt_nil show ?case by (unfold cntCS_def, auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) qedqedlemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" by (auto simp:s_waiting_def cs_waiting_def wq_def)lemma dm_RAG_threads: fixes th s assumes vt: "vt s" and in_dom: "(Th th) \<in> Domain (RAG s)" shows "th \<in> threads s"proof - from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto ultimately have "(Th th, Cs cs) \<in> RAG s" by simp hence "th \<in> set (wq s cs)" by (unfold s_RAG_def, auto simp:cs_waiting_def) from wq_threads [OF vt this] show ?thesis .qedlemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"unfolding cp_def wq_defapply(induct s rule: schs.induct)thm cpreced_initialapply(simp add: Let_def cpreced_initial)apply(simp add: Let_def)apply(simp add: Let_def)apply(simp add: Let_def)apply(subst (2) schs.simps)apply(simp add: Let_def)apply(subst (2) schs.simps)apply(simp add: Let_def)done(* FIXME: NOT NEEDED *)lemma runing_unique: fixes th1 th2 s assumes vt: "vt s" and runing_1: "th1 \<in> runing s" and runing_2: "th2 \<in> runing s" shows "th1 = th2"proof - from runing_1 and runing_2 have "cp s th1 = cp s th2" unfolding runing_def apply(simp) done hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) = Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))" (is "Max (?f ` ?A) = Max (?f ` ?B)") thm cp_def image_Collect unfolding cp_eq_cpreced unfolding cpreced_def . obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)" thm Max_in proof - have h1: "finite (?f ` ?A)" proof - have "finite ?A" proof - have "finite (dependants (wq s) th1)" proof- have "finite {th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+}" proof - let ?F = "\<lambda> (x, y). the_th x" have "{th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)" apply (auto simp:image_def) by (rule_tac x = "(Th x, Th th1)" in bexI, auto) moreover have "finite \<dots>" proof - from finite_RAG[OF vt] have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) thus ?thesis by auto qed ultimately show ?thesis by (auto intro:finite_subset) qed thus ?thesis by (simp add:cs_dependants_def) qed thus ?thesis by simp qed thus ?thesis by auto qed moreover have h2: "(?f ` ?A) \<noteq> {}" proof - have "?A \<noteq> {}" by simp thus ?thesis by simp qed thm Max_in from Max_in [OF h1 h2] have "Max (?f ` ?A) \<in> (?f ` ?A)" . thus ?thesis thm cpreced_def unfolding cpreced_def[symmetric] unfolding cp_eq_cpreced[symmetric] unfolding cpreced_def using that[intro] by (auto) qed obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)" proof - have h1: "finite (?f ` ?B)" proof - have "finite ?B" proof - have "finite (dependants (wq s) th2)" proof- have "finite {th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+}" proof - let ?F = "\<lambda> (x, y). the_th x" have "{th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)" apply (auto simp:image_def) by (rule_tac x = "(Th x, Th th2)" in bexI, auto) moreover have "finite \<dots>" proof - from finite_RAG[OF vt] have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) thus ?thesis by auto qed ultimately show ?thesis by (auto intro:finite_subset) qed thus ?thesis by (simp add:cs_dependants_def) qed thus ?thesis by simp qed thus ?thesis by auto qed moreover have h2: "(?f ` ?B) \<noteq> {}" proof - have "?B \<noteq> {}" by simp thus ?thesis by simp qed from Max_in [OF h1 h2] have "Max (?f ` ?B) \<in> (?f ` ?B)" . thus ?thesis by (auto intro:that) qed from eq_f_th1 eq_f_th2 eq_max have eq_preced: "preced th1' s = preced th2' s" by auto hence eq_th12: "th1' = th2'" proof (rule preced_unique) from th1_in have "th1' = th1 \<or> (th1' \<in> dependants (wq s) th1)" by simp thus "th1' \<in> threads s" proof assume "th1' \<in> dependants (wq s) th1" hence "(Th th1') \<in> Domain ((RAG s)^+)" apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain) from dm_RAG_threads[OF vt this] show ?thesis . next assume "th1' = th1" with runing_1 show ?thesis by (unfold runing_def readys_def, auto) qed next from th2_in have "th2' = th2 \<or> (th2' \<in> dependants (wq s) th2)" by simp thus "th2' \<in> threads s" proof assume "th2' \<in> dependants (wq s) th2" hence "(Th th2') \<in> Domain ((RAG s)^+)" apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain) from dm_RAG_threads[OF vt this] show ?thesis . next assume "th2' = th2" with runing_2 show ?thesis by (unfold runing_def readys_def, auto) qed qed from th1_in have "th1' = th1 \<or> th1' \<in> dependants (wq s) th1" by simp thus ?thesis proof assume eq_th': "th1' = th1" from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp thus ?thesis proof assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp next assume "th2' \<in> dependants (wq s) th2" with eq_th12 eq_th' have "th1 \<in> dependants (wq s) th2" by simp hence "(Th th1, Th th2) \<in> (RAG s)^+" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) hence "Th th1 \<in> Domain ((RAG s)^+)" apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "Th th1 \<in> Domain (RAG s)" by (simp add:trancl_domain) then obtain n where d: "(Th th1, n) \<in> RAG s" by (auto simp:Domain_def) from RAG_target_th [OF this] obtain cs' where "n = Cs cs'" by auto with d have "(Th th1, Cs cs') \<in> RAG s" by simp with runing_1 have "False" apply (unfold runing_def readys_def s_RAG_def) by (auto simp:eq_waiting) thus ?thesis by simp qed next assume th1'_in: "th1' \<in> dependants (wq s) th1" from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp thus ?thesis proof assume "th2' = th2" with th1'_in eq_th12 have "th2 \<in> dependants (wq s) th1" by simp hence "(Th th2, Th th1) \<in> (RAG s)^+" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) hence "Th th2 \<in> Domain ((RAG s)^+)" apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) by (auto simp:Domain_def) hence "Th th2 \<in> Domain (RAG s)" by (simp add:trancl_domain) then obtain n where d: "(Th th2, n) \<in> RAG s" by (auto simp:Domain_def) from RAG_target_th [OF this] obtain cs' where "n = Cs cs'" by auto with d have "(Th th2, Cs cs') \<in> RAG s" by simp with runing_2 have "False" apply (unfold runing_def readys_def s_RAG_def) by (auto simp:eq_waiting) thus ?thesis by simp next assume "th2' \<in> dependants (wq s) th2" with eq_th12 have "th1' \<in> dependants (wq s) th2" by simp hence h1: "(Th th1', Th th2) \<in> (RAG s)^+" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) show ?thesis proof(rule dchain_unique[OF vt h1 _ h2, symmetric]) from runing_1 show "th1 \<in> readys s" by (simp add:runing_def) from runing_2 show "th2 \<in> readys s" by (simp add:runing_def) qed qed qedqedlemma "vt s \<Longrightarrow> card (runing s) \<le> 1"apply(subgoal_tac "finite (runing s)")prefer 2apply (metis finite_nat_set_iff_bounded lessI runing_unique)apply(rule ccontr)apply(simp)apply(case_tac "Suc (Suc 0) \<le> card (runing s)")apply(subst (asm) card_le_Suc_iff)apply(simp)apply(auto)[1]apply (metis insertCI runing_unique)apply(auto) donelemma create_pre: assumes stp: "step s e" and not_in: "th \<notin> threads s" and is_in: "th \<in> threads (e#s)" obtains prio where "e = Create th prio"proof - from assms show ?thesis proof(cases) case (thread_create thread prio) with is_in not_in have "e = Create th prio" by simp from that[OF this] show ?thesis . next case (thread_exit thread) with assms show ?thesis by (auto intro!:that) next case (thread_P thread) with assms show ?thesis by (auto intro!:that) next case (thread_V thread) with assms show ?thesis by (auto intro!:that) next case (thread_set thread) with assms show ?thesis by (auto intro!:that) qedqedlemma length_down_to_in: assumes le_ij: "i \<le> j" and le_js: "j \<le> length s" shows "length (down_to j i s) = j - i"proof - have "length (down_to j i s) = length (from_to i j (rev s))" by (unfold down_to_def, auto) also have "\<dots> = j - i" proof(rule length_from_to_in[OF le_ij]) from le_js show "j \<le> length (rev s)" by simp qed finally show ?thesis .qedlemma moment_head: assumes le_it: "Suc i \<le> length t" obtains e where "moment (Suc i) t = e#moment i t"proof - have "i \<le> Suc i" by simp from length_down_to_in [OF this le_it] have "length (down_to (Suc i) i t) = 1" by auto then obtain e where "down_to (Suc i) i t = [e]" apply (cases "(down_to (Suc i) i t)") by auto moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" by (rule down_to_conc[symmetric], auto) ultimately have eq_me: "moment (Suc i) t = e#(moment i t)" by (auto simp:down_to_moment) from that [OF this] show ?thesis .qedlemma cnp_cnv_eq: fixes th s assumes "vt s" and "th \<notin> threads s" shows "cntP s th = cntV s th" by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)lemma eq_RAG: "RAG (wq s) = RAG s"by (unfold cs_RAG_def s_RAG_def, auto)lemma count_eq_dependants: assumes vt: "vt s" and eq_pv: "cntP s th = cntV s th" shows "dependants (wq s) th = {}"proof - from cnp_cnv_cncs[OF vt] and eq_pv have "cntCS s th = 0" by (auto split:if_splits) moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}" proof - from finite_holding[OF vt, of th] show ?thesis by (simp add:holdents_test) qed ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}" by (unfold cntCS_def holdents_test cs_dependants_def, auto) show ?thesis proof(unfold cs_dependants_def) { assume "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" then obtain th' where "(Th th', Th th) \<in> (RAG (wq s))\<^sup>+" by auto hence "False" proof(cases) assume "(Th th', Th th) \<in> RAG (wq s)" thus "False" by (auto simp:cs_RAG_def) next fix c assume "(c, Th th) \<in> RAG (wq s)" with h and eq_RAG show "False" by (cases c, auto simp:cs_RAG_def) qed } thus "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} = {}" by auto qedqedlemma dependants_threads: fixes s th assumes vt: "vt s" shows "dependants (wq s) th \<subseteq> threads s"proof { fix th th' assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (RAG (wq s))\<^sup>+}" have "Th th \<in> Domain (RAG s)" proof - from h obtain th' where "(Th th, Th th') \<in> (RAG (wq s))\<^sup>+" by auto hence "(Th th) \<in> Domain ( (RAG (wq s))\<^sup>+)" by (auto simp:Domain_def) with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp thus ?thesis using eq_RAG by simp qed from dm_RAG_threads[OF vt this] have "th \<in> threads s" . } note hh = this fix th1 assume "th1 \<in> dependants (wq s) th" hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (RAG (wq s))\<^sup>+}" by (unfold cs_dependants_def, simp) from hh [OF this] show "th1 \<in> threads s" .qedlemma finite_threads: assumes vt: "vt s" shows "finite (threads s)"using vtby (induct) (auto elim: step.cases)lemma Max_f_mono: assumes seq: "A \<subseteq> B" and np: "A \<noteq> {}" and fnt: "finite B" shows "Max (f ` A) \<le> Max (f ` B)"proof(rule Max_mono) from seq show "f ` A \<subseteq> f ` B" by autonext from np show "f ` A \<noteq> {}" by autonext from fnt and seq show "finite (f ` B)" by autoqedlemma cp_le: assumes vt: "vt s" and th_in: "th \<in> threads s" shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+})) \<le> Max ((\<lambda>th. preced th s) ` threads s)" (is "Max (?f ` ?A) \<le> Max (?f ` ?B)") proof(rule Max_f_mono) show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp next from finite_threads [OF vt] show "finite (threads s)" . next from th_in show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s" apply (auto simp:Domain_def) apply (rule_tac dm_RAG_threads[OF vt]) apply (unfold trancl_domain [of "RAG s", symmetric]) by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) qedqedlemma le_cp: assumes vt: "vt s" shows "preced th s \<le> cp s th"proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) show "Prc (priority th s) (last_set th s) \<le> Max (insert (Prc (priority th s) (last_set th s)) ((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))" (is "?l \<le> Max (insert ?l ?A)") proof(cases "?A = {}") case False have "finite ?A" (is "finite (?f ` ?B)") proof - have "finite ?B" proof- have "finite {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}" proof - let ?F = "\<lambda> (x, y). the_th x" have "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)" apply (auto simp:image_def) by (rule_tac x = "(Th x, Th th)" in bexI, auto) moreover have "finite \<dots>" proof - from finite_RAG[OF vt] have "finite (RAG s)" . hence "finite ((RAG (wq s))\<^sup>+)" apply (unfold finite_trancl) by (auto simp: s_RAG_def cs_RAG_def wq_def) thus ?thesis by auto qed ultimately show ?thesis by (auto intro:finite_subset) qed thus ?thesis by (simp add:cs_dependants_def) qed thus ?thesis by simp qed from Max_insert [OF this False, of ?l] show ?thesis by auto next case True thus ?thesis by auto qedqedlemma max_cp_eq: assumes vt: "vt s" shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)" (is "?l = ?r")proof(cases "threads s = {}") case True thus ?thesis by autonext case False have "?l \<in> ((cp s) ` threads s)" proof(rule Max_in) from finite_threads[OF vt] show "finite (cp s ` threads s)" by auto next from False show "cp s ` threads s \<noteq> {}" by auto qed then obtain th where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto have "\<dots> \<le> ?r" by (rule cp_le[OF vt th_in]) moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th") proof - have "?r \<in> (?f ` ?A)" proof(rule Max_in) from finite_threads[OF vt] show " finite ((\<lambda>th. preced th s) ` threads s)" by auto next from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto qed then obtain th' where th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto from le_cp [OF vt, of th'] eq_r have "?r \<le> cp s th'" by auto moreover have "\<dots> \<le> cp s th" proof(fold eq_l) show " cp s th' \<le> Max (cp s ` threads s)" proof(rule Max_ge) from th_in' show "cp s th' \<in> cp s ` threads s" by auto next from finite_threads[OF vt] show "finite (cp s ` threads s)" by auto qed qed ultimately show ?thesis by auto qed ultimately show ?thesis using eq_l by autoqedlemma max_cp_readys_threads_pre: assumes vt: "vt s" and np: "threads s \<noteq> {}" shows "Max (cp s ` readys s) = Max (cp s ` threads s)"proof(unfold max_cp_eq[OF vt]) show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)" proof - let ?p = "Max ((\<lambda>th. preced th s) ` threads s)" let ?f = "(\<lambda>th. preced th s)" have "?p \<in> ((\<lambda>th. preced th s) ` threads s)" proof(rule Max_in) from finite_threads[OF vt] show "finite (?f ` threads s)" by simp next from np show "?f ` threads s \<noteq> {}" by simp qed then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s" by (auto simp:Image_def) from th_chain_to_ready [OF vt tm_in] have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" . thus ?thesis proof assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+ " then obtain th' where th'_in: "th' \<in> readys s" and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto have "cp s th' = ?f tm" proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) from dependants_threads[OF vt] finite_threads[OF vt] show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))" by (auto intro:finite_subset) next fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')" from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" . moreover have "p \<le> \<dots>" proof(rule Max_ge) from finite_threads[OF vt] show "finite ((\<lambda>th. preced th s) ` threads s)" by simp next from p_in and th'_in and dependants_threads[OF vt, of th'] show "p \<in> (\<lambda>th. preced th s) ` threads s" by (auto simp:readys_def) qed ultimately show "p \<le> preced tm s" by auto next show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')" proof - from tm_chain have "tm \<in> dependants (wq s) th'" by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto) thus ?thesis by auto qed qed with tm_max have h: "cp s th' = Max ((\<lambda>th. preced th s) ` threads s)" by simp show ?thesis proof (fold h, rule Max_eqI) fix q assume "q \<in> cp s ` readys s" then obtain th1 where th1_in: "th1 \<in> readys s" and eq_q: "q = cp s th1" by auto show "q \<le> cp s th'" apply (unfold h eq_q) apply (unfold cp_eq_cpreced cpreced_def) apply (rule Max_mono) proof - from dependants_threads [OF vt, of th1] th1_in show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq> (\<lambda>th. preced th s) ` threads s" by (auto simp:readys_def) next show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp next from finite_threads[OF vt] show " finite ((\<lambda>th. preced th s) ` threads s)" by simp qed next from finite_threads[OF vt] show "finite (cp s ` readys s)" by (auto simp:readys_def) next from th'_in show "cp s th' \<in> cp s ` readys s" by simp qed next assume tm_ready: "tm \<in> readys s" show ?thesis proof(fold tm_max) have cp_eq_p: "cp s tm = preced tm s" proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) fix y assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)" show "y \<le> preced tm s" proof - { fix y' assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)" have "y' \<le> preced tm s" proof(unfold tm_max, rule Max_ge) from hy' dependants_threads[OF vt, of tm] show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto next from finite_threads[OF vt] show "finite ((\<lambda>th. preced th s) ` threads s)" by simp qed } with hy show ?thesis by auto qed next from dependants_threads[OF vt, of tm] finite_threads[OF vt] show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))" by (auto intro:finite_subset) next show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)" by simp qed moreover have "Max (cp s ` readys s) = cp s tm" proof(rule Max_eqI) from tm_ready show "cp s tm \<in> cp s ` readys s" by simp next from finite_threads[OF vt] show "finite (cp s ` readys s)" by (auto simp:readys_def) next fix y assume "y \<in> cp s ` readys s" then obtain th1 where th1_readys: "th1 \<in> readys s" and h: "y = cp s th1" by auto show "y \<le> cp s tm" apply(unfold cp_eq_p h) apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) proof - from finite_threads[OF vt] show "finite ((\<lambda>th. preced th s) ` threads s)" by simp next show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp next from dependants_threads[OF vt, of th1] th1_readys show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq> (\<lambda>th. preced th s) ` threads s" by (auto simp:readys_def) qed qed ultimately show " Max (cp s ` readys s) = preced tm s" by simp qed qed qedqedtext {* (* ccc *) \noindent Since the current precedence of the threads in ready queue will always be boosted, there must be one inside it has the maximum precedence of the whole system. *}lemma max_cp_readys_threads: assumes vt: "vt s" shows "Max (cp s ` readys s) = Max (cp s ` threads s)"proof(cases "threads s = {}") case True thus ?thesis by (auto simp:readys_def)next case False show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])qedlemma eq_holding: "holding (wq s) th cs = holding s th cs" apply (unfold s_holding_def cs_holding_def wq_def, simp) donelemma f_image_eq: assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a" shows "f ` A = g ` A"proof show "f ` A \<subseteq> g ` A" by(rule image_subsetI, auto intro:h)next show "g ` A \<subseteq> f ` A" by (rule image_subsetI, auto intro:h[symmetric])qeddefinition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"lemma detached_test: shows "detached s th = (Th th \<notin> Field (RAG s))"apply(simp add: detached_def Field_def)apply(simp add: s_RAG_def)apply(simp add: s_holding_abv s_waiting_abv)apply(simp add: Domain_iff Range_iff)apply(simp add: wq_def)apply(auto)donelemma detached_intro: fixes s th assumes vt: "vt s" and eq_pv: "cntP s th = cntV s th" shows "detached s th"proof - from cnp_cnv_cncs[OF vt] have eq_cnt: "cntP s th = cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . hence cncs_zero: "cntCS s th = 0" by (auto simp:eq_pv split:if_splits) with eq_cnt have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:eq_pv) thus ?thesis proof assume "th \<notin> threads s" with range_in[OF vt] dm_RAG_threads[OF vt] show ?thesis by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) next assume "th \<in> readys s" moreover have "Th th \<notin> Range (RAG s)" proof - from card_0_eq [OF finite_holding [OF vt]] and cncs_zero have "holdents s th = {}" by (simp add:cntCS_def) thus ?thesis apply(auto simp:holdents_test) apply(case_tac a) apply(auto simp:holdents_test s_RAG_def) done qed ultimately show ?thesis by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def readys_def) qedqedlemma detached_elim: fixes s th assumes vt: "vt s" and dtc: "detached s th" shows "cntP s th = cntV s th"proof - from cnp_cnv_cncs[OF vt] have eq_pv: " cntP s th = cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . have cncs_z: "cntCS s th = 0" proof - from dtc have "holdents s th = {}" unfolding detached_def holdents_test s_RAG_def by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) thus ?thesis by (auto simp:cntCS_def) qed show ?thesis proof(cases "th \<in> threads s") case True with dtc have "th \<in> readys s" by (unfold readys_def detached_def Field_def Domain_def Range_def, auto simp:eq_waiting s_RAG_def) with cncs_z and eq_pv show ?thesis by simp next case False with cncs_z and eq_pv show ?thesis by simp qedqedlemma detached_eq: fixes s th assumes vt: "vt s" shows "(detached s th) = (cntP s th = cntV s th)" by (insert vt, auto intro:detached_intro detached_elim)text {* The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived from the concise and miniature model of PIP given in PrioGDef.thy.*}end