
diff -r 2af87bb52fca -r 25fd656667a7 Correctness.thy
--- a/Correctness.thy	Thu Jan 07 22:10:06 2016 +0800
+++ b/Correctness.thy	Sat Jan 09 22:19:27 2016 +0800
@@ -79,7 +79,6 @@
   ultimately show ?thesis by auto
 qed
 
-(* ccc *)
 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
   by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)
 
@@ -135,7 +134,6 @@
   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
   by (unfold highest_gen_def, auto dest:step_back_vt_app)
 
-
 context extend_highest_gen
 begin
 
@@ -458,268 +456,6 @@
     vat_s.le_cp)
 
 text {*
-  Counting of the number of @{term "P"} and @{term "V"} operations 
-  is the cornerstone of a large number of the following proofs. 
-  The reason is that this counting is quite easy to calculate and 
-  convenient to use in the reasoning. 
-
-  The following lemma shows that the counting controls whether 
-  a thread is running or not.
-*}
-
-lemma pv_blocked_pre: (* ddd *)
-  assumes th'_in: "th' \<in> threads (t@s)"
-  and neq_th': "th' \<noteq> th"
-  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)"
-  show False
-  proof -
-    have "th' = th"
-    proof(rule preced_unique)
-      show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
-      proof -
-        have "?L = cp (t@s) th'"
-          by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
-        also have "... = cp (t @ s) th" using otherwise 
-          by (metis (mono_tags, lifting) mem_Collect_eq 
-                    runing_def th_cp_max vat_t.max_cp_readys_threads)
-        also have "... = ?R" by (metis th_cp_preced th_kept) 
-        finally show ?thesis .
-      qed
-    qed (auto simp: th'_in th_kept)
-    moreover have "th' \<noteq> th" using neq_th' .
-    ultimately show ?thesis by simp
- qed
-qed
-
-lemmas pv_blocked = pv_blocked_pre[folded detached_eq]
-
-lemma runing_precond_pre: (* ddd *)
-  fixes th'
-  assumes th'_in: "th' \<in> threads s"
-  and eq_pv: "cntP s th' = cntV s th'"
-  and neq_th': "th' \<noteq> th"
-  shows "th' \<in> threads (t@s) \<and>
-         cntP (t@s) th' = cntV (t@s) th'"
-proof(induct rule:ind)
-  case (Cons e t)
-    interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
-    interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
-    show ?case
-    proof(cases e)
-      case (P thread cs)
-      show ?thesis
-      proof -
-        have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
-        proof -
-          have "thread \<noteq> th'"
-          proof -
-            have "step (t@s) (P thread cs)" using Cons P by auto
-            thus ?thesis
-            proof(cases)
-              assume "thread \<in> runing (t@s)"
-              moreover have "th' \<notin> runing (t@s)" using Cons(5)
-                by (metis neq_th' vat_t.pv_blocked_pre) 
-              ultimately show ?thesis by auto
-            qed
-          qed with Cons show ?thesis
-            by (unfold P, simp add:cntP_def cntV_def count_def)
-        qed
-        moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp)
-        ultimately show ?thesis by auto
-      qed
-    next
-      case (V thread cs)
-      show ?thesis
-      proof -
-        have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
-        proof -
-          have "thread \<noteq> th'"
-          proof -
-            have "step (t@s) (V thread cs)" using Cons V by auto
-            thus ?thesis
-            proof(cases)
-              assume "thread \<in> runing (t@s)"
-              moreover have "th' \<notin> runing (t@s)" using Cons(5)
-                by (metis neq_th' vat_t.pv_blocked_pre) 
-              ultimately show ?thesis by auto
-            qed
-          qed with Cons show ?thesis
-            by (unfold V, simp add:cntP_def cntV_def count_def)
-        qed
-        moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp)
-        ultimately show ?thesis by auto
-      qed
-    next
-      case (Create thread prio')
-      show ?thesis
-      proof -
-        have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
-        proof -
-          have "thread \<noteq> th'"
-          proof -
-            have "step (t@s) (Create thread prio')" using Cons Create by auto
-            thus ?thesis using Cons(5) by (cases, auto)
-          qed with Cons show ?thesis
-            by (unfold Create, simp add:cntP_def cntV_def count_def)
-        qed
-        moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp)
-        ultimately show ?thesis by auto
-      qed
-    next
-      case (Exit thread)
-      show ?thesis
-      proof -
-        have neq_thread: "thread \<noteq> th'"
-        proof -
-          have "step (t@s) (Exit thread)" using Cons Exit by auto
-          thus ?thesis apply (cases) using Cons(5)
-                by (metis neq_th' vat_t.pv_blocked_pre) 
-        qed 
-        hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons
-            by (unfold Exit, simp add:cntP_def cntV_def count_def)
-        moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread 
-          by (unfold Exit, simp) 
-        ultimately show ?thesis by auto
-      qed
-    next
-      case (Set thread prio')
-      with Cons
-      show ?thesis 
-        by (auto simp:cntP_def cntV_def count_def)
-    qed
-next
-  case Nil
-  with assms
-  show ?case by auto
-qed
-
-text {* Changing counting balance to detachedness *}
-lemmas runing_precond_pre_dtc = runing_precond_pre
-         [folded vat_t.detached_eq vat_s.detached_eq]
-
-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)"
-  shows "cntP s th' > cntV s th'"
-  using assms
-proof -
-  have "cntP s th' \<noteq> cntV s th'"
-    by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in)
-  moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
-  ultimately show ?thesis by auto
-qed
-
-lemma moment_blocked_pre:
-  assumes neq_th': "th' \<noteq> th"
-  and th'_in: "th' \<in> threads ((moment i t)@s)"
-  and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
-  shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and>
-         th' \<in> threads ((moment (i+j) t)@s)"
-proof -
-  interpret h_i: red_extend_highest_gen _ _ _ _ _ i
-      by (unfold_locales)
-  interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j"
-      by (unfold_locales)
-  interpret h:  extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)"
-  proof(unfold_locales)
-    show "vt (moment i t @ s)" by (metis h_i.vt_t) 
-  next
-    show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept)
-  next
-    show "preced th (moment i t @ s) = 
-            Max (cp (moment i t @ s) ` threads (moment i t @ s))"
-              by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept)
-  next
-    show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) 
-  next
-    show "vt (moment j (restm i t) @ moment i t @ s)"
-      using moment_plus_split by (metis add.commute append_assoc h_j.vt_t)
-  next
-    fix th' prio'
-    assume "Create th' prio' \<in> set (moment j (restm i t))"
-    thus "prio' \<le> prio" using assms
-       by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append)
-  next
-    fix th' prio'
-    assume "Set th' prio' \<in> set (moment j (restm i t))"
-    thus "th' \<noteq> th \<and> prio' \<le> prio"
-    by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append)
-  next
-    fix th'
-    assume "Exit th' \<in> set (moment j (restm i t))"
-    thus "th' \<noteq> th"
-      by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append)
-  qed
-  show ?thesis 
-    by (metis add.commute append_assoc eq_pv h.runing_precond_pre
-          moment_plus_split neq_th' th'_in)
-qed
-
-lemma moment_blocked_eqpv: (* ddd *)
-  assumes neq_th': "th' \<noteq> th"
-  and th'_in: "th' \<in> threads ((moment i t)@s)"
-  and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
-  and le_ij: "i \<le> j"
-  shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and>
-         th' \<in> threads ((moment j t)@s) \<and>
-         th' \<notin> runing ((moment j t)@s)"
-proof -
-  from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij
-  have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"
-   and h2: "th' \<in> threads ((moment j t)@s)" by auto
-  moreover have "th' \<notin> runing ((moment j t)@s)"
-  proof -
-    interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
-    show ?thesis
-      using h.pv_blocked_pre h1 h2 neq_th' by auto 
-  qed
-  ultimately show ?thesis by auto
-qed
-
-(* 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"
-  and th'_in: "th' \<in> threads ((moment i t)@s)"
-  and dtc: "detached (moment i t @ s) th'"
-  and le_ij: "i \<le> j"
-  shows "detached (moment j t @ s) th' \<and>
-         th' \<in> threads ((moment j t)@s) \<and>
-         th' \<notin> runing ((moment j t)@s)"
-proof -
-  interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)
-  interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) 
-  have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'"
-                by (metis dtc h_i.detached_elim)
-  from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij]
-  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.
@@ -735,67 +471,190 @@
   finally show ?thesis .
 qed
 
+section {* The `blocking thread` *}
+
+text {*
+  Counting of the number of @{term "P"} and @{term "V"} operations 
+  is the cornerstone of a large number of the following proofs. 
+  The reason is that this counting is quite easy to calculate and 
+  convenient to use in the reasoning. 
+
+  The following lemma shows that the counting controls whether 
+  a thread is running or not.
+*} (* ccc *)
+                      
+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)"
+proof
+  assume otherwise: "th' \<in> runing (t@s)"
+  show False
+  proof -
+    have th'_in: "th' \<in> threads (t@s)"
+        using otherwise readys_threads runing_def by auto 
+    have "th' = th"
+    proof(rule preced_unique)
+      -- {* The proof goes like this: 
+            it is first shown that the @{term preced}-value of @{term th'} 
+            equals to that of @{term th}, then by uniqueness 
+            of @{term preced}-values (given by lemma @{thm preced_unique}), 
+            @{term th'} equals to @{term th}: *}
+      show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
+      proof -
+        -- {* 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'"
+          by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
+        -- {* Since @{term "th'"} is running by @{thm otherwise},
+              it has the highest @{term cp}-value, by definition, 
+              which in turn equals to the @{term cp}-value of @{term th}. *}
+        also have "... = ?R" 
+            using runing_preced_inversion[OF otherwise] th_kept by simp
+        finally show ?thesis .
+      qed
+    qed (auto simp: th'_in th_kept)
+    moreover have "th' \<noteq> th" using neq_th' .
+    ultimately show ?thesis by simp
+ qed
+qed
+
+text {*
+  The following lemma is the extrapolation of @{thm eq_pv_blocked}.
+  It says if a thread, different from @{term th}, 
+  does not hold any resource at the very beginning,
+  it will keep hand-emptied in the future @{term "t@s"}.
+*}
+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. *}
+  -- {* 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"}: *}
+  interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
+  interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
+  show ?case
+  proof -
+    -- {* It can be proved that @{term cntP}-value of @{term th'} does not change
+          by the happening of event @{term e}: *}
+    have "cntP ((e#t)@s) th' = cntP (t@s) th'"
+    proof(rule ccontr) -- {* Proof by contradiction. *}
+      -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *}
+      assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'"
+      -- {* Then the actor of @{term e} must be @{term th'} and @{term e}
+            must be a @{term P}-event: *}
+      hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) 
+      with vat_t.actor_inv[OF Cons(2)]
+      -- {* According to @{thm actor_inv}, @{term th'} must be running at 
+            the moment @{term "t@s"}: *}
+      have "th' \<in> runing (t@s)" by (cases e, auto)
+      -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
+            shows @{term th'} can not be running at moment  @{term "t@s"}: *}
+      moreover have "th' \<notin> runing (t@s)" 
+               using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
+      -- {* Contradiction is finally derived: *}
+      ultimately show False by simp
+    qed
+    -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change
+          by the happening of event @{term e}: *}
+    -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *}
+    moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'"
+    proof(rule ccontr) -- {* Proof by contradiction. *}
+      assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"
+      hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) 
+      with vat_t.actor_inv[OF Cons(2)]
+      have "th' \<in> runing (t@s)" by (cases e, auto)
+      moreover have "th' \<notin> runing (t@s)"
+          using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
+      ultimately show False by simp
+    qed
+    -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} 
+          value for @{term th'} are still in balance, so @{term th'} 
+          is still hand-emptied after the execution of event @{term e}: *}
+    ultimately show ?thesis using Cons(5) by metis
+  qed
+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:
+*}
+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)"
+  using assms
+  by (simp add: eq_pv_blocked eq_pv_persist) 
+
+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: 
+*}
+
+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 is_runing: "th' \<in> runing (t@s)"
+  and neq_th': "th' \<noteq> th"
+  shows "cntP s th' > cntV s th'"
+  using assms
+proof -
+  -- {* First, it can be shown that the number of @{term P} and
+        @{term V} operations can not be equal for thred @{term th'} *}
+  have "cntP s th' \<noteq> cntV s th'"
+  proof
+     -- {* The proof goes by contradiction, suppose otherwise: *}
+    assume otherwise: "cntP s th' = cntV s th'"
+    -- {* By applying @{thm  eq_pv_blocked_persist} to this: *}
+    from eq_pv_blocked_persist[OF neq_th' otherwise] 
+    -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *}
+    have "th' \<notin> runing (t@s)" .
+    -- {* This is obvious in contradiction with assumption @{thm is_runing}  *}
+    thus False using is_runing by simp
+  qed
+  -- {* However, the number of @{term V} is always less or equal to @{term P}: *}
+  moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
+  -- {* Thesis is finally derived by combining the these two results: *}
+  ultimately show ?thesis by auto
+qed
+
 
 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 proof is a  simple combination of the results above:
 *}
-lemma runing_threads_inv: (* ddd *)
+lemma runing_threads_inv: 
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th': "th' \<noteq> th"
   shows "th' \<in> threads s"
-proof -
-    -- {* The proof is by contradiction: *}
-    { assume otherwise: "\<not> ?thesis"
-      have "th' \<notin> runing (t @ s)"
-      proof -
-        -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *}
-        have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def)
-        -- {* However, @{text "th'"} does not exist at very beginning. *}
-        have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise
-          by (metis append.simps(1) moment_zero)
-        -- {* Therefore, there must be a moment during @{text "t"}, when 
-              @{text "th'"} came into being. *}
-        -- {* Let us suppose the moment being @{text "i"}: *}
-        from p_split_gen[OF th'_in th'_notin]
-        obtain i where lt_its: "i < length t"
-                 and le_i: "0 \<le> i"
-                 and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")
-                 and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto)
-        interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)
-        interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales)
-        from lt_its have "Suc i \<le> length t" by auto
-        -- {* Let us also suppose the event which makes this change is @{text e}: *}
-        from moment_head[OF this] obtain e where 
-          eq_me: "moment (Suc i) t = e # moment i t" by blast
-        hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) 
-        hence "PIP (moment i t @ s) e" by (cases, simp)
-        -- {* It can be derived that this event @{text "e"}, which 
-              gives birth to @{term "th'"} must be a @{term "Create"}: *}
-        from create_pre[OF this, of th']
-        obtain prio where eq_e: "e = Create th' prio"
-            by (metis append_Cons eq_me lessI post pre) 
-        have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto 
-        have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'"
-        proof -
-          have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
-            by (metis h_i.cnp_cnv_eq pre)
-          thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def)
-        qed
-        show ?thesis 
-          using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge
-            by auto
-      qed
-      with `th' \<in> runing (t@s)`
-      have False by simp
-    } thus ?thesis by auto
+proof(rule ccontr) -- {* Proof by contradiction: *}
+  assume otherwise: "th' \<notin> threads s" 
+  have "th' \<notin> runing (t @ s)"
+  proof -
+    from vat_s.cnp_cnv_eq[OF otherwise]
+    have "cntP s th' = cntV s th'" .
+    from eq_pv_blocked_persist[OF neq_th' this]
+    show ?thesis .
+  qed
+  with runing' show False by simp
 qed
 
 text {*
   The following lemma summarizes several foregoing 
   lemmas to give an overall picture of the blocking thread @{text "th'"}:
 *}
-lemma runing_inversion:
+lemma runing_inversion: (* ddd, one of the main lemmas to present *)
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
   shows "th' \<in> threads s"
@@ -805,13 +664,15 @@
   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']
+  from runing_cntP_cntV_inv[OF runing' neq_th]
   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
 
+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'"} 
@@ -822,7 +683,7 @@
   is the @{term runing}-thread. However, we are going to show more: this running thread
   is exactly @{term "th'"}.
      *}
-lemma th_blockedE: (* ddd *)
+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)"
                     "th' \<in> runing (t@s)"
@@ -898,6 +759,3 @@
 
 end
 end
-
-
-




