theory CpsGimports PIPDefs beginlemma 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 autoqed(* I am going to use this file as a start point to retrofiting PIPBasics.thy, which is originally called CpsG.ghy *)locale valid_trace = fixes s assumes vt : "vt s"locale valid_trace_e = valid_trace + fixes e assumes vt_e: "vt (e#s)"beginlemma pip_e: "PIP s e" using vt_e by (cases, simp) endlocale valid_trace_create = valid_trace_e + fixes th prio assumes is_create: "e = Create th prio"locale valid_trace_exit = valid_trace_e + fixes th assumes is_exit: "e = Exit th"locale valid_trace_p = valid_trace_e + fixes th cs assumes is_p: "e = P th cs"locale valid_trace_v = valid_trace_e + fixes th cs assumes is_v: "e = V th cs"begin definition "rest = tl (wq s cs)" definition "wq' = (SOME q. distinct q \<and> set q = set rest)"endlocale valid_trace_v_n = valid_trace_v + assumes rest_nnl: "rest \<noteq> []"locale valid_trace_v_e = valid_trace_v + assumes rest_nil: "rest = []"locale valid_trace_set= valid_trace_e + fixes th prio assumes is_set: "e = Set th prio"context valid_tracebeginlemma ind [consumes 0, case_names Nil Cons, induct type]: assumes "PP []" and "(\<And>s e. valid_trace_e s e \<Longrightarrow> PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))" shows "PP s"proof(induct rule:vt.induct[OF vt, case_names Init Step]) case Init from assms(1) show ?case .next case (Step s e) show ?case proof(rule assms(2)) show "valid_trace_e s e" using Step by (unfold_locales, auto) next show "PP s" using Step by simp next show "PIP s e" using Step by simp qedqedendlemma 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 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 [simp]: "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 runing_head: assumes "th \<in> runing s" and "th \<in> set (wq_fun (schs s) cs)" shows "th = hd (wq_fun (schs s) cs)" using assms by (simp add:runing_def readys_def s_waiting_def wq_def)context valid_tracebeginlemma runing_wqE: assumes "th \<in> runing s" and "th \<in> set (wq s cs)" obtains rest where "wq s cs = th#rest"proof - from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest" by (meson list.set_cases) have "th' = th" proof(rule ccontr) assume "th' \<noteq> th" hence "th \<noteq> hd (wq s cs)" using eq_wq by auto with assms(2) have "waiting s th cs" by (unfold s_waiting_def, fold wq_def, auto) with assms show False by (unfold runing_def readys_def, auto) qed with eq_wq that show ?thesis by metisqedendcontext valid_trace_pbeginlemma wq_neq_simp [simp]: assumes "cs' \<noteq> cs" shows "wq (e#s) cs' = wq s cs'" using assms unfolding is_p wq_def by (auto simp:Let_def)lemma runing_th_s: shows "th \<in> runing s"proof - from pip_e[unfolded is_p] show ?thesis by (cases, simp)qedlemma th_not_waiting: "\<not> waiting s th c"proof - have "th \<in> readys s" using runing_ready runing_th_s by blast thus ?thesis by (unfold readys_def, auto)qedlemma waiting_neq_th: assumes "waiting s t c" shows "t \<noteq> th" using assms using th_not_waiting by blast lemma th_not_in_wq: shows "th \<notin> set (wq s cs)"proof assume otherwise: "th \<in> set (wq s cs)" from runing_wqE[OF runing_th_s this] obtain rest where eq_wq: "wq s cs = th#rest" by blast with otherwise have "holding s th cs" by (unfold s_holding_def, fold wq_def, simp) hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s" by (unfold s_RAG_def, fold holding_eq, auto) from pip_e[unfolded is_p] show False proof(cases) case (thread_P) with cs_th_RAG show ?thesis by auto qedqedlemma wq_es_cs: "wq (e#s) cs = wq s cs @ [th]" by (unfold is_p wq_def, auto simp:Let_def)lemma wq_distinct_kept: assumes "distinct (wq s cs')" shows "distinct (wq (e#s) cs')"proof(cases "cs' = cs") case True show ?thesis using True assms th_not_in_wq by (unfold True wq_es_cs, auto)qed (insert assms, simp)endcontext valid_trace_vbeginlemma wq_neq_simp [simp]: assumes "cs' \<noteq> cs" shows "wq (e#s) cs' = wq s cs'" using assms unfolding is_v wq_def by (auto simp:Let_def)lemma runing_th_s: shows "th \<in> runing s"proof - from pip_e[unfolded is_v] show ?thesis by (cases, simp)qedlemma th_not_waiting: "\<not> waiting s th c"proof - have "th \<in> readys s" using runing_ready runing_th_s by blast thus ?thesis by (unfold readys_def, auto)qedlemma waiting_neq_th: assumes "waiting s t c" shows "t \<noteq> th" using assms using th_not_waiting by blast lemma wq_s_cs: "wq s cs = th#rest"proof - from pip_e[unfolded is_v] show ?thesis proof(cases) case (thread_V) from this(2) show ?thesis by (unfold rest_def s_holding_def, fold wq_def, metis empty_iff list.collapse list.set(1)) qedqedlemma wq_es_cs: "wq (e#s) cs = wq'" using wq_s_cs[unfolded wq_def] by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp) lemma wq_distinct_kept: assumes "distinct (wq s cs')" shows "distinct (wq (e#s) cs')"proof(cases "cs' = cs") case True show ?thesis proof(unfold True wq_es_cs wq'_def, rule someI2) show "distinct rest \<and> set rest = set rest" using assms[unfolded True wq_s_cs] by auto qed simpqed (insert assms, simp)endcontext valid_tracebeginlemma actor_inv: assumes "PIP s e" and "\<not> isCreate e" shows "actor e \<in> runing s" using assms by (induct, auto)lemma isP_E: assumes "isP e" obtains cs where "e = P (actor e) cs" using assms by (cases e, auto)lemma isV_E: assumes "isV e" obtains cs where "e = V (actor e) cs" using assms by (cases e, auto) lemma wq_distinct: "distinct (wq s cs)"proof(induct rule:ind) case (Cons s e) interpret vt_e: valid_trace_e s e using Cons by simp show ?case proof(cases e) case (V th cs) interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp) show ?thesis using Cons by (simp add: vt_v.wq_distinct_kept) qedqed (unfold wq_def Let_def, simp)endcontext valid_trace_ebegintext {* 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 wq_in_inv: assumes s_ni: "thread \<notin> set (wq s cs)" and s_i: "thread \<in> set (wq (e#s) cs)" shows "e = P thread cs"proof(cases e) -- {* This is the only non-trivial case: *} case (V th cs1) have False proof(cases "cs1 = cs") case True show ?thesis proof(cases "(wq s cs1)") case (Cons w_hd w_tl) have "set (wq (e#s) cs) \<subseteq> set (wq s cs)" proof - have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)" using Cons V by (auto simp:wq_def Let_def True split:if_splits) moreover have "set ... \<subseteq> set (wq s cs)" proof(rule someI2) show "distinct w_tl \<and> set w_tl = set w_tl" by (metis distinct.simps(2) local.Cons wq_distinct) qed (insert Cons True, auto) ultimately show ?thesis by simp qed with assms show ?thesis by auto qed (insert assms V True, auto simp:wq_def Let_def split:if_splits) qed (insert assms V, auto simp:wq_def Let_def split:if_splits) thus ?thesis by autoqed (insert assms, auto simp:wq_def Let_def split:if_splits)lemma wq_out_inv: assumes s_in: "thread \<in> set (wq s cs)" and s_hd: "thread = hd (wq s cs)" and s_i: "thread \<noteq> hd (wq (e#s) cs)" shows "e = V thread cs"proof(cases e)-- {* There are only two non-trivial cases: *} case (V th cs1) show ?thesis proof(cases "cs1 = cs") case True have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] . thus ?thesis proof(cases) case (thread_V) moreover have "th = thread" using thread_V(2) s_hd by (unfold s_holding_def wq_def, simp) ultimately show ?thesis using V True by simp qed qed (insert assms V, auto simp:wq_def Let_def split:if_splits)next case (P th cs1) show ?thesis proof(cases "cs1 = cs") case True with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]" by (auto simp:wq_def Let_def split:if_splits) with s_i s_hd s_in have False by (metis empty_iff hd_append2 list.set(1) wq_def) thus ?thesis by simp qed (insert assms P, auto simp:wq_def Let_def split:if_splits)qed (insert assms, auto simp:wq_def Let_def split:if_splits)endcontext valid_tracebegintext {* (* 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 lost 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: (* ddd *) assumes 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" = "\<lambda> 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> ?Q cs1 (moment t1 s)" and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto from p_split [of "?Q cs2", OF q2 nq2] obtain t2 where lt2: "t2 < length s" and np2: "\<not> ?Q cs2 (moment t2 s)" and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto { fix s cs assume q: "?Q cs s" have "thread \<notin> runing s" proof assume "thread \<in> runing s" hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and> thread \<noteq> hd (wq_fun (schs s) cs))" by (unfold runing_def s_waiting_def readys_def, auto) from this[rule_format, of cs] q show False by (simp add: wq_def) qed } note q_not_runing = this { fix t1 t2 cs1 cs2 assume lt1: "t1 < length s" and np1: "\<not> ?Q cs1 (moment t1 s)" and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" and lt2: "t2 < length s" and np2: "\<not> ?Q cs2 (moment t2 s)" and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" and 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#moment t2 s)" proof - from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed then interpret vt_e: valid_trace_e "moment t2 s" "e" by (unfold_locales, auto, cases, simp) have ?thesis proof - have "thread \<in> runing (moment t2 s)" proof(cases "thread \<in> set (wq (moment t2 s) cs2)") case True have "e = V thread cs2" proof - have eq_th: "thread = hd (wq (moment t2 s) cs2)" using True and np2 by auto from vt_e.wq_out_inv[OF True this h2] show ?thesis . qed thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto next case False have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] . with vt_e.actor_inv[OF vt_e.pip_e] show ?thesis by auto qed moreover have "thread \<notin> runing (moment t2 s)" by (rule q_not_runing[OF nn1[rule_format, OF lt12]]) ultimately show ?thesis by simp qed } note lt_case = this show ?thesis proof - { assume "t1 < t2" from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this] have ?thesis . } moreover { assume "t2 < t1" from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this] have ?thesis . } moreover { assume eq_12: "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 lt_2: "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 from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12] have g1: "thread \<in> set (wq (e#moment t1 s) cs1)" and g2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto have "vt (e#moment t2 s)" proof - from vt_moment have "vt (moment ?t3 s)" . with eq_m show ?thesis by simp qed then interpret vt_e: valid_trace_e "moment t2 s" "e" by (unfold_locales, auto, cases, simp) have "e = V thread cs2 \<or> e = P thread cs2" proof(cases "thread \<in> set (wq (moment t2 s) cs2)") case True have "e = V thread cs2" proof - have eq_th: "thread = hd (wq (moment t2 s) cs2)" using True and np2 by auto from vt_e.wq_out_inv[OF True this h2] show ?thesis . qed thus ?thesis by auto next case False have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] . thus ?thesis by auto qed moreover have "e = V thread cs1 \<or> e = P thread cs1" proof(cases "thread \<in> set (wq (moment t1 s) cs1)") case True have eq_th: "thread = hd (wq (moment t1 s) cs1)" using True and np1 by auto from vt_e.wq_out_inv[folded eq_12, OF True this g2] have "e = V thread cs1" . thus ?thesis by auto next case False have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] . thus ?thesis by auto qed ultimately have ?thesis using neq12 by auto } ultimately show ?thesis using nat_neq_iff by blast qedqedtext {* This lemma is a simple corrolary of @{text "waiting_unique_pre"}.*}lemma waiting_unique: assumes "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2" using waiting_unique_pre assms unfolding wq_def s_waiting_def by autoend(* 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: assumes "holding (s::event list) th1 cs" and "holding s th2 cs" shows "th1 = th2" by (insert assms, unfold s_holding_def, auto)lemma 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: 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: 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: 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)context valid_trace_vbeginlemma distinct_rest: "distinct rest" by (simp add: distinct_tl rest_def wq_distinct)definition "wq' = (SOME q. distinct q \<and> set q = set rest)"lemma runing_th_s: shows "th \<in> runing s"proof - from pip_e[unfolded is_v] show ?thesis by (cases, simp)qedlemma holding_cs_eq_th: assumes "holding s t cs" shows "t = th"proof - from pip_e[unfolded is_v] show ?thesis proof(cases) case (thread_V) from held_unique[OF this(2) assms] show ?thesis by simp qedqedlemma th_not_waiting: "\<not> waiting s th c"proof - have "th \<in> readys s" using runing_ready runing_th_s by blast thus ?thesis by (unfold readys_def, auto)qedlemma waiting_neq_th: assumes "waiting s t c" shows "t \<noteq> th" using assms using th_not_waiting by blast lemma wq_s_cs: "wq s cs = th#rest"proof - from pip_e[unfolded is_v] show ?thesis proof(cases) case (thread_V) from this(2) show ?thesis by (unfold rest_def s_holding_def, fold wq_def, metis empty_iff list.collapse list.set(1)) qedqedlemma wq_es_cs: "wq (e#s) cs = wq'" using wq_s_cs[unfolded wq_def] by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp) lemma distinct_wq': "distinct wq'" by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def)lemma th'_in_inv: assumes "th' \<in> set wq'" shows "th' \<in> set rest" using assms by (metis (mono_tags, lifting) distinct.simps(2) rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) lemma neq_t_th: assumes "waiting (e#s) t c" shows "t \<noteq> th"proof assume otherwise: "t = th" show False proof(cases "c = cs") case True have "t \<in> set wq'" using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs] by simp from th'_in_inv[OF this] have "t \<in> set rest" . with wq_s_cs[folded otherwise] wq_distinct[of cs] show ?thesis by simp next case False have "wq (e#s) c = wq s c" using False by (unfold is_v, simp) hence "waiting s t c" using assms by (simp add: cs_waiting_def waiting_eq) hence "t \<notin> readys s" by (unfold readys_def, auto) hence "t \<notin> runing s" using runing_ready by auto with runing_th_s[folded otherwise] show ?thesis by auto qedqedlemma waiting_esI1: assumes "waiting s t c" and "c \<noteq> cs" shows "waiting (e#s) t c" proof - have "wq (e#s) c = wq s c" using assms(2) is_v by auto with assms(1) show ?thesis using cs_waiting_def waiting_eq by auto qedlemma holding_esI2: assumes "c \<noteq> cs" and "holding s t c" shows "holding (e#s) t c"proof - from assms(1) have "wq (e#s) c = wq s c" using is_v by auto from assms(2)[unfolded s_holding_def, folded wq_def, folded this, unfolded wq_def, folded s_holding_def] show ?thesis .qedlemma holding_esI1: assumes "holding s t c" and "t \<noteq> th" shows "holding (e#s) t c"proof - have "c \<noteq> cs" using assms using holding_cs_eq_th by blast from holding_esI2[OF this assms(1)] show ?thesis .qedendcontext valid_trace_v_nbeginlemma neq_wq': "wq' \<noteq> []" proof (unfold wq'_def, rule someI2) show "distinct rest \<and> set rest = set rest" by (simp add: distinct_rest) next fix x assume " distinct x \<and> set x = set rest" thus "x \<noteq> []" using rest_nnl by autoqed definition "taker = hd wq'"definition "rest' = tl wq'"lemma eq_wq': "wq' = taker # rest'" by (simp add: neq_wq' rest'_def taker_def)lemma next_th_taker: shows "next_th s th cs taker" using rest_nnl taker_def wq'_def wq_s_cs by (auto simp:next_th_def)lemma taker_unique: assumes "next_th s th cs taker'" shows "taker' = taker"proof - from assms obtain rest' where h: "wq s cs = th # rest'" "taker' = hd (SOME q. distinct q \<and> set q = set rest')" by (unfold next_th_def, auto) with wq_s_cs have "rest' = rest" by auto thus ?thesis using h(2) taker_def wq'_def by auto qedlemma waiting_set_eq: "{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}" by (smt all_not_in_conv bot.extremum insertI1 insert_subset mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)lemma holding_set_eq: "{(Cs cs, Th th') |th'. next_th s th cs th'} = {(Cs cs, Th taker)}" using next_th_taker taker_def waiting_set_eq by fastforcelemma holding_taker: shows "holding (e#s) taker cs" by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, auto simp:neq_wq' taker_def)lemma waiting_esI2: assumes "waiting s t cs" and "t \<noteq> taker" shows "waiting (e#s) t cs" proof - have "t \<in> set wq'" proof(unfold wq'_def, rule someI2) show "distinct rest \<and> set rest = set rest" by (simp add: distinct_rest) next fix x assume "distinct x \<and> set x = set rest" moreover have "t \<in> set rest" using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto ultimately show "t \<in> set x" by simp qed moreover have "t \<noteq> hd wq'" using assms(2) taker_def by auto ultimately show ?thesis by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp)qedlemma waiting_esE: assumes "waiting (e#s) t c" obtains "c \<noteq> cs" "waiting s t c" | "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"proof(cases "c = cs") case False hence "wq (e#s) c = wq s c" using is_v by auto with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto from that(1)[OF False this] show ?thesis .next case True from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs] have "t \<noteq> hd wq'" "t \<in> set wq'" by auto hence "t \<noteq> taker" by (simp add: taker_def) moreover hence "t \<noteq> th" using assms neq_t_th by blast moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) ultimately have "waiting s t cs" by (metis cs_waiting_def list.distinct(2) list.sel(1) list.set_sel(2) rest_def waiting_eq wq_s_cs) show ?thesis using that(2) using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto qedlemma holding_esI1: assumes "c = cs" and "t = taker" shows "holding (e#s) t c" by (unfold assms, simp add: holding_taker)lemma holding_esE: assumes "holding (e#s) t c" obtains "c = cs" "t = taker" | "c \<noteq> cs" "holding s t c"proof(cases "c = cs") case True from assms[unfolded True, unfolded s_holding_def, folded wq_def, unfolded wq_es_cs] have "t = taker" by (simp add: taker_def) from that(1)[OF True this] show ?thesis .next case False hence "wq (e#s) c = wq s c" using is_v by auto from assms[unfolded s_holding_def, folded wq_def, unfolded this, unfolded wq_def, folded s_holding_def] have "holding s t c" . from that(2)[OF False this] show ?thesis .qedend context valid_trace_v_nbeginlemma nil_wq': "wq' = []" proof (unfold wq'_def, rule someI2) show "distinct rest \<and> set rest = set rest" by (simp add: distinct_rest) next fix x assume " distinct x \<and> set x = set rest" thus "x = []" using rest_nil by autoqed lemma no_taker: assumes "next_th s th cs taker" shows "False"proof - from assms[unfolded next_th_def] obtain rest' where "wq s cs = th # rest'" "rest' \<noteq> []" by auto thus ?thesis using rest_def rest_nil by auto qedlemma waiting_set_eq: "{(Th th', Cs cs) |th'. next_th s th cs th'} = {}" using no_taker by autolemma holding_set_eq: "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}" using no_taker by autolemma no_holding: assumes "holding (e#s) taker cs" shows Falseproof - from wq_es_cs[unfolded nil_wq'] have " wq (e # s) cs = []" . from assms[unfolded s_holding_def, folded wq_def, unfolded this] show ?thesis by autoqedlemma no_waiting: assumes "waiting (e#s) t cs" shows Falseproof - from wq_es_cs[unfolded nil_wq'] have " wq (e # s) cs = []" . from assms[unfolded s_waiting_def, folded wq_def, unfolded this] show ?thesis by autoqedlemma waiting_esI2: assumes "waiting s t c" shows "waiting (e#s) t c"proof - have "c \<noteq> cs" using assms using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto from waiting_esI1[OF assms this] show ?thesis .qedlemma waiting_esE: assumes "waiting (e#s) t c" obtains "c \<noteq> cs" "waiting s t c"proof(cases "c = cs") case False hence "wq (e#s) c = wq s c" using is_v by auto with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto from that(1)[OF False this] show ?thesis .next case True from no_waiting[OF assms[unfolded True]] show ?thesis by autoqedlemma holding_esE: assumes "holding (e#s) t c" obtains "c \<noteq> cs" "holding s t c"proof(cases "c = cs") case True from no_holding[OF assms[unfolded True]] show ?thesis by autonext case False hence "wq (e#s) c = wq s c" using is_v by auto from assms[unfolded s_holding_def, folded wq_def, unfolded this, unfolded wq_def, folded s_holding_def] have "holding s t c" . from that[OF False this] show ?thesis .qedend (* ccc *)lemma rel_eqI: assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B" and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A" shows "A = B" using assms by autolemma in_RAG_E: assumes "(n1, n2) \<in> RAG (s::state)" obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs" | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs" using assms[unfolded s_RAG_def, folded waiting_eq holding_eq] by autocontext valid_trace_vbeginlemma RAG_es: "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 = ?R")proof(rule rel_eqI) fix n1 n2 assume "(n1, n2) \<in> ?L" thus "(n1, n2) \<in> ?R" proof(cases rule:in_RAG_E) case (waiting th' cs') show ?thesis proof(cases "rest = []") case False interpret h_n: valid_trace_v_n s e th cs by (unfold_locales, insert False, simp) from waiting(3) show ?thesis proof(cases rule:h_n.waiting_esE) case 1 with waiting(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, fold waiting_eq, auto) next case 2 with waiting(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, fold waiting_eq, auto) qed next case True interpret h_e: valid_trace_v_e s e th cs by (unfold_locales, insert True, simp) from waiting(3) show ?thesis proof(cases rule:h_e.waiting_esE) case 1 with waiting(1,2) show ?thesis by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, fold waiting_eq, auto) qed qed next case (holding th' cs') show ?thesis proof(cases "rest = []") case False interpret h_n: valid_trace_v_n s e th cs by (unfold_locales, insert False, simp) from holding(3) show ?thesis proof(cases rule:h_n.holding_esE) case 1 with holding(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, fold waiting_eq, auto) next case 2 with holding(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, fold holding_eq, auto) qed next case True interpret h_e: valid_trace_v_e s e th cs by (unfold_locales, insert True, simp) from holding(3) show ?thesis proof(cases rule:h_e.holding_esE) case 1 with holding(1,2) show ?thesis by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, fold holding_eq, auto) qed qed qednext fix n1 n2 assume h: "(n1, n2) \<in> ?R" show "(n1, n2) \<in> ?L" proof(cases "rest = []") case False interpret h_n: valid_trace_v_n s e th cs by (unfold_locales, insert False, simp) from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq] have "((n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)) \<or> (n2 = Th h_n.taker \<and> n1 = Cs cs)" by auto thus ?thesis proof assume "n2 = Th h_n.taker \<and> n1 = Cs cs" with h_n.holding_taker show ?thesis by (unfold s_RAG_def, fold holding_eq, auto) next assume h: "(n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)" hence "(n1, n2) \<in> RAG s" by simp thus ?thesis proof(cases rule:in_RAG_E) case (waiting th' cs') from h and this(1,2) have "th' \<noteq> h_n.taker \<or> cs' \<noteq> cs" by auto hence "waiting (e#s) th' cs'" proof assume "cs' \<noteq> cs" from waiting_esI1[OF waiting(3) this] show ?thesis . next assume neq_th': "th' \<noteq> h_n.taker" show ?thesis proof(cases "cs' = cs") case False from waiting_esI1[OF waiting(3) this] show ?thesis . next case True from h_n.waiting_esI2[OF waiting(3)[unfolded True] neq_th', folded True] show ?thesis . qed qed thus ?thesis using waiting(1,2) by (unfold s_RAG_def, fold waiting_eq, auto) next case (holding th' cs') from h this(1,2) have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto hence "holding (e#s) th' cs'" proof assume "cs' \<noteq> cs" from holding_esI2[OF this holding(3)] show ?thesis . next assume "th' \<noteq> th" from holding_esI1[OF holding(3) this] show ?thesis . qed thus ?thesis using holding(1,2) by (unfold s_RAG_def, fold holding_eq, auto) qed qed next case True interpret h_e: valid_trace_v_e s e th cs by (unfold_locales, insert True, simp) from h[unfolded h_e.waiting_set_eq h_e.holding_set_eq] have h_s: "(n1, n2) \<in> RAG s" "(n1, n2) \<noteq> (Cs cs, Th th)" by auto from h_s(1) show ?thesis proof(cases rule:in_RAG_E) case (waiting th' cs') from h_e.waiting_esI2[OF this(3)] show ?thesis using waiting(1,2) by (unfold s_RAG_def, fold waiting_eq, auto) next case (holding th' cs') with h_s(2) have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto thus ?thesis proof assume neq_cs: "cs' \<noteq> cs" from holding_esI2[OF this holding(3)] show ?thesis using holding(1,2) by (unfold s_RAG_def, fold holding_eq, auto) next assume "th' \<noteq> th" from holding_esI1[OF holding(3) this] show ?thesis using holding(1,2) by (unfold s_RAG_def, fold holding_eq, auto) qed qed qedqedendcontext valid_tracebeginlemma finite_threads: shows "finite (threads s)"using vt by (induct) (auto elim: step.cases)lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"unfolding cp_def wq_defapply(induct s rule: schs.induct)apply(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)donelemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs" by (unfold s_RAG_def, auto)lemma wq_threads: assumes h: "th \<in> set (wq s cs)" shows "th \<in> threads s"lemma wq_threads: assumes 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) interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, auto) 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 vt_s.wq_distinct[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 dm_RAG_threads: assumes 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 this] show ?thesis .qedlemma cp_le: assumes 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 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) apply (unfold trancl_domain [of "RAG s", symmetric]) by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) qedqedlemma le_cp: 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 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: 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 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 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 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 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 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_eq_the_preced: shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" using max_cp_eq using the_preced_def by presburger endlemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s" by (unfold preced_def, simp)lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"proof fix th' show "the_preced (V th cs # s) th' = the_preced s th'" by (unfold the_preced_def preced_def, simp)qedlemma step_RAG_v: assumes 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'}" (is "?L = ?R")proof - interpret vt_v: valid_trace_v s "V th cs" using assms step_back_vt by (unfold_locales, auto) show ?thesis using vt_v.RAG_es .qedtext {* (* 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:assumes 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)context valid_tracebegintext {* 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: shows "acyclic (RAG s)"using vtproof(induct) case (vt_cons s e) interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) 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 vt_s.waiting_unique) from eq_wq vt_s.wq_distinct[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 vt_s.wq_distinct[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 vt_s.wq_distinct[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 vt_s.wq_distinct[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 vt_s.wq_distinct[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: shows "finite (RAG s)"proof - from vt show ?thesis proof(induct) case (vt_cons s e) interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) 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: shows "wf ((RAG s)^-1)"proof(rule finite_acyclic_wf_converse) from finite_RAG show "finite (RAG s)" .next from acyclic_RAG show "acyclic (RAG s)" .qedendlemma 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)context valid_tracebeginlemma wq_threads: assumes 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) interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, auto) 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 vt_s.wq_distinct[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>(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: assumes 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 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: 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 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 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: assumes 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 this] show ?thesis by autoqedendlemma 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)context valid_tracebeginlemma unique_RAG: "\<lbrakk>(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)endlemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"by (induct rule:trancl_induct, auto)context valid_tracebeginlemma dchain_unique: assumes 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 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 autoqedendlemma step_holdents_p_add: 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: 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 (in valid_trace) finite_holding : shows "finite (holdents s th)"proof - let ?F = "\<lambda> (x, y). the_cs x" from finite_RAG 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: assumes vtv: "vt (V thread cs#s)" shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"proof - from vtv interpret vt_s: valid_trace s by (cases, unfold_locales, simp) from vtv interpret vt_v: valid_trace "V thread cs#s" by (unfold_locales, simp) 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 vt_s.wq_distinct[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 vt_v.finite_holding 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 lemma count_rec1 [simp]: assumes "Q e" shows "count Q (e#es) = Suc (count Q es)" using assms by (unfold count_def, auto)lemma count_rec2 [simp]: assumes "\<not>Q e" shows "count Q (e#es) = (count Q es)" using assms by (unfold count_def, auto)lemma count_rec3 [simp]: shows "count Q [] = 0" by (unfold count_def, auto)lemma cntP_diff_inv: assumes "cntP (e#s) th \<noteq> cntP s th" shows "isP e \<and> actor e = th"proof(cases e) case (P th' pty) show ?thesis by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", insert assms P, auto simp:cntP_def)qed (insert assms, auto simp:cntP_def)lemma cntV_diff_inv: assumes "cntV (e#s) th \<noteq> cntV s th" shows "isV e \<and> actor e = th"proof(cases e) case (V th' pty) show ?thesis by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", insert assms V, auto simp:cntV_def)qed (insert assms, auto simp:cntV_def)context valid_tracebegintext {* (* ddd *) \noindent The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} of one particular thread. t*} lemma cnp_cnv_cncs: 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) interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) 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 vt_s.wq_threads [OF 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 then interpret vt_p: valid_trace "(P thread cs#s)" by (unfold_locales, simp) 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 vt_s.finite_holding [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 vt_p.wq_distinct [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 then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp) 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 vt_v.wq_distinct[of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by (metis distinct.simps(2) vt_s.wq_distinct) 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 vt_v.wq_distinct[of cs] and eq_wq show False by (metis distinct.simps(2) vt_s.wq_distinct) 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 (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq) 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 vt_s.wq_distinct[ 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 vt_s.wq_distinct[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 vt_s.wq_distinct[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 vt_s.wq_threads) 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 vt_s.wq_distinct[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 vt_s.waiting_unique[OF 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 vt_s.wq_threads [OF 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 vt_s.finite_RAG 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: assumes 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) interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) 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 then interpret vt_v: valid_trace "(V thread cs#s)" by (unfold_locales, simp) 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 vt_v.wq_distinct[of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by (metis distinct.simps(2) vt_s.wq_distinct) 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 vt_s.wq_threads[OF this] and ni show False using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)` ni vt_s.wq_threads by blast 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) qedqedendcontext valid_tracebeginlemma dm_RAG_threads: assumes 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 this] show ?thesis .qedendlemma 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)donecontext valid_tracebeginlemma runing_unique: assumes 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)") unfolding cp_eq_cpreced unfolding cpreced_def . obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)" 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 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 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 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 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 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:waiting_eq) 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:waiting_eq) 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 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 "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) doneendlemma 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) qedqedcontext valid_tracebeginlemma cnp_cnv_eq: assumes "th \<notin> threads s" shows "cntP s th = cntV s th" using assms using cnp_cnv_cncs not_thread_cncs by autoendlemma eq_RAG: "RAG (wq s) = RAG s"by (unfold cs_RAG_def s_RAG_def, auto)context valid_tracebeginlemma count_eq_dependants: assumes eq_pv: "cntP s th = cntV s th" shows "dependants (wq s) th = {}"proof - from cnp_cnv_cncs 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 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: 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 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: shows "finite (threads s)"using vt by (induct) (auto elim: step.cases)endlemma 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 autoqedcontext valid_tracebeginlemma cp_le: assumes 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 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) apply (unfold trancl_domain [of "RAG s", symmetric]) by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) qedqedlemma le_cp: 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 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: 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 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 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 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 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 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 np: "threads s \<noteq> {}" shows "Max (cp s ` readys s) = Max (cp s ` threads s)"proof(unfold max_cp_eq) 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 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 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 finite_threads 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 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp next from p_in and th'_in and dependants_threads[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 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 show " finite ((\<lambda>th. preced th s) ` threads s)" by simp qed next from finite_threads 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 tm] show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto next from finite_threads show "finite ((\<lambda>th. preced th s) ` threads s)" by simp qed } with hy show ?thesis by auto qed next from dependants_threads[of tm] finite_threads 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 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 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 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: 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 False])qedendlemma 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)donecontext valid_tracebeginlemma detached_intro: assumes eq_pv: "cntP s th = cntV s th" shows "detached s th"proof - from cnp_cnv_cncs 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 dm_RAG_threads 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] 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: assumes dtc: "detached s th" shows "cntP s th = cntV s th"proof - from cnp_cnv_cncs 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:waiting_eq 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: shows "(detached s th) = (cntP s th = cntV s th)" by (insert vt, auto intro:detached_intro detached_elim)endtext {* 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.*}lemma eq_dependants: "dependants (wq s) = dependants s" by (simp add: s_dependants_abv wq_def)lemma next_th_unique: assumes nt1: "next_th s th cs th1" and nt2: "next_th s th cs th2" shows "th1 = th2"using assms by (unfold next_th_def, auto)lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s" apply (induct s, simp)proof - fix a s assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s" and eq_as: "a # s \<noteq> []" show "last_set th (a # s) < length (a # s)" proof(cases "s \<noteq> []") case False from False show ?thesis by (cases a, auto simp:last_set.simps) next case True from ih [OF True] show ?thesis by (cases a, auto simp:last_set.simps) qedqedlemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []" by (induct s, auto simp:threads.simps)lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s" apply (drule_tac th_in_ne) by (unfold preced_def, auto intro: birth_time_lt)lemma inj_the_preced: "inj_on (the_preced s) (threads s)" by (metis inj_onI preced_unique the_preced_def)lemma tRAG_alt_def: "tRAG s = {(Th th1, Th th2) | th1 th2. \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)lemma tRAG_Field: "Field (tRAG s) \<subseteq> Field (RAG s)" by (unfold tRAG_alt_def Field_def, auto)lemma tRAG_ancestorsE: assumes "x \<in> ancestors (tRAG s) u" obtains th where "x = Th th"proof - from assms have "(u, x) \<in> (tRAG s)^+" by (unfold ancestors_def, auto) from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto then obtain th where "x = Th th" by (unfold tRAG_alt_def, auto) from that[OF this] show ?thesis .qedlemma tRAG_mono: assumes "RAG s' \<subseteq> RAG s" shows "tRAG s' \<subseteq> tRAG s" using assms by (unfold tRAG_alt_def, auto)lemma holding_next_thI: assumes "holding s th cs" and "length (wq s cs) > 1" obtains th' where "next_th s th cs th'"proof - from assms(1)[folded eq_holding, unfolded cs_holding_def] have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" . then obtain rest where h1: "wq s cs = th#rest" by (cases "wq s cs", auto) with assms(2) have h2: "rest \<noteq> []" by auto let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)" have "next_th s th cs ?th'" using h1(1) h2 by (unfold next_th_def, auto) from that[OF this] show ?thesis .qedlemma RAG_tRAG_transfer: assumes "vt s'" assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}" and "(Cs cs, Th th'') \<in> RAG s'" shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")proof - interpret vt_s': valid_trace "s'" using assms(1) by (unfold_locales, simp) interpret rtree: rtree "RAG s'" proof show "single_valued (RAG s')" apply (intro_locales) by (unfold single_valued_def, auto intro:vt_s'.unique_RAG) show "acyclic (RAG s')" by (rule vt_s'.acyclic_RAG) qed { fix n1 n2 assume "(n1, n2) \<in> ?L" from this[unfolded tRAG_alt_def] obtain th1 th2 cs' where h: "n1 = Th th1" "n2 = Th th2" "(Th th1, Cs cs') \<in> RAG s" "(Cs cs', Th th2) \<in> RAG s" by auto from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto from h(3) and assms(2) have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> (Th th1, Cs cs') \<in> RAG s'" by auto hence "(n1, n2) \<in> ?R" proof assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" hence eq_th1: "th1 = th" by simp moreover have "th2 = th''" proof - from h1 have "cs' = cs" by simp from assms(3) cs_in[unfolded this] rtree.sgv show ?thesis by (unfold single_valued_def, auto) qed ultimately show ?thesis using h(1,2) by auto next assume "(Th th1, Cs cs') \<in> RAG s'" with cs_in have "(Th th1, Th th2) \<in> tRAG s'" by (unfold tRAG_alt_def, auto) from this[folded h(1, 2)] show ?thesis by auto qed } moreover { fix n1 n2 assume "(n1, n2) \<in> ?R" hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto hence "(n1, n2) \<in> ?L" proof assume "(n1, n2) \<in> tRAG s'" moreover have "... \<subseteq> ?L" proof(rule tRAG_mono) show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto) qed ultimately show ?thesis by auto next assume eq_n: "(n1, n2) = (Th th, Th th'')" from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto ultimately show ?thesis by (unfold eq_n tRAG_alt_def, auto) qed } ultimately show ?thesis by autoqedcontext valid_tracebeginlemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]endlemma cp_alt_def: "cp s th = Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"proof - have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" (is "Max (_ ` ?L) = Max (_ ` ?R)") proof - have "?L = ?R" by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def) thus ?thesis by simp qed thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)qedlemma cp_gen_alt_def: "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" by (auto simp:cp_gen_def)lemma tRAG_nodeE: assumes "(n1, n2) \<in> tRAG s" obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" using assms by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)lemma subtree_nodeE: assumes "n \<in> subtree (tRAG s) (Th th)" obtains th1 where "n = Th th1"proof - show ?thesis proof(rule subtreeE[OF assms]) assume "n = Th th" from that[OF this] show ?thesis . next assume "Th th \<in> ancestors (tRAG s) n" hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def) hence "\<exists> th1. n = Th th1" proof(induct) case (base y) from tRAG_nodeE[OF this] show ?case by metis next case (step y z) thus ?case by auto qed with that show ?thesis by auto qedqedlemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"proof - have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" by (rule rtrancl_mono, auto simp:RAG_split) also have "... \<subseteq> ((RAG s)^*)^*" by (rule rtrancl_mono, auto) also have "... = (RAG s)^*" by simp finally show ?thesis by (unfold tRAG_def, simp)qedlemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"proof - { fix a assume "a \<in> subtree (tRAG s) x" hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def) with tRAG_star_RAG[of s] have "(a, x) \<in> (RAG s)^*" by auto hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def) } thus ?thesis by autoqedlemma tRAG_trancl_eq: "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {th'. (Th th', Th th) \<in> (RAG s)^+}" (is "?L = ?R")proof - { fix th' assume "th' \<in> ?L" hence "(Th th', Th th) \<in> (tRAG s)^+" by auto from tranclD[OF this] obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto from tRAG_subtree_RAG[of s] and this(2) have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto ultimately have "th' \<in> ?R" by auto } moreover { fix th' assume "th' \<in> ?R" hence "(Th th', Th th) \<in> (RAG s)^+" by (auto) from plus_rpath[OF this] obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto hence "(Th th', Th th) \<in> (tRAG s)^+" proof(induct xs arbitrary:th' th rule:length_induct) case (1 xs th' th) then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) show ?case proof(cases "xs1") case Nil from 1(2)[unfolded Cons1 Nil] have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . hence "(Th th', x1) \<in> (RAG s)" by (cases, simp) then obtain cs where "x1 = Cs cs" by (unfold s_RAG_def, auto) from rpath_nnl_lastE[OF rp[unfolded this]] show ?thesis by auto next case (Cons x2 xs2) from 1(2)[unfolded Cons1[unfolded this]] have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . from rpath_edges_on[OF this] have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" . have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)" by (simp add: edges_on_unfold) with eds have rg1: "(Th th', x1) \<in> RAG s" by auto then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)" by (simp add: edges_on_unfold) from this eds have rg2: "(x1, x2) \<in> RAG s" by auto from this[unfolded eq_x1] obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto) from rp have "rpath (RAG s) x2 xs2 (Th th)" by (elim rpath_ConsE, simp) from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . show ?thesis proof(cases "xs2 = []") case True from rpath_nilE[OF rp'[unfolded this]] have "th1 = th" by auto from rt1[unfolded this] show ?thesis by auto next case False from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp with rt1 show ?thesis by auto qed qed qed hence "th' \<in> ?L" by auto } ultimately show ?thesis by blastqedlemma tRAG_trancl_eq_Th: "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" using tRAG_trancl_eq by autolemma dependants_alt_def: "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" by (metis eq_RAG s_dependants_def tRAG_trancl_eq)context valid_tracebeginlemma count_eq_tRAG_plus: assumes "cntP s th = cntV s th" shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" using assms count_eq_dependants dependants_alt_def eq_dependants by auto lemma count_eq_RAG_plus: assumes "cntP s th = cntV s th" shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" using assms count_eq_dependants cs_dependants_def eq_RAG by autolemma count_eq_RAG_plus_Th: assumes "cntP s th = cntV s th" shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}" using count_eq_RAG_plus[OF assms] by autolemma count_eq_tRAG_plus_Th: assumes "cntP s th = cntV s th" shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" using count_eq_tRAG_plus[OF assms] by autoendlemma tRAG_subtree_eq: "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")proof - { fix n assume h: "n \<in> ?L" hence "n \<in> ?R" by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) } moreover { fix n assume "n \<in> ?R" then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def) from rtranclD[OF this(2)] have "n \<in> ?L" proof assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+" with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto thus ?thesis using subtree_def tRAG_trancl_eq by fastforce qed (insert h, auto simp:subtree_def) } ultimately show ?thesis by autoqedlemma threads_set_eq: "the_thread ` (subtree (tRAG s) (Th th)) = {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)lemma cp_alt_def1: "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"proof - have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))" by auto thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)qedlemma cp_gen_def_cond: assumes "x = Th th" shows "cp s th = cp_gen s (Th th)"by (unfold cp_alt_def1 cp_gen_def, simp)lemma cp_gen_over_set: assumes "\<forall> x \<in> A. \<exists> th. x = Th th" shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"proof(rule f_image_eq) fix a assume "a \<in> A" from assms[rule_format, OF this] obtain th where eq_a: "a = Th th" by auto show "cp_gen s a = (cp s \<circ> the_thread) a" by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)qedcontext valid_tracebeginlemma RAG_threads: assumes "(Th th) \<in> Field (RAG s)" shows "th \<in> threads s" using assms by (metis Field_def UnE dm_RAG_threads range_in vt)lemma subtree_tRAG_thread: assumes "th \<in> threads s" shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")proof - have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" by (unfold tRAG_subtree_eq, simp) also have "... \<subseteq> ?R" proof fix x assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto from this(2) show "x \<in> ?R" proof(cases rule:subtreeE) case 1 thus ?thesis by (simp add: assms h(1)) next case 2 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) qed qed finally show ?thesis .qedlemma readys_root: assumes "th \<in> readys s" shows "root (RAG s) (Th th)"proof - { fix x assume "x \<in> ancestors (RAG s) (Th th)" hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) from tranclD[OF this] obtain z where "(Th th, z) \<in> RAG s" by auto with assms(1) have False apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) by (fold wq_def, blast) } thus ?thesis by (unfold root_def, auto)qedlemma readys_in_no_subtree: assumes "th \<in> readys s" and "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 readys_root[OF assms(1)] show ?thesis by (auto simp:root_def) qedqedlemma not_in_thread_isolated: assumes "th \<notin> threads s" shows "(Th th) \<notin> Field (RAG s)"proof assume "(Th th) \<in> Field (RAG s)" with dm_RAG_threads and range_in assms show False by (unfold Field_def, blast)qedlemma wf_RAG: "wf (RAG s)"proof(rule finite_acyclic_wf) from finite_RAG show "finite (RAG s)" .next from acyclic_RAG show "acyclic (RAG s)" .qedlemma sgv_wRAG: "single_valued (wRAG s)" using waiting_unique by (unfold single_valued_def wRAG_def, auto)lemma sgv_hRAG: "single_valued (hRAG s)" using holding_unique by (unfold single_valued_def hRAG_def, auto)lemma sgv_tRAG: "single_valued (tRAG s)" by (unfold tRAG_def, rule single_valued_relcomp, insert sgv_wRAG sgv_hRAG, auto)lemma acyclic_tRAG: "acyclic (tRAG s)"proof(unfold tRAG_def, rule acyclic_compose) show "acyclic (RAG s)" using acyclic_RAG .next show "wRAG s \<subseteq> RAG s" unfolding RAG_split by autonext show "hRAG s \<subseteq> RAG s" unfolding RAG_split by autoqedlemma sgv_RAG: "single_valued (RAG s)" using unique_RAG by (auto simp:single_valued_def)lemma rtree_RAG: "rtree (RAG s)" using sgv_RAG acyclic_RAG by (unfold rtree_def rtree_axioms_def sgv_def, auto)endsublocale valid_trace < rtree_RAG: rtree "RAG s"proof show "single_valued (RAG s)" apply (intro_locales) by (unfold single_valued_def, auto intro:unique_RAG) show "acyclic (RAG s)" by (rule acyclic_RAG)qedsublocale valid_trace < rtree_s: rtree "tRAG s"proof(unfold_locales) from sgv_tRAG show "single_valued (tRAG s)" .next from acyclic_tRAG show "acyclic (tRAG s)" .qedsublocale valid_trace < fsbtRAGs : fsubtree "RAG s"proof - show "fsubtree (RAG s)" proof(intro_locales) show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] . next show "fsubtree_axioms (RAG s)" proof(unfold fsubtree_axioms_def) from wf_RAG show "wf (RAG s)" . qed qedqedsublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"proof - have "fsubtree (tRAG s)" proof - have "fbranch (tRAG s)" proof(unfold tRAG_def, rule fbranch_compose) show "fbranch (wRAG s)" proof(rule finite_fbranchI) from finite_RAG show "finite (wRAG s)" by (unfold RAG_split, auto) qed next show "fbranch (hRAG s)" proof(rule finite_fbranchI) from finite_RAG show "finite (hRAG s)" by (unfold RAG_split, auto) qed qed moreover have "wf (tRAG s)" proof(rule wf_subset) show "wf (RAG s O RAG s)" using wf_RAG by (fold wf_comp_self, simp) next show "tRAG s \<subseteq> (RAG s O RAG s)" by (unfold tRAG_alt_def, auto) qed ultimately show ?thesis by (unfold fsubtree_def fsubtree_axioms_def,auto) qed from this[folded tRAG_def] show "fsubtree (tRAG s)" .qedlemma Max_UNION: assumes "finite A" and "A \<noteq> {}" and "\<forall> M \<in> f ` A. finite M" and "\<forall> M \<in> f ` A. M \<noteq> {}" shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") using assms[simp]proof - have "?L = Max (\<Union>(f ` A))" by (fold Union_image_eq, simp) also have "... = ?R" by (subst Max_Union, simp+) finally show ?thesis .qedlemma max_Max_eq: assumes "finite A" and "A \<noteq> {}" and "x = y" shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")proof - have "?R = Max (insert y A)" by simp also from assms have "... = ?L" by (subst Max.insert, simp+) finally show ?thesis by simpqedcontext valid_tracebegin(* ddd *)lemma cp_gen_rec: assumes "x = Th th" shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"proof(cases "children (tRAG s) x = {}") case True show ?thesis by (unfold True cp_gen_def subtree_children, simp add:assms)next case False hence [simp]: "children (tRAG s) x \<noteq> {}" by auto note fsbttRAGs.finite_subtree[simp] have [simp]: "finite (children (tRAG s) x)" by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], rule children_subtree) { fix r x have "subtree r x \<noteq> {}" by (auto simp:subtree_def) } note this[simp] have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}" proof - from False obtain q where "q \<in> children (tRAG s) x" by blast moreover have "subtree (tRAG s) q \<noteq> {}" by simp ultimately show ?thesis by blast qed have h: "Max ((the_preced s \<circ> the_thread) ` ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) = Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)" (is "?L = ?R") proof - let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L let "Max (_ \<union> (?h ` ?B))" = ?R let ?L1 = "?f ` \<Union>(?g ` ?B)" have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" proof - have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto finally have "Max ?L1 = Max ..." by simp also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)" by (subst Max_UNION, simp+) also have "... = Max (cp_gen s ` children (tRAG s) x)" by (unfold image_comp cp_gen_alt_def, simp) finally show ?thesis . qed show ?thesis proof - have "?L = Max (?f ` ?A \<union> ?L1)" by simp also have "... = max (the_preced s (the_thread x)) (Max ?L1)" by (subst Max_Un, simp+) also have "... = max (?f x) (Max (?h ` ?B))" by (unfold eq_Max_L1, simp) also have "... =?R" by (rule max_Max_eq, (simp)+, unfold assms, simp) finally show ?thesis . qed qed thus ?thesis by (fold h subtree_children, unfold cp_gen_def, simp) qedlemma cp_rec: "cp s th = Max ({the_preced s th} \<union> (cp s o the_thread) ` children (tRAG s) (Th th))"proof - have "Th th = Th th" by simp note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] show ?thesis proof - have "cp_gen s ` children (tRAG s) (Th th) = (cp s \<circ> the_thread) ` children (tRAG s) (Th th)" proof(rule cp_gen_over_set) show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th" by (unfold tRAG_alt_def, auto simp:children_def) qed thus ?thesis by (subst (1) h(1), unfold h(2), simp) qedqedend(* keep *)lemma next_th_holding: assumes vt: "vt s" and nxt: "next_th s th cs th'" shows "holding (wq s) th cs"proof - from nxt[unfolded next_th_def] obtain rest where h: "wq s cs = th # rest" "rest \<noteq> []" "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto thus ?thesis by (unfold cs_holding_def, auto)qedcontext valid_tracebeginlemma next_th_waiting: assumes nxt: "next_th s th cs th'" shows "waiting (wq s) th' cs"proof - from nxt[unfolded next_th_def] obtain rest where h: "wq s cs = th # rest" "rest \<noteq> []" "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto from wq_distinct[of cs, unfolded h] have dst: "distinct (th # rest)" . have in_rest: "th' \<in> set rest" proof(unfold h, rule someI2) show "distinct rest \<and> set rest = set rest" using dst by auto next fix x assume "distinct x \<and> set x = set rest" with h(2) show "hd x \<in> set (rest)" by (cases x, auto) qed hence "th' \<in> set (wq s cs)" by (unfold h(1), auto) moreover have "th' \<noteq> hd (wq s cs)" by (unfold h(1), insert in_rest dst, auto) ultimately show ?thesis by (auto simp:cs_waiting_def)qedlemma next_th_RAG: assumes nxt: "next_th (s::event list) th cs th'" shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" using vt assms next_th_holding next_th_waiting by (unfold s_RAG_def, simp)end-- {* A useless definition *}definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"where "cps s = {(th, cp s th) | th . th \<in> threads s}"lemma "wq (V th cs # s) cs1 = ttt" apply (unfold wq_def, auto simp:Let_def)end