--- a/PIPBasics.thy	Mon Feb 08 10:57:01 2016 +0800
+++ b/PIPBasics.thy	Tue Feb 09 22:30:43 2016 +0800
@@ -2951,9 +2951,19 @@
 
 section {* Chain to readys *}
 
+text {*
+  In this section, a more complete view of @{term RAG} and @{term threads}
+  are given. 
+*}
+
 context valid_trace
 begin
 
+text {*
+  The first lemma is technical, which says out of any node in the domain 
+  of @{term RAG}, there is a path leading to a ready thread.
+*}
+
 lemma chain_building:
   assumes "node \<in> Domain (RAG s)"
   obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"
@@ -2998,7 +3008,10 @@
 qed
 
 text {* \noindent
-  The following lemma is proved easily by instantiating @{thm "chain_building"}.
+  The following lemma says for any living thread, 
+  either it is ready or there is a path in @{term RAG}
+  leading from it to a ready thread. The lemma is proved easily
+  by instantiating @{thm "chain_building"}.
 *}                    
 lemma th_chain_to_ready:
   assumes th_in: "th \<in> threads s"
@@ -3014,6 +3027,11 @@
   show ?thesis by auto
 qed
 
+text {*
+  The following lemma is a technical one to show 
+  that the set of threads in the subtree of any thread
+  is finite.
+*}
 lemma finite_subtree_threads:
     "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A")
 proof -
@@ -3031,6 +3049,10 @@
   ultimately show ?thesis by auto
 qed
 
+text {*
+  The following two lemmas shows there is at most one running thread 
+  in the system.
+*}
 lemma runing_unique:
   assumes runing_1: "th1 \<in> runing s"
   and runing_2: "th2 \<in> runing s"
@@ -3156,14 +3178,117 @@
   thus ?thesis by auto
 qed
 
+text {*
+  The following two lemmas show that the set of living threads
+  in the system can be partitioned into subtrees of those 
+  threads in the @{term readys} set. The first lemma
+  @{text threads_alt_def} shows the union of 
+  these subtrees equals to the set of living threads
+  and the second lemma @{text "readys_subtree_disjoint"} shows 
+  subtrees of different threads in @{term readys}-set
+  are disjoint.
+*}
+
+lemma threads_alt_def:
+  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+    (is "?L = ?R")
+proof -
+  { fix th1
+    assume "th1 \<in> ?L"
+    from th_chain_to_ready[OF this]
+    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .
+    hence "th1 \<in> ?R" by (auto simp:subtree_def)
+  } moreover 
+  { fix th'
+    assume "th' \<in> ?R"
+    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"
+      by auto
+    from this(2)
+    have "th' \<in> ?L" 
+    proof(cases rule:subtreeE)
+      case 1
+      with h(1) show ?thesis by (auto simp:readys_def)
+    next
+      case 2
+      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]
+      have "Th th' \<in> Domain (RAG s)" by auto
+      from dm_RAG_threads[OF this]
+      show ?thesis .
+    qed
+  } ultimately show ?thesis by auto
+qed
+
+lemma readys_subtree_disjoint:
+  assumes "th1 \<in> readys s"
+  and "th2 \<in> readys s"
+  and "th1 \<noteq> th2"
+  shows "subtree (RAG s) (Th th1) \<inter> subtree (RAG s) (Th th2) = {}"
+proof -
+  { fix n
+    assume "n \<in> subtree (RAG s) (Th th1) \<inter> subtree (RAG s) (Th th2)"
+    hence "(n, Th th1) \<in> (RAG s)^*" "(n, Th th2) \<in> (RAG s)^*"
+      by (auto simp:subtree_def)
+    from star_rpath[OF this(1)] star_rpath[OF this(2)]
+    obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)"
+                         "rpath (RAG s) n xs2 (Th th2)" by metis
+    hence False
+    proof(cases rule:rtree_RAG.rpath_overlap')
+      case (less_1 xs3)
+      from rpath_star[OF this(3)]
+      have "Th th1 \<in> subtree (RAG s) (Th th2)"
+        by (auto simp:subtree_def)
+      thus ?thesis
+      proof(cases rule:subtreeE)
+        case 1
+        with assms(3) show ?thesis by auto
+      next
+        case 2
+        hence "(Th th1, Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
+        from tranclD[OF this]
+        obtain z where "(Th th1, z) \<in> RAG s" by auto
+        from this[unfolded s_RAG_def, folded wq_def]
+        obtain cs' where "waiting s th1 cs'"
+          by (auto simp:waiting_eq)
+        with assms(1) show False by (auto simp:readys_def)
+      qed
+    next
+      case (less_2 xs3)
+      from rpath_star[OF this(3)]
+      have "Th th2 \<in> subtree (RAG s) (Th th1)"
+        by (auto simp:subtree_def)
+      thus ?thesis
+      proof(cases rule:subtreeE)
+        case 1
+        with assms(3) show ?thesis by auto
+      next
+        case 2
+        hence "(Th th2, Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
+        from tranclD[OF this]
+        obtain z where "(Th th2, z) \<in> RAG s" by auto
+        from this[unfolded s_RAG_def, folded wq_def]
+        obtain cs' where "waiting s th2 cs'"
+          by (auto simp:waiting_eq)
+        with assms(2) show False by (auto simp:readys_def)
+      qed
+    qed
+  } thus ?thesis by auto
+qed
+
 end
 
-
+(* ccc *)
 section {* Relating @{term cp} and @{term the_preced} and @{term preced} *}
 
 context valid_trace
 begin
 
+lemma finite_threads:
+  shows "finite (threads s)"
+  using vt by (induct) (auto elim: step.cases)
+
+lemma  finite_readys: "finite (readys s)"
+  using finite_threads readys_threads rev_finite_subset by blast
+
 lemma le_cp:
   shows "preced th s \<le> cp s th"
   proof(unfold cp_alt_def, rule Max_ge)
@@ -3174,10 +3299,6 @@
       by (simp add: subtree_def the_preced_def)   
   qed
 
-lemma finite_threads:
-  shows "finite (threads s)"
-  using vt by (induct) (auto elim: step.cases)
-
 lemma cp_le:
   assumes th_in: "th \<in> threads s"
   shows "cp s th \<le> Max (the_preced s ` threads s)"
@@ -3212,39 +3333,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma threads_alt_def:
-  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
-    (is "?L = ?R")
-proof -
-  { fix th1
-    assume "th1 \<in> ?L"
-    from th_chain_to_ready[OF this]
-    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .
-    hence "th1 \<in> ?R" by (auto simp:subtree_def)
-  } moreover 
-  { fix th'
-    assume "th' \<in> ?R"
-    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"
-      by auto
-    from this(2)
-    have "th' \<in> ?L" 
-    proof(cases rule:subtreeE)
-      case 1
-      with h(1) show ?thesis by (auto simp:readys_def)
-    next
-      case 2
-      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]
-      have "Th th' \<in> Domain (RAG s)" by auto
-      from dm_RAG_threads[OF this]
-      show ?thesis .
-    qed
-  } ultimately show ?thesis by auto
-qed
-
-lemma  finite_readys: "finite (readys s)"
-  using finite_threads readys_threads rev_finite_subset by blast
-
-text {* (* ccc *) \noindent
+text {* (* ddd *) \noindent
   Since the current precedence of the threads in ready queue will always be boosted,
   there must be one inside it has the maximum precedence of the whole system. 
 *}