diff -r 633b1fc8631b -r 2af87bb52fca Correctness.thy
--- a/Correctness.thy	Thu Jan 07 08:33:13 2016 +0800
+++ b/Correctness.thy	Thu Jan 07 22:10:06 2016 +0800
@@ -600,8 +600,24 @@
 lemmas runing_precond_pre_dtc = runing_precond_pre
          [folded vat_t.detached_eq vat_s.detached_eq]
 
-lemma runing_precond: (* ddd *)
-  fixes th'
+section {* The blocking thread *}
+
+text {* 
+  The purpose of PIP is to ensure that the most 
+  urgent thread @{term th} is not blocked unreasonably. 
+  Therefore, a clear picture of the blocking thread is essential 
+  to assure people that the purpose is fulfilled. 
+  
+  The following lemmas will give us such a picture: 
+*}
+
+(* ccc *)
+
+text {*
+  The following lemma shows the blocking thread @{term th'}
+  must hold some resource in the very beginning. 
+*}
+lemma runing_cntP_cntV_inv: (* ddd *)
   assumes th'_in: "th' \<in> threads s"
   and neq_th': "th' \<noteq> th"
   and is_runing: "th' \<in> runing (t@s)"
@@ -683,6 +699,7 @@
 
 (* The foregoing two lemmas are preparation for this one, but
    in long run can be combined. Maybe I am wrong.
+   This one is useless (* XY *)
 *)
 lemma moment_blocked:
   assumes neq_th': "th' \<noteq> th"
@@ -701,6 +718,12 @@
   show ?thesis by (metis h_j.detached_intro) 
 qed
 
+
+text {*
+  The following lemmas shows that the @{term cp}-value 
+  of the blocking thread @{text th'} equals to the highest
+  precedence in the whole system.
+*}
 lemma runing_preced_inversion:
   assumes runing': "th' \<in> runing (t@s)"
   shows "cp (t@s) th' = preced th s" (is "?L = ?R")
@@ -712,20 +735,14 @@
   finally show ?thesis .
 qed
 
-text {*
-  The situation when @{term "th"} is blocked is analyzed by the following lemmas.
-*}
 
 text {*
-  The following lemmas shows the running thread @{text "th'"}, if it is different from
-  @{term th}, must be live at the very beginning. By the term {\em the very beginning},
-  we mean the moment where the formal investigation starts, i.e. the moment (or state)
-  @{term s}. 
+  The following lemmas shows the blocking thread @{text th'} must be live 
+  at the very beginning, i.e. the moment (or state) @{term s}. 
 *}
-
-lemma runing_inversion_0:
-  assumes neq_th': "th' \<noteq> th"
-  and runing': "th' \<in> runing (t@s)"
+lemma runing_threads_inv: (* ddd *)
+  assumes runing': "th' \<in> runing (t@s)"
+  and neq_th': "th' \<noteq> th"
   shows "th' \<in> threads s"
 proof -
     -- {* The proof is by contradiction: *}
@@ -774,61 +791,26 @@
     } thus ?thesis by auto
 qed
 
-text {* 
-  The second lemma says, if the running thread @{text th'} is different from 
-  @{term th}, then this @{text th'} must in the possession of some resources
-  at the very beginning. 
-
-  To ease the reasoning of resource possession of one particular thread, 
-  we used two auxiliary functions @{term cntV} and @{term cntP}, 
-  which are the counters of @{term P}-operations and 
-  @{term V}-operations respectively. 
-  If the number of @{term V}-operation is less than the number of 
-  @{term "P"}-operations, the thread must have some unreleased resource. 
+text {*
+  The following lemma summarizes several foregoing 
+  lemmas to give an overall picture of the blocking thread @{text "th'"}:
 *}
-
-lemma runing_inversion_1: (* ddd *)
-  assumes neq_th': "th' \<noteq> th"
-  and runing': "th' \<in> runing (t@s)"
-  -- {* thread @{term "th'"} is a live on in state @{term "s"} and 
-        it has some unreleased resource. *}
-  shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
-proof -
-  -- {* The proof is a simple composition of @{thm runing_inversion_0} and 
-        @{thm runing_precond}: *}
-  -- {* By applying @{thm runing_inversion_0} to assumptions,
-        it can be shown that @{term th'} is live in state @{term s}: *}
-  have "th' \<in> threads s"  using runing_inversion_0[OF assms(1,2)] .
-  -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *}
-  with runing_precond [OF this neq_th' runing'] show ?thesis by simp
-qed
-
-text {* 
-  The following lemma is just a rephrasing of @{thm runing_inversion_1}:
-*}
-lemma runing_inversion_2:
-  assumes runing': "th' \<in> runing (t@s)"
-  shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
-proof -
-  from runing_inversion_1[OF _ runing']
-  show ?thesis by auto
-qed
-
-lemma runing_inversion_3:
-  assumes runing': "th' \<in> runing (t@s)"
-  and neq_th: "th' \<noteq> th"
-  shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
-  by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)
-
-lemma runing_inversion_4:
+lemma runing_inversion:
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
   shows "th' \<in> threads s"
   and    "\<not>detached s th'"
   and    "cp (t@s) th' = preced th s"
-  apply (metis neq_th runing' runing_inversion_2)
-  apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)
-  by (metis neq_th runing' runing_inversion_3)
+proof -
+  from runing_threads_inv[OF assms]
+  show "th' \<in> threads s" .
+next
+  from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing']
+  show "\<not>detached s th'" using vat_s.detached_eq by simp
+next
+  from runing_preced_inversion[OF runing']
+  show "cp (t@s) th' = preced th s" .
+qed
 
 text {* 
   Suppose @{term th} is not running, it is first shown that