diff -r 031d2ae9c9b8 -r b620a2a0806a CpsG.thy
--- a/CpsG.thy	Tue Dec 22 23:13:31 2015 +0800
+++ b/CpsG.thy	Wed Jan 06 20:46:14 2016 +0800
@@ -91,15 +91,17 @@
   and "(Cs cs, Th th'') \<in> RAG s'"
   shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")
 proof -
+  interpret vt_s': valid_trace "s'" using assms(1)
+    by (unfold_locales, simp)
   interpret rtree: rtree "RAG s'"
   proof
   show "single_valued (RAG s')"
   apply (intro_locales)
     by (unfold single_valued_def, 
-        auto intro:unique_RAG[OF assms(1)])
+        auto intro:vt_s'.unique_RAG)
 
   show "acyclic (RAG s')"
-     by (rule acyclic_RAG[OF assms(1)])
+     by (rule vt_s'.acyclic_RAG)
   qed
   { fix n1 n2
     assume "(n1, n2) \<in> ?L"
@@ -152,6 +154,13 @@
   } ultimately show ?thesis by auto
 qed
 
+context valid_trace
+begin
+
+lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
+
+end
+
 lemma cp_alt_def:
   "cp s th =  
            Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
@@ -221,76 +230,133 @@
   } 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[of s] 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, simp)
+        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)
+  
+context valid_trace
+begin
+
+lemma count_eq_tRAG_plus:
+  assumes "cntP s th = cntV s th"
+  shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
+  using assms count_eq_dependants dependants_alt_def eq_dependants by auto 
+
+lemma count_eq_RAG_plus:
+  assumes "cntP s th = cntV s th"
+  shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+  using assms count_eq_dependants cs_dependants_def eq_RAG by auto
+
+lemma count_eq_RAG_plus_Th:
+  assumes "cntP s th = cntV s th"
+  shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+  using count_eq_RAG_plus[OF assms] by auto
+
+lemma count_eq_tRAG_plus_Th:
+  assumes "cntP s th = cntV s th"
+  shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
+   using count_eq_tRAG_plus[OF assms] by auto
+
+end
+
 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
+  { fix n 
+    assume h: "n \<in> ?L"
+    hence "n \<in> ?R"
+    by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 
   } moreover {
     fix n
     assume "n \<in> ?R"
-    then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" 
+    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)
-      case (1 xs th' th)
-      show ?case
-      proof(cases xs)
-        case Nil
-          from rpath_nilE[OF 1(2)[unfolded this]]
-          have "th' = th" by auto
-          thus ?thesis by (auto simp:subtree_def)
-      next
-        case (Cons x1 xs1) note Cons1 = Cons
-        show ?thesis
-        proof(cases "xs1")
-          case Nil
-            from 1(2)[unfolded Cons[unfolded this]]
-            have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
-            hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
-            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 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)" .
-          from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons]
-          have "Th th1 \<in> subtree (tRAG s) (Th th)" by simp
-          moreover have "(Th th', Th th1) \<in> (tRAG s)^*"
-          proof -
-            from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
-            show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto)
-          qed
-          ultimately show ?thesis by (auto simp:subtree_def)
-        qed
-      qed
-    qed
-    from this[folded h(1)]
-    have "n \<in> ?L" .
+    from rtranclD[OF this(2)]
+    have "n \<in> ?L"
+    proof
+      assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
+      with h have "n \<in> {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}" by auto
+      thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
+    qed (insert h, auto simp:subtree_def)
   } ultimately show ?thesis by auto
 qed
 
@@ -325,13 +391,40 @@
     by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
 qed
 
-locale valid_trace = 
-  fixes s
-  assumes vt : "vt s"
 
 context valid_trace
 begin
 
+lemma RAG_threads:
+  assumes "(Th th) \<in> Field (RAG s)"
+  shows "th \<in> threads s"
+  using assms
+  by (metis Field_def UnE dm_RAG_threads range_in vt)
+
+lemma subtree_tRAG_thread:
+  assumes "th \<in> threads s"
+  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
+proof -
+  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    by (unfold tRAG_subtree_eq, simp)
+  also have "... \<subseteq> ?R"
+  proof
+    fix x
+    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
+    from this(2)
+    show "x \<in> ?R"
+    proof(cases rule:subtreeE)
+      case 1
+      thus ?thesis by (simp add: assms h(1)) 
+    next
+      case 2
+      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
+    qed
+  qed
+  finally show ?thesis .
+qed
+
 lemma readys_root:
   assumes "th \<in> readys s"
   shows "root (RAG s) (Th th)"
@@ -369,19 +462,19 @@
   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
