610 

   611 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

   612        difference is the order of arguemts. *}

   613 definition "the_preced s th = preced th s"

   614 

   615 text {* @{term "the_thread"} extracts thread out of RAG node. *}

   616 fun the_thread :: "node \<Rightarrow> thread" where

   617    "the_thread (Th th) = th"

   618 

   619 text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}

   620 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"

   621 

   622 text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}

   623 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"

   624 

   625 text {* 

   626   The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.

   627   It characterizes the dependency between threads when calculating current

   628   precedences. It is defined as the composition of the above two sub-graphs, 

   629   names @{term "wRAG"} and @{term "hRAG"}.

   630  *}

   631 definition "tRAG s = wRAG s O hRAG s"

   632 

   633 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}

   634 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"

   635   by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 

   636              s_holding_abv cs_RAG_def, auto)

   637 

   638 definition "cp_gen s x =

   639                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

   640