31 next |
31 next |
32 show "g ` A \<subseteq> f ` A" |
32 show "g ` A \<subseteq> f ` A" |
33 by (rule image_subsetI, auto intro:h[symmetric]) |
33 by (rule image_subsetI, auto intro:h[symmetric]) |
34 qed |
34 qed |
35 |
35 |
36 lemma Max_fg_mono: |
36 |
37 assumes "finite A" |
|
38 and "\<forall> a \<in> A. f a \<le> g a" |
|
39 shows "Max (f ` A) \<le> Max (g ` A)" |
|
40 proof(cases "A = {}") |
|
41 case True |
|
42 thus ?thesis by auto |
|
43 next |
|
44 case False |
|
45 show ?thesis |
|
46 proof(rule Max.boundedI) |
|
47 from assms show "finite (f ` A)" by auto |
|
48 next |
|
49 from False show "f ` A \<noteq> {}" by auto |
|
50 next |
|
51 fix fa |
|
52 assume "fa \<in> f ` A" |
|
53 then obtain a where h_fa: "a \<in> A" "fa = f a" by auto |
|
54 show "fa \<le> Max (g ` A)" |
|
55 proof(rule Max_ge_iff[THEN iffD2]) |
|
56 from assms show "finite (g ` A)" by auto |
|
57 next |
|
58 from False show "g ` A \<noteq> {}" by auto |
|
59 next |
|
60 from h_fa have "g a \<in> g ` A" by auto |
|
61 moreover have "fa \<le> g a" using h_fa assms(2) by auto |
|
62 ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto |
|
63 qed |
|
64 qed |
|
65 qed |
|
66 |
|
67 lemma Max_f_mono: |
|
68 assumes seq: "A \<subseteq> B" |
|
69 and np: "A \<noteq> {}" |
|
70 and fnt: "finite B" |
|
71 shows "Max (f ` A) \<le> Max (f ` B)" |
|
72 proof(rule Max_mono) |
|
73 from seq show "f ` A \<subseteq> f ` B" by auto |
|
74 next |
|
75 from np show "f ` A \<noteq> {}" by auto |
|
76 next |
|
77 from fnt and seq show "finite (f ` B)" by auto |
|
78 qed |
|
79 |
|
80 lemma Max_UNION: |
|
81 assumes "finite A" |
|
82 and "A \<noteq> {}" |
|
83 and "\<forall> M \<in> f ` A. finite M" |
|
84 and "\<forall> M \<in> f ` A. M \<noteq> {}" |
|
85 shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") |
|
86 using assms[simp] |
|
87 proof - |
|
88 have "?L = Max (\<Union>(f ` A))" |
|
89 by (fold Union_image_eq, simp) |
|
90 also have "... = ?R" |
|
91 by (subst Max_Union, simp+) |
|
92 finally show ?thesis . |
|
93 qed |
|
94 |
|
95 lemma max_Max_eq: |
|
96 assumes "finite A" |
|
97 and "A \<noteq> {}" |
|
98 and "x = y" |
|
99 shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R") |
|
100 proof - |
|
101 have "?R = Max (insert y A)" by simp |
|
102 also from assms have "... = ?L" |
|
103 by (subst Max.insert, simp+) |
|
104 finally show ?thesis by simp |
|
105 qed |
|
106 |
37 |
107 section {* Lemmas do not depend on trace validity *} |
38 section {* Lemmas do not depend on trace validity *} |
108 |
39 |
109 text {* The following lemma serves to proof @{text "preced_tm_lt"} *} |
40 text {* The following lemma serves to proof @{text "preced_tm_lt"} *} |
110 |
41 |
3819 the maximum precedence of its own subtree, by applying |
3750 the maximum precedence of its own subtree, by applying |
3820 the absorbing property of @{term Max} (lemma @{thm Max_UNION}) |
3751 the absorbing property of @{term Max} (lemma @{thm Max_UNION}) |
3821 over the union of subtrees, the following equation can be derived: |
3752 over the union of subtrees, the following equation can be derived: |
3822 *} |
3753 *} |
3823 |
3754 |
3824 thm the_preced_def cpreceds_def |
3755 |
|
3756 lemma cp_alt_def3: |
|
3757 shows "cp s th = Max (preceds (subtree (tG s) th) s)" |
|
3758 unfolding cp_alt_def2 |
|
3759 unfolding image_def |
|
3760 unfolding the_preced_def |
|
3761 by meson |
|
3762 |
|
3763 lemma KK: |
|
3764 shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})" |
|
3765 (* and "\<Union>" *) |
|
3766 by (simp_all add: Setcompr_eq_image) |
|
3767 |
|
3768 lemma Max_Segments: |
|
3769 assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}" |
|
3770 shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}" |
|
3771 using assms |
|
3772 apply(subst KK(1)) |
|
3773 apply(subst Max_Union) |
|
3774 apply(auto)[3] |
|
3775 apply(simp add: Setcompr_eq_image) |
|
3776 apply(simp add: image_eq_UN) |
|
3777 done |
3825 |
3778 |
3826 lemma max_cp_readys_max_preced_tG: |
3779 lemma max_cp_readys_max_preced_tG: |
3827 shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R") |
3780 shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R") |
3828 proof(cases "readys s = {}") |
3781 proof(cases "readys s = {}") |
3829 case False |
3782 case False |
3830 have "?R = |
3783 have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)" |
3831 Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))" |
3784 unfolding threads_alt_def1 by simp |
3832 by (simp add: threads_alt_def1) |
3785 also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}" |
3833 also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) " |
3786 apply(subst Max_Segments[symmetric]) |
3834 by (unfold image_UN, simp) |
3787 prefer 5 |
3835 also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)" |
3788 apply(rule arg_cong) |
3836 proof(rule Max_UNION) |
3789 back |
3837 show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M" |
3790 apply(blast) |
3838 using fsbttGs.finite_subtree by auto |
3791 apply (simp add: finite_readys) |
3839 qed (auto simp:False subtree_def finite_readys) |
3792 apply (simp add: fsbttGs.finite_subtree) |
3840 also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)" |
3793 apply blast |
3841 by (simp add: image_comp) |
3794 using False by blast |
3842 also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") |
3795 also have "... = Max {cp s th | th. th \<in> readys s}" |
3843 proof - |
3796 unfolding cp_alt_def3 .. |
3844 have "(?f ` ?A) = (?g ` ?A)" |
3797 finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)" |
3845 proof(rule f_image_eq) |
3798 by (simp add: Setcompr_eq_image image_def) |
3846 fix th1 |
|
3847 assume "th1 \<in> ?A" |
|
3848 thus "?f th1 = ?g th1" |
|
3849 by (unfold cp_alt_def2, simp) |
|
3850 qed |
|
3851 thus ?thesis by simp |
|
3852 qed |
|
3853 finally show ?thesis by simp |
|
3854 qed (auto simp:threads_alt_def) |
3799 qed (auto simp:threads_alt_def) |
|
3800 |
|
3801 |
|
3802 lemma LL: |
|
3803 shows "the_preced s ` threads s = preceds (threads s) s" |
|
3804 using the_preced_def by auto |
3855 |
3805 |
3856 |
3806 |
3857 text {* |
3807 text {* |
3858 The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG} |
3808 The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG} |
3859 and @{thm max_cp_eq}: |
3809 and @{thm max_cp_eq}: |
3860 *} |
3810 *} |
3861 lemma max_cp_readys_threads: |
3811 lemma max_cp_readys_threads: |
3862 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" |
3812 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" |
3863 using max_cp_readys_max_preced_tG max_cp_eq by auto |
3813 apply(simp add: max_cp_readys_max_preced_tG) |
|
3814 apply(simp add: max_cp_eq) |
|
3815 apply(simp add: LL) |
|
3816 done |
3864 |
3817 |
3865 end |
3818 end |
3866 |
3819 |
3867 |
3820 |
3868 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |
3821 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |