
diff -r 0a069a667301 -r f98a95f3deae CpsG.thy
--- a/CpsG.thy	Tue Dec 15 15:10:40 2015 +0000
+++ b/CpsG.thy	Fri Dec 18 19:13:19 2015 +0800
@@ -21,6 +21,22 @@
                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
 
+lemma tRAG_Field:
+  "Field (tRAG s) \<subseteq> Field (RAG s)"
+  by (unfold tRAG_alt_def Field_def, auto)
+
+lemma tRAG_ancestorsE:
+  assumes "x \<in> ancestors (tRAG s) u"
+  obtains th where "x = Th th"
+proof -
+  from assms have "(u, x) \<in> (tRAG s)^+" 
+      by (unfold ancestors_def, auto)
+  from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
+  then obtain th where "x = Th th"
+    by (unfold tRAG_alt_def, auto)
+  from that[OF this] show ?thesis .
+qed
+
 lemma tRAG_mono:
   assumes "RAG s' \<subseteq> RAG s"
   shows "tRAG s' \<subseteq> tRAG s"
@@ -205,45 +221,43 @@
   qed
 qed
 
-lemma threads_set_eq: 
-   "the_thread ` (subtree (tRAG s) (Th th)) = 
-                  {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
+lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"
+proof -
+  have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" 
+    by (rule rtrancl_mono, auto simp:RAG_split)
+  also have "... \<subseteq> ((RAG s)^*)^*"
+    by (rule rtrancl_mono, auto)
+  also have "... = (RAG s)^*" by simp
+  finally show ?thesis by (unfold tRAG_def, simp)
+qed
+
+lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"
 proof -
-  { fix th'
-    assume "th' \<in> ?L"
-    then obtain n where h: "th' = the_thread n" "n \<in>  subtree (tRAG s) (Th th)" by auto
-    from subtree_nodeE[OF this(2)]
-    obtain th1 where "n = Th th1" by auto
-    with h have "Th th' \<in>  subtree (tRAG s) (Th th)" by auto
-    hence "Th th' \<in>  subtree (RAG s) (Th th)"
-    proof(cases rule:subtreeE[consumes 1])
-      case 1
-      thus ?thesis by (auto simp:subtree_def)
-    next
-      case 2
-      hence "(Th th', Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
-      thus ?thesis
-      proof(induct)
-        case (step y z)
-        from this(2)[unfolded tRAG_alt_def]
-        obtain u where 
-         h: "(y, u) \<in> RAG s" "(u, z) \<in> RAG s"
-          by auto
-        hence "y \<in> subtree (RAG s) z" by (auto simp:subtree_def)
-        with step(3)
-        show ?case by (auto simp:subtree_def)
-      next
-        case (base y)
-        from this[unfolded tRAG_alt_def]
-        show ?case by (auto simp:subtree_def)
-      qed
-    qed
-    hence "th' \<in> ?R" by auto
+  { fix a
+    assume "a \<in> subtree (tRAG s) x"
+    hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)
+    with tRAG_star_RAG[of s]
+    have "(a, x) \<in> (RAG s)^*" by auto
+    hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)
+  } thus ?thesis by auto
+qed
+
+lemma tRAG_subtree_eq: 
+   "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"
+   (is "?L = ?R")
+proof -
+  { fix n
+    assume "n \<in> ?L"
+    with subtree_nodeE[OF this]
+    obtain th' where "n = Th th'" "Th th' \<in>  subtree (tRAG s) (Th th)" by auto
+    with tRAG_subtree_RAG[of s "Th th"]
+    have "n \<in> ?R" by auto
   } moreover {
-    fix th'
-    assume "th' \<in> ?R"
-    hence "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def)
-    from star_rpath[OF this]
+    fix n
+    assume "n \<in> ?R"
+    then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" 
+      by (auto simp:subtree_def)
+    from star_rpath[OF this(2)]
     obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto
     hence "Th th' \<in> subtree (tRAG s) (Th th)"
     proof(induct xs arbitrary:th' th rule:length_induct)
@@ -264,7 +278,6 @@
             hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
             then obtain cs where "x1 = Cs cs" 
               by (unfold s_RAG_def, auto)
-              find_theorems rpath "_ = _@[_]"
             from rpath_nnl_lastE[OF rp[unfolded this]]
             show ?thesis by auto
         next
@@ -297,11 +310,16 @@
         qed
       qed
     qed
-    from imageI[OF this, of the_thread]
-    have "th' \<in> ?L" by simp
+    from this[folded h(1)]
+    have "n \<in> ?L" .
   } ultimately show ?thesis by auto
 qed
-                  
+
+lemma threads_set_eq: 
+   "the_thread ` (subtree (tRAG s) (Th th)) = 
+                  {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
+   by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
+
 lemma cp_alt_def1: 
   "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
 proof -
@@ -337,6 +355,15 @@
 context valid_trace
 begin
 
+lemma not_in_thread_isolated:
+  assumes "th \<notin> threads s"
+  shows "(Th th) \<notin> Field (RAG s)"
+proof
+  assume "(Th th) \<in> Field (RAG s)"
+  with dm_RAG_threads[OF vt] and range_in[OF vt] assms
+  show False by (unfold Field_def, blast)
+qed
+
 lemma wf_RAG: "wf (RAG s)"
 proof(rule finite_acyclic_wf)
   from finite_RAG[OF vt] show "finite (RAG s)" .
@@ -1572,25 +1599,30 @@
 context step_P_cps
 begin
 
-lemma rtree_RAGs: "rtree (RAG s)"
-proof
-  show "single_valued (RAG s)"
-  apply (intro_locales)
-    by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
-
-  show "acyclic (RAG s)"
-     by (rule acyclic_RAG[OF vt_s])
+lemma readys_th: "th \<in> readys s'"
+proof -
+    from step_back_step [OF vt_s[unfolded s_def]]
+    have "PIP s' (P th cs)" .
+    hence "th \<in> runing s'" by (cases, simp)
+    thus ?thesis by (simp add:readys_def runing_def)
 qed
 
-lemma rtree_RAGs': "rtree (RAG s')"
+lemma root_th: "root (RAG s') (Th th)"
+  using readys_root[OF vat_s'.vt readys_th] .
+
+lemma in_no_others_subtree:
+  assumes "th' \<noteq> th"
+  shows "Th th \<notin> subtree (RAG s') (Th th')"
 proof
-  show "single_valued (RAG s')"
-  apply (intro_locales)
-    by (unfold single_valued_def, 
-        auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
-
-  show "acyclic (RAG s')"
-     by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+  assume "Th th \<in> subtree (RAG s') (Th th')"
+  thus False
+  proof(cases rule:subtreeE)
+    case 1
+    with assms show ?thesis by auto
+  next
+    case 2
+    with root_th show ?thesis by (auto simp:root_def)
+  qed
 qed
 
 lemma preced_kept: "the_preced s = the_preced s'"
@@ -1615,143 +1647,26 @@
   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
+lemma subtree_kept:
+  assumes "th' \<noteq> th"
+  shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')"
+proof(unfold RAG_s, rule subtree_insert_next)
+  from in_no_others_subtree[OF assms] 
+  show "Th th \<notin> subtree (RAG s') (Th th')" .
 qed
 
-lemma  child_kept_right:
-  assumes
-  "(n1, n2) \<in> (child s)^+"
-  shows "(n1, n2) \<in> (child s')^+"
+lemma cp_kept: 
+  assumes "th' \<noteq> th"
+  shows "cp s th' = cp s' th'"
 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
+  have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =
+        (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"
+        by (unfold preced_kept subtree_kept[OF assms], simp)
+  thus ?thesis by (unfold cp_alt_def, simp)
 qed
 
 end
 
-lemma tRAG_ancestorsE:
-  assumes "x \<in> ancestors (tRAG s) u"
-  obtains th where "x = Th th"
-proof -
-  from assms have "(u, x) \<in> (tRAG s)^+" 
-      by (unfold ancestors_def, auto)
-  from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
-  then obtain th where "x = Th th"
-    by (unfold tRAG_alt_def, auto)
-  from that[OF this] show ?thesis .
-qed
-
-
 context step_P_cps_ne 
 begin
 
@@ -1813,19 +1728,7 @@
   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
 qed
 
-lemma set_prop_split:
-  "A = {x. x \<in> A \<and> PP x} \<union> {x. x \<in> A \<and> \<not> PP x}"
-  by auto
-
-lemma f_image_union_eq:
-  assumes "f ` A = g ` A"
-  and "f ` B = g ` B"
-  shows "f ` (A \<union> B) = g ` (A \<union> B)"
-  using assms by auto
-
-(* ccc *)
-
-lemma cp_gen_update_stop:
+lemma cp_gen_update_stop: (* ddd *)
   assumes "u \<in> ancestors (tRAG s) (Th th)"
   and "cp_gen s u = cp_gen s' u"
   and "y \<in> ancestors (tRAG s) u"
@@ -1919,7 +1822,22 @@
               case False
               from a_in obtain th_a where eq_a: "a = Th th_a"
                 by (auto simp:RTree.children_def tRAG_alt_def)
-              have "a \<notin> ancestors (tRAG s) (Th th)" sorry
+              have "a \<notin> ancestors (tRAG s) (Th th)"
+              proof
+                assume a_in': "a \<in> ancestors (tRAG s) (Th th)"
+                have "a = z"
+                proof(rule vat_s.rtree_s.ancestors_children_unique)
+                  from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)"
+                      by (auto simp:ancestors_def)
+                  with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter> 
+                                       RTree.children (tRAG s) x" by auto
+                next
+                  from a_in a_in'
+                  show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x"
+                    by auto
+                qed
+                with False show False by auto
+              qed
               from cp_kept[OF this[unfolded eq_a]]
               have "cp s th_a = cp s' th_a" .
               from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
@@ -1937,314 +1855,19 @@
   qed
 qed
 
-
-
-(* ccc *)
-
-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:
-  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:
-  assumes dp1: "th \<in> dependants s th'"
-  and dp2: "th' \<in> dependants s th''"
-  and eq_cps: "cp s th' = cp s' th'"
+lemma cp_up:
+  assumes "(Th th') \<in> ancestors (tRAG s) (Th th)"
+  and "cp s th' = cp s' th'"
+  and "(Th th'') \<in> ancestors (tRAG s) (Th 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
+  have "cp_gen s (Th th'') = cp_gen s' (Th th'')"
+  proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])
+    from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]
+    show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis
+  qed
+  with cp_gen_def_cond[OF refl[of "Th th''"]]
+  show ?thesis by metis
 qed
 
 end
