739 (*

   740 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)

   741   assumes "th \<notin> running (t @ s)"

   742   obtains th' where "th' \<in> ancestors (tG (t @ s)) th"

   743                     "th' \<in> running (t @ s)"

   744 proof -

   745   -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either 

   746         @{term "th"} is in @{term "readys"} or there is path leading from it to 

   747         one thread in @{term "readys"}. *}

   748   have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (th, th') \<in> (tG (t @ s))\<^sup>+)" 

   749     using th_kept vat_t.th_chain_to_ready_tG by blast

   750   

   751   -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 

   752        @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *}

   753   moreover have "th \<notin> readys (t @ s)" 

   754     using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 

   755   

   756   -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 

   757         term @{term readys}: *}

   758   ultimately obtain th' where th'_readys: "th' \<in> readys (t @ s)"

   759                           and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto

   760 

   761   -- {* @{text "th'"} is an ancestor of @{term "th"} *}

   762   have "th' \<in> ancestors (tG (t @ s)) th" using dp

   763     unfolding ancestors_def by simp

   764 

   765   moreover

   766   -- {* We are going to show that this @{term th'} is running. *}

   767   have "th' \<in> running (t @ s)"

   768   proof -

   769     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}

   770     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R")

   771     proof -

   772       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),

   773             the  @{term cp}-value of @{term th'} is the maximum of 

   774             all precedences of all thread nodes in its @{term tRAG}-subtree: *}

   775       

   776       have "?L =  Max (preceds (subtree (tG (t @ s)) th') (t @ s))"

   777             unfolding cp_alt_def2 image_def the_preced_def by meson 

   778       also have "... = (preced th (t @ s))"

   779       thm subset_Max

   780       thm preced_unique

   781       proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"])

   782         show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)

   783       next

   784         have "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"

   785           using readys_def th'_readys vat_t.subtree_tG_thread by auto 

   786         then show "preceds (subtree (tG (t @ s)) th') (t @ s) \<subseteq> preceds (threads (t @ s)) (t @ s)"

   787           by auto

   788       next

   789         have "th \<in> subtree (tG (t @ s)) th'"

   790           by (simp add: dp subtree_def trancl_into_rtrancl)   

   791         then show " preced th (t @ s) \<in> preceds (subtree (tG (t @ s)) th') (t @ s)"

   792           by blast

   793       next

   794         have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"

   795           apply(simp only: the_preced_def)

   796           by simp 

   797         show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)"

   798           thm th_kept max_kept

   799           apply(simp del: th_kept)

   800           apply(simp only: the_preced_def image_def)

   801           apply(simp add: Bex_def_raw)

   802           

   803       qed

   804       also have "... = ?R"

   805         using th_cp_max th_cp_preced th_kept 

   806               the_preced_def vat_t.max_cp_readys_threads by auto

   807       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .

   808     qed 

   809 

   810     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 

   811           it is @{term running} by definition. *}

   812     then show "th' \<in> running (t @ s)" using th'_readys 

   813       unfolding running_def by simp

   814   qed

   815 

   816   ultimately show ?thesis using that by metis

   817 qed

   818 *)

   819