791 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
791 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
792 ultimately show ?thesis using that by metis |
792 ultimately show ?thesis using that by metis |
793 qed |
793 qed |
794 |
794 |
795 lemma (* new proof of th_blockedE *) |
795 lemma (* new proof of th_blockedE *) |
796 assumes "th \<notin> runing (t@s)" |
796 assumes "th \<notin> runing (t @ s)" |
797 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
797 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
798 "th' \<in> runing (t@s)" |
798 "th' \<in> runing (t @ s)" |
799 proof - |
799 proof - |
800 -- {* According to @{thm vat_t.th_chain_to_ready}, either |
800 |
801 @{term "th"} is in @{term "readys"} or there is path leading from it to |
801 -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is |
802 one thread in @{term "readys"}. *} |
802 in @{term "readys"} or there is path in the @{term RAG} leading from |
803 have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" |
803 it to a thread that is in @{term "readys"}. However, @{term th} cannot |
|
804 be in @{term readys}, because otherwise, since @{term th} holds the |
|
805 highest @{term cp}-value, it must be @{term "runing"}. This would |
|
806 violate our assumption. *} |
|
807 have "th \<notin> readys (t @ s)" |
|
808 using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto |
|
809 then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" |
804 using th_kept vat_t.th_chain_to_ready by auto |
810 using th_kept vat_t.th_chain_to_ready by auto |
805 -- {* However, @{term th} can not be in @{term readys}, because otherwise, since |
811 then obtain th' where th'_in: "th' \<in> readys (t@s)" |
806 @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} |
812 and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto |
807 moreover have "th \<notin> readys (t@s)" |
813 |
808 using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto |
814 -- {* We are going to first show that this @{term th'} is running. *} |
809 -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in |
815 have "th' \<in> runing (t @ s)" |
810 term @{term readys}: *} |
|
811 ultimately obtain th' where th'_in: "th' \<in> readys (t@s)" |
|
812 and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto |
|
813 -- {* We are going to show that this @{term th'} is running. *} |
|
814 have "th' \<in> runing (t@s)" |
|
815 proof - |
816 proof - |
816 -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} |
817 -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *} |
817 have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") |
818 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R") |
818 proof - |
819 proof - |
819 -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), |
820 -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), |
820 the @{term cp}-value of @{term th'} is the maximum of |
821 the @{term cp}-value of @{term th'} is the maximum of |
821 all precedences of all thread nodes in its @{term tRAG}-subtree: *} |
822 all precedences of all thread nodes in its @{term tRAG}-subtree: *} |
822 have "?L = Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))" |
823 have "?L = Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))" |
826 by fastforce |
827 by fastforce |
827 thus ?thesis by (unfold cp_alt_def1, simp) |
828 thus ?thesis by (unfold cp_alt_def1, simp) |
828 qed |
829 qed |
829 also have "... = (the_preced (t @ s) th)" |
830 also have "... = (the_preced (t @ s) th)" |
830 proof(rule image_Max_subset) |
831 proof(rule image_Max_subset) |
831 show "finite (threads (t@s))" by (simp add: vat_t.finite_threads) |
832 show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) |
832 next |
833 next |
833 show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)" |
834 show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)" |
834 by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in |
835 by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in |
835 the_thread.simps vat_t.subtree_tRAG_thread) |
836 the_thread.simps vat_t.subtree_tRAG_thread) |
836 next |
837 next |
845 by simp |
846 by simp |
846 qed |
847 qed |
847 also have "... = ?R" |
848 also have "... = ?R" |
848 using th_cp_max th_cp_preced th_kept |
849 using th_cp_max th_cp_preced th_kept |
849 the_preced_def vat_t.max_cp_readys_threads by auto |
850 the_preced_def vat_t.max_cp_readys_threads by auto |
850 thm th_cp_max th_cp_preced th_kept |
851 finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . |
851 the_preced_def vat_t.max_cp_readys_threads |
|
852 finally show ?thesis . |
|
853 qed |
852 qed |
854 -- {* Now, since @{term th'} holds the highest @{term cp} |
853 |
855 and we have already show it is in @{term readys}, |
854 -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, |
856 it is @{term runing} by definition. *} |
855 it is @{term runing} by definition. *} |
857 with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) |
856 with `th' \<in> readys (t @ s)` show "th' \<in> runing (t @ s)" by (simp add: runing_def) |
858 qed |
857 qed |
|
858 |
859 -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} |
859 -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} |
860 moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
860 moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
861 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
861 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
862 ultimately show ?thesis using that by metis |
862 ultimately show ?thesis using that by metis |
863 qed |
863 qed |
|
864 |
|
865 lemma th_blockedE_pretty: |
|
866 assumes "th \<notin> runing (t@s)" |
|
867 shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> runing (t@s)" |
|
868 using th_blockedE assms by blast |
864 |
869 |
865 text {* |
870 text {* |
866 Now it is easy to see there is always a thread to run by case analysis |
871 Now it is easy to see there is always a thread to run by case analysis |
867 on whether thread @{term th} is running: if the answer is Yes, the |
872 on whether thread @{term th} is running: if the answer is Yes, the |
868 the running thread is obviously @{term th} itself; otherwise, the running |
873 the running thread is obviously @{term th} itself; otherwise, the running |