@@ -2254,147 +1877,182 @@
   defines s_def : "s \<equiv> (Create th prio#s')"
   assumes vt_s: "vt s"
 
+sublocale step_create_cps < vat_s: valid_trace "s"
+  by (unfold_locales, insert vt_s, simp)
+
+sublocale step_create_cps < vat_s': valid_trace "s'"
+  by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)
+
 context step_create_cps
 begin
 
-lemma eq_dep: "RAG s = RAG s'"
+lemma RAG_kept: "RAG s = RAG s'"
   by (unfold s_def RAG_create_unchanged, auto)
 
+lemma tRAG_kept: "tRAG s = tRAG s'"
+  by (unfold tRAG_alt_def RAG_kept, auto)
+
+lemma preced_kept:
+  assumes "th' \<noteq> th"
+  shows "the_preced s th' = the_preced s' th'"
+  by (unfold s_def the_preced_def preced_def, insert assms, auto)
+
+lemma th_not_in: "Th th \<notin> Field (tRAG s')"
+proof -
+  from vt_s[unfolded s_def]
+  have "PIP s' (Create th prio)" by (cases, simp)
+  hence "th \<notin> threads s'" by(cases, simp)
+  from vat_s'.not_in_thread_isolated[OF this]
+  have "Th th \<notin> Field (RAG s')" .
+  with tRAG_Field show ?thesis by auto
+qed
+
 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
