--- a/PIPDefs.thy~	Thu Jan 07 22:10:06 2016 +0800
+++ b/PIPDefs.thy~	Sat Jan 09 22:19:27 2016 +0800
@@ -1,7 +1,7 @@
 chapter {* Definitions *}
 (*<*)
 theory PIPDefs
-imports Precedence_ord Moment
+imports Precedence_ord Moment RTree Max
 begin
 (*>*)
 
@@ -607,6 +607,37 @@
   *}
 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
+
+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}"
+
+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"
+
+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)
+
+definition "cp_gen s x =
+                  Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
+
 (*<*)
 
 end