+  with dm_RAG_threads and range_in 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)" .
+  from finite_RAG show "finite (RAG s)" .
 next
-  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
+  from acyclic_RAG show "acyclic (RAG s)" .
 qed
 
 lemma sgv_wRAG: "single_valued (wRAG s)"
-  using waiting_unique[OF vt] 
+  using waiting_unique
   by (unfold single_valued_def wRAG_def, auto)
 
 lemma sgv_hRAG: "single_valued (hRAG s)"
@@ -394,7 +487,7 @@
 
 lemma acyclic_tRAG: "acyclic (tRAG s)"
 proof(unfold tRAG_def, rule acyclic_compose)
-  show "acyclic (RAG s)" using acyclic_RAG[OF vt] .
+  show "acyclic (RAG s)" using acyclic_RAG .
 next
   show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
 next
@@ -402,11 +495,12 @@
 qed
 
 lemma sgv_RAG: "single_valued (RAG s)"
-  using unique_RAG[OF vt] by (auto simp:single_valued_def)
+  using unique_RAG by (auto simp:single_valued_def)
 
 lemma rtree_RAG: "rtree (RAG s)"
-  using sgv_RAG acyclic_RAG[OF vt]
+  using sgv_RAG acyclic_RAG
   by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+
 end
 
 
@@ -415,10 +509,10 @@
   show "single_valued (RAG s)"
   apply (intro_locales)
     by (unfold single_valued_def, 
-        auto intro:unique_RAG[OF vt])
+        auto intro:unique_RAG)
 
   show "acyclic (RAG s)"
-     by (rule acyclic_RAG[OF vt])
+     by (rule acyclic_RAG)
 qed
 
 sublocale valid_trace < rtree_s: rtree "tRAG s"
@@ -432,7 +526,7 @@
 proof -
   show "fsubtree (RAG s)"
   proof(intro_locales)
-    show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG[OF vt]] .
+    show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
   next
     show "fsubtree_axioms (RAG s)"
     proof(unfold fsubtree_axioms_def)
@@ -450,13 +544,13 @@
     proof(unfold tRAG_def, rule fbranch_compose)
         show "fbranch (wRAG s)"
         proof(rule finite_fbranchI)
-           from finite_RAG[OF vt] show "finite (wRAG s)"
+           from finite_RAG show "finite (wRAG s)"
            by (unfold RAG_split, auto)
         qed
     next
         show "fbranch (hRAG s)"
         proof(rule finite_fbranchI)
-           from finite_RAG[OF vt] 
+           from finite_RAG 
            show "finite (hRAG s)" by (unfold RAG_split, auto)
         qed
     qed
@@ -596,16 +690,18 @@
     by (unfold cs_holding_def, auto)
 qed
 
+context valid_trace
+begin
+
 lemma next_th_waiting:
-  assumes vt: "vt s"
-  and nxt: "next_th s th cs th'"
+  assumes nxt: "next_th s th cs th'"
   shows "waiting (wq s) th' cs"
 proof -
   from nxt[unfolded next_th_def]
   obtain rest where h: "wq s cs = th # rest"
                        "rest \<noteq> []" 
                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
-  from wq_distinct[OF vt, of cs, unfolded h]
+  from wq_distinct[of cs, unfolded h]
   have dst: "distinct (th # rest)" .
   have in_rest: "th' \<in> set rest"
   proof(unfold h, rule someI2)
@@ -622,11 +718,12 @@
 qed
 
 lemma next_th_RAG:
-  assumes vt: "vt s"
-  and nxt: "next_th s th cs th'"
+  assumes nxt: "next_th (s::event list) th cs th'"
   shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
-  using assms next_th_holding next_th_waiting
-by (unfold s_RAG_def, simp)
+  using vt assms next_th_holding next_th_waiting
+  by (unfold s_RAG_def, simp)
+
+end
 
 -- {* A useless definition *}
 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
@@ -909,7 +1006,7 @@
 *)
 
 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
-                using next_th_RAG[OF vat_s'.vt nt]  .
+                using next_th_RAG[OF nt]  .
 
 lemma ancestors_th': 
   "ancestors (RAG s') (Th th') = {Th th, Cs cs}" 
@@ -1175,7 +1272,7 @@
 
 lemma tRAG_s: 
   "tRAG s = tRAG s' \<union> {(Th th, Th th')}"
-  using RAG_tRAG_transfer[OF step_back_vt[OF vt_s[unfolded s_def]] RAG_s cs_held] .
+  using RAG_tRAG_transfer[OF RAG_s cs_held] .
 
 lemma cp_kept:
   assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)"