diff -r f98a95f3deae -r f8194fd6214f CpsG.thy
--- a/CpsG.thy	Fri Dec 18 19:13:19 2015 +0800
+++ b/CpsG.thy	Fri Dec 18 22:47:32 2015 +0800
@@ -6,16 +6,38 @@
 imports PrioG Max RTree
 begin
 
+text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
+       difference is the order of arguemts. *}
+definition "the_preced s th = preced th s"
+
+text {* @{term "the_thread"} extracts thread out of RAG node. *}
+fun the_thread :: "node \<Rightarrow> thread" where
+   "the_thread (Th th) = th"
+
+text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}
 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
 
+text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}
 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"
 
-definition "tRAG s = wRAG s O hRAG s"
-
+text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
   by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 
              s_holding_abv cs_RAG_def, auto)
 
+text {* 
+  The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.
+  It characterizes the dependency between threads when calculating current
+  precedences. It is defined as the composition of the above two sub-graphs, 
+  names @{term "wRAG"} and @{term "hRAG"}.
+ *}
+definition "tRAG s = wRAG s O hRAG s"
+
+(* ccc *)
+
+definition "cp_gen s x =
+                  Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
+
 lemma tRAG_alt_def: 
   "tRAG s = {(Th th1, Th th2) | th1 th2. 
                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
@@ -126,47 +148,6 @@
   } ultimately show ?thesis by auto
 qed
 
-lemma readys_root:
-  assumes "vt s"
-  and "th \<in> readys s"
-  shows "root (RAG s) (Th th)"
-proof -
-  { fix x
-    assume "x \<in> ancestors (RAG s) (Th th)"
-    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
-    from tranclD[OF this]
-    obtain z where "(Th th, z) \<in> RAG s" by auto
-    with assms(2) have False
-         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
-         by (fold wq_def, blast)
-  } thus ?thesis by (unfold root_def, auto)
-qed
-
-lemma readys_in_no_subtree:
-  assumes "vt s"
-  and "th \<in> readys s"
-  and "th' \<noteq> th"
-  shows "Th th \<notin> subtree (RAG s) (Th th')" 
-proof
-   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 readys_root[OF assms(1,2)]
-      show ?thesis by (auto simp:root_def)
-   qed
-qed
-
-lemma image_id:
-  assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x"
-  shows "f ` A = A"
-  using assms by (auto simp:image_def)
-
-definition "the_preced s th = preced th s"
-
 lemma cp_alt_def:
   "cp s th =  
            Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
@@ -182,12 +163,6 @@
   thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
 qed
 
-fun the_thread :: "node \<Rightarrow> thread" where
-   "the_thread (Th th) = th"
-
-definition "cp_gen s x =
-                  Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
-
 lemma cp_gen_alt_def:
   "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
     by (auto simp:cp_gen_def)
@@ -346,8 +321,6 @@
     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"
@@ -355,6 +328,38 @@
 context valid_trace
 begin
 
+lemma readys_root:
+  assumes "th \<in> readys s"
+  shows "root (RAG s) (Th th)"
+proof -
+  { fix x
+    assume "x \<in> ancestors (RAG s) (Th th)"
+    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
+    from tranclD[OF this]
+    obtain z where "(Th th, z) \<in> RAG s" by auto
+    with assms(1) have False
+         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
+         by (fold wq_def, blast)
+  } thus ?thesis by (unfold root_def, auto)
+qed
+
+lemma readys_in_no_subtree:
+  assumes "th \<in> readys s"
+  and "th' \<noteq> th"
+  shows "Th th \<notin> subtree (RAG s) (Th th')" 
+proof
+   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 readys_root[OF assms(1)]
+      show ?thesis by (auto simp:root_def)
+   qed
+qed
+
 lemma not_in_thread_isolated:
   assumes "th \<notin> threads s"
   shows "(Th th) \<notin> Field (RAG s)"
@@ -371,11 +376,6 @@
   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
 
-end
-
-context valid_trace
-begin
-
 lemma sgv_wRAG: "single_valued (wRAG s)"
   using waiting_unique[OF vt] 
   by (unfold single_valued_def wRAG_def, auto)
@@ -403,8 +403,19 @@
 lemma rtree_RAG: "rtree (RAG s)"
   using sgv_RAG acyclic_RAG[OF vt]
   by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+end
 
