pip: comparison CpsG.thy

equal deleted inserted replaced

-:313acffe63b6
+:92f61f6a0fe7
 theory CpsG
-imports PrioG
+imports PrioG Max
 begin
 lemma not_thread_holdents:
 fixes th s
 assumes vt: "vt s"
 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:depend_create_unchanged)
+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
 show ?thesis
 proof(cases "th = thread")
 case True
 with nh eq_e
 show ?thesis
-by (auto simp:holdents_test depend_exit_unchanged)
+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 depend_exit_unchanged)
+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"
 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_depend_p[OF vtp], auto)
+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
 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_depend_v[OF vtv], auto)
+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
 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:depend_set_unchanged)
+by (simp add:RAG_set_unchanged)
 qed
 next
 case vt_nil
 show ?case
-by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
+by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
 qed
 qed
 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_depend:
+lemma wf_RAG:
 assumes vt: "vt s"
-shows "wf (depend s)"
+shows "wf (RAG s)"
 proof(rule finite_acyclic_wf)
-from finite_depend[OF vt] show "finite (depend s)" .
+from finite_RAG[OF vt] show "finite (RAG s)" .
 next
-from acyclic_depend[OF vt] show "acyclic (depend s)" .
+from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
-lemma 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
-qed
-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> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+{(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> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+"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"
+lemma children_dependants:
-by (unfold children_def child_def cs_dependants_def, auto simp:eq_depend)
+"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> depend s"
+assume h1: "(Th th, Cs cs) \<in> RAG s"
-and h2: "(Cs cs, Th th1) \<in> depend s"
+and h2: "(Cs cs, Th th1) \<in> RAG s"
-and h3: "(Th th, Cs csa) \<in> depend s"
+and h3: "(Th th, Cs csa) \<in> RAG s"
-and h4: "(Cs csa, Th th2) \<in> depend s"
+and h4: "(Cs csa, Th th2) \<in> RAG s"
-from unique_depend[OF vt h1 h3] have "cs = csa" by simp
+from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
-with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
+with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
-from unique_depend[OF vt h2 this]
+from unique_RAG[OF vt h2 this]
 show "th1 = th2" by simp
 qed
-lemma depend_children:
+lemma RAG_children:
-assumes h: "(Th th1, Th th2) \<in> (depend s)^+"
+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> (depend 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> (depend s)\<^sup>+"
+assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
-and h2: "(c, Th th2) \<in> depend s"
+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_depend_def)
+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> (depend s)\<^sup>+)"
+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> (depend s)\<^sup>+"
+assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
-and h4: "(ca, c) \<in> depend s"
+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> (depend s)\<^sup>+)"
+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_depend_def)
+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> (depend s)\<^sup>+" by simp
+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> depend s"
+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> depend s"
+assume "(Th th1, Th th2) \<in> RAG s"
 thus ?thesis
-by (auto simp:s_depend_def)
+by (auto simp:s_RAG_def)
 qed
 qed
-lemma sub_child: "child s \<subseteq> (depend s)^+"
+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_depend[OF vt]])
+apply(rule wf_trancl[OF wf_RAG[OF vt]])
 apply(rule sub_child)
 done
-lemma depend_child_pre:
+lemma RAG_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")
+"(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_depend[OF vt]]
+from wf_trancl[OF wf_RAG[OF vt]]
-have wf: "wf ((depend s)^+)" .
+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> (depend s)\<^sup>+ \<longrightarrow>
+assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG 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>+)"
+(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> (depend s)\<^sup>+"
+and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
 show "(Th th, Th th') \<in> (child s)\<^sup>+"
 proof -
-from depend_children[OF h]
+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> (depend s)\<^sup>+)" .
+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> (depend s)\<^sup>+"
+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> (depend s)\<^sup>+" by auto
+and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
-from th3_in have "(Th th3, Th th') \<in> (depend s)^+" by (auto simp:children_def child_def)
+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 depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
-by (insert depend_child_pre, auto)
+by (insert RAG_child_pre, auto)
-lemma child_depend_p:
+lemma child_RAG_p:
 assumes "(n1, n2) \<in> (child s)^+"
-shows "(n1, n2) \<in> (depend 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> (depend s)^+" by auto
+with sub_child have "(y, z) \<in> (RAG s)^+" by auto
-moreover have "(n1, y) \<in> (depend s)^+" by fact
+moreover have "(n1, y) \<in> (RAG s)^+" by fact
 ultimately show ?case by auto
 qed
 qed
