--- a/Correctness.thy	Fri Oct 21 14:47:01 2016 +0100
+++ b/Correctness.thy	Fri Dec 09 12:51:29 2016 +0000
@@ -736,87 +736,6 @@
   running thread is exactly @{term "th'"}. *}
 
 
-(*
-lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  assumes "th \<notin> running (t @ s)"
-  obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
-                    "th' \<in> running (t @ s)"
-proof -
-  -- {* According to @{thm vat_t.th_chain_to_ready_tG}, 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') \<in> (tG (t @ s))\<^sup>+)" 
-    using th_kept vat_t.th_chain_to_ready_tG by blast
-  
-  -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 
-       @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *}
-  moreover have "th \<notin> readys (t @ s)" 
-    using assms running_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'_readys: "th' \<in> readys (t @ s)"
-                          and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
-
-  -- {* @{text "th'"} is an ancestor of @{term "th"} *}
-  have "th' \<in> ancestors (tG (t @ s)) th" using dp
-    unfolding ancestors_def by simp
-
-  moreover
-  -- {* We are going to show that this @{term th'} is running. *}
-  have "th' \<in> running (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")
-    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 
-            all precedences of all thread nodes in its @{term tRAG}-subtree: *}
-      
-      have "?L =  Max (preceds (subtree (tG (t @ s)) th') (t @ s))"
-            unfolding cp_alt_def2 image_def the_preced_def by meson 
-      also have "... = (preced th (t @ s))"
-      thm subset_Max
-      thm preced_unique
-      proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"])
-        show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
-      next
-        have "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
-          using readys_def th'_readys vat_t.subtree_tG_thread by auto 
-        then show "preceds (subtree (tG (t @ s)) th') (t @ s) \<subseteq> preceds (threads (t @ s)) (t @ s)"
-          by auto
-      next
-        have "th \<in> subtree (tG (t @ s)) th'"
-          by (simp add: dp subtree_def trancl_into_rtrancl)   
-        then show " preced th (t @ s) \<in> preceds (subtree (tG (t @ s)) th') (t @ s)"
-          by blast
-      next
-        have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
-          apply(simp only: the_preced_def)
-          by simp 
-        show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)"
-          thm th_kept max_kept
-          apply(simp del: th_kept)
-          apply(simp only: the_preced_def image_def)
-          apply(simp add: Bex_def_raw)
-          
-      qed
-      also have "... = ?R"
-        using th_cp_max th_cp_preced th_kept 
-              the_preced_def vat_t.max_cp_readys_threads by auto
-      finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
-    qed 
-
-    -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
-          it is @{term running} by definition. *}
-    then show "th' \<in> running (t @ s)" using th'_readys 
-      unfolding running_def by simp
-  qed
-
-  ultimately show ?thesis using that by metis
-qed
-*)
-
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
   obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
                     "th' \<in> running (t @ s)"