theory CpsGimports PrioG beginlemma 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_def) by (simp add:depend_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_def depend_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_def depend_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_def eq_e) by (unfold step_depend_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_def step_depend_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_def) by (simp add:depend_set_unchanged) qed next case vt_nil show ?case by (auto simp:count_def holdents_def s_depend_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"proof - from assms show ?thesis by (unfold next_th_def, auto)qedlemma pp_sub: "(r^+)^+ \<subseteq> r^+" by autolemma wf_depend: assumes vt: "vt s" shows "wf (depend s)"proof(rule finite_acyclic_wf) from finite_depend[OF vt] show "finite (depend s)" .next from acyclic_depend[OF vt] show "acyclic (depend s)" .qedlemma Max_Union: assumes fc: "finite C" and ne: "C \<noteq> {}" and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}" shows "Max (\<Union> C) = Max (Max ` C)"proof - from fc ne fa show ?thesis proof(induct) case (insert x F) assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)" and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}" show ?case (is "?L = ?R") proof(cases "F = {}") case False from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp also have "\<dots> = max (Max x) (Max(\<Union> F))" proof(rule Max_Un) from h[of x] show "finite x" by auto next from h[of x] show "x \<noteq> {}" by auto next show "finite (\<Union>F)" proof(rule finite_Union) show "finite F" by fact next from h show "\<And>M. M \<in> F \<Longrightarrow> finite M" by auto qed next from False and h show "\<Union>F \<noteq> {}" by auto qed also have "\<dots> = ?R" proof - have "?R = Max (Max ` ({x} \<union> F))" by simp also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp also have "\<dots> = max (Max x) (Max (\<Union>F))" proof - have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))" proof(rule Max_Un) show "finite {Max x}" by simp next show "{Max x} \<noteq> {}" by simp next from insert show "finite (Max ` F)" by auto next from False show "Max ` F \<noteq> {}" by auto qed moreover have "Max {Max x} = Max x" by simp moreover have "Max (\<Union>F) = Max (Max ` F)" proof(rule ih) show "F \<noteq> {}" by fact next from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}" by auto qed ultimately show ?thesis by auto qed finally show ?thesis by simp qed finally show ?thesis by simp next case True thus ?thesis by auto qed next case empty assume "{} \<noteq> {}" show ?case by auto qedqeddefinition child :: "state \<Rightarrow> (node \<times> node) set" where "child s \<equiv> {(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend 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> depend s \<and> (Cs cs, Th th) \<in> depend s}"unfolding child_def children_def by simplemma children_dependents: "children s th \<subseteq> dependents (wq s) th" by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)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"proof - from ch1 ch2 show ?thesis proof(unfold child_def, clarsimp) fix cs csa assume h1: "(Th th, Cs cs) \<in> depend s" and h2: "(Cs cs, Th th1) \<in> depend s" and h3: "(Th th, Cs csa) \<in> depend s" and h4: "(Cs csa, Th th2) \<in> depend s" from unique_depend[OF vt h1 h3] have "cs = csa" by simp with h4 have "(Cs cs, Th th2) \<in> depend s" by simp from unique_depend[OF vt h2 this] show "th1 = th2" by simp qed qedlemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s"proof - from fun_eq_iff have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto show ?thesis proof(rule h) from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto qedqedlemma depend_children: assumes h: "(Th th1, Th th2) \<in> (depend s)^+" shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"proof - from h show ?thesis proof(induct rule: tranclE) fix c th2 assume h1: "(Th th1, c) \<in> (depend s)\<^sup>+" and h2: "(c, Th th2) \<in> depend s" from h2 obtain cs where eq_c: "c = Cs cs" by (case_tac c, auto simp:s_depend_def) show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)" proof(rule tranclE[OF h1]) fix ca assume h3: "(Th th1, ca) \<in> (depend s)\<^sup>+" and h4: "(ca, c) \<in> depend s" show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)" proof - from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3" by (case_tac ca, auto simp:s_depend_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> (depend s)\<^sup>+" by simp ultimately show ?thesis by auto qed next assume "(Th th1, c) \<in> depend 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> depend s" thus ?thesis by (auto simp:s_depend_def) qedqedlemma sub_child: "child s \<subseteq> (depend s)^+" by (unfold child_def, auto)lemma wf_child: assumes vt: "vt s" shows "wf (child s)"proof(rule wf_subset) from wf_trancl[OF wf_depend[OF vt]] show "wf ((depend s)\<^sup>+)" .next from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .qedlemma depend_child_pre: assumes vt: "vt s" shows "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")proof - from wf_trancl[OF wf_depend[OF vt]] have wf: "wf ((depend s)^+)" . show ?thesis proof(rule wf_induct[OF wf, of ?P], clarsimp) fix th' assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (depend s)\<^sup>+ \<longrightarrow> (Th th, y) \<in> (depend s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)" and h: "(Th th, Th th') \<in> (depend s)\<^sup>+" show "(Th th, Th th') \<in> (child s)\<^sup>+" proof - from depend_children[OF h] have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend 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> (depend s)\<^sup>+" then obtain th3 where th3_in: "th3 \<in> children s th'" and th_dp: "(Th th, Th th3) \<in> (depend s)\<^sup>+" by auto from th3_in have "(Th th3, Th th') \<in> (depend 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 depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+" by (insert depend_child_pre, auto)lemma child_depend_p: assumes "(n1, n2) \<in> (child s)^+" shows "(n1, n2) \<in> (depend 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> (depend s)^+" by auto moreover have "(n1, y) \<in> (depend s)^+" by fact ultimately show ?case by auto qedqedlemma child_depend_eq: assumes vt: "vt s" shows "((Th th1, Th th2) \<in> (child s)^+) = ((Th th1, Th th2) \<in> (depend s)^+)" by (auto intro: depend_child[OF vt] child_depend_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> (depend s)^+" shows "False"proof - from depend_child[OF vt ch3] have "(Th th1, Th th2) \<in> (child s)\<^sup>+" . thus ?thesis proof(rule converse_tranclE) thm tranclD 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_depend_p: assumes vt: "vt s" and dp1: "(n, n1) \<in> (depend s)^+" and dp2: "(n, n2) \<in> (depend s)^+" and neq: "n1 \<noteq> n2" shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"proof(rule unique_chain [OF _ dp1 dp2 neq]) from unique_depend[OF vt] show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by autoqedlemma dependents_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> dependents s th1" and dp2: "th3 \<in> dependents s th2"shows "th1 = th2"proof - { assume neq: "th1 \<noteq> th2" from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend) from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend) from unique_depend_p[OF vt dp1 dp2] and neq have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto hence False proof assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ " from children_no_dep[OF vt ch1 ch2 this] show ?thesis . next assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+" from children_no_dep[OF vt ch2 ch1 this] show ?thesis . qed } thus ?thesis by autoqedlemma cp_rec: fixes s th assumes vt: "vt s" shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"proof(unfold cp_eq_cpreced_f cpreced_def) let ?f = "(\<lambda>th. preced th s)" show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)" proof(cases " children s th = {}") case False have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th = {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}" (is "?L = ?R") by auto also have "\<dots> = Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}" (is "_ = Max ` ?C") by auto finally have "Max ?L = Max (Max ` ?C)" by auto also have "\<dots> = Max (\<Union> ?C)" proof(rule Max_Union[symmetric]) from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th] show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}" by (auto simp:finite_subset) next from False show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}" by simp next show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow> finite A \<and> A \<noteq> {}" apply (auto simp:finite_subset) proof - fix th' from finite_threads[OF vt] and dependents_threads[OF vt, of th'] show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset) qed qed also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)" (is "Max ?A = Max ?B") proof - have "?A = ?B" proof show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th" proof fix x assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}" then obtain th' where th'_in: "th' \<in> children s th" and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto thus "x \<in> ?f ` dependents (wq s) th" proof assume "x = preced th' s" with th'_in and children_dependents show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto next assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'" moreover note th'_in ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend) qed qed next show "?f ` dependents (wq s) th \<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}" proof fix x assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" then obtain th' where eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+" by (auto simp:cs_dependents_def eq_depend) from depend_children[OF dp] have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" . thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}" proof assume "th' \<in> children s th" with eq_x show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}" by auto next assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+" then obtain th3 where th3_in: "th3 \<in> children s th" and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}" proof - from dp3 have "th' \<in> dependents (wq s) th3" by (auto simp:cs_dependents_def eq_depend) with eq_x th3_in show ?thesis by auto qed qed qed qed thus ?thesis by simp qed finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)" (is "?X = ?Y") by auto moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = max (?f th) ?X" proof - have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))" proof(rule Max_Un, auto) from finite_threads[OF vt] and dependents_threads[OF vt, of th] show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset) next assume "dependents (wq s) th = {}" with False and children_dependents show False by auto qed also have "\<dots> = max (?f th) ?X" by simp finally show ?thesis . qed moreover have "Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) = max (?f th) ?Y" proof - have "Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) = max (Max {preced th s}) ?Y" proof(rule Max_Un, auto) from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th] show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) ` children s th)" by (auto simp:finite_subset) next assume "children s th = {}" with False show False by auto qed thus ?thesis by simp qed ultimately show ?thesis by auto next case True moreover have "dependents (wq s) th = {}" proof - { fix th' assume "th' \<in> dependents (wq s) th" hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend) from depend_children[OF this] and True have "False" by auto } thus ?thesis by auto qed ultimately show ?thesis by auto 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: "depend s = depend s'" by (unfold s_def depend_set_unchanged, auto)lemma eq_cp_pre: fixes th' assumes neq_th: "th' \<noteq> th" and nd: "th \<notin> dependents s th'" shows "cp s th' = cp s' th'" apply (unfold cp_eq_cpreced cpreced_def)proof - have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th" by (unfold cs_dependents_def, auto simp:eq_dep eq_depend) moreover { fix th1 assume "th1 \<in> {th'} \<union> dependents (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependents (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> dependents (wq s') th'" with nd and eq_dp have "th1 \<noteq> th" by (auto simp:eq_depend cs_dependents_def s_dependents_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> dependents (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simpqedlemma no_dependents: assumes "th' \<noteq> th" shows "th \<notin> dependents s th'"proof assume h: "th \<in> dependents 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> (depend s')\<^sup>+" by (unfold s_dependents_def, unfold eq_depend, unfold eq_dep, auto) from tranclD[OF this] obtain z where "(Th th, z) \<in> depend s'" by auto with rd_th show "False" apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_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_dependents[OF neq_th] show "th \<notin> dependents s th'" .qedlemma eq_up: fixes th' th'' assumes dp1: "th \<in> dependents s th'" and dp2: "th' \<in> dependents 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> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def) from depend_child[OF vt_s this[unfolded eq_depend]] 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> (depend s)^+" by (auto simp:s_dependents_def eq_depend) moreover from child_depend_p[OF ch'] and eq_y have "(Th th', Th thy) \<in> (depend s)^+" by simp ultimately have dp_thy: "(Th th, Th thy) \<in> (depend 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> (depend s)^+" by (auto simp:child_def) with wf_trancl[OF wf_depend[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> (depend 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> dependents s th1" proof assume h:"th \<in> dependents s th1" from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) from dependents_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 depend_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> (depend s)^+" by (auto simp:child_def s_dependents_def eq_depend) with wf_trancl[OF wf_depend[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> (depend s)^+" by (auto simp:s_dependents_def eq_depend) 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> dependents s th1" proof assume "th \<in> dependents s th1" from dependents_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 depend_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> dependents 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> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def) from depend_child[OF vt_s this[unfolded eq_depend]] 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_depend_p[OF ch'] and eq_y have dp_thy: "(Th th, Th thy) \<in> (depend 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> (depend s)^+" by (auto simp:child_def) with wf_trancl[OF wf_depend[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> (depend 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> dependents s th1" proof assume h:"th \<in> dependents s th1" from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) from dependents_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 depend_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> (depend s)^+" by (auto simp:child_def s_dependents_def eq_depend) with wf_trancl[OF wf_depend[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> dependents s th1" proof assume "th \<in> dependents s th1" hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend) 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 depend_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 depend_s: "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> {(Cs cs, Th th')}"proof - from step_depend_v[OF vt_s[unfolded s_def], folded s_def] and nt show ?thesis by (auto intro:next_th_unique)qedlemma dependents_kept: fixes th'' assumes neq1: "th'' \<noteq> th" and neq2: "th'' \<noteq> th'" shows "dependents (wq s) th'' = dependents (wq s') th''"proof(auto) fix x assume "x \<in> dependents (wq s) th''" hence dp: "(Th x, Th th'') \<in> (depend s)^+" by (auto simp:cs_dependents_def eq_depend) { fix n have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow> (n, Th th'') \<in> (depend s')^+" proof(induct rule:converse_trancl_induct) fix y assume "(y, Th th'') \<in> depend s" with depend_s neq1 neq2 have "(y, Th th'') \<in> depend s'" by auto thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto next fix y z assume yz: "(y, z) \<in> depend s" and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+" and ztp': "(z, Th th'') \<in> (depend 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> depend s" by simp from depend_s have cst': "(Cs cs, Th th') \<in> depend s" by simp from unique_depend[OF vt_s this dp_yz] have eq_z: "z = Th th'" by simp with ztp have "(Th th', Th th'') \<in> (depend s)^+" by simp from converse_tranclE[OF this] obtain cs' where dp'': "(Th th', Cs cs') \<in> depend s" by (auto simp:s_depend_def) with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (depend 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> depend s'" by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def) from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp'] show ?thesis by simp qed ultimately have "(Cs cs, Cs cs) \<in> (depend s)^+" by simp moreover note wf_trancl[OF wf_depend[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> depend s" by simp with depend_s have dps': "(Th th', z) \<in> depend 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> depend s'" by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def) from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this] show ?thesis . qed with dps depend_s show False by auto qed qed with depend_s yz have "(y, z) \<in> depend s'" by auto with ztp' show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto qed } from this[OF dp] show "x \<in> dependents (wq s') th''" by (auto simp:cs_dependents_def eq_depend)next fix x assume "x \<in> dependents (wq s') th''" hence dp: "(Th x, Th th'') \<in> (depend s')^+" by (auto simp:cs_dependents_def eq_depend) { fix n have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow> (n, Th th'') \<in> (depend s)^+" proof(induct rule:converse_trancl_induct) fix y assume "(y, Th th'') \<in> depend s'" with depend_s neq1 neq2 have "(y, Th th'') \<in> depend s" by auto thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto next fix y z assume yz: "(y, z) \<in> depend s'" and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+" and ztp': "(z, Th th'') \<in> (depend 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> depend 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> depend s'" by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def) from unique_depend[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> depend 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_depend_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> depend 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> depend s'" by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def) from unique_depend[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> (depend s')\<^sup>+" by simp from step_back_step[OF vt_s[unfolded s_def]] have cs_th: "(Cs cs, Th th) \<in> depend s'" by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def) have "(Cs cs, Th th'') \<notin> depend s'" proof assume "(Cs cs, Th th'') \<in> depend s'" from unique_depend[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> depend s'" and u_t: "(u, Th th'') \<in> (depend s')\<^sup>+" by auto have "u = Th th" proof - from unique_depend[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> (depend s')\<^sup>+" by simp from converse_tranclE[OF this] obtain v where "(Th th, v) \<in> (depend 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_depend_def s_waiting_def cs_waiting_def) qed qed with depend_s yz have "(y, z) \<in> depend s" by auto with ztp' show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto qed } from this[OF dp] show "x \<in> dependents (wq s) th''" by (auto simp:cs_dependents_def eq_depend)qedlemma cp_kept: fixes th'' assumes neq1: "th'' \<noteq> th" and neq2: "th'' \<noteq> th'" shows "cp s th'' = cp s' th''"proof - from dependents_kept[OF neq1 neq2] have "dependents (wq s) th'' = dependents (wq s') th''" . moreover { fix th1 assume "th1 \<in> dependents (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> dependents (wq s) th'')) = ((\<lambda>th. preced th s') ` ({th''} \<union> dependents (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> depend s'"proof assume "(Th th1, Cs cs) \<in> depend s'" thus "False" apply (auto simp:s_depend_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 depend_s: "depend s = depend s' - {(Cs cs, Th th)}"proof - from nnt and step_depend_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> depend s'" and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp with nw_cs eq_cs show False by auto qed with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s" and h2': "(Cs cs1, Th th2) \<in> depend 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> depend s'" and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp with nw_cs eq_cs show False by auto qed with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s" and h2': "(Cs cs1, Th th2) \<in> depend 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 depend_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 depend_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. dependents (wq s) th = dependents (wq s') th" apply (unfold cs_dependents_def, unfold eq_depend) 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_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}" by simp qed moreover { fix th1 assume "th1 \<in> {th'} \<union> dependents (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependents (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> dependents (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> dependents (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (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 depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"proof - from ee and step_depend_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> depend s'" and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp with ee show False by (auto simp:s_depend_def cs_waiting_def) qed with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s" and h2': "(Cs cs1, Th th2) \<in> depend 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> depend s'" and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp with ee show False by (auto simp:s_depend_def cs_waiting_def) qed with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s" and h2': "(Cs cs1, Th th2) \<in> depend 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 depend_s have "(n1, y) \<in> child s'" apply (auto simp:child_def) proof - fix th' assume "(Th th', Cs cs) \<in> depend s'" with ee have "False" by (auto simp:s_depend_def cs_waiting_def) thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto qed thus ?case by auto next case (step y z) have "(y, z) \<in> child s" by fact with depend_s have "(y, z) \<in> child s'" apply (auto simp:child_def) proof - fix th' assume "(Th th', Cs cs) \<in> depend s'" with ee have "False" by (auto simp:s_depend_def cs_waiting_def) thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend 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. dependents (wq s) th = dependents (wq s') th" apply (unfold cs_dependents_def, unfold eq_depend) 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_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}" by simp qed moreover { fix th1 assume "th1 \<in> {th'} \<union> dependents (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependents (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> dependents (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> dependents (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simpqedendcontext step_P_cps_nebeginlemma depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"proof - from step_depend_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> depend s" and h2: "(Cs cs1, Th th') \<in> depend 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 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'" and h2': "(Cs cs1, Th th') \<in> depend 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> depend s" and h2: "(Cs cs1, Th th2) \<in> depend 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 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'" and h2': "(Cs cs1, Th th2) \<in> depend 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 depend_s show ?case by (auto simp:child_def)next case (step y z) have "(y, z) \<in> child s'" by fact with depend_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> dependents 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_depend_eq[OF vt_s] have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp with nd show False by (simp add:s_dependents_def eq_depend) qed have eq_dp: "dependents (wq s) th' = dependents (wq s') th'" proof(auto) fix x assume " x \<in> dependents (wq s) th'" thus "x \<in> dependents (wq s') th'" apply (auto simp:cs_dependents_def eq_depend) proof - assume "(Th x, Th th') \<in> (depend s)\<^sup>+" with child_depend_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_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp qed next fix x assume "x \<in> dependents (wq s') th'" thus "x \<in> dependents (wq s) th'" apply (auto simp:cs_dependents_def eq_depend) proof - assume "(Th x, Th th') \<in> (depend s')\<^sup>+" with child_depend_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_depend_eq[OF vt_s] show "(Th x, Th th') \<in> (depend 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> dependents (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simpqedlemma eq_up: fixes th' th'' assumes dp1: "th \<in> dependents s th'" and dp2: "th' \<in> dependents 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> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def) from depend_child[OF vt_s this[unfolded eq_depend]] 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> (depend s)^+" by (auto simp:s_dependents_def eq_depend) moreover from child_depend_p[OF ch'] and eq_y have "(Th th', Th thy) \<in> (depend s)^+" by simp ultimately have dp_thy: "(Th th, Th thy) \<in> (depend 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> (depend 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> dependents s th1" proof assume h:"th \<in> dependents s th1" from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) from dependents_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 depend_set_unchanged, simp) apply (fold s_def, auto simp:depend_s) proof - assume "(Cs cs, Th th'') \<in> depend s'" with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend) from converse_tranclE[OF this] obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s" and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+" by (auto simp:s_depend_def) have eq_cs: "cs1 = cs" proof - from depend_s have "(Th th, Cs cs) \<in> depend s" by simp from unique_depend[OF vt_s this h1] show ?thesis by simp qed have False proof(rule converse_tranclE[OF h2]) assume "(Cs cs1, Th th') \<in> depend s" with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp from unique_depend[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> depend s" and ytd: " (y, Th th') \<in> (depend s)\<^sup>+" with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp from unique_depend[OF vt_s this cs_th'] have "y = Th th''" . with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp from depend_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> depend s' \<and> (Cs cs, Th th'') \<in> depend 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> (depend s)^+" by (auto simp:s_dependents_def eq_depend) 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> dependents s th1" proof assume "th \<in> dependents s th1" from dependents_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 depend_set_unchanged, simp) apply (fold s_def, auto simp:depend_s) proof - assume "(Cs cs, Th th'') \<in> depend s'" with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend) from converse_tranclE[OF this] obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s" and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+" by (auto simp:s_depend_def) have eq_cs: "cs1 = cs" proof - from depend_s have "(Th th, Cs cs) \<in> depend s" by simp from unique_depend[OF vt_s this h1] show ?thesis by simp qed have False proof(rule converse_tranclE[OF h2]) assume "(Cs cs1, Th th') \<in> depend s" with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp from unique_depend[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> depend s" and ytd: " (y, Th th') \<in> (depend s)\<^sup>+" with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp from unique_depend[OF vt_s this cs_th'] have "y = Th th''" . with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp from depend_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> depend s' \<and> (Cs cs, Th th'') \<in> depend 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: "depend s = depend s'" by (unfold s_def depend_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> dependents s th'" proof assume "th \<in> dependents s th'" hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend) with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp from converse_tranclE[OF this] obtain y where "(Th th, y) \<in> depend s'" by auto with dm_depend_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. dependents (wq s) th = dependents (wq s') th" by (unfold cs_dependents_def, auto simp:eq_dep eq_depend) moreover { fix th1 assume "th1 \<in> {th'} \<union> dependents (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependents (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> dependents (wq s') th'" with nd and eq_dp have "th1 \<noteq> th" by (auto simp:eq_depend cs_dependents_def s_dependents_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> dependents (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simpqedlemma nil_dependents: "dependents 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 "dependents s' th = {}" proof - { assume "dependents s' th \<noteq> {}" then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+" by (auto simp:s_dependents_def eq_depend) from tranclE[OF this] obtain cs' where "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def) with hdn have False by (auto simp:holdents_def) } thus ?thesis by auto qed thus ?thesis by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp) qedqedlemma eq_cp_th: "cp s th = preced th s" apply (unfold cp_eq_cpreced cpreced_def) by (insert nil_dependents, unfold s_dependents_def cs_dependents_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: "depend s = depend s'" by (unfold s_def depend_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> dependents s th'" proof assume "th \<in> dependents s th'" hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend) with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp from converse_tranclE[OF this] obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'" by (auto simp:s_depend_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_depend_def) by (auto simp:cs_waiting_def wq_def) qed qed have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th" by (unfold cs_dependents_def, auto simp:eq_dep eq_depend) moreover { fix th1 assume "th1 \<in> {th'} \<union> dependents (wq s') th'" hence "th1 = th' \<or> th1 \<in> dependents (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> dependents (wq s') th'" with nd and eq_dp have "th1 \<noteq> th" by (auto simp:eq_depend cs_dependents_def s_dependents_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> dependents (wq s) th')) = ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by (auto simp:image_def) thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simpqedendend