-lemma child_depend_eq:
+lemma child_RAG_eq:
 assumes vt: "vt s"
-shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (depend s)^+"
+shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
-by (auto intro: depend_child[OF vt] child_depend_p)
+by (auto intro: RAG_child[OF vt] child_RAG_p)
 lemma children_no_dep:
 fixes s th th1 th2 th3
 assumes vt: "vt s"
 and ch1: "(Th th1, Th th) \<in> child s"
 and ch2: "(Th th2, Th th) \<in> child s"
-and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
+and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
 shows "False"
 proof -
-from depend_child[OF vt ch3]
+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
 qed
 ultimately show False by auto
 qed
 qed
-lemma unique_depend_p:
+lemma unique_RAG_p:
 assumes vt: "vt s"
-and dp1: "(n, n1) \<in> (depend s)^+"
+and dp1: "(n, n1) \<in> (RAG s)^+"
-and dp2: "(n, n2) \<in> (depend s)^+"
+and dp2: "(n, n2) \<in> (RAG s)^+"
 and neq: "n1 \<noteq> n2"
-shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"
+shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
 proof(rule unique_chain [OF _ dp1 dp2 neq])
-from unique_depend[OF vt]
+from unique_RAG[OF vt]
-show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
+show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 qed
 lemma dependants_child_unique:
 fixes s th th1 th2 th3
 assumes vt: "vt 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> (depend s)^+"
+from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+"
-by (simp add:s_dependants_def eq_depend)
+by (simp add:s_dependants_def eq_RAG)
-from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+"
+from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+"
-by (simp add:s_dependants_def eq_depend)
+by (simp add:s_dependants_def eq_RAG)
-from unique_depend_p[OF vt dp1 dp2] and neq
+from unique_RAG_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
+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> (depend s)\<^sup>+ "
+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> (depend s)\<^sup>+"
+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 depend_plus_elim:
+lemma RAG_plus_elim:
 assumes "vt s"
 fixes x
-assumes "(Th x, Th th) \<in> (depend (wq s))\<^sup>+"
+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> (depend (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_depend, folded child_depend_eq[OF `vt s`]]
+using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
 apply (unfold children_def)
-by (metis assms(2) children_def depend_children eq_depend)
+by (metis assms(2) children_def RAG_children eq_RAG)
-lemma dependants_expand_pre:
-assumes "vt s"
-shows "dependants (wq s) th = (\<Union> th' \<in> children s th. {th'} \<union> dependants (wq s) th')"
-apply (unfold cs_dependants_def)
-apply (auto elim!:depend_plus_elim[OF assms])
-apply (metis children_def eq_depend mem_Collect_eq set_mp sub_child)
-apply (unfold children_def, auto)
-apply (unfold eq_depend, fold  child_depend_eq[OF `vt s`])
-by (metis trancl.simps)
 lemma dependants_expand:
 assumes "vt s"
-shows "dependants (wq s) th = (\<Union> ((\<lambda> th. {th} \<union> dependants (wq s) th) ` (children s th)))"
+shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-apply (subst dependants_expand_pre[OF assms])
+apply(simp add: image_def)
-by simp
+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]
 assumes "vt s"
 shows "finite (dependants (wq s) th')"
 using dependants_threads[OF assms] finite_threads[OF assms]
 by (metis rev_finite_subset)
-lemma Max_insert:
-assumes "finite B"
-and  "B \<noteq> {}"
-shows "Max ({x} \<union> B) = max x (Max B)"
-by (metis Max_insert assms insert_is_Un)
-lemma dependands_expand2:
-assumes "vt s"
-shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-by (subst dependants_expand[OF assms]) (auto)
 abbreviation
-"preceds s Ths \<equiv> {preced th s| th. th \<in> Ths}"
+"preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
-lemma image_compr:
+abbreviation
-"f ` A = {f x | x. x \<in> A}"
+"cpreceds s ths \<equiv> (cp s) ` ths"
-by auto
 lemma Un_compr:
 "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
 by auto
 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_compr[symmetric])