-end
+
+sublocale valid_trace < rtree_RAG: rtree "RAG s"
+proof
+  show "single_valued (RAG s)"
+  apply (intro_locales)
+    by (unfold single_valued_def, 
+        auto intro:unique_RAG[OF vt])
+
+  show "acyclic (RAG s)"
+     by (rule acyclic_RAG[OF vt])
+qed
 
 sublocale valid_trace < rtree_s: rtree "tRAG s"
 proof(unfold_locales)
@@ -486,7 +497,6 @@
   finally show ?thesis by simp
 qed
 
-
 context valid_trace
 begin
 
@@ -568,521 +578,7 @@
 
 end
 
-
-lemma eq_dependants: "dependants (wq s) = dependants s"
-  by (simp add: s_dependants_abv wq_def)
- 
-
-(* obvious lemma *)
-lemma not_thread_holdents:
-  fixes th s
-  assumes vt: "vt s"
-  and not_in: "th \<notin> threads s" 
-  shows "holdents s th = {}"
-proof -
-  from vt not_in show ?thesis
-  proof(induct arbitrary:th)
-    case (vt_cons s e th)
-    assume vt: "vt s"
-      and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
-      and stp: "step s e"
-      and not_in: "th \<notin> threads (e # s)"
-    from stp show ?case
-    proof(cases)
-      case (thread_create thread prio)
-      assume eq_e: "e = Create thread prio"
-        and not_in': "thread \<notin> threads s"
-      have "holdents (e # s) th = holdents s th"
-        apply (unfold eq_e holdents_test)
-        by (simp add:RAG_create_unchanged)
-      moreover have "th \<notin> threads s" 
-      proof -
-        from not_in eq_e show ?thesis by simp
-      qed
-      moreover note ih ultimately show ?thesis by auto
-    next
-      case (thread_exit thread)
-      assume eq_e: "e = Exit thread"
-      and nh: "holdents s thread = {}"
-      show ?thesis
-      proof(cases "th = thread")
-        case True
-        with nh eq_e
-        show ?thesis 
-          by (auto simp:holdents_test RAG_exit_unchanged)
-      next
-        case False
-        with not_in and eq_e
-        have "th \<notin> threads s" by simp
-        from ih[OF this] False eq_e show ?thesis 
-          by (auto simp:holdents_test RAG_exit_unchanged)
-      qed
-    next
-      case (thread_P thread cs)
-      assume eq_e: "e = P thread cs"
-      and is_runing: "thread \<in> runing s"
-      from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto
-      have neq_th: "th \<noteq> thread" 
-      proof -
-        from not_in eq_e have "th \<notin> threads s" by simp
-        moreover from is_runing have "thread \<in> threads s"
-          by (simp add:runing_def readys_def)
-        ultimately show ?thesis by auto
-      qed
-      hence "holdents (e # s) th  = holdents s th "
-        apply (unfold cntCS_def holdents_test eq_e)
-        by (unfold step_RAG_p[OF vtp], auto)
-      moreover have "holdents s th = {}"
-      proof(rule ih)
-        from not_in eq_e show "th \<notin> threads s" by simp
-      qed
-      ultimately show ?thesis by simp
-    next
-      case (thread_V thread cs)
-      assume eq_e: "e = V thread cs"
-        and is_runing: "thread \<in> runing s"
-        and hold: "holding s thread cs"
-      have neq_th: "th \<noteq> thread" 
-      proof -
-        from not_in eq_e have "th \<notin> threads s" by simp
-        moreover from is_runing have "thread \<in> threads s"
-          by (simp add:runing_def readys_def)
-        ultimately show ?thesis by auto
-      qed
-      from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto
-      from hold obtain rest 
-        where eq_wq: "wq s cs = thread # rest"
-        by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
-      from not_in eq_e eq_wq
-      have "\<not> next_th s thread cs th"
-        apply (auto simp:next_th_def)
-      proof -
-        assume ne: "rest \<noteq> []"
-          and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
-        have "?t \<in> set rest"
-        proof(rule someI2)
-          from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
-          show "distinct rest \<and> set rest = set rest" by auto
-        next
-          fix x assume "distinct x \<and> set x = set rest" with ne
-          show "hd x \<in> set rest" by (cases x, auto)
-        qed
-        with eq_wq have "?t \<in> set (wq s cs)" by simp
-        from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
-        show False by auto
-      qed
-      moreover note neq_th eq_wq
-      ultimately have "holdents (e # s) th  = holdents s th"
-        by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
-      moreover have "holdents s th = {}"
-      proof(rule ih)
-        from not_in eq_e show "th \<notin> threads s" by simp
-      qed
-      ultimately show ?thesis by simp
-    next
-      case (thread_set thread prio)
-      print_facts
-      assume eq_e: "e = Set thread prio"
-        and is_runing: "thread \<in> runing s"
-      from not_in and eq_e have "th \<notin> threads s" by auto
-      from ih [OF this] and eq_e
-      show ?thesis 
-        apply (unfold eq_e cntCS_def holdents_test)
-        by (simp add:RAG_set_unchanged)
-    qed
-    next
-      case vt_nil
-      show ?case
-      by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
-  qed
-qed
-
-(* obvious lemma *)
-lemma next_th_neq: 
-  assumes vt: "vt s"
-  and nt: "next_th s th cs th'"
-  shows "th' \<noteq> th"
-proof -
-  from nt show ?thesis
-    apply (auto simp:next_th_def)
-  proof -
-    fix rest
-    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
-      and ne: "rest \<noteq> []"
-    have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" 
-    proof(rule someI2)
-      from wq_distinct[OF vt, of cs] eq_wq
-      show "distinct rest \<and> set rest = set rest" by auto
-    next
-      fix x
-      assume "distinct x \<and> set x = set rest"
-      hence eq_set: "set x = set rest" by auto
-      with ne have "x \<noteq> []" by auto
-      hence "hd x \<in> set x" by auto
-      with eq_set show "hd x \<in> set rest" by auto
-    qed
-    with wq_distinct[OF vt, of cs] eq_wq show False by auto
-  qed
-qed
-
-(* obvious lemma *)
-lemma next_th_unique: 
-  assumes nt1: "next_th s th cs th1"
-  and nt2: "next_th s th cs th2"
-  shows "th1 = th2"
-using assms by (unfold next_th_def, auto)
-
-lemma wf_RAG:
-  assumes vt: "vt s"
-  shows "wf (RAG s)"
-proof(rule finite_acyclic_wf)
-  from finite_RAG[OF vt] show "finite (RAG s)" .
-next
-  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
-qed
-
-definition child :: "state \<Rightarrow> (node \<times> node) set"
-  where "child s \<equiv>
-            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-
-definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
-  where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
-
-lemma children_def2:
-  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-unfolding child_def children_def by simp
-
-lemma children_dependants: 
-  "children s th \<subseteq> dependants (wq s) th"
-  unfolding children_def2
-  unfolding cs_dependants_def
-  by (auto simp add: eq_RAG)
-
-lemma child_unique:
-  assumes vt: "vt s"
-  and ch1: "(Th th, Th th1) \<in> child s"
-  and ch2: "(Th th, Th th2) \<in> child s"
-  shows "th1 = th2"
-using ch1 ch2 
-proof(unfold child_def, clarsimp)
-  fix cs csa
-  assume h1: "(Th th, Cs cs) \<in> RAG s"
-    and h2: "(Cs cs, Th th1) \<in> RAG s"
-    and h3: "(Th th, Cs csa) \<in> RAG s"
-    and h4: "(Cs csa, Th th2) \<in> RAG s"
-  from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
-  with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
-  from unique_RAG[OF vt h2 this]
-  show "th1 = th2" by simp
-qed 
-
-lemma RAG_children:
-  assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
-  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
-proof -
-  from h show ?thesis
-  proof(induct rule: tranclE)
-    fix c th2
-    assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
-    and h2: "(c, Th th2) \<in> RAG s"
-    from h2 obtain cs where eq_c: "c = Cs cs"
-      by (case_tac c, auto simp:s_RAG_def)
-    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
-    proof(rule tranclE[OF h1])
-      fix ca
-      assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
-        and h4: "(ca, c) \<in> RAG s"
-      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
-      proof -
-        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
-          by (case_tac ca, auto simp:s_RAG_def)
-        from eq_ca h4 h2 eq_c
-        have "th3 \<in> children s th2" by (auto simp:children_def child_def)
-        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
-        ultimately show ?thesis by auto
-      qed
-    next
-      assume "(Th th1, c) \<in> RAG s"
-      with h2 eq_c
-      have "th1 \<in> children s th2"
-        by (auto simp:children_def child_def)
-      thus ?thesis by auto
-    qed
-  next
-    assume "(Th th1, Th th2) \<in> RAG s"
-    thus ?thesis
-      by (auto simp:s_RAG_def)
-  qed
-qed
-
-lemma sub_child: "child s \<subseteq> (RAG s)^+"
-  by (unfold child_def, auto)
-
-lemma wf_child: 
-  assumes vt: "vt s"
-  shows "wf (child s)"
-apply(rule wf_subset)
-apply(rule wf_trancl[OF wf_RAG[OF vt]])
-apply(rule sub_child)
-done
-
-lemma RAG_child_pre:
-  assumes vt: "vt s"
-  shows
-  "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
-proof -
-  from wf_trancl[OF wf_RAG[OF vt]]
-  have wf: "wf ((RAG s)^+)" .
-  show ?thesis
-  proof(rule wf_induct[OF wf, of ?P], clarsimp)
-    fix th'
-    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
-               (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
-    and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
-    show "(Th th, Th th') \<in> (child s)\<^sup>+"
-    proof -
-      from RAG_children[OF h]
-      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
-      thus ?thesis
-      proof
-        assume "th \<in> children s th'"
-        thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
-      next
-        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
-        then obtain th3 where th3_in: "th3 \<in> children s th'" 
-          and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
-        from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
-        from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
-        with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
-      qed
-    qed
-  qed
-qed
-
-lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
-  by (insert RAG_child_pre, auto)
-
-lemma child_RAG_p:
-  assumes "(n1, n2) \<in> (child s)^+"
-  shows "(n1, n2) \<in> (RAG s)^+"
-proof -
-  from assms show ?thesis
-  proof(induct)
-    case (base y)
-    with sub_child show ?case by auto
-  next
-    case (step y z)
-    assume "(y, z) \<in> child s"
-    with sub_child have "(y, z) \<in> (RAG s)^+" by auto
-    moreover have "(n1, y) \<in> (RAG s)^+" by fact
-    ultimately show ?case by auto
-  qed
-qed
-
-text {* (* ddd *)
-*}
-lemma child_RAG_eq: 
-  assumes vt: "vt s"
-  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
-  by (auto intro: RAG_child[OF vt] child_RAG_p)
-
-text {* (* ddd *)
-*}
-lemma children_no_dep:
-  fixes s th th1 th2 th3
-  assumes vt: "vt s"
-  and ch1: "(Th th1, Th th) \<in> child s"
-  and ch2: "(Th th2, Th th) \<in> child s"
-  and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
-  shows "False"
-proof -
-  from RAG_child[OF vt ch3]
-  have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
-  thus ?thesis
-  proof(rule converse_tranclE)
-    assume "(Th th1, Th th2) \<in> child s"
-    from child_unique[OF vt ch1 this] have "th = th2" by simp
-    with ch2 have "(Th th2, Th th2) \<in> child s" by simp
-    with wf_child[OF vt] show ?thesis by auto
-  next
-    fix c
-    assume h1: "(Th th1, c) \<in> child s"
-      and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
-    from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
-    with h1 have "(Th th1, Th th3) \<in> child s" by simp
-    from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
-    with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
-    with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
-    moreover have "wf ((child s)\<^sup>+)"
-    proof(rule wf_trancl)
-      from wf_child[OF vt] show "wf (child s)" .
-    qed
-    ultimately show False by auto
-  qed
-qed
-
-text {* (* ddd *)
-*}
-lemma unique_RAG_p:
-  assumes vt: "vt s"
-  and dp1: "(n, n1) \<in> (RAG s)^+"
-  and dp2: "(n, n2) \<in> (RAG s)^+"
-  and neq: "n1 \<noteq> n2"
-  shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
-proof(rule unique_chain [OF _ dp1 dp2 neq])
-  from unique_RAG[OF vt]
-  show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
-qed
-
-text {* (* ddd *)
-*}
-lemma dependants_child_unique:
-  fixes s th th1 th2 th3
-  assumes vt: "vt s"
-  and ch1: "(Th th1, Th th) \<in> child s"
-  and ch2: "(Th th2, Th th) \<in> child s"
-  and dp1: "th3 \<in> dependants s th1"
-  and dp2: "th3 \<in> dependants s th2"
-shows "th1 = th2"
-proof -
-  { assume neq: "th1 \<noteq> th2"
-    from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" 
-      by (simp add:s_dependants_def eq_RAG)
-    from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" 
-      by (simp add:s_dependants_def eq_RAG)
-    from unique_RAG_p[OF vt dp1 dp2] and neq
-    have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
-    hence False
-    proof
-      assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "
-      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
-    next
-      assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
-      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
-    qed
-  } thus ?thesis by auto
-qed
-
-lemma RAG_plus_elim:
-  assumes "vt s"
-  fixes x
-  assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
-  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
-  using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
-  apply (unfold children_def)
-  by (metis assms(2) children_def RAG_children eq_RAG)
-
-text {* (* ddd *)
-*}
-lemma dependants_expand:
-  assumes "vt s"
-  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-apply(simp add: image_def)
-unfolding cs_dependants_def
-apply(auto)
-apply (metis assms RAG_plus_elim mem_Collect_eq)
-apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
-by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
-
-lemma finite_children:
-  assumes "vt s"
-  shows "finite (children s th)"
-  using children_dependants dependants_threads[OF assms] finite_threads[OF assms]
-  by (metis rev_finite_subset)
-  
-lemma finite_dependants:
-  assumes "vt s"
-  shows "finite (dependants (wq s) th')"
-  using dependants_threads[OF assms] finite_threads[OF assms]
-  by (metis rev_finite_subset)
-
-abbreviation
-  "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
-
-abbreviation
-  "cpreceds s ths \<equiv> (cp s) ` ths"
-
-lemma Un_compr:
-  "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
-by auto
-
-lemma in_disj:
-  shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"
-by metis
-
-lemma UN_exists:
-  shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
-by auto
-
-text {* (* ddd *)
-  This is the recursive equation used to compute the current precedence of 
-  a thread (the @{text "th"}) here. 
-*}
-lemma cp_rec:
-  fixes s th
-  assumes vt: "vt s"
-  shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
-proof(cases "children s th = {}")
-  case True
-  show ?thesis
-    unfolding cp_eq_cpreced cpreced_def 
-    by (subst dependants_expand[OF `vt s`]) (simp add: True)
-next
-  case False
-  show ?thesis (is "?LHS = ?RHS")
-  proof -
-    have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
-      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
-  
-    have not_emptyness_facts[simp]: 
-      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
-      using False dependants_expand[OF assms] by(auto simp only: Un_empty)
-
-    have finiteness_facts[simp]:
-      "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
-      by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
-
-    (* expanding definition *)
-    have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
-      unfolding eq_cp by (simp add: Un_compr)
-    
-    (* moving Max in *)
-    also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
-      by (simp add: Max_Un)
-
-    (* expanding dependants *)
-    also have "\<dots> = max (Max {preced th s}) 
-      (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
-      by (subst dependants_expand[OF `vt s`]) (simp)
-
-    (* moving out big Union *)
-    also have "\<dots> = max (Max {preced th s})
-      (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  
-      by simp
-
-    (* moving in small union *)
-    also have "\<dots> = max (Max {preced th s})
-      (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  
-      by (simp add: in_disj)
-
-    (* moving in preceds *)
-    also have "\<dots> = max (Max {preced th s})  
-      (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" 
-      by (simp add: UN_exists)
-
-    (* moving in Max *)
-    also have "\<dots> = max (Max {preced th s})  
-      (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" 
-       by (subst Max_Union) (auto simp add: image_image) 
-
-    (* folding cp + moving out Max *)
-    also have "\<dots> = ?RHS" 
-      unfolding eq_cp by (simp add: Max_insert)
-
-    finally show "?LHS = ?RHS" .
-  qed
-qed
-
+(* keep *)
 lemma next_th_holding:
   assumes vt: "vt s"
   and nxt: "next_th s th cs th'"
@@ -1172,6 +668,16 @@
          the legitimacy of @{text "s"} can be derived. *}
   assumes vt_s: "vt s"
 
+sublocale step_set_cps < vat_s : valid_trace "s"
+proof
+  from vt_s show "vt s" .
+qed
+
+sublocale step_set_cps < vat_s' : valid_trace "s'"
+proof
+  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
+qed
+
 context step_set_cps 
 begin
 
@@ -1181,7 +687,6 @@
 *}
 
 lemma eq_preced:
-  fixes th'
   assumes "th' \<noteq> th"
   shows "preced th' s = preced th' s'"
 proof -
@@ -1255,7 +760,8 @@
     hence "th \<in> runing s'" by (cases, simp)
     thus ?thesis by (simp add:readys_def runing_def)
   qed
-  from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] this assms(1)]
+  find_theorems readys subtree
+  from vat_s'.readys_in_no_subtree[OF this assms(1)]
   show ?thesis by blast
 qed
 
@@ -1284,40 +790,26 @@
   -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
   assumes vt_s: "vt s"
 
-context step_v_cps
-begin
-
-lemma rtree_RAGs: "rtree (RAG s)"
+sublocale step_v_cps < vat_s : valid_trace "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])
+  from vt_s show "vt s" .
 qed
 
-lemma rtree_RAGs': "rtree (RAG s')"
+sublocale step_v_cps < vat_s' : valid_trace "s'"
 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]]])
