# HG changeset patch
# User zhangx
# Date 1454504715 -28800
# Node ID 3a801bbd26871ed5512b7debad45a0eea9bc8eec
# Parent  c7db2ccba18a535274362e90b61e8d8af785c900
Reorganizing PIPBasics.thy and making small changes to Implementation.thy and Correctness.thy.

diff -r c7db2ccba18a -r 3a801bbd2687 Correctness.thy
--- a/Correctness.thy	Wed Feb 03 12:04:03 2016 +0800
+++ b/Correctness.thy	Wed Feb 03 21:05:15 2016 +0800
@@ -580,6 +580,7 @@
   -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
   interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
   interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
+  interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto)
   show ?case
   proof -
     -- {* It can be proved that @{term cntP}-value of @{term th'} does not change
@@ -591,8 +592,8 @@
       -- {* Then the actor of @{term e} must be @{term th'} and @{term e}
             must be a @{term P}-event: *}
       hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) 
-      with vat_t.actor_inv[OF Cons(2)]
-      -- {* According to @{thm actor_inv}, @{term th'} must be running at 
+      with vat_es.actor_inv
+      -- {* According to @{thm vat_es.actor_inv}, @{term th'} must be running at 
             the moment @{term "t@s"}: *}
       have "th' \<in> runing (t@s)" by (cases e, auto)
       -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
@@ -609,7 +610,7 @@
     proof(rule ccontr) -- {* Proof by contradiction. *}
       assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"
       hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) 
-      with vat_t.actor_inv[OF Cons(2)]
+      with vat_es.actor_inv
       have "th' \<in> runing (t@s)" by (cases e, auto)
       moreover have "th' \<notin> runing (t@s)"
           using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
diff -r c7db2ccba18a -r 3a801bbd2687 Implementation.thy
--- a/Implementation.thy	Wed Feb 03 12:04:03 2016 +0800
+++ b/Implementation.thy	Wed Feb 03 21:05:15 2016 +0800
@@ -376,9 +376,6 @@
 context valid_trace_p_w
 begin
 
-interpretation vat_e: valid_trace "e#s"
-  by (unfold_locales, insert vt_e, simp)
-
 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
   using holding_s_holder
   by (unfold s_RAG_def, fold holding_eq, auto)
@@ -428,13 +425,13 @@
   and "y \<in> ancestors (tRAG (e#s)) u"
   shows "cp_gen (e#s) y = cp_gen s y"
   using assms(3)
-proof(induct rule:wf_induct[OF vat_e.fsbttRAGs.wf])
+proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf])
   case (1 x)
   show ?case (is "?L = ?R")
   proof -
     from tRAG_ancestorsE[OF 1(2)]
     obtain th2 where eq_x: "x = Th th2" by blast
-    from vat_e.cp_gen_rec[OF this]
+    from vat_es.cp_gen_rec[OF this]
     have "?L = 
           Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" .
     also have "... = 
@@ -454,15 +451,15 @@
             assume "x \<in> Range {(Th th, Th holder)}"
             hence eq_x: "x = Th holder" using RangeE by auto
             show False
-            proof(cases rule:vat_e.ancestors_headE[OF assms(1) start])
+            proof(cases rule:vat_es.ancestors_headE[OF assms(1) start])
               case 1
-              from x_u[folded this, unfolded eq_x] vat_e.acyclic_tRAG
+              from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG
               show ?thesis by (auto simp:ancestors_def acyclic_def)
             next
               case 2
               with x_u[unfolded eq_x]
               have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def)
-              with vat_e.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
+              with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
             qed
           qed
         qed
@@ -473,7 +470,7 @@
           assume a_in: "a \<in> ?A"
           from 1(2)
           show "?f a = ?g a"
-          proof(cases rule:vat_e.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+          proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
              case in_ch
              show ?thesis
              proof(cases "a = u")
@@ -485,7 +482,7 @@
                 proof
                   assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                   have "a = u"
-                  proof(rule vat_e.rtree_s.ancestors_children_unique)
+                  proof(rule vat_es.rtree_s.ancestors_children_unique)
                     from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
                                           RTree.children (tRAG (e#s)) x" by auto
                   next 
@@ -519,7 +516,7 @@
               proof
                 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                 have "a = z"
-                proof(rule vat_e.rtree_s.ancestors_children_unique)
+                proof(rule vat_es.rtree_s.ancestors_children_unique)
                   from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
                       by (auto simp:ancestors_def)
                   with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
@@ -570,9 +567,6 @@
 context valid_trace_create
 begin 
 
-interpretation vat_e: valid_trace "e#s"
-  by (unfold_locales, insert vt_e, simp)
-
 lemma tRAG_kept: "tRAG (e#s) = tRAG s"
   by (unfold tRAG_alt_def RAG_unchanged, auto)
 
@@ -632,7 +626,7 @@
 qed
 
 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"
- by (unfold vat_e.cp_rec children_of_th, simp add:the_preced_def)
+ by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
 
 end
 
@@ -706,4 +700,3 @@
 
 end
 
-
diff -r c7db2ccba18a -r 3a801bbd2687 PIPBasics.thy
--- a/PIPBasics.thy	Wed Feb 03 12:04:03 2016 +0800
+++ b/PIPBasics.thy	Wed Feb 03 21:05:15 2016 +0800
@@ -2590,6 +2590,64 @@
                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
 
+context valid_trace
+begin
+
+lemma RAG_tRAG_transfer:
+  assumes  "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
+  and "(Cs cs, Th th'') \<in> RAG s"
+  shows "tRAG s' = tRAG s \<union> {(Th th, Th th'')}" (is "?L = ?R")
+proof -
+  { fix n1 n2
+    assume "(n1, n2) \<in> ?L"
+    from this[unfolded tRAG_alt_def]
+    obtain th1 th2 cs' where 
+      h: "n1 = Th th1" "n2 = Th th2" 
+         "(Th th1, Cs cs') \<in> RAG s'"
+         "(Cs cs', Th th2) \<in> RAG s'" by auto
+    from h(4) and assms(1) have cs_in: "(Cs cs', Th th2) \<in> RAG s" by auto
+    from h(3) and assms(1) 
+    have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 
+          (Th th1, Cs cs') \<in> RAG s" by auto
+    hence "(n1, n2) \<in> ?R"
+    proof
+      assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
+      hence eq_th1: "th1 = th" by simp
+      moreover have "th2 = th''"
+      proof -
+        from h1 have "cs' = cs" by simp
+        from assms(2) cs_in[unfolded this]
+        show ?thesis using unique_RAG by auto 
+      qed
+      ultimately show ?thesis using h(1,2) by auto
+    next
+      assume "(Th th1, Cs cs') \<in> RAG s"
+      with cs_in have "(Th th1, Th th2) \<in> tRAG s"
+        by (unfold tRAG_alt_def, auto)
+      from this[folded h(1, 2)] show ?thesis by auto
+    qed
+  } moreover {
+    fix n1 n2
+    assume "(n1, n2) \<in> ?R"
+    hence "(n1, n2) \<in>tRAG s \<or> (n1, n2) = (Th th, Th th'')" by auto
+    hence "(n1, n2) \<in> ?L" 
+    proof
+      assume "(n1, n2) \<in> tRAG s"
+      moreover have "... \<subseteq> ?L"
+      proof(rule tRAG_mono)
+        show "RAG s \<subseteq> RAG s'" by (unfold assms(1), auto)
+      qed
+      ultimately show ?thesis by auto
+    next
+      assume eq_n: "(n1, n2) = (Th th, Th th'')"
+      from assms(1, 2) have "(Cs cs, Th th'') \<in> RAG s'" by auto
+      moreover have "(Th th, Cs cs) \<in> RAG s'" using assms(1) by auto
+      ultimately show ?thesis 
+        by (unfold eq_n tRAG_alt_def, auto)
+    qed
+  } ultimately show ?thesis by auto
+qed
+
 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)
@@ -2598,6 +2656,8 @@
   "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
   using dependants_alt_def tRAG_trancl_eq by auto
 
+end
+
 section {* Chain to readys *}
 
 context valid_trace
@@ -4206,173 +4266,9 @@
 
 end
 
-section {* hhh *}
-
-lemma RAG_tRAG_transfer:
-  assumes "vt s'"
-  assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
-  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)
-  { fix n1 n2
-    assume "(n1, n2) \<in> ?L"
-    from this[unfolded tRAG_alt_def]
-    obtain th1 th2 cs' where 
-      h: "n1 = Th th1" "n2 = Th th2" 
-         "(Th th1, Cs cs') \<in> RAG s"
-         "(Cs cs', Th th2) \<in> RAG s" by auto
-    from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto
-    from h(3) and assms(2) 
-    have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 
-          (Th th1, Cs cs') \<in> RAG s'" by auto
-    hence "(n1, n2) \<in> ?R"
-    proof
-      assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
-      hence eq_th1: "th1 = th" by simp
-      moreover have "th2 = th''"
-      proof -
-        from h1 have "cs' = cs" by simp
-        from assms(3) cs_in[unfolded this]
-        show ?thesis using vt_s'.unique_RAG by auto 
-      qed
-      ultimately show ?thesis using h(1,2) by auto
-    next
-      assume "(Th th1, Cs cs') \<in> RAG s'"
-      with cs_in have "(Th th1, Th th2) \<in> tRAG s'"
-        by (unfold tRAG_alt_def, auto)
-      from this[folded h(1, 2)] show ?thesis by auto
-    qed
-  } moreover {
-    fix n1 n2
-    assume "(n1, n2) \<in> ?R"
-    hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto
-    hence "(n1, n2) \<in> ?L" 
-    proof
-      assume "(n1, n2) \<in> tRAG s'"
-      moreover have "... \<subseteq> ?L"
-      proof(rule tRAG_mono)
-        show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)
-      qed
-      ultimately show ?thesis by auto
-    next
-      assume eq_n: "(n1, n2) = (Th th, Th th'')"
-      from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto
-      moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto
-      ultimately show ?thesis 
-        by (unfold eq_n tRAG_alt_def, auto)
-    qed
-  } ultimately show ?thesis by auto
-qed
-
-context valid_trace
-begin
-
-lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
-
-end
-
-lemma cp_alt_def1: 
-  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
-proof -
-  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
-       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
-       by auto
-  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
-qed
-
-lemma cp_gen_def_cond: 
-  assumes "x = Th th"
-  shows "cp s th = cp_gen s (Th th)"
-by (unfold cp_alt_def1 cp_gen_def, simp)
-
-lemma cp_gen_over_set:
-  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
-  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
-proof(rule f_image_eq)
-  fix a
-  assume "a \<in> A"
-  from assms[rule_format, OF this]
-  obtain th where eq_a: "a = Th th" by auto
-  show "cp_gen s a = (cp s \<circ> the_thread) a"
-    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")
-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)"
-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)"
-proof
-  assume "(Th th) \<in> Field (RAG s)"
-  with dm_RAG_threads and rg_RAG_threads assms
-  show False by (unfold Field_def, blast)
-qed
-
-end
-
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
   where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
 
-
 lemma detached_test:
   shows "detached s th = (Th th \<notin> Field (RAG s))"
 apply(simp add: detached_def Field_def)
@@ -4445,6 +4341,35 @@
 
 end
 
+section {* hhh *}
+
+lemma cp_alt_def1: 
+  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
+proof -
+  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
+       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
+       by auto
+  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
+qed
+
+lemma cp_gen_def_cond: 
+  assumes "x = Th th"
+  shows "cp s th = cp_gen s (Th th)"
+by (unfold cp_alt_def1 cp_gen_def, simp)
+
+lemma cp_gen_over_set:
+  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
+  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
+proof(rule f_image_eq)
+  fix a
+  assume "a \<in> A"
+  from assms[rule_format, OF this]
+  obtain th where eq_a: "a = Th th" by auto
+  show "cp_gen s a = (cp s \<circ> the_thread) a"
+    by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
+qed
+
+
 context valid_trace
 begin
 (* ddd *)
@@ -4523,58 +4448,7 @@
   qed
 qed
 
-lemma next_th_holding:
-  assumes nxt: "next_th s th cs th'"
-  shows "holding (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
-  thus ?thesis
-    by (unfold cs_holding_def, auto)
-qed
-
-lemma next_th_waiting:
-  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 cs, unfolded h]
-  have dst: "distinct (th # rest)" .
-  have in_rest: "th' \<in> set rest"
-  proof(unfold h, rule someI2)
-    show "distinct rest \<and> set rest = set rest" using dst by auto
-  next
-    fix x assume "distinct x \<and> set x = set rest"
-    with h(2)
-    show "hd x \<in> set (rest)" by (cases x, auto)
-  qed
-  hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
-  moreover have "th' \<noteq> hd (wq s cs)"
-    by (unfold h(1), insert in_rest dst, auto)
-  ultimately show ?thesis by (auto simp:cs_waiting_def)
-qed
-
-lemma next_th_RAG:
-  assumes nxt: "next_th (s::event list) th cs th'"
-  shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
-  using vt assms next_th_holding next_th_waiting
-  by (unfold s_RAG_def, simp)
-
-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)
-
-context valid_trace
-begin
+section {* Relating @{term cp}-values of @{term threads} and @{term readys }*}
 
 lemma threads_alt_def:
   "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
