equal
deleted
inserted
replaced
728 running thread is exactly @{term "th'"}. |
728 running thread is exactly @{term "th'"}. |
729 |
729 |
730 *} |
730 *} |
731 |
731 |
732 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
732 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
733 assumes "th \<notin> runing (t@s)" |
733 assumes "th \<notin> runing (t @ s)" |
734 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
734 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
735 "th' \<in> runing (t@s)" |
735 "th' \<in> runing (t @ s)" |
736 proof - |
736 proof - |
737 -- {* According to @{thm vat_t.th_chain_to_ready}, either |
737 -- {* According to @{thm vat_t.th_chain_to_ready}, either |
738 @{term "th"} is in @{term "readys"} or there is path leading from it to |
738 @{term "th"} is in @{term "readys"} or there is path leading from it to |
739 one thread in @{term "readys"}. *} |
739 one thread in @{term "readys"}. *} |
740 have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" |
740 have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" |