3627 and the second lemma @{text "readys_subtree_disjoint"} shows |
3627 and the second lemma @{text "readys_subtree_disjoint"} shows |
3628 subtrees of different threads in @{term readys}-set |
3628 subtrees of different threads in @{term readys}-set |
3629 are disjoint. |
3629 are disjoint. |
3630 *} |
3630 *} |
3631 |
3631 |
|
3632 lemma subtree_RAG_tG: |
|
3633 shows "subtree (tG s) th = {th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
3634 using subtree_tG_tRAG threads_set_eq by auto |
|
3635 |
|
3636 |
3632 lemma threads_alt_def: |
3637 lemma threads_alt_def: |
3633 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
3638 "threads s = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
3634 (is "?L = ?R") |
3639 (is "?L = ?R") |
3635 proof - |
3640 proof - |
3636 { fix th1 |
3641 { fix th1 |
3637 assume "th1 \<in> ?L" |
3642 assume "th1 \<in> ?L" |
3638 from th_chain_to_ready[OF this] |
3643 from th_chain_to_ready[OF this] |
3810 the maximum precedence of its own subtree, by applying |
3819 the maximum precedence of its own subtree, by applying |
3811 the absorbing property of @{term Max} (lemma @{thm Max_UNION}) |
3820 the absorbing property of @{term Max} (lemma @{thm Max_UNION}) |
3812 over the union of subtrees, the following equation can be derived: |
3821 over the union of subtrees, the following equation can be derived: |
3813 *} |
3822 *} |
3814 |
3823 |
3815 lemma max_cp_readys_max_preced: |
3824 thm the_preced_def cpreceds_def |
|
3825 |
|
3826 lemma max_cp_readys_max_preced_tG: |
3816 shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R") |
3827 shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R") |
3817 proof(cases "readys s = {}") |
3828 proof(cases "readys s = {}") |
3818 case False |
3829 case False |
3819 have "?R = |
3830 have "?R = |
3820 Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
3831 Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))" |
3821 by (simp add: threads_alt_def) |
3832 by (simp add: threads_alt_def1) |
3822 also have "... = |
3833 also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) " |
3823 Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))" |
3834 by (unfold image_UN, simp) |
3824 by (unfold image_UN, simp) |
3835 also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)" |
3825 also have "... = |
|
3826 Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" |
|
3827 proof(rule Max_UNION) |
3836 proof(rule Max_UNION) |
3828 show "\<forall>M\<in>(\<lambda>x. the_preced s ` |
3837 show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M" |
3829 {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M" |
3838 using fsbttGs.finite_subtree by auto |
3830 using finite_subtree_threads by auto |
|
3831 qed (auto simp:False subtree_def finite_readys) |
3839 qed (auto simp:False subtree_def finite_readys) |
3832 also have "... = |
3840 also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)" |
3833 Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` |
3841 by (simp add: image_comp) |
3834 readys s)" |
|
3835 by (simp add: image_comp) |
|
3836 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") |
3842 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") |
3837 proof - |
3843 proof - |
3838 have "(?f ` ?A) = (?g ` ?A)" |
3844 have "(?f ` ?A) = (?g ` ?A)" |
3839 proof(rule f_image_eq) |
3845 proof(rule f_image_eq) |
3840 fix th1 |
3846 fix th1 |
3841 assume "th1 \<in> ?A" |
3847 assume "th1 \<in> ?A" |
3842 thus "?f th1 = ?g th1" |
3848 thus "?f th1 = ?g th1" |
3843 by (unfold cp_alt_def, simp) |
3849 by (unfold cp_alt_def2, simp) |
3844 qed |
3850 qed |
3845 thus ?thesis by simp |
3851 thus ?thesis by simp |
3846 qed |
3852 qed |
3847 finally show ?thesis by simp |
3853 finally show ?thesis by simp |
3848 qed (auto simp:threads_alt_def) |
3854 qed (auto simp:threads_alt_def) |
3849 |
3855 |
3850 text {* |
3856 |
3851 The following lemma is simply a corollary of @{thm max_cp_readys_max_preced} |
3857 text {* |
|
3858 The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG} |
3852 and @{thm max_cp_eq}: |
3859 and @{thm max_cp_eq}: |
3853 *} |
3860 *} |
3854 lemma max_cp_readys_threads: |
3861 lemma max_cp_readys_threads: |
3855 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" |
3862 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" |
3856 using max_cp_readys_max_preced max_cp_eq by auto |
3863 using max_cp_readys_max_preced_tG max_cp_eq by auto |
3857 |
3864 |
3858 end |
3865 end |
3859 |
3866 |
3860 |
3867 |
3861 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |
3868 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |