
diff -r b6ea51cd2e88 -r c0a4e840aefe Correctness.thy
--- a/Correctness.thy	Fri Jan 15 02:05:29 2016 +0000
+++ b/Correctness.thy	Wed Jan 27 13:47:08 2016 +0000
@@ -474,42 +474,37 @@
 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. 
-  
-  In this section, we are going to derive a series of lemmas 
-  with finally give rise to a picture of the blocking thread. 
 
-  By `blocking thread`, we mean a thread in running state but 
-  different from thread @{term th}.
+  The purpose of PIP is to ensure that the most urgent thread @{term
+  th} is not blocked unreasonably. Therefore, below, we will derive
+  properties of the blocking thread. By blocking thread, we mean a
+  thread in running state t @ s, but is different from thread @{term
+  th}.
+
+  The first lemmas shows that the @{term cp}-value of the blocking
+  thread @{text th'} equals to the highest precedence in the whole
+  system.
+
 *}
 
-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")
+  assumes runing': "th' \<in> runing (t @ s)"
+  shows "cp (t @ s) th' = preced th s" 
 proof -
-  have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
-      by (unfold runing_def, auto)
-  also have "\<dots> = ?R"
-      by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 
+  have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" 
+    using assms by (unfold runing_def, auto)
+  also have "\<dots> = preced th s"
+    by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 
   finally show ?thesis .
 qed
 
 text {*
 
-  The following lemma shows how the counters for @{term "P"} and
-  @{term "V"} operations relate to the running threads in the states
-  @{term s} and @{term "t @ s"}.  The lemma shows that if a thread's
-  @{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.
+  The next lemma shows how the counters for @{term "P"} and @{term
+  "V"} operations relate to the running threads in the states @{term
+  s} and @{term "t @ s"}: if a thread's @{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.
 
   The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
   The key is the use of @{thm count_eq_dependants} to derive the
@@ -521,7 +516,7 @@
   runing_preced_inversion}, its @{term cp}-value equals to the
   precedence of @{term th}.
 
-  Combining the above two resukts we have that @{text th'} and @{term
+  Combining the above two results 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"}.
@@ -530,13 +525,13 @@
                       
 lemma eq_pv_blocked: (* ddd *)
   assumes neq_th': "th' \<noteq> th"
-  and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
-  shows "th' \<notin> runing (t@s)"
+  and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'"
+  shows "th' \<notin> runing (t @ s)"
 proof
-  assume otherwise: "th' \<in> runing (t@s)"
+  assume otherwise: "th' \<in> runing (t @ s)"
   show False
   proof -
-    have th'_in: "th' \<in> threads (t@s)"
+    have th'_in: "th' \<in> threads (t @ s)"
         using otherwise readys_threads runing_def by auto 
     have "th' = th"
     proof(rule preced_unique)
@@ -550,13 +545,12 @@
         -- {* Since the counts of @{term th'} are balanced, the subtree
               of it contains only itself, so, its @{term cp}-value
               equals its @{term preced}-value: *}
-        have "?L = cp (t@s) th'"
+        have "?L = cp (t @ s) th'"
           by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
         -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
               its @{term cp}-value equals @{term "preced th s"}, 
               which equals to @{term "?R"} by simplification: *}
         also have "... = ?R" 
-        thm runing_preced_inversion
             using runing_preced_inversion[OF otherwise] by simp
         finally show ?thesis .
       qed
@@ -574,8 +568,8 @@
 lemma eq_pv_persist: (* ddd *)
   assumes neq_th': "th' \<noteq> th"
   and eq_pv: "cntP s th' = cntV s th'"
-  shows "cntP (t@s) th' = cntV (t@s) th'"
-proof(induction rule:ind) -- {* The proof goes by induction. *}
+  shows "cntP (t @ s) th' = cntV (t @ s) th'"
+proof(induction rule: ind) 
   -- {* The nontrivial case is for the @{term Cons}: *}
   case (Cons e t)
   -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
@@ -624,22 +618,28 @@
 qed (auto simp:eq_pv)
 
 text {*
-  By combining @{thm  eq_pv_blocked} and @{thm eq_pv_persist},
-  it can be derived easily that @{term th'} can not be running in the future:
+
+  By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can
+  be derived easily that @{term th'} can not be running in the future:
+
 *}
+
 lemma eq_pv_blocked_persist:
   assumes neq_th': "th' \<noteq> th"
   and eq_pv: "cntP s th' = cntV s th'"
-  shows "th' \<notin> runing (t@s)"
+  shows "th' \<notin> runing (t @ s)"
   using assms
   by (simp add: eq_pv_blocked eq_pv_persist) 
 
 text {*
-  The following lemma shows the blocking thread @{term th'}
-  must hold some resource in the very beginning. 
+
+  The following lemma shows the blocking thread @{term th'} must hold
+  some resource in the very beginning.
+
 *}
+
 lemma runing_cntP_cntV_inv: (* ddd *)
-  assumes is_runing: "th' \<in> runing (t@s)"
+  assumes is_runing: "th' \<in> runing (t @ s)"
   and neq_th': "th' \<noteq> th"
   shows "cntP s th' > cntV s th'"
   using assms
@@ -665,11 +665,13 @@
 
 
 text {*
-  The following lemmas shows the blocking thread @{text th'} must be live 
-  at the very beginning, 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}.
   The proof is a  simple combination of the results above:
+
 *}
+
 lemma runing_threads_inv: 
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th': "th' \<noteq> th"
@@ -687,9 +689,12 @@
 qed
 
 text {*
-  The following lemma summarizes several foregoing 
-  lemmas to give an overall picture of the blocking thread @{text "th'"}:
+
+  The following lemma summarises the above lemmas to give an overall
+  characterisationof the blocking thread @{text "th'"}:
+
 *}
+
 lemma runing_inversion: (* ddd, one of the main lemmas to present *)
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
@@ -707,18 +712,23 @@
   show "cp (t@s) th' = preced th s" .
 qed
 
+
 section {* The existence of `blocking thread` *}
 
 text {* 
-  Suppose @{term th} is not running, it is first shown that
-  there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
-  in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
+
+  Suppose @{term th} is not running, it is first shown that there is a
+  path in RAG leading from node @{term th} to another thread @{text
+  "th'"} in the @{term readys}-set (So @{text "th'"} is an ancestor of
+  @{term th}}).
 
-  Now, since @{term readys}-set is non-empty, there must be
-  one in it which holds the highest @{term cp}-value, which, by definition, 
-  is the @{term runing}-thread. However, we are going to show more: this running thread
-  is exactly @{term "th'"}.
-     *}
+  Now, since @{term readys}-set is non-empty, there must be one in it
+  which holds the highest @{term cp}-value, which, by definition, is
+  the @{term runing}-thread. However, we are going to show more: this
+  running thread is exactly @{term "th'"}.
+
+*}
+
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
   assumes "th \<notin> runing (t@s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
@@ -780,11 +790,15 @@
 qed
 
 text {*
-  Now it is easy to see there is always a thread to run by case analysis
-  on whether thread @{term th} is running: if the answer is Yes, the 
-  the running thread is obviously @{term th} itself; otherwise, the running
-  thread is the @{text th'} given by lemma @{thm th_blockedE}.
+
+  Now it is easy to see there is always a thread to run by case
+  analysis on whether thread @{term th} is running: if the answer is
+  yes, the the running thread is obviously @{term th} itself;
+  otherwise, the running thread is the @{text th'} given by lemma
+  @{thm th_blockedE}.
+
 *}
+
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)") 
   case True thus ?thesis by auto