@@ -4645,37 +4519,16 @@
   finally show ?thesis by simp
 qed (auto simp:threads_alt_def)
 
-lemma create_pre:
-  assumes stp: "step s e"
-  and not_in: "th \<notin> threads s"
-  and is_in: "th \<in> threads (e#s)"
-  obtains prio where "e = Create th prio"
-proof -
-  from assms  
-  show ?thesis
-  proof(cases)
-    case (thread_create thread prio)
-    with is_in not_in have "e = Create th prio" by simp
-    from that[OF this] show ?thesis .
-  next
-    case (thread_exit thread)
-    with assms show ?thesis by (auto intro!:that)
-  next
-    case (thread_P thread)
-    with assms show ?thesis by (auto intro!:that)
-  next
-    case (thread_V thread)
-    with assms show ?thesis by (auto intro!:that)
-  next 
-    case (thread_set thread)
-    with assms show ?thesis by (auto intro!:that)
-  qed
-qed
-
 end
 
 section {* Pending properties *}
 
+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 holding_next_thI:
   assumes "holding s th cs"
   and "length (wq s cs) > 1"
@@ -4704,5 +4557,143 @@
 
 end
 
+context valid_trace
+begin
+
+lemma create_pre:
+  assumes stp: "step s e"
+  and not_in: "th \<notin> threads s"
+  and is_in: "th \<in> threads (e#s)"
+  obtains prio where "e = Create th prio"
+proof -
+  from assms  
+  show ?thesis
+  proof(cases)
+    case (thread_create thread prio)
+    with is_in not_in have "e = Create th prio" by simp
+    from that[OF this] show ?thesis .
+  next
+    case (thread_exit thread)
+    with assms show ?thesis by (auto intro!:that)
+  next
+    case (thread_P thread)
+    with assms show ?thesis by (auto intro!:that)
+  next
+    case (thread_V thread)
+    with assms show ?thesis by (auto intro!:that)
+  next 
+    case (thread_set thread)
+    with assms show ?thesis by (auto intro!:that)
+  qed
+qed
+
+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)"
+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)"
+proof
+  assume "(Th th) \<in> Field (RAG s)"
+  with dm_RAG_threads and rg_RAG_threads assms
+  show False by (unfold Field_def, blast)
+qed
+
+lemma next_th_holding:
+  assumes nxt: "next_th s th cs th'"
+  shows "holding (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
+  thus ?thesis
+    by (unfold cs_holding_def, auto)
+qed
+
+lemma next_th_waiting:
+  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 cs, unfolded h]
+  have dst: "distinct (th # rest)" .
+  have in_rest: "th' \<in> set rest"
+  proof(unfold h, rule someI2)
+    show "distinct rest \<and> set rest = set rest" using dst by auto
+  next
+    fix x assume "distinct x \<and> set x = set rest"
+    with h(2)
+    show "hd x \<in> set (rest)" by (cases x, auto)
+  qed
+  hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
+  moreover have "th' \<noteq> hd (wq s cs)"
+    by (unfold h(1), insert in_rest dst, auto)
+  ultimately show ?thesis by (auto simp:cs_waiting_def)
+qed
+
+lemma next_th_RAG:
+  assumes nxt: "next_th (s::event list) th cs th'"
+  shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
+  using vt assms next_th_holding next_th_waiting
+  by (unfold s_RAG_def, simp)
+
 end
 
+end
\ No newline at end of file