+  have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =
+        (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"
+  proof(unfold tRAG_kept, rule f_image_eq)
+    fix a
+    assume a_in: "a \<in> subtree (tRAG s') (Th th')"
+    then obtain th_a where eq_a: "a = Th th_a" 
+    proof(cases rule:subtreeE)
+      case 2
+      from ancestors_Field[OF 2(2)]
+      and that show ?thesis by (unfold tRAG_alt_def, auto)
+    qed auto
+    have neq_th_a: "th_a \<noteq> th"
+    proof -
+      have "(Th th) \<notin> subtree (tRAG s') (Th th')"
+      proof
+        assume "Th th \<in> subtree (tRAG s') (Th th')"
+        thus False
+        proof(cases rule:subtreeE)
+          case 2
+          from ancestors_Field[OF this(2)]
+          and th_not_in[unfolded Field_def]
+          show ?thesis by auto
+        qed (insert assms, auto)
+      qed
+      with a_in[unfolded eq_a] show ?thesis by auto
     qed
+    from preced_kept[OF this]
+    show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"
+      by (unfold eq_a, simp)
   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
+  thus ?thesis by (unfold cp_alt_def1, simp)
 qed
 
-lemma nil_dependants: "dependants s th = {}"
+lemma children_of_th: "RTree.children (tRAG s) (Th 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
+  { fix a
+    assume "a \<in> RTree.children (tRAG s) (Th th)"
+    hence "(a, Th th) \<in> tRAG s" by (auto simp:RTree.children_def)
+    with th_not_in have False 
+     by (unfold Field_def tRAG_kept, auto)
+  } thus ?thesis by auto
 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)