+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 dependands_expand2[OF assms] by(auto simp only: Un_empty)
+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`])
 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 dependands_expand2[OF `vt s`]) (simp)
+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
 proof -
 from assms show ?thesis
 by (unfold s_def, auto simp:preced_def)
 qed
-lemma eq_dep: "depend s = depend s'"
+lemma eq_dep: "RAG s = RAG s'"
-by (unfold s_def depend_set_unchanged, auto)
+by (unfold s_def RAG_set_unchanged, auto)
 lemma eq_cp_pre:
 fixes th'
 assumes neq_th: "th' \<noteq> th"
 and nd: "th \<notin> dependants s th'"
 shows "cp s th' = cp s' th'"
 apply (unfold cp_eq_cpreced cpreced_def)
 proof -
 have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
+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'"
 with eq_preced[OF neq_th]
 show "preced th1 s = preced th1 s'" by simp
 next
 assume "th1 \<in> dependants (wq s') th'"
 with nd and eq_dp have "th1 \<noteq> th"
-by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
+by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
 from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
 qed
 } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
 ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
 by (auto simp:image_def)
 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>+"
+from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
-by (unfold s_dependants_def, unfold eq_depend, unfold eq_dep, auto)
+by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
 from tranclD[OF this]
-obtain z where "(Th th, z) \<in> depend s'" by auto
+obtain z where "(Th th, z) \<in> RAG s'" by auto
 with rd_th show "False"
-apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def)
+apply (case_tac z, auto simp:readys_def s_waiting_def s_RAG_def s_waiting_def cs_waiting_def)
 by (fold wq_def, blast)
 qed
 (* Result improved *)
 lemma eq_cp:
 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> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
+have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
-from depend_child[OF vt_s this[unfolded eq_depend]]
+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)
 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_dependants_def eq_depend)
+from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
-moreover from child_depend_p[OF ch'] and eq_y
+moreover from child_RAG_p[OF ch'] and eq_y
-have "(Th th', Th thy) \<in> (depend s)^+" by simp
+have "(Th th', Th thy) \<in> (RAG s)^+" by simp
-ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
+ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
 show "cp s th'' = cp s' th''"
 apply (subst cp_rec[OF vt_s])
 proof -
 have "preced th'' s = preced th'' s'"
 proof(rule eq_preced)
 show "th'' \<noteq> th"
 proof
 assume "th'' = th"
 with dp_thy y_ch[unfolded eq_y]
-have "(Th th, Th th) \<in> (depend s)^+"
+have "(Th th, Th th) \<in> (RAG s)^+"
 by (auto simp:child_def)
-with wf_trancl[OF wf_depend[OF vt_s]]
+with wf_trancl[OF wf_RAG[OF vt_s]]
 show False by auto
 qed
 qed
 moreover {
 fix th1
 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
+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_depend)
+from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
 from dependants_child_unique[OF vt_s _ _ h this]
 th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
 with False show False by auto
 qed
 from eq_cp_pre[OF neq_th1 this]
 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)
+by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 qed
 next
 fix th''
 proof(rule eq_preced)
 show "th'' \<noteq> th"
 proof
 assume "th'' = th"
 with dp1 dp'
-have "(Th th, Th th) \<in> (depend s)^+"
+have "(Th th, Th th) \<in> (RAG s)^+"
-by (auto simp:child_def s_dependants_def eq_depend)
+by (auto simp:child_def s_dependants_def eq_RAG)
-with wf_trancl[OF wf_depend[OF vt_s]]
+with wf_trancl[OF wf_RAG[OF vt_s]]
 show False by auto
 qed
 qed
 moreover {
 fix th1
 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)^+"
+with dp1 have "(Th th1, Th th') \<in> (RAG s)^+"
-by (auto simp:s_dependants_def eq_depend)
+by (auto simp:s_dependants_def eq_RAG)
 from children_no_dep[OF vt_s _ _ this]
 th1_in dp'
 show False by (auto simp:children_def)
 qed
 thus ?thesis
 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)
+by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 qed
 qed
 }
 assumes dp: "th \<in> dependants s th''"
 and eq_cps: "cp s th = cp s' th"
 shows "cp s th'' = cp s' th''"
 proof -
 from dp
-have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
+have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
-from depend_child[OF vt_s this[unfolded eq_depend]]
+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)
 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
+from child_RAG_p[OF ch'] and eq_y
-have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by simp
+have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
 show "cp s th'' = cp s' th''"
 apply (subst cp_rec[OF vt_s])
 proof -
 have "preced th'' s = preced th'' s'"
 proof(rule eq_preced)
 show "th'' \<noteq> th"
 proof
 assume "th'' = th"
 with dp_thy y_ch[unfolded eq_y]
-have "(Th th, Th th) \<in> (depend s)^+"
+have "(Th th, Th th) \<in> (RAG s)^+"
 by (auto simp:child_def)
-with wf_trancl[OF wf_depend[OF vt_s]]
+with wf_trancl[OF wf_RAG[OF vt_s]]
 show False by auto
 qed
 qed
 moreover {
 fix th1
 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
+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_depend)
+from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
 from dependants_child_unique[OF vt_s _ _ h this]
 th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
 with False show False by auto
 qed
 from eq_cp_pre[OF neq_th1 this]
 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)
+by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 qed
 next
 fix th''
 proof(rule eq_preced)
 show "th'' \<noteq> th"
 proof
 assume "th'' = th"
 with dp dp'
-have "(Th th, Th th) \<in> (depend s)^+"
+have "(Th th, Th th) \<in> (RAG s)^+"
-by (auto simp:child_def s_dependants_def eq_depend)
+by (auto simp:child_def s_dependants_def eq_RAG)
-with wf_trancl[OF wf_depend[OF vt_s]]
+with wf_trancl[OF wf_RAG[OF vt_s]]
 show False by auto
 qed
 qed
 moreover {
 fix th1
 thus ?thesis
 proof(rule eq_cp_pre)
 show "th \<notin> dependants s th1"
 proof
 assume "th \<in> dependants s th1"
-hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
+hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
 from children_no_dep[OF vt_s _ _ this]
 and th1_in dp' show False
 by (auto simp:children_def)
 qed
 qed
 qed
 }
 ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
 {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
 moreover have "children s th'' = children s' th''"
-by (unfold children_def child_def s_def depend_set_unchanged, simp)
+by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 qed
 qed
 }
 assumes nt: "next_th s' th cs th'"
 context step_v_cps_nt
 begin
-lemma depend_s:
+lemma RAG_s:
-"depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
+"RAG s = (RAG 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]
+from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
 and nt show ?thesis  by (auto intro:next_th_unique)
 qed
 lemma dependants_kept:
 fixes th''
 and neq2: "th'' \<noteq> th'"
 shows "dependants (wq s) th'' = dependants (wq s') th''"
 proof(auto)
 fix x
 assume "x \<in> dependants (wq s) th''"
-hence dp: "(Th x, Th th'') \<in> (depend s)^+"
+hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
-by (auto simp:cs_dependants_def eq_depend)
+by (auto simp:cs_dependants_def eq_RAG)
 { fix n
-have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s')^+"
+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> depend s"
+assume "(y, Th th'') \<in> RAG s"
-with depend_s neq1 neq2
+with RAG_s neq1 neq2
-have "(y, Th th'') \<in> depend s'" by auto
+have "(y, Th th'') \<in> RAG s'" by auto
-thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
 next
 fix y z
-assume yz: "(y, z) \<in> depend s"
+assume yz: "(y, z) \<in> RAG s"
-and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+"
+and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+"
-and ztp': "(z, Th th'') \<in> (depend 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> depend s" by simp
+with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp
-from depend_s
+from RAG_s
-have cst': "(Cs cs, Th th') \<in> depend s" by simp
+have cst': "(Cs cs, Th th') \<in> RAG s" by simp
-from unique_depend[OF vt_s this dp_yz]
+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> (depend s)^+" 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> depend s"
+obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s"
-by (auto simp:s_depend_def)
+by (auto simp:s_RAG_def)
-with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto
+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> (depend 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> depend s'"
+have "(Th th', Cs cs) \<in> RAG s'"
-by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
+by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
-from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
+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> (depend s)^+" by simp
+ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp
-moreover note wf_trancl[OF wf_depend[OF vt_s]]
+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> depend s" by simp
+with yz have dps: "(Th th', z) \<in> RAG s" by simp
-with depend_s have dps': "(Th th', z) \<in> depend s'" by auto
+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> depend s'"
+have "(Th th', Cs cs) \<in> RAG s'"
-by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
+by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
-from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
+from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
 show ?thesis .
 qed
-with dps depend_s show False by auto
+with dps RAG_s show False by auto
 qed
 qed
-with depend_s yz have "(y, z) \<in> depend s'" by auto
+with RAG_s yz have "(y, z) \<in> RAG s'" by auto
 with ztp'
-show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+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_depend)
+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> (depend s')^+"
+hence dp: "(Th x, Th th'') \<in> (RAG s')^+"
-by (auto simp:cs_dependants_def eq_depend)
+by (auto simp:cs_dependants_def eq_RAG)
 { fix n
-have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s)^+"
+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> depend s'"
+assume "(y, Th th'') \<in> RAG s'"
-with depend_s neq1 neq2
+with RAG_s neq1 neq2
-have "(y, Th th'') \<in> depend s" by auto
+have "(y, Th th'') \<in> RAG s" by auto
-thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
 next
 fix y z
-assume yz: "(y, z) \<in> depend s'"
+assume yz: "(y, z) \<in> RAG s'"
-and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+"
+and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+"
-and ztp': "(z, Th th'') \<in> (depend 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> depend s'" by simp
+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> depend s'"
+have "(Cs cs, Th th) \<in> RAG s'"
-by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
+by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def)
-from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
+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> depend s'" by auto
+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_depend_def s_waiting_def cs_waiting_def)
+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> depend s'" by simp
+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> depend s'"
+have "(Th th', Cs cs) \<in> RAG s'"
-by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
+by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
-from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
+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>  (depend s')\<^sup>+" by simp
+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> depend s'"
+have cs_th: "(Cs cs, Th th) \<in> RAG s'"
-by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
+by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def)
-have "(Cs cs, Th th'') \<notin>  depend s'"
+have "(Cs cs, Th th'') \<notin>  RAG s'"
 proof
-assume "(Cs cs, Th th'') \<in> depend s'"
+assume "(Cs cs, Th th'') \<in> RAG s'"
-from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
+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> depend s'"
+obtain u where cu: "(Cs cs, u) \<in> RAG s'"
-and u_t: "(u, Th th'') \<in> (depend s')\<^sup>+" by auto
+and u_t: "(u, Th th'') \<in> (RAG 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]
+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> (depend s')\<^sup>+" by simp
+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> (depend s')" by auto
+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_depend_def s_waiting_def cs_waiting_def)
+by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
 qed
 qed
-with depend_s yz have "(y, z) \<in> depend s" by auto
+with RAG_s yz have "(y, z) \<in> RAG s" by auto
 with ztp'
-show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+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_depend)
+by (auto simp:cs_dependants_def eq_RAG)
 qed
 lemma cp_kept:
 fixes th''
 assumes neq1: "th'' \<noteq> th"
 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> depend s'"
+lemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"
 proof
-assume "(Th th1, Cs cs) \<in> depend s'"
+assume "(Th th1, Cs cs) \<in> RAG s'"
 thus "False"
-apply (auto simp:s_depend_def cs_waiting_def)
+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"
 with nnt show ?thesis by auto
 qed
 qed
 qed
-lemma depend_s: "depend s = depend s' - {(Cs cs, Th th)}"
+lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"
 proof -
-from nnt and  step_depend_v[OF vt_s[unfolded s_def], folded s_def]
+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
 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'"
+where h1: "(Th th1, Cs cs1) \<in> RAG s'"
-and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp
+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 depend_s have
+with h1 h2 RAG_s have
-h1': "(Th th1, Cs cs1) \<in> depend s" and
+h1': "(Th th1, Cs cs1) \<in> RAG s" and
-h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+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> depend s'"
+where h1: "(Th th1, Cs cs1) \<in> RAG s'"
-and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp
+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 depend_s have
+with h1 h2 RAG_s have
-h1': "(Th th1, Cs cs1) \<in> depend s" and
+h1': "(Th th1, Cs cs1) \<in> RAG s" and
-h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+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
 shows "(n1, n2) \<in> (child s')^+"
 proof -
 from assms show ?thesis
 proof(induct)
 case (base y)
-from base and depend_s
+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 depend_s have "(y, z) \<in> child s'"
+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
 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_depend)
+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_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+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> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+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'"
 assumes ee: "wq s' cs = []"
 context step_P_cps_e
 begin
-lemma depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"
+lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"
 proof -
-from ee and  step_depend_p[OF vt_s[unfolded s_def], folded s_def]
+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
 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'"
+where h1: "(Th th1, Cs cs1) \<in> RAG s'"
-and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp
+with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
 with ee show False
-by (auto simp:s_depend_def cs_waiting_def)
+by (auto simp:s_RAG_def cs_waiting_def)
 qed
-with h1 h2 depend_s have
+with h1 h2 RAG_s have
-h1': "(Th th1, Cs cs1) \<in> depend s" and
+h1': "(Th th1, Cs cs1) \<in> RAG s" and
-h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+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> depend s'"
+where h1: "(Th th1, Cs cs1) \<in> RAG s'"
-and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp
+with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
 with ee show False
-by (auto simp:s_depend_def cs_waiting_def)
+by (auto simp:s_RAG_def cs_waiting_def)
 qed
-with h1 h2 depend_s have
+with h1 h2 RAG_s have
-h1': "(Th th1, Cs cs1) \<in> depend s" and
+h1': "(Th th1, Cs cs1) \<in> RAG s" and
-h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+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
 shows "(n1, n2) \<in> (child s')^+"
 proof -
 from assms show ?thesis
 proof(induct)
 case (base y)
-from base and depend_s
+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> depend s'"
+assume "(Th th', Cs cs) \<in> RAG s'"
 with ee have "False"
-by (auto simp:s_depend_def cs_waiting_def)
+by (auto simp:s_RAG_def cs_waiting_def)
-thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto
+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 depend_s have "(y, z) \<in> child s'"
+with RAG_s have "(y, z) \<in> child s'"
 apply (auto simp:child_def)
 proof -
 fix th'
-assume "(Th th', Cs cs) \<in> depend s'"
+assume "(Th th', Cs cs) \<in> RAG s'"
 with ee have "False"
-by (auto simp:s_depend_def cs_waiting_def)
+by (auto simp:s_RAG_def cs_waiting_def)
-thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto
+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
 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_depend)
+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_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+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> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+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'"
 end
 context step_P_cps_ne
 begin
-lemma depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"
+lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
 proof -
-from step_depend_p[OF vt_s[unfolded s_def]] and ne
+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> depend s"
+where h1: "(Th th1, Cs cs1) \<in> RAG s"
-and h2: "(Cs cs1, Th th') \<in> depend 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 depend_s
+with h1 h2 RAG_s
-have h1': "(Th th1, Cs cs1) \<in> depend s'" and
+have h1': "(Th th1, Cs cs1) \<in> RAG s'" and
-h2': "(Cs cs1, Th th') \<in> depend s'" by auto
+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> depend s"
+where h1: "(Th th1, Cs cs1) \<in> RAG s"
-and h2: "(Cs cs1, Th th2) \<in> depend 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 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'"
+with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"
-and h2': "(Cs cs1, Th th2) \<in> depend s'" by auto
+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 depend_s show ?case by (auto simp:child_def)
+with RAG_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)
+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:
 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]
+with child_RAG_eq[OF vt_s]
-have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp
+have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp
 with nd show False
-by (simp add:s_dependants_def eq_depend)
+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_depend)
+apply (auto simp:cs_dependants_def eq_RAG)
 proof -
-assume "(Th x, Th th') \<in> (depend s)\<^sup>+"
+assume "(Th x, Th th') \<in> (RAG s)\<^sup>+"
-with  child_depend_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
+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_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
-show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
+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_depend)
+apply (auto simp:cs_dependants_def eq_RAG)
 proof -
-assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
+assume "(Th x, Th th') \<in> (RAG s')\<^sup>+"
-with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+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_depend_eq[OF vt_s]
+with  child_RAG_eq[OF vt_s]
-show "(Th x, Th th') \<in> (depend s)\<^sup>+" by simp
+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')) =
 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> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
+have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
-from depend_child[OF vt_s this[unfolded eq_depend]]
+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'')"
 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_dependants_def eq_depend)
+from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
-moreover from child_depend_p[OF ch'] and eq_y
+moreover from child_RAG_p[OF ch'] and eq_y
-have "(Th th', Th thy) \<in> (depend s)^+" by simp
+have "(Th th', Th thy) \<in> (RAG s)^+" by simp
-ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
+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)
 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
+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_depend)
+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]
 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 (unfold children_def child_def s_def RAG_set_unchanged, simp)
-apply (fold s_def, auto simp:depend_s)
+apply (fold s_def, auto simp:RAG_s)
 proof -
-assume "(Cs cs, Th th'') \<in> depend s'"
+assume "(Cs cs, Th th'') \<in> RAG s'"
-with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
+with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
-from dp1 have "(Th th, Th th') \<in> (depend s)^+"
+from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
-by (auto simp:s_dependants_def eq_depend)
+by (auto simp:s_dependants_def eq_RAG)
 from converse_tranclE[OF this]
-obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
+obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
-and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
+and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
-by (auto simp:s_depend_def)
+by (auto simp:s_RAG_def)
 have eq_cs: "cs1 = cs"
 proof -
-from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
+from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
-from unique_depend[OF vt_s this h1]
+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> depend s"
+assume "(Cs cs1, Th th') \<in> RAG s"
-with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
+with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
-from unique_depend[OF vt_s this cs_th']
+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> depend s"
+assume "(Cs cs1, y) \<in> RAG s"
-and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
+and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
-with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
+with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
-from unique_depend[OF vt_s this cs_th']
+from unique_RAG[OF vt_s this cs_th']
 have "y = Th th''" .
-with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
+with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
-from depend_child[OF vt_s this]
+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> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
+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
 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)^+"
+with dp1 have "(Th th1, Th th') \<in> (RAG s)^+"
-by (auto simp:s_dependants_def eq_depend)
+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
 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 (unfold children_def child_def s_def RAG_set_unchanged, simp)
-apply (fold s_def, auto simp:depend_s)
+apply (fold s_def, auto simp:RAG_s)
 proof -
-assume "(Cs cs, Th th'') \<in> depend s'"
+assume "(Cs cs, Th th'') \<in> RAG s'"
-with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
+with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
-from dp1 have "(Th th, Th th') \<in> (depend s)^+"
+from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
-by (auto simp:s_dependants_def eq_depend)
+by (auto simp:s_dependants_def eq_RAG)
 from converse_tranclE[OF this]
-obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
+obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
-and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
+and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
-by (auto simp:s_depend_def)
+by (auto simp:s_RAG_def)
 have eq_cs: "cs1 = cs"
 proof -
-from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
+from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
-from unique_depend[OF vt_s this h1]
+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> depend s"
+assume "(Cs cs1, Th th') \<in> RAG s"
-with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
+with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
-from unique_depend[OF vt_s this cs_th']
+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> depend s"
+assume "(Cs cs1, y) \<in> RAG s"
-and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
+and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
-with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
+with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
-from unique_depend[OF vt_s this cs_th']
+from unique_RAG[OF vt_s this cs_th']
 have "y = Th th''" .
-with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
+with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
-from depend_child[OF vt_s this]
+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> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
+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
 assumes vt_s: "vt s"
 context step_create_cps
 begin
-lemma eq_dep: "depend s = depend s'"
+lemma eq_dep: "RAG s = RAG s'"
-by (unfold s_def depend_create_unchanged, auto)
+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> (depend s)^+" by (simp add:s_dependants_def eq_depend)
+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> (depend s')^+" by simp
+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> depend s'" by auto
+obtain y where "(Th th, y) \<in> RAG s'" by auto
-with dm_depend_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
+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_depend)
+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'"
 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_depend cs_dependants_def s_dependants_def eq_dep)
+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)
 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> (depend s')^+"
+then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+"
-by (auto simp:s_dependants_def eq_depend)
+by (auto simp:s_dependants_def eq_RAG)
 from tranclE[OF this] obtain cs' where
-"(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
+"(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_depend depend_create_unchanged, simp)
+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)
 assumes vt_s: "vt s"
 context step_exit_cps
 begin
-lemma eq_dep: "depend s = depend s'"
+lemma eq_dep: "RAG s = RAG s'"
-by (unfold s_def depend_exit_unchanged, auto)
+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> (depend s)^+" by (simp add:s_dependants_def eq_depend)
+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> (depend s')^+" by simp
+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> depend s'"
+obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'"
-by (auto simp:s_depend_def)
+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_depend_def)
+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_depend)
+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'"
 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_depend cs_dependants_def s_dependants_def eq_dep)
+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)

changeset 35	92f61f6a0fe7
parent 33	9b9f2117561f
child 45	fc83f79009bd