added a bit more text to the paper and separated a theory about Max
theory CpsGimports PrioG Maxbeginlemma not_thread_holdents: fixes th s assumes vt: "vt s" and not_in: "th \<notin> threads s" shows "holdents s th = {}"proof - from vt not_in show ?thesis proof(induct arbitrary:th) case (vt_cons s e th) assume vt: "vt s" and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}" 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 "holdents (e # s) th = holdents s th" apply (unfold eq_e 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 = {}" show ?thesis proof(cases "th = thread") case True with nh eq_e show ?thesis by (auto simp:holdents_test RAG_exit_unchanged) next case False with not_in and eq_e have "th \<notin> threads s" by simp from ih[OF this] False eq_e show ?thesis by (auto simp:holdents_test RAG_exit_unchanged) qed next case (thread_P thread cs) assume eq_e: "e = P thread cs" and is_runing: "thread \<in> runing s" from assms thread_exit ih stp not_in vt eq_e 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 "holdents (e # s) th = holdents s th " apply (unfold cntCS_def holdents_test eq_e) by (unfold step_RAG_p[OF vtp], auto) moreover have "holdents s th = {}" 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 eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto from hold obtain rest where eq_wq: "wq s cs = thread # rest" by (case_tac "wq s cs", auto simp: wq_def s_holding_def) from not_in eq_e eq_wq have "\<not> next_th s thread cs th" apply (auto simp:next_th_def) proof - assume ne: "rest \<noteq> []" and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s") have "?t \<in> set rest" proof(rule someI2) from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq show "distinct rest \<and> set rest = set rest" by auto next fix x assume "distinct x \<and> set x = set rest" with ne show "hd x \<in> set rest" by (cases x, auto) qed with eq_wq have "?t \<in> set (wq s cs)" by simp from wq_threads[OF step_back_vt[OF vtv], OF this] and ni show False by auto qed moreover note neq_th eq_wq ultimately have "holdents (e # s) th = holdents s th" by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) moreover have "holdents s th = {}" 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 (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) qedqedlemma next_th_neq: assumes vt: "vt s" and nt: "next_th s th cs th'" shows "th' \<noteq> th"proof - from nt show ?thesis apply (auto simp:next_th_def) proof - fix rest assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest" and ne: "rest \<noteq> []" have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" proof(rule someI2) from wq_distinct[OF vt, of cs] eq_wq show "distinct rest \<and> set rest = set rest" by auto next fix x assume "distinct x \<and> set x = set rest" hence eq_set: "set x = set rest" by auto with ne have "x \<noteq> []" by auto hence "hd x \<in> set x" by auto with eq_set show "hd x \<in> set rest" by auto qed with wq_distinct[OF vt, of cs] eq_wq show False by auto qedqedlemma 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 wf_RAG: assumes vt: "vt s" shows "wf (RAG s)"proof(rule finite_acyclic_wf) from finite_RAG[OF vt] show "finite (RAG s)" .next from acyclic_RAG[OF vt] show "acyclic (RAG s)" .qeddefinition child :: "state \<Rightarrow> (node \<times> node) set" where "child s \<equiv> {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set" where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"lemma children_def2: "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"unfolding child_def children_def by simplemma children_dependants: "children s th \<subseteq> dependants (wq s) th" unfolding children_def2 unfolding cs_dependants_def by (auto simp add: eq_RAG)lemma child_unique: assumes vt: "vt s" and ch1: "(Th th, Th th1) \<in> child s" and ch2: "(Th th, Th th2) \<in> child s" shows "th1 = th2"using ch1 ch2 proof(unfold child_def, clarsimp) fix cs csa assume h1: "(Th th, Cs cs) \<in> RAG s" and h2: "(Cs cs, Th th1) \<in> RAG s" and h3: "(Th th, Cs csa) \<in> RAG s" and h4: "(Cs csa, Th th2) \<in> RAG s" from unique_RAG[OF vt h1 h3] have "cs = csa" by simp with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp from unique_RAG[OF vt h2 this] show "th1 = th2" by simpqed lemma RAG_children: assumes h: "(Th th1, Th th2) \<in> (RAG s)^+" shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"proof - from h show ?thesis proof(induct rule: tranclE) fix c th2 assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+" and h2: "(c, Th th2) \<in> RAG s" from h2 obtain cs where eq_c: "c = Cs cs" by (case_tac c, auto simp:s_RAG_def) show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)" proof(rule tranclE[OF h1]) fix ca assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+" and h4: "(ca, c) \<in> RAG s" show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)" proof - from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3" by (case_tac ca, auto simp:s_RAG_def) from eq_ca h4 h2 eq_c have "th3 \<in> children s th2" by (auto simp:children_def child_def) moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp ultimately show ?thesis by auto qed next assume "(Th th1, c) \<in> RAG s" with h2 eq_c have "th1 \<in> children s th2" by (auto simp:children_def child_def) thus ?thesis by auto qed next assume "(Th th1, Th th2) \<in> RAG s" thus ?thesis by (auto simp:s_RAG_def) qedqedlemma sub_child: "child s \<subseteq> (RAG s)^+" by (unfold child_def, auto)lemma wf_child: assumes vt: "vt s" shows "wf (child s)"apply(rule wf_subset)apply(rule wf_trancl[OF wf_RAG[OF vt]])apply(rule sub_child)donelemma RAG_child_pre: assumes vt: "vt s" shows "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")proof - from wf_trancl[OF wf_RAG[OF vt]] have wf: "wf ((RAG s)^+)" . show ?thesis proof(rule wf_induct[OF wf, of ?P], clarsimp) fix th' assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow> (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)" and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+" show "(Th th, Th th') \<in> (child s)\<^sup>+" proof - from RAG_children[OF h] have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" . thus ?thesis proof assume "th \<in> children s th'" thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def) next assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+" then obtain th3 where th3_in: "th3 \<in> children s th'" and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def) from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def) qed qed qedqedlemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+" by (insert RAG_child_pre, auto)lemma child_RAG_p: assumes "(n1, n2) \<in> (child s)^+" shows "(n1, n2) \<in> (RAG s)^+"proof - from assms show ?thesis proof(induct) case (base y) with sub_child show ?case by auto next case (step y z) assume "(y, z) \<in> child s" with sub_child have "(y, z) \<in> (RAG s)^+" by auto moreover have "(n1, y) \<in> (RAG s)^+" by fact ultimately show ?case by auto qedqedlemma child_RAG_eq: assumes vt: "vt s" shows "(Th th1, Th th2) \<in> (child s)^+ \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+" by (auto intro: RAG_child[OF vt] child_RAG_p)lemma children_no_dep: fixes s th th1 th2 th3 assumes vt: "vt s" and ch1: "(Th th1, Th th) \<in> child s" and ch2: "(Th th2, Th th) \<in> child s" and ch3: "(Th th1, Th th2) \<in> (RAG s)^+" shows "False"proof - from RAG_child[OF vt ch3] have "(Th th1, Th th2) \<in> (child s)\<^sup>+" . thus ?thesis proof(rule converse_tranclE) assume "(Th th1, Th th2) \<in> child s" from child_unique[OF vt ch1 this] have "th = th2" by simp with ch2 have "(Th th2, Th th2) \<in> child s" by simp with wf_child[OF vt] show ?thesis by auto next fix c assume h1: "(Th th1, c) \<in> child s" and h2: "(c, Th th2) \<in> (child s)\<^sup>+" from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto) with h1 have "(Th th1, Th th3) \<in> child s" by simp from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto moreover have "wf ((child s)\<^sup>+)" proof(rule wf_trancl) from wf_child[OF vt] show "wf (child s)" . qed ultimately show False by auto qedqedlemma unique_RAG_p: assumes vt: "vt s" and dp1: "(n, n1) \<in> (RAG s)^+" and dp2: "(n, n2) \<in> (RAG s)^+" and neq: "n1 \<noteq> n2" shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"proof(rule unique_chain [OF _ dp1 dp2 neq]) from unique_RAG[OF vt] show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by autoqedlemma dependants_child_unique: fixes s th th1 th2 th3 assumes vt: "vt s" and ch1: "(Th th1, Th th) \<in> child s" and ch2: "(Th th2, Th th) \<in> child s" and dp1: "th3 \<in> dependants s th1" and dp2: "th3 \<in> dependants s th2"shows "th1 = th2"proof - { assume neq: "th1 \<noteq> th2" from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG) from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG) from unique_RAG_p[OF vt dp1 dp2] and neq 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 children_no_dep[OF vt ch1 ch2 this] show ?thesis . next assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+" from children_no_dep[OF vt ch2 ch1 this] show ?thesis . qed } thus ?thesis by autoqedlemma RAG_plus_elim: assumes "vt s" fixes x assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+" shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+" using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]] apply (unfold children_def) by (metis assms(2) children_def RAG_children eq_RAG)lemma dependants_expand: assumes "vt s" shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"apply(simp add: image_def)unfolding cs_dependants_defapply(auto)apply (metis assms RAG_plus_elim mem_Collect_eq)apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)lemma finite_children: assumes "vt s" shows "finite (children s th)" using children_dependants dependants_threads[OF assms] finite_threads[OF assms] by (metis rev_finite_subset)lemma finite_dependants: assumes "vt s" shows "finite (dependants (wq s) th')" using dependants_threads[OF assms] finite_threads[OF assms] by (metis rev_finite_subset)abbreviation "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"abbreviation "cpreceds s ths \<equiv> (cp s) ` ths"lemma Un_compr: "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"by autolemma in_disj: shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"by metislemma UN_exists: shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"by autolemma cp_rec: fixes s th assumes vt: "vt s" shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"proof(cases "children s th = {}") case True show ?thesis unfolding cp_eq_cpreced cpreced_def by (subst dependants_expand[OF `vt s`]) (simp add: True)next case False show ?thesis (is "?LHS = ?RHS") proof - have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))" by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric]) have not_emptyness_facts[simp]: "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}" using False dependants_expand[OF assms] by(auto simp only: Un_empty) have finiteness_facts[simp]: "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)" by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`]) (* expanding definition *) have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))" unfolding eq_cp by (simp add: Un_compr) (* moving Max in *) also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))" by (simp add: Max_Un) (* expanding dependants *) also have "\<dots> = max (Max {preced th s}) (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))" by (subst dependants_expand[OF `vt s`]) (simp) (* moving out big Union *) also have "\<dots> = max (Max {preced th s}) (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))" by simp (* moving in small union *) also have "\<dots> = max (Max {preced th s}) (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))" by (simp add: in_disj) (* moving in preceds *) also have "\<dots> = max (Max {preced th s}) (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" by (simp add: UN_exists) (* moving in Max *) also have "\<dots> = max (Max {preced th s}) (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" by (subst Max_Union) (auto simp add: image_image) (* folding cp + moving out Max *) also have "\<dots> = ?RHS" unfolding eq_cp by (simp add: Max_insert) finally show "?LHS = ?RHS" . qedqeddefinition cps:: "state \<Rightarrow> (thread \<times> precedence) set"where "cps s = {(th, cp s th) | th . th \<in> threads s}"locale step_set_cps = fixes s' th prio s defines s_def : "s \<equiv> (Set th prio#s')" assumes vt_s: "vt s"context step_set_cps beginlemma eq_preced: fixes th' assumes "th' \<noteq> th" shows "preced th' s = preced th' s'"proof - from assms show ?thesis by (unfold s_def, auto simp:preced_def)qedlemma eq_dep: "RAG s = RAG s'" by (unfold s_def RAG_set_unchanged, auto)lemma eq_cp_pre: fixes th' assumes neq_th: "th' \<noteq> th" and nd: "th \<notin> dependants s th'" shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) moreover { fix th1 assume "th1 \<in> {th'} \<union> dependants (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto hence "preced th1 s = preced th1 s'" proof assume "th1 = th'" with eq_preced[OF neq_th] show "preced th1 s = preced th1 s'" by simp next assume "th1 \<in> dependants (wq s') th'" with nd and eq_dp have "th1 \<noteq> th" by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep) from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp qed } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simpqedlemma no_dependants: assumes "th' \<noteq> th" shows "th \<notin> dependants s th'"proof assume h: "th \<in> dependants s th'" from step_back_step [OF vt_s[unfolded s_def]] have "step s' (Set th prio)" . hence "th \<in> runing s'" by (cases, simp) hence rd_th: "th \<in> readys s'" by (simp add:readys_def runing_def) from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+" by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto) from tranclD[OF this] obtain z where "(Th th, z) \<in> RAG s'" by auto with rd_th show "False" apply (case_tac z, auto simp:readys_def s_waiting_def s_RAG_def s_waiting_def cs_waiting_def) by (fold wq_def, blast)qed(* Result improved *)lemma eq_cp: fixes th' assumes neq_th: "th' \<noteq> th" shows "cp s th' = cp s' th'"proof(rule eq_cp_pre [OF neq_th]) from no_dependants[OF neq_th] show "th \<notin> dependants s th'" .qedlemma eq_up: fixes th' th'' assumes dp1: "th \<in> dependants s th'" and dp2: "th' \<in> dependants s th''" and eq_cps: "cp s th' = cp s' th'" shows "cp s th'' = cp s' th''"proof - from dp2 have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def) from RAG_child[OF vt_s this[unfolded eq_RAG]] have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" . moreover { fix n th'' have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow> (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')" proof(erule trancl_induct, auto) fix y th'' assume y_ch: "(y, Th th'') \<in> child s" and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''" and ch': "(Th th', y) \<in> (child s)\<^sup>+" from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def) with ih have eq_cpy:"cp s thy = cp s' thy" by blast from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) moreover from child_RAG_p[OF ch'] and eq_y have "(Th th', Th thy) \<in> (RAG s)^+" by simp ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto show "cp s th'' = cp s' th''" apply (subst cp_rec[OF vt_s]) proof - have "preced th'' s = preced th'' s'" proof(rule eq_preced) show "th'' \<noteq> th" proof assume "th'' = th" with dp_thy y_ch[unfolded eq_y] have "(Th th, Th th) \<in> (RAG s)^+" by (auto simp:child_def) with wf_trancl[OF wf_RAG[OF vt_s]] show False by auto qed qed moreover { fix th1 assume th1_in: "th1 \<in> children s th''" have "cp s th1 = cp s' th1" proof(cases "th1 = thy") case True with eq_cpy show ?thesis by simp next case False have neq_th1: "th1 \<noteq> th" proof assume eq_th1: "th1 = th" with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp from children_no_dep[OF vt_s _ _ this] and th1_in y_ch eq_y show False by (auto simp:children_def) qed have "th \<notin> dependants s th1" proof assume h:"th \<in> dependants s th1" from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG) from dependants_child_unique[OF vt_s _ _ h this] th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) with False show False by auto qed from eq_cp_pre[OF neq_th1 this] show ?thesis . qed } ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) moreover have "children s th'' = children s' th''" by (unfold children_def child_def s_def RAG_set_unchanged, simp) ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''" by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) qed next fix th'' assume dp': "(Th th', Th th'') \<in> child s" show "cp s th'' = cp s' th''" apply (subst cp_rec[OF vt_s]) proof - have "preced th'' s = preced th'' s'" proof(rule eq_preced) show "th'' \<noteq> th" proof assume "th'' = th" with dp1 dp' have "(Th th, Th th) \<in> (RAG s)^+" by (auto simp:child_def s_dependants_def eq_RAG) with wf_trancl[OF wf_RAG[OF vt_s]] show False by auto qed qed moreover { fix th1 assume th1_in: "th1 \<in> children s th''" have "cp s th1 = cp s' th1" proof(cases "th1 = th'") case True with eq_cps show ?thesis by simp next case False have neq_th1: "th1 \<noteq> th" proof assume eq_th1: "th1 = th" with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) from children_no_dep[OF vt_s _ _ this] th1_in dp' show False by (auto simp:children_def) qed thus ?thesis proof(rule eq_cp_pre) show "th \<notin> dependants s th1" proof assume "th \<in> dependants s th1" from dependants_child_unique[OF vt_s _ _ this dp1] th1_in dp' have "th1 = th'" by (auto simp:children_def) with False show False by auto qed qed qed } ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) moreover have "children s th'' = children s' th''" by (unfold children_def child_def s_def RAG_set_unchanged, simp) ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''" by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) qed qed } ultimately show ?thesis by autoqedlemma eq_up_self: fixes th' th'' assumes dp: "th \<in> dependants s th''" and eq_cps: "cp s th = cp s' th" shows "cp s th'' = cp s' th''"proof - from dp have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def) from RAG_child[OF vt_s this[unfolded eq_RAG]] have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" . moreover { fix n th'' have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow> (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')" proof(erule trancl_induct, auto) fix y th'' assume y_ch: "(y, Th th'') \<in> child s" and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''" and ch': "(Th th, y) \<in> (child s)\<^sup>+" from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def) with ih have eq_cpy:"cp s thy = cp s' thy" by blast from child_RAG_p[OF ch'] and eq_y have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp show "cp s th'' = cp s' th''" apply (subst cp_rec[OF vt_s]) proof - have "preced th'' s = preced th'' s'" proof(rule eq_preced) show "th'' \<noteq> th" proof assume "th'' = th" with dp_thy y_ch[unfolded eq_y] have "(Th th, Th th) \<in> (RAG s)^+" by (auto simp:child_def) with wf_trancl[OF wf_RAG[OF vt_s]] show False by auto qed qed moreover { fix th1 assume th1_in: "th1 \<in> children s th''" have "cp s th1 = cp s' th1" proof(cases "th1 = thy") case True with eq_cpy show ?thesis by simp next case False have neq_th1: "th1 \<noteq> th" proof assume eq_th1: "th1 = th" with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp from children_no_dep[OF vt_s _ _ this] and th1_in y_ch eq_y show False by (auto simp:children_def) qed have "th \<notin> dependants s th1" proof assume h:"th \<in> dependants s th1" from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG) from dependants_child_unique[OF vt_s _ _ h this] th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) with False show False by auto qed from eq_cp_pre[OF neq_th1 this] show ?thesis . qed } ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) moreover have "children s th'' = children s' th''" by (unfold children_def child_def s_def RAG_set_unchanged, simp) ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''" by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) qed next fix th'' assume dp': "(Th th, Th th'') \<in> child s" show "cp s th'' = cp s' th''" apply (subst cp_rec[OF vt_s]) proof - have "preced th'' s = preced th'' s'" proof(rule eq_preced) show "th'' \<noteq> th" proof assume "th'' = th" with dp dp' have "(Th th, Th th) \<in> (RAG s)^+" by (auto simp:child_def s_dependants_def eq_RAG) with wf_trancl[OF wf_RAG[OF vt_s]] show False by auto qed qed moreover { fix th1 assume th1_in: "th1 \<in> children s th''" have "cp s th1 = cp s' th1" proof(cases "th1 = th") case True with eq_cps show ?thesis by simp next case False assume neq_th1: "th1 \<noteq> th" thus ?thesis proof(rule eq_cp_pre) show "th \<notin> dependants s th1" proof assume "th \<in> dependants s th1" hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) from children_no_dep[OF vt_s _ _ this] and th1_in dp' show False by (auto simp:children_def) qed qed qed } ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) moreover have "children s th'' = children s' th''" by (unfold children_def child_def s_def RAG_set_unchanged, simp) ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''" by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) qed qed } ultimately show ?thesis by autoqedendlemma next_waiting: assumes vt: "vt s" and nxt: "next_th s th cs th'" shows "waiting s th' cs"proof - from assms show ?thesis apply (auto simp:next_th_def s_waiting_def[folded wq_def]) proof - fix rest assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest" and eq_wq: "wq s cs = th # rest" and ne: "rest \<noteq> []" have "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs] 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 with ni have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)" by simp moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from wq_distinct[OF vt, of cs] eq_wq show "distinct rest \<and> set rest = set rest" by auto next from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto qed ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto next fix rest assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest" and ne: "rest \<noteq> []" have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" proof(rule someI2) from wq_distinct[OF vt, of cs] eq_wq show "distinct rest \<and> set rest = set rest" by auto next from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> 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 "set (SOME q. distinct q \<and> set q = set rest) = set rest" proof(rule someI2) from wq_distinct[OF vt, of cs] 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 ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp with eq_wq and wq_distinct[OF vt, of cs] show False by auto qedqedlocale step_v_cps = fixes s' th cs s defines s_def : "s \<equiv> (V th cs#s')" assumes vt_s: "vt s"locale step_v_cps_nt = step_v_cps + fixes th' assumes nt: "next_th s' th cs th'"context step_v_cps_ntbeginlemma RAG_s: "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> {(Cs cs, Th th')}"proof - from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] and nt show ?thesis by (auto intro:next_th_unique)qedlemma dependants_kept: fixes th'' assumes neq1: "th'' \<noteq> th" and neq2: "th'' \<noteq> th'" shows "dependants (wq s) th'' = dependants (wq s') th''"proof(auto) fix x assume "x \<in> dependants (wq s) th''" hence dp: "(Th x, Th th'') \<in> (RAG s)^+" by (auto simp:cs_dependants_def eq_RAG) { fix n have "(n, Th th'') \<in> (RAG s)^+ \<Longrightarrow> (n, Th th'') \<in> (RAG s')^+" proof(induct rule:converse_trancl_induct) fix y assume "(y, Th th'') \<in> RAG s" with RAG_s neq1 neq2 have "(y, Th th'') \<in> RAG s'" by auto thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto next fix y z assume yz: "(y, z) \<in> RAG s" and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+" and ztp': "(z, Th th'') \<in> (RAG s')\<^sup>+" have "y \<noteq> Cs cs \<and> y \<noteq> Th th'" proof show "y \<noteq> Cs cs" proof assume eq_y: "y = Cs cs" with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp from RAG_s have cst': "(Cs cs, Th th') \<in> RAG s" by simp from unique_RAG[OF vt_s this dp_yz] have eq_z: "z = Th th'" by simp with ztp have "(Th th', Th th'') \<in> (RAG s)^+" by simp from converse_tranclE[OF this] obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s" by (auto simp:s_RAG_def) with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (RAG s)^+" by auto moreover have "cs' = cs" proof - from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt] have "(Th th', Cs cs) \<in> RAG s'" by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def) from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp'] show ?thesis by simp qed ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp moreover note wf_trancl[OF wf_RAG[OF vt_s]] ultimately show False by auto qed next show "y \<noteq> Th th'" proof assume eq_y: "y = Th th'" with yz have dps: "(Th th', z) \<in> RAG s" by simp with RAG_s have dps': "(Th th', z) \<in> RAG s'" by auto have "z = Cs cs" proof - from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt] have "(Th th', Cs cs) \<in> RAG s'" by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def) from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this] show ?thesis . qed with dps RAG_s show False by auto qed qed with RAG_s yz have "(y, z) \<in> RAG s'" by auto with ztp' show "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto qed } from this[OF dp] show "x \<in> dependants (wq s') th''" by (auto simp:cs_dependants_def eq_RAG)next fix x assume "x \<in> dependants (wq s') th''" hence dp: "(Th x, Th th'') \<in> (RAG s')^+" by (auto simp:cs_dependants_def eq_RAG) { fix n have "(n, Th th'') \<in> (RAG s')^+ \<Longrightarrow> (n, Th th'') \<in> (RAG s)^+" proof(induct rule:converse_trancl_induct) fix y assume "(y, Th th'') \<in> RAG s'" with RAG_s neq1 neq2 have "(y, Th th'') \<in> RAG s" by auto thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto next fix y z assume yz: "(y, z) \<in> RAG s'" and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+" and ztp': "(z, Th th'') \<in> (RAG s)\<^sup>+" have "y \<noteq> Cs cs \<and> y \<noteq> Th th'" proof show "y \<noteq> Cs cs" proof assume eq_y: "y = Cs cs" with yz have dp_yz: "(Cs cs, z) \<in> RAG s'" by simp from this have eq_z: "z = Th th" proof - from step_back_step[OF vt_s[unfolded s_def]] have "(Cs cs, Th th) \<in> RAG s'" by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def) from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz] show ?thesis by simp qed from converse_tranclE[OF ztp] obtain u where "(z, u) \<in> RAG s'" by auto moreover from step_back_step[OF vt_s[unfolded s_def]] have "th \<in> readys s'" by (cases, simp add:runing_def) moreover note eq_z ultimately show False by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) qed next show "y \<noteq> Th th'" proof assume eq_y: "y = Th th'" with yz have dps: "(Th th', z) \<in> RAG s'" by simp have "z = Cs cs" proof - from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt] have "(Th th', Cs cs) \<in> RAG s'" by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def) from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps this] show ?thesis . qed with ztp have cs_i: "(Cs cs, Th th'') \<in> (RAG s')\<^sup>+" by simp from step_back_step[OF vt_s[unfolded s_def]] have cs_th: "(Cs cs, Th th) \<in> RAG s'" by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def) have "(Cs cs, Th th'') \<notin> RAG s'" proof assume "(Cs cs, Th th'') \<in> RAG s'" from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th] and neq1 show "False" by simp qed with converse_tranclE[OF cs_i] obtain u where cu: "(Cs cs, u) \<in> RAG s'" and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto have "u = Th th" proof - from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th] show ?thesis . qed with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp from converse_tranclE[OF this] obtain v where "(Th th, v) \<in> (RAG s')" by auto moreover from step_back_step[OF vt_s[unfolded s_def]] have "th \<in> readys s'" by (cases, simp add:runing_def) ultimately show False by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) qed qed with RAG_s yz have "(y, z) \<in> RAG s" by auto with ztp' show "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto qed } from this[OF dp] show "x \<in> dependants (wq s) th''" by (auto simp:cs_dependants_def eq_RAG)qedlemma cp_kept: fixes th'' assumes neq1: "th'' \<noteq> th" and neq2: "th'' \<noteq> th'" shows "cp s th'' = cp s' th''"proof - from dependants_kept[OF neq1 neq2] have "dependants (wq s) th'' = dependants (wq s') th''" . moreover { fix th1 assume "th1 \<in> dependants (wq s) th''" have "preced th1 s = preced th1 s'" by (unfold s_def, auto simp:preced_def) } moreover have "preced th'' s = preced th'' s'" by (unfold s_def, auto simp:preced_def) ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) = ((\<lambda>th. preced th s') ` ({th''} \<union> dependants (wq s') th''))" by (auto simp:image_def) thus ?thesis by (unfold cp_eq_cpreced cpreced_def, simp)qedendlocale step_v_cps_nnt = step_v_cps + assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"context step_v_cps_nntbeginlemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"proof assume "(Th th1, Cs cs) \<in> RAG s'" thus "False" apply (auto simp:s_RAG_def cs_waiting_def) proof - assume h1: "th1 \<in> set (wq s' cs)" and h2: "th1 \<noteq> hd (wq s' cs)" from step_back_step[OF vt_s[unfolded s_def]] show "False" proof(cases) assume "holding s' th cs" then obtain rest where eq_wq: "wq s' cs = th#rest" apply (unfold s_holding_def wq_def[symmetric]) by (case_tac "(wq s' cs)", auto) with h1 h2 have ne: "rest \<noteq> []" by auto with eq_wq have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))" by(unfold next_th_def, rule_tac x = "rest" in exI, auto) with nnt show ?thesis by auto qed qedqedlemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"proof - from nnt and step_RAG_v[OF vt_s[unfolded s_def], folded s_def] show ?thesis by autoqedlemma child_kept_left: assumes "(n1, n2) \<in> (child s')^+" shows "(n1, n2) \<in> (child s)^+"proof - from assms show ?thesis proof(induct rule: converse_trancl_induct) case (base y) from base obtain th1 cs1 th2 where h1: "(Th th1, Cs cs1) \<in> RAG s'" and h2: "(Cs cs1, Th th2) \<in> RAG s'" and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def) have "cs1 \<noteq> cs" proof assume eq_cs: "cs1 = cs" with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp with nw_cs eq_cs show False by auto qed with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s" and h2': "(Cs cs1, Th th2) \<in> RAG s" by auto hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def) with eq_y eq_n2 have "(y, n2) \<in> child s" by simp thus ?case by auto next case (step y z) have "(y, z) \<in> child s'" by fact then obtain th1 cs1 th2 where h1: "(Th th1, Cs cs1) \<in> RAG s'" and h2: "(Cs cs1, Th th2) \<in> RAG s'" and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) have "cs1 \<noteq> cs" proof assume eq_cs: "cs1 = cs" with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp with nw_cs eq_cs show False by auto qed with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s" and h2': "(Cs cs1, Th th2) \<in> RAG s" by auto hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def) with eq_y eq_z have "(y, z) \<in> child s" by simp moreover have "(z, n2) \<in> (child s)^+" by fact ultimately show ?case by auto qedqedlemma child_kept_right: assumes "(n1, n2) \<in> (child s)^+" shows "(n1, n2) \<in> (child s')^+"proof - from assms show ?thesis proof(induct) case (base y) from base and RAG_s have "(n1, y) \<in> child s'" by (auto simp:child_def) thus ?case by auto next case (step y z) have "(y, z) \<in> child s" by fact with RAG_s have "(y, z) \<in> child s'" by (auto simp:child_def) moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact ultimately show ?case by auto qedqedlemma eq_child: "(child s)^+ = (child s')^+" by (insert child_kept_left child_kept_right, auto)lemma eq_cp: fixes th' shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th" apply (unfold cs_dependants_def, unfold eq_RAG) proof - from eq_child have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}" by simp with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}" by simp qed moreover { fix th1 assume "th1 \<in> {th'} \<union> dependants (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto hence "preced th1 s = preced th1 s'" proof assume "th1 = th'" show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) next assume "th1 \<in> dependants (wq s') th'" show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) qed } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simpqedendlocale step_P_cps = fixes s' th cs s defines s_def : "s \<equiv> (P th cs#s')" assumes vt_s: "vt s"locale step_P_cps_ne =step_P_cps + assumes ne: "wq s' cs \<noteq> []"locale step_P_cps_e =step_P_cps + assumes ee: "wq s' cs = []"context step_P_cps_ebeginlemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"proof - from ee and step_RAG_p[OF vt_s[unfolded s_def], folded s_def] show ?thesis by autoqedlemma child_kept_left: assumes "(n1, n2) \<in> (child s')^+" shows "(n1, n2) \<in> (child s)^+"proof - from assms show ?thesis proof(induct rule: converse_trancl_induct) case (base y) from base obtain th1 cs1 th2 where h1: "(Th th1, Cs cs1) \<in> RAG s'" and h2: "(Cs cs1, Th th2) \<in> RAG s'" and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def) have "cs1 \<noteq> cs" proof assume eq_cs: "cs1 = cs" with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp with ee show False by (auto simp:s_RAG_def cs_waiting_def) qed with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s" and h2': "(Cs cs1, Th th2) \<in> RAG s" by auto hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def) with eq_y eq_n2 have "(y, n2) \<in> child s" by simp thus ?case by auto next case (step y z) have "(y, z) \<in> child s'" by fact then obtain th1 cs1 th2 where h1: "(Th th1, Cs cs1) \<in> RAG s'" and h2: "(Cs cs1, Th th2) \<in> RAG s'" and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) have "cs1 \<noteq> cs" proof assume eq_cs: "cs1 = cs" with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp with ee show False by (auto simp:s_RAG_def cs_waiting_def) qed with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s" and h2': "(Cs cs1, Th th2) \<in> RAG s" by auto hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def) with eq_y eq_z have "(y, z) \<in> child s" by simp moreover have "(z, n2) \<in> (child s)^+" by fact ultimately show ?case by auto qedqedlemma child_kept_right: assumes "(n1, n2) \<in> (child s)^+" shows "(n1, n2) \<in> (child s')^+"proof - from assms show ?thesis proof(induct) case (base y) from base and RAG_s have "(n1, y) \<in> child s'" apply (auto simp:child_def) proof - fix th' assume "(Th th', Cs cs) \<in> RAG s'" with ee have "False" by (auto simp:s_RAG_def cs_waiting_def) thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto qed thus ?case by auto next case (step y z) have "(y, z) \<in> child s" by fact with RAG_s have "(y, z) \<in> child s'" apply (auto simp:child_def) proof - fix th' assume "(Th th', Cs cs) \<in> RAG s'" with ee have "False" by (auto simp:s_RAG_def cs_waiting_def) thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto qed moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact ultimately show ?case by auto qedqedlemma eq_child: "(child s)^+ = (child s')^+" by (insert child_kept_left child_kept_right, auto)lemma eq_cp: fixes th' shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th" apply (unfold cs_dependants_def, unfold eq_RAG) proof - from eq_child have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}" by auto with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}" by simp qed moreover { fix th1 assume "th1 \<in> {th'} \<union> dependants (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto hence "preced th1 s = preced th1 s'" proof assume "th1 = th'" show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) next assume "th1 \<in> dependants (wq s') th'" show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) qed } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simpqedendcontext step_P_cps_nebeginlemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"proof - from step_RAG_p[OF vt_s[unfolded s_def]] and ne show ?thesis by (simp add:s_def)qedlemma eq_child_left: assumes nd: "(Th th, Th th') \<notin> (child s)^+" shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"proof(induct rule:converse_trancl_induct) case (base y) from base obtain th1 cs1 where h1: "(Th th1, Cs cs1) \<in> RAG s" and h2: "(Cs cs1, Th th') \<in> RAG s" and eq_y: "y = Th th1" by (auto simp:child_def) have "th1 \<noteq> th" proof assume "th1 = th" with base eq_y have "(Th th, Th th') \<in> child s" by simp with nd show False by auto qed with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'" and h2': "(Cs cs1, Th th') \<in> RAG s'" by auto with eq_y show ?case by (auto simp:child_def)next case (step y z) have yz: "(y, z) \<in> child s" by fact then obtain th1 cs1 th2 where h1: "(Th th1, Cs cs1) \<in> RAG s" and h2: "(Cs cs1, Th th2) \<in> RAG s" and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def) have "th1 \<noteq> th" proof assume "th1 = th" with yz eq_y have "(Th th, z) \<in> child s" by simp moreover have "(z, Th th') \<in> (child s)^+" by fact ultimately have "(Th th, Th th') \<in> (child s)^+" by auto with nd show False by auto qed with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'" and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def) moreover have "(z, Th th') \<in> (child s')^+" by fact ultimately show ?case by autoqedlemma eq_child_right: shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"proof(induct rule:converse_trancl_induct) case (base y) with RAG_s show ?case by (auto simp:child_def)next case (step y z) have "(y, z) \<in> child s'" by fact with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def) moreover have "(z, Th th') \<in> (child s)^+" by fact ultimately show ?case by autoqedlemma eq_child: assumes nd: "(Th th, Th th') \<notin> (child s)^+" shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)" by (insert eq_child_left[OF nd] eq_child_right, auto)lemma eq_cp: fixes th' assumes nd: "th \<notin> dependants s th'" shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have nd': "(Th th, Th th') \<notin> (child s)^+" proof assume "(Th th, Th th') \<in> (child s)\<^sup>+" with child_RAG_eq[OF vt_s] have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp with nd show False by (simp add:s_dependants_def eq_RAG) qed have eq_dp: "dependants (wq s) th' = dependants (wq s') th'" proof(auto) fix x assume " x \<in> dependants (wq s) th'" thus "x \<in> dependants (wq s') th'" apply (auto simp:cs_dependants_def eq_RAG) proof - assume "(Th x, Th th') \<in> (RAG s)\<^sup>+" with child_RAG_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] show "(Th x, Th th') \<in> (RAG s')\<^sup>+" by simp qed next fix x assume "x \<in> dependants (wq s') th'" thus "x \<in> dependants (wq s) th'" apply (auto simp:cs_dependants_def eq_RAG) proof - assume "(Th x, Th th') \<in> (RAG s')\<^sup>+" with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp with child_RAG_eq[OF vt_s] show "(Th x, Th th') \<in> (RAG s)\<^sup>+" by simp qed qed moreover { fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def) } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simpqedlemma eq_up: fixes th' th'' assumes dp1: "th \<in> dependants s th'" and dp2: "th' \<in> dependants s th''" and eq_cps: "cp s th' = cp s' th'" shows "cp s th'' = cp s' th''"proof - from dp2 have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def) from RAG_child[OF vt_s this[unfolded eq_RAG]] have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" . moreover { fix n th'' have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow> (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')" proof(erule trancl_induct, auto) fix y th'' assume y_ch: "(y, Th th'') \<in> child s" and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''" and ch': "(Th th', y) \<in> (child s)\<^sup>+" from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def) with ih have eq_cpy:"cp s thy = cp s' thy" by blast from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) moreover from child_RAG_p[OF ch'] and eq_y have "(Th th', Th thy) \<in> (RAG s)^+" by simp ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto show "cp s th'' = cp s' th''" apply (subst cp_rec[OF vt_s]) proof - have "preced th'' s = preced th'' s'" by (simp add:s_def preced_def) moreover { fix th1 assume th1_in: "th1 \<in> children s th''" have "cp s th1 = cp s' th1" proof(cases "th1 = thy") case True with eq_cpy show ?thesis by simp next case False have neq_th1: "th1 \<noteq> th" proof assume eq_th1: "th1 = th" with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp from children_no_dep[OF vt_s _ _ this] and th1_in y_ch eq_y show False by (auto simp:children_def) qed have "th \<notin> dependants s th1" proof assume h:"th \<in> dependants s th1" from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG) from dependants_child_unique[OF vt_s _ _ h this] th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) with False show False by auto qed from eq_cp[OF this] show ?thesis . qed } ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) moreover have "children s th'' = children s' th''" apply (unfold children_def child_def s_def RAG_set_unchanged, simp) apply (fold s_def, auto simp:RAG_s) proof - assume "(Cs cs, Th th'') \<in> RAG s'" with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) from converse_tranclE[OF this] obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s" and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+" by (auto simp:s_RAG_def) have eq_cs: "cs1 = cs" proof - from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp from unique_RAG[OF vt_s this h1] show ?thesis by simp qed have False proof(rule converse_tranclE[OF h2]) assume "(Cs cs1, Th th') \<in> RAG s" with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp from unique_RAG[OF vt_s this cs_th'] have "th' = th''" by simp with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto with wf_trancl[OF wf_child[OF vt_s]] show False by auto next fix y assume "(Cs cs1, y) \<in> RAG s" and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+" with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp from unique_RAG[OF vt_s this cs_th'] have "y = Th th''" . with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp from RAG_child[OF vt_s this] have "(Th th'', Th th') \<in> (child s)\<^sup>+" . moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto with wf_trancl[OF wf_child[OF vt_s]] show False by auto qed thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto qed ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''" by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) qed next fix th'' assume dp': "(Th th', Th th'') \<in> child s" show "cp s th'' = cp s' th''" apply (subst cp_rec[OF vt_s]) proof - have "preced th'' s = preced th'' s'" by (simp add:s_def preced_def) moreover { fix th1 assume th1_in: "th1 \<in> children s th''" have "cp s th1 = cp s' th1" proof(cases "th1 = th'") case True with eq_cps show ?thesis by simp next case False have neq_th1: "th1 \<noteq> th" proof assume eq_th1: "th1 = th" with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) from children_no_dep[OF vt_s _ _ this] th1_in dp' show False by (auto simp:children_def) qed show ?thesis proof(rule eq_cp) show "th \<notin> dependants s th1" proof assume "th \<in> dependants s th1" from dependants_child_unique[OF vt_s _ _ this dp1] th1_in dp' have "th1 = th'" by (auto simp:children_def) with False show False by auto qed qed qed } ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) moreover have "children s th'' = children s' th''" apply (unfold children_def child_def s_def RAG_set_unchanged, simp) apply (fold s_def, auto simp:RAG_s) proof - assume "(Cs cs, Th th'') \<in> RAG s'" with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG) from converse_tranclE[OF this] obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s" and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+" by (auto simp:s_RAG_def) have eq_cs: "cs1 = cs" proof - from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp from unique_RAG[OF vt_s this h1] show ?thesis by simp qed have False proof(rule converse_tranclE[OF h2]) assume "(Cs cs1, Th th') \<in> RAG s" with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp from unique_RAG[OF vt_s this cs_th'] have "th' = th''" by simp with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto with wf_trancl[OF wf_child[OF vt_s]] show False by auto next fix y assume "(Cs cs1, y) \<in> RAG s" and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+" with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp from unique_RAG[OF vt_s this cs_th'] have "y = Th th''" . with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp from RAG_child[OF vt_s this] have "(Th th'', Th th') \<in> (child s)\<^sup>+" . moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto with wf_trancl[OF wf_child[OF vt_s]] show False by auto qed thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto qed ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''" by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]]) qed qed } ultimately show ?thesis by autoqedendlocale step_create_cps = fixes s' th prio s defines s_def : "s \<equiv> (Create th prio#s')" assumes vt_s: "vt s"context step_create_cpsbeginlemma eq_dep: "RAG s = RAG s'" by (unfold s_def RAG_create_unchanged, auto)lemma eq_cp: fixes th' assumes neq_th: "th' \<noteq> th" shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have nd: "th \<notin> dependants s th'" proof assume "th \<in> dependants s th'" hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG) with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp from converse_tranclE[OF this] obtain y where "(Th th, y) \<in> RAG s'" by auto with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]] have in_th: "th \<in> threads s'" by auto from step_back_step[OF vt_s[unfolded s_def]] show False proof(cases) assume "th \<notin> threads s'" with in_th show ?thesis by simp qed qed have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) moreover { fix th1 assume "th1 \<in> {th'} \<union> dependants (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto hence "preced th1 s = preced th1 s'" proof assume "th1 = th'" with neq_th show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) next assume "th1 \<in> dependants (wq s') th'" with nd and eq_dp have "th1 \<noteq> th" by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep) thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) qed } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simpqedlemma nil_dependants: "dependants s th = {}"proof - from step_back_step[OF vt_s[unfolded s_def]] show ?thesis proof(cases) assume "th \<notin> threads s'" from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this] have hdn: " holdents s' th = {}" . have "dependants s' th = {}" proof - { assume "dependants s' th \<noteq> {}" then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+" by (auto simp:s_dependants_def eq_RAG) from tranclE[OF this] obtain cs' where "(Cs cs', Th th) \<in> RAG s'" by (auto simp:s_RAG_def) with hdn have False by (auto simp:holdents_test) } thus ?thesis by auto qed thus ?thesis by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp) qedqedlemma eq_cp_th: "cp s th = preced th s" apply (unfold cp_eq_cpreced cpreced_def) by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)endlocale step_exit_cps = fixes s' th prio s defines s_def : "s \<equiv> Exit th # s'" assumes vt_s: "vt s"context step_exit_cpsbeginlemma eq_dep: "RAG s = RAG s'" by (unfold s_def RAG_exit_unchanged, auto)lemma eq_cp: fixes th' assumes neq_th: "th' \<noteq> th" shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have nd: "th \<notin> dependants s th'" proof assume "th \<in> dependants s th'" hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG) with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp from converse_tranclE[OF this] obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'" by (auto simp:s_RAG_def) from step_back_step[OF vt_s[unfolded s_def]] show False proof(cases) assume "th \<in> runing s'" with bk show ?thesis apply (unfold runing_def readys_def s_waiting_def s_RAG_def) by (auto simp:cs_waiting_def wq_def) qed qed have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG) moreover { fix th1 assume "th1 \<in> {th'} \<union> dependants (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto hence "preced th1 s = preced th1 s'" proof assume "th1 = th'" with neq_th show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) next assume "th1 \<in> dependants (wq s') th'" with nd and eq_dp have "th1 \<noteq> th" by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep) thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def) qed } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simpqedendend