diff -r 95e7933968f8 -r a88af0e4731f Correctness.thy
--- a/Correctness.thy	Thu Jun 02 13:15:03 2016 +0100
+++ b/Correctness.thy	Tue Jun 07 13:51:39 2016 +0100
@@ -793,28 +793,29 @@
 qed
 
 lemma (* new proof of th_blockedE *)
-  assumes "th \<notin> runing (t@s)"
+  assumes "th \<notin> runing (t @ s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-                    "th' \<in> runing (t@s)"
+                    "th' \<in> runing (t @ s)"
 proof -
-  -- {* According to @{thm vat_t.th_chain_to_ready}, either 
-        @{term "th"} is in @{term "readys"} or there is path leading from it to 
-        one thread in @{term "readys"}. *}
-  have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" 
+  
+  -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is 
+        in @{term "readys"} or there is path in the @{term RAG} leading from 
+        it to a thread that is in @{term "readys"}. However, @{term th} cannot 
+        be in @{term readys}, because otherwise, since @{term th} holds the 
+        highest @{term cp}-value, it must be @{term "runing"}. This would
+        violate our assumption. *}
+  have "th \<notin> readys (t @ s)" 
+    using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 
+  then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" 
     using th_kept vat_t.th_chain_to_ready by auto
-  -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 
-       @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
-  moreover have "th \<notin> readys (t@s)" 
-    using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 
-  -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
-        term @{term readys}: *}
-  ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
-                          and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
-  -- {* We are going to show that this @{term th'} is running. *}
-  have "th' \<in> runing (t@s)"
+  then obtain th' where th'_in: "th' \<in> readys (t@s)"
+                    and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
+  
+  -- {* We are going to first show that this @{term th'} is running. *}
+  have "th' \<in> runing (t @ s)"
   proof -
-    -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
-    have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
+    -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
+    have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
     proof -
       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
             the  @{term cp}-value of @{term th'} is the maximum of 
@@ -828,7 +829,7 @@
       qed
       also have "... = (the_preced (t @ s) th)"
       proof(rule image_Max_subset)
-        show "finite (threads (t@s))" by (simp add: vat_t.finite_threads)
+        show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
       next
         show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
           by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in 
@@ -847,21 +848,25 @@
       also have "... = ?R"
         using th_cp_max th_cp_preced th_kept 
               the_preced_def vat_t.max_cp_readys_threads by auto
-              thm th_cp_max th_cp_preced th_kept 
-              the_preced_def vat_t.max_cp_readys_threads
-      finally show ?thesis .
+      finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
     qed 
-    -- {* Now, since @{term th'} holds the highest @{term cp} 
-          and we have already show it is in @{term readys},
+
+    -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
           it is @{term runing} by definition. *}
-    with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) 
+    with `th' \<in> readys (t @ s)` show "th' \<in> runing (t @ s)" by (simp add: runing_def) 
   qed
+
   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
   ultimately show ?thesis using that by metis
 qed
 
+lemma th_blockedE_pretty:
+  assumes "th \<notin> runing (t@s)"
+  shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> runing (t@s)"
+using th_blockedE assms by blast
+
 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