--- a/Correctness.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/Correctness.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -2,6 +2,8 @@
 imports PIPBasics
 begin
 
+(* hg cat -r 176 Correctness.thy *)
+
 lemma actions_of_len_cons [iff]: 
     "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1"
       by  (unfold actions_of_def, simp)
@@ -521,21 +523,27 @@
   @{term "P"}-count equals its @{term "V"}-count (which means it no
   longer has any resource in its possession), it cannot be a running
   thread.
+  
+  (* eee *)
+  The proof is by contradiction:
+  If @{text th'} is running, it can be derived that @{text "th' = th"} which 
+  is in contradiction with the assume @{text "th' \<noteq> th"}.
 
-  The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
-  The key is the use of @{thm eq_pv_dependants} to derive the
-  emptiness of @{text th'}s @{term dependants}-set from the balance of
-  its @{term P} and @{term V} counts.  From this, it can be shown
-  @{text th'}s @{term cp}-value equals to its own precedence.
+  The derivation of @{text "th' = th"} uses @{thm preced_unique}, according to which
+  we need to show the @{text th'} and @{text th} have the same precedence. The proof
+  of this is based on the combination of the following two facts:
 
-  On the other hand, since @{text th'} is running, by @{thm
-  running_preced_inversion}, its @{term cp}-value equals to the
-  precedence of @{term th}.
+  From @{thm vat_t.detached_intro} and assume 
+  @{text "cntP (t@s) th' = cntV (t@s) th'"} it can be derived that 
+  @{text th'} is detached. From this and @{thm detached_cp_preced}
+  it following the precedence of @{text th'} equals to its own @{text cp}-value.
 
-  Combining the above two resukts we have that @{text th'} and @{term
-  th} have the same precedence. By uniqueness of precedences, we have
-  @{text "th' = th"}, which is in contradiction with the assumption
-  @{text "th' \<noteq> th"}.
+  Since @{text th'} is running, from this and @{thm
+  running_preced_inversion}, the precedence of @{text th'} equals to
+  the precedence of @{term th}.
+
+  By combining the above two results we have that @{text th'} and @{term
+  th} have the same precedence. 
 
 *} 
                       
@@ -567,7 +575,6 @@
               its @{term cp}-value equals @{term "preced th s"}, 
               which equals to @{term "?R"} by simplification: *}
         also have "... = ?R" 
-        thm running_preced_inversion
             using running_preced_inversion[OF otherwise] by simp
         finally show ?thesis .
       qed
@@ -1689,5 +1696,4 @@
 
 end
 
-
 end