+ by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def)
 
 end
 
-
 locale step_exit_cps =
   fixes s' th prio s 
   defines s_def : "s \<equiv> Exit th # s'"
   assumes vt_s: "vt s"
 
+sublocale step_exit_cps < vat_s: valid_trace "s"
+  by (unfold_locales, insert vt_s, simp)
+
+sublocale step_exit_cps < vat_s': valid_trace "s'"
+  by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)
+
 context step_exit_cps
 begin
 
-lemma eq_dep: "RAG s = RAG s'"
+lemma preced_kept:
+  assumes "th' \<noteq> th"
+  shows "the_preced s th' = the_preced s' th'"
+  by (unfold s_def the_preced_def preced_def, insert assms, auto)
+
+lemma RAG_kept: "RAG s = RAG s'"
   by (unfold s_def RAG_exit_unchanged, auto)
 
+lemma tRAG_kept: "tRAG s = tRAG s'"
+  by (unfold tRAG_alt_def RAG_kept, auto)
+
+lemma th_ready: "th \<in> readys s'"
+proof -
+  from vt_s[unfolded s_def]
+  have "PIP s' (Exit th)" by (cases, simp)
+  hence h: "th \<in> runing s' \<and> holdents s' th = {}" by (cases, metis)
+  thus ?thesis by (unfold runing_def, auto)
+qed
+
+lemma th_holdents: "holdents s' th = {}"
+proof -
+ from vt_s[unfolded s_def]
+  have "PIP s' (Exit th)" by (cases, simp)
+  thus ?thesis by (cases, metis)
+qed
+
+lemma th_RAG: "Th th \<notin> Field (RAG s')"
+proof -
+  have "Th th \<notin> Range (RAG s')"
+  proof
+    assume "Th th \<in> Range (RAG s')"
+    then obtain cs where "holding (wq s') th cs"
+      by (unfold Range_iff s_RAG_def, auto)
+    with th_holdents[unfolded holdents_def]
+    show False by (unfold eq_holding, auto)
+  qed
+  moreover have "Th th \<notin> Domain (RAG s')"
+  proof
+    assume "Th th \<in> Domain (RAG s')"
+    then obtain cs where "waiting (wq s') th cs"
+      by (unfold Domain_iff s_RAG_def, auto)
+    with th_ready show False by (unfold readys_def eq_waiting, auto)
+  qed
+  ultimately show ?thesis by (auto simp:Field_def)
+qed
+
+lemma th_tRAG: "(Th th) \<notin> Field (tRAG s')"
+  using th_RAG tRAG_Field[of s'] by 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)
+  have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =
+        (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"
+  proof(unfold tRAG_kept, rule f_image_eq)
+    fix a
+    assume a_in: "a \<in> subtree (tRAG s') (Th th')"
+    then obtain th_a where eq_a: "a = Th th_a" 
+    proof(cases rule:subtreeE)
+      case 2
+      from ancestors_Field[OF 2(2)]
+      and that show ?thesis by (unfold tRAG_alt_def, auto)
+    qed auto
+    have neq_th_a: "th_a \<noteq> th"
+    proof -
+      from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
+      have "(Th th) \<notin> subtree (RAG s') (Th th')" .
+      with tRAG_subtree_RAG[of s' "Th th'"]
+      have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto
+      with a_in[unfolded eq_a] show ?thesis by auto
     qed
+    from preced_kept[OF this]
+    show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"
+      by (unfold eq_a, simp)
   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
+  thus ?thesis by (unfold cp_alt_def1, simp)
 qed
 
 end
+
 end
 




