--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/CpsG.thy~ Thu Dec 03 14:34:29 2015 +0800
@@ -0,0 +1,1811 @@
+section {*
+ This file contains lemmas used to guide the recalculation of current precedence
+ after every system call (or system operation)
+*}
+theory CpsG
+imports PrioG Max RTree
+begin
+
+locale pip =
+ fixes s
+ assumes vt: "vt s"
+
+context pip
+begin
+
+interpretation rtree_RAG: rtree "RAG s"
+proof
+ show "single_valued (RAG s)"
+ by (unfold single_valued_def, auto intro: unique_RAG[OF vt])
+
+ show "acyclic (RAG s)"
+ by (rule acyclic_RAG[OF vt])
+qed
+
+thm rtree_RAG.rpath_overlap_oneside
+
+end
+
+
+
+definition "the_preced s th = preced th s"
+
+lemma cp_alt_def:
+ "cp s th =
+ Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+proof -
+ have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
+ Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+ (is "Max (_ ` ?L) = Max (_ ` ?R)")
+ proof -
+ have "?L = ?R"
+ by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
+ thus ?thesis by simp
+ qed
+ thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
+qed
+
+lemma eq_dependants: "dependants (wq s) = dependants s"
+ by (simp add: s_dependants_abv wq_def)
+
+(* obvious lemma *)
+lemma 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)
+ qed
+qed
+
+(* obvious lemma *)
+lemma 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
+ qed
+qed
+
+(* obvious lemma *)
+lemma next_th_unique:
+ assumes nt1: "next_th s th cs th1"
+ and nt2: "next_th s th cs th2"
+ shows "th1 = th2"
+using assms by (unfold next_th_def, auto)
+
+lemma 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)" .
+qed
+
+definition 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 simp
+
+lemma 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 simp
+qed
+
+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)
+ qed
+qed
+
+lemma 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)
+done
+
+lemma 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
+ qed
+qed
+
+lemma 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
+ qed
+qed
+
+text {* (* ddd *)
+*}
+lemma 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)
+
+text {* (* ddd *)
+*}
+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
+ qed
+qed
+
+text {* (* ddd *)
+*}
+lemma 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 auto
+qed
+
+text {* (* ddd *)
+*}
+lemma 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 auto
+qed
+
+lemma 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)
+
+text {* (* ddd *)
+*}
+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_def
+apply(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 auto
+
+lemma 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 metis
+
+lemma UN_exists:
+ shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
+by auto
+
+text {* (* ddd *)
+ This is the recursive equation used to compute the current precedence of
+ a thread (the @{text "th"}) here.
+*}
+lemma 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" .
+ qed
+qed
+
+lemma 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
+ qed
+qed
+
+-- {* A useless definition *}
+definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
+where "cps s = {(th, cp s th) | th . th \<in> threads s}"
+
+
+text {* (* ddd *)
+ One beauty of our modelling is that we follow the definitional extension tradition of HOL.
+ The benefit of such a concise and miniature model is that large number of intuitively
+ obvious facts are derived as lemmas, rather than asserted as axioms.
+*}
+
+text {*
+ However, the lemmas in the forthcoming several locales are no longer
+ obvious. These lemmas show how the current precedences should be recalculated
+ after every execution step (in our model, every step is represented by an event,
+ which in turn, represents a system call, or operation). Each operation is
+ treated in a separate locale.
+
+ The complication of current precedence recalculation comes
+ because the changing of RAG needs to be taken into account,
+ in addition to the changing of precedence.
+ The reason RAG changing affects current precedence is that,
+ according to the definition, current precedence
+ of a thread is the maximum of the precedences of its dependants,
+ where the dependants are defined in terms of RAG.
+
+ Therefore, each operation, lemmas concerning the change of the precedences
+ and RAG are derived first, so that the lemmas about
+ current precedence recalculation can be based on.
+*}
+
+text {* (* ddd *)
+ The following locale @{text "step_set_cps"} investigates the recalculation
+ after the @{text "Set"} operation.
+*}
+locale step_set_cps =
+ fixes s' th prio s
+ -- {* @{text "s'"} is the system state before the operation *}
+ -- {* @{text "s"} is the system state after the operation *}
+ defines s_def : "s \<equiv> (Set th prio#s')"
+ -- {* @{text "s"} is assumed to be a legitimate state, from which
+ the legitimacy of @{text "s"} can be derived. *}
+ assumes vt_s: "vt s"
+
+context step_set_cps
+begin
+
+interpretation h: pip "s"
+ by (unfold pip_def, insert vt_s, simp)
+
+find_theorems
+
+(* *)
+
+text {* (* ddd *)
+ The following lemma confirms that @{text "Set"}-operating only changes the precedence
+ of initiating thread.
+*}
+
+lemma 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)
+qed
+
+text {* (* ddd *)
+ The following lemma assures that the resetting of priority does not change the RAG.
+*}
+
+lemma eq_dep: "RAG s = RAG s'"
+ by (unfold s_def RAG_set_unchanged, auto)
+
+text {*
+ Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation.
+ It says, thread other than the initiating thread @{text "th"} does not need recalculation
+ unless it lies upstream of @{text "th"} in the RAG.
+
+ The reason behind this lemma is that:
+ the change of precedence of one thread can only affect it's upstream threads, according to
+ lemma @{text "eq_preced"}. Since the only thread which might change precedence is
+ @{text "th"}, so only @{text "th"} and its upstream threads need recalculation.
+ (* ccc *)
+*}
+
+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'"
+proof -
+ -- {* This is what we need to prove after expanding the definition of @{text "cp"} *}
+ have "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
+ (is "Max (?f1 ` ({th'} \<union> ?A)) = Max (?f2 ` ({th'} \<union> ?B))")
+ proof -
+ -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of
+ any threads are not changed, this is one of key facts underpinning this
+ lemma *}
+ have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
+ have "(?f1 ` ({th'} \<union> ?A)) = (?f2 ` ({th'} \<union> ?B))"
+ proof(rule image_cong)
+ show "{th'} \<union> ?A = {th'} \<union> ?B" by (simp only:eq_ab)
+ next
+ fix x
+ assume x_in: "x \<in> {th'} \<union> ?B"
+ show "?f1 x = ?f2 x"
+ proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *}
+ from x_in[folded eq_ab, unfolded eq_dependants]
+ have "x \<in> {th'} \<union> dependants s th'" .
+ thus "x \<noteq> th"
+ proof
+ assume "x \<in> {th'}"
+ with `th' \<noteq> th` show ?thesis by simp
+ next
+ assume "x \<in> dependants s th'"
+ with `th \<notin> dependants s th'` show ?thesis by auto
+ qed
+ qed
+ qed
+ thus ?thesis by simp
+ qed
+ thus ?thesis by (unfold cp_eq_cpreced cpreced_def)
+qed
+
+text {*
+ The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}.
+ The reason for this is that only no-blocked thread can initiate
+ a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any
+ critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG.
+ Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}.
+*}
+lemma no_dependants:
+ shows "th \<notin> dependants s th'"
+proof
+ assume "th \<in> dependants s th'"
+ from `th \<in> dependants s th'` 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
+ moreover have "th \<in> readys s'"
+ proof -
+ from step_back_step [OF vt_s[unfolded s_def]]
+ have "step s' (Set th prio)" .
+ hence "th \<in> runing s'" by (cases, simp)
+ thus ?thesis by (simp add:readys_def runing_def)
+ qed
+ ultimately show "False"
+ apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
+ by (fold wq_def, blast)
+qed
+
+(* Result improved *)
+text {*
+ A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"}
+ gives the main lemma of this locale, which shows that
+ only the initiating thread needs a recalculation of current precedence.
+*}
+lemma eq_cp:
+ fixes th'
+ assumes "th' \<noteq> th"
+ shows "cp s th' = cp s' th'"
+ by (rule eq_cp_pre[OF assms no_dependants])
+
+end
+
+text {*
+ The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
+*}
+
+locale step_v_cps =
+ -- {* @{text "th"} is the initiating thread *}
+ -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}
+ fixes s' th cs s -- {* @{text "s'"} is the state before operation*}
+ defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}
+ -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
+ assumes vt_s: "vt s"
+
+text {*
+ The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation,
+ which represents the case when there is another thread @{text "th'"}
+ to take over the critical resource released by the initiating thread @{text "th"}.
+*}
+locale step_v_cps_nt = step_v_cps +
+ fixes th'
+ -- {* @{text "th'"} is assumed to take over @{text "cs"} *}
+ assumes nt: "next_th s' th cs th'"
+
+context step_v_cps_nt
+begin
+
+text {*
+ Lemma @{text "RAG_s"} confirms the change of RAG:
+ two edges removed and one added, as shown by the following diagram.
+*}
+
+(*
+ RAG before the V-operation
+ th1 ----|
+ |
+ th' ----|
+ |----> cs -----|
+ th2 ----| |
+ | |
+ th3 ----| |
+ |------> th
+ th4 ----| |
+ | |
+ th5 ----| |
+ |----> cs'-----|
+ th6 ----|
+ |
+ th7 ----|
+
+ RAG after the V-operation
+ th1 ----|
+ |
+ |----> cs ----> th'
+ th2 ----|
+ |
+ th3 ----|
+
+ th4 ----|
+ |
+ th5 ----|
+ |----> cs'----> th
+ th6 ----|
+ |
+ th7 ----|
+*)
+
+lemma 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)
+qed
+
+text {*
+ Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"}
+ have their dependants changed.
+*}
+lemma 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) (* ccc *)
+ 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)
+qed
+
+lemma 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)
+qed
+
+end
+
+locale step_v_cps_nnt = step_v_cps +
+ assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"
+
+context step_v_cps_nnt
+begin
+
+lemma 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
+ qed
+qed
+
+lemma 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 auto
+qed
+
+lemma 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
+ qed
+qed
+
+lemma 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
+ qed
+qed
+
+lemma 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 simp
+qed
+
+end
+
+locale 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_e
+begin
+
+lemma 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 auto
+qed
+
+lemma 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
+ qed
+qed
+
+lemma 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
+ qed
+qed
+
+lemma 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 simp
+qed
+
+end
+
+context step_P_cps_ne
+begin
+
+lemma 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)
+qed
+
+
+lemma 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 auto
+qed
+
+lemma 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 auto
+qed
+
+lemma 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 simp
+qed
+
+lemma 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 auto
+qed
+
+end
+
+locale 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_cps
+begin
+
+lemma 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 simp
+qed
+
+lemma 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)
+ qed
+qed
+
+lemma 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)
+
+end
+
+
+locale step_exit_cps =
+ fixes s' th prio s
+ defines s_def : "s \<equiv> Exit th # s'"
+ assumes vt_s: "vt s"
+
+context step_exit_cps
+begin
+
+lemma 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 simp
+qed
+
+end
+end
+