--- a/CpsG.thy	Wed Jan 27 19:28:42 2016 +0800
+++ b/CpsG.thy	Wed Jan 27 23:34:23 2016 +0800
@@ -4114,6 +4114,8 @@
 
 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
 
+end
+
 lemma tRAG_subtree_eq: 
    "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"
    (is "?L = ?R")
@@ -4168,6 +4170,9 @@
     by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
 qed
 
+context valid_trace
+begin
+
 lemma subtree_tRAG_thread:
   assumes "th \<in> threads s"
   shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
@@ -4309,138 +4314,10 @@
   shows "(detached s th) = (cntP s th = cntV s th)"
   by (insert vt, auto intro:detached_intro detached_elim)
 
-lemma tRAG_nodeE:
-  assumes "(n1, n2) \<in> tRAG s"
-  obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"
-  using assms
-  by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)
-
-lemma subtree_nodeE:
-  assumes "n \<in> subtree (tRAG s) (Th th)"
-  obtains th1 where "n = Th th1"
-proof -
-  show ?thesis
-  proof(rule subtreeE[OF assms])
-    assume "n = Th th"
-    from that[OF this] show ?thesis .
-  next
-    assume "Th th \<in> ancestors (tRAG s) n"
-    hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
-    hence "\<exists> th1. n = Th th1"
-    proof(induct)
-      case (base y)
-      from tRAG_nodeE[OF this] show ?case by metis
-    next
-      case (step y z)
-      thus ?case by auto
-    qed
-    with that show ?thesis by auto
-  qed
-qed
-
-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 a
-    assume "a \<in> subtree (tRAG s) x"
-    hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)
-    with tRAG_star_RAG
-    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_trancl_eq:
-   "{th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
-    {th'. (Th th', Th th)  \<in> (RAG s)^+}"
-   (is "?L = ?R")
-proof -
-  { fix th'
-    assume "th' \<in> ?L"
-    hence "(Th th', Th th) \<in> (tRAG s)^+" by auto
-    from tranclD[OF this]
-    obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto
-    from tRAG_subtree_RAG and this(2)
-    have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) 
-    moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto 
-    ultimately have "th' \<in> ?R"  by auto 
-  } moreover 
-  { fix th'
-    assume "th' \<in> ?R"
-    hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)
-    from plus_rpath[OF this]
-    obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto
-    hence "(Th th', Th th) \<in> (tRAG s)^+"
-    proof(induct xs arbitrary:th' th rule:length_induct)
-      case (1 xs th' th)
-      then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)
-      show ?case
-      proof(cases "xs1")
-        case Nil
-        from 1(2)[unfolded Cons1 Nil]
-        have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
-        hence "(Th th', x1) \<in> (RAG s)" by (cases, auto)
-        then obtain cs where "x1 = Cs cs" 
-              by (unfold s_RAG_def, auto)
-        from rpath_nnl_lastE[OF rp[unfolded this]]
-        show ?thesis by auto
-      next
-        case (Cons x2 xs2)
-        from 1(2)[unfolded Cons1[unfolded this]]
-        have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .
-        from rpath_edges_on[OF this]
-        have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .
-        have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"
-            by (simp add: edges_on_unfold)
-        with eds have rg1: "(Th th', x1) \<in> RAG s" by auto
-        then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)
-        have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"
-            by (simp add: edges_on_unfold)
-        from this eds
-        have rg2: "(x1, x2) \<in> RAG s" by auto
-        from this[unfolded eq_x1] 
-        obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)
-        from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
-        have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)
-        from rp have "rpath (RAG s) x2 xs2 (Th th)"
-           by  (elim rpath_ConsE, simp)
-        from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .
-        show ?thesis
-        proof(cases "xs2 = []")
-          case True
-          from rpath_nilE[OF rp'[unfolded this]]
-          have "th1 = th" by auto
-          from rt1[unfolded this] show ?thesis by auto
-        next
-          case False
-          from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]
-          have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp
-          with rt1 show ?thesis by auto
-        qed
-      qed
-    qed
-    hence "th' \<in> ?L" by auto
-  } ultimately show ?thesis by blast
-qed
-
-lemma tRAG_trancl_eq_Th:
-   "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
-    {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"
-    using tRAG_trancl_eq by auto
-
-lemma dependants_alt_def:
-  "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
-  by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
-
+end
+
+context valid_trace
+begin
 (* ddd *)
 lemma cp_gen_rec:
   assumes "x = Th th"
@@ -4561,5 +4438,11 @@
 
 end
 
+lemma next_th_unique: 
+  assumes nt1: "next_th s th cs th1"
+  and nt2: "next_th s th cs th2"
+  shows "th1 = th2"
+using assms by (unfold next_th_def, auto)
+
 end