--- a/PIPDefs.thy	Tue Feb 09 22:30:43 2016 +0800
+++ b/PIPDefs.thy	Fri Feb 12 12:32:57 2016 +0800
@@ -483,13 +483,6 @@
 by (simp)
 
 text {* \noindent
-  Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
-  state @{text "s"}:
-  *}
-definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
-  where "cntCS s th = card (holdents s th)"
-
-text {* \noindent
   According to the convention of Paulson's inductive method,
   the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"} 
   is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as 
@@ -613,27 +606,39 @@
 definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
   where "count Q l = length (filter Q l)"
 
-text {* \noindent
-  The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened 
-  before reaching state @{text "s"}.
-  *}
+text {*
+  The operation @{term P} is used by a thread to request for resources, while
+  @{term V} is used to release. Therefore, the number of resources
+  held by a thread roughly equals to the number of @{term P} it made minus 
+  the number of @{term V}. The equality is rough because the @{term P}-operation
+  might be blocked and fail to give back the holding of the requested resource.
+  In the following, @{text "cntP"} and @{text "cntV"} are the number of @{term P}
+  and @{term "V"} respectively, while @{term cntCS} is the number 
+  resources held by a thread and @{text "pvD"} is introduced to account for 
+  the above mentioned situation when @{term P} is blocked, so that 
+  a equation between @{text cntP}, @{text "cntV"}, @{text "cntCS"} can be established
+  (in the lemma named @{text "valid_trace.cnp_cnv_cncs"}).
+
+  Such a equation, once established, is very handy, because the number of resources 
+  held by a thread can be calculated by counting the number of @{term P} and @{text V},
+  which is relatively easy.
+*}
+
 definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
 
-text {* \noindent
-  The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened 
-  before reaching state @{text "s"}.
-  *}
 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
 
+definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
+  where "cntCS s th = card (holdents s th)"
+
 definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))"
 
 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"
@@ -663,14 +668,6 @@
                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
 
-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)
-
-
 (*<*)
 
 end