+  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
 qed
 
-lemmas vt_s' = step_back_vt[OF vt_s[unfolded s_def]]
+context step_v_cps
+begin
 
 lemma ready_th_s': "th \<in> readys s'"
   using step_back_step[OF vt_s[unfolded s_def]]
   by (cases, simp add:runing_def)
 
-
 lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"
 proof -
-  from readys_root[OF vt_s' ready_th_s']
+  from vat_s'.readys_root[OF ready_th_s']
   show ?thesis
   by (unfold root_def, simp)
 qed
@@ -1340,9 +832,8 @@
 lemma ancestors_cs: 
   "ancestors (RAG s') (Cs cs) = {Th th}"
 proof -
-  find_theorems ancestors
   have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th)  \<union>  {Th th}"
-  proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+  proof(rule vat_s'.rtree_RAG.ancestors_accum)
     from vt_s[unfolded s_def]
     have " PIP s' (V th cs)" by (cases, simp)
     thus "(Cs cs, Th th) \<in> RAG s'" 
@@ -1360,7 +851,6 @@
 
 end
 
-
 text {*
   The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 
   which represents the case when there is another thread @{text "th'"}
@@ -1415,13 +905,13 @@
 *)
 
 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
-                using next_th_RAG[OF vt_s' nt] .
+                using next_th_RAG[OF vat_s'.vt nt]  .
 
 lemma ancestors_th': 
   "ancestors (RAG s') (Th th') = {Th th, Cs cs}" 
 proof -
   have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"
-  proof(rule  RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+  proof(rule  vat_s'.rtree_RAG.ancestors_accum)
     from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto
   qed
   thus ?thesis using ancestors_th ancestors_cs by auto
@@ -1552,7 +1042,8 @@
 
 lemma subtree_th: 
   "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs'])
+find_theorems "subtree" "_ - _" RAG
+proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)
   from edge_of_th
   show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)"
     by (unfold edges_in_def, auto simp:subtree_def)
@@ -1567,18 +1058,8 @@
   shows "cp s th' = cp s' th'"
   using cp_kept_1 cp_kept_2
   by (cases "th' = th", auto)
- 
 end
 
-find_theorems "_`_" "\<Union> _"
-
-find_theorems "Max" "\<Union> _"
-
-find_theorems wf RAG
-
-thm wf_def
-
-thm image_Union
 
 locale step_P_cps =
   fixes s' th cs s 
@@ -1595,7 +1076,6 @@
   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
 qed
 
-
 context step_P_cps
 begin
 
@@ -1608,7 +1088,7 @@
 qed
 
 lemma root_th: "root (RAG s') (Th th)"
-  using readys_root[OF vat_s'.vt readys_th] .
+  using readys_root[OF readys_th] .
 
 lemma in_no_others_subtree:
   assumes "th' \<noteq> th"
@@ -2039,7 +1519,8 @@
     qed auto
     have neq_th_a: "th_a \<noteq> th"
     proof -
-      from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
+    find_theorems readys subtree s'
+      from vat_s'.readys_in_no_subtree[OF 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