73 case empty |
73 case empty |
74 assume "{} \<noteq> {}" show ?case by auto |
74 assume "{} \<noteq> {}" show ?case by auto |
75 qed |
75 qed |
76 |
76 |
77 |
77 |
|
78 lemma Max_fg_mono: |
|
79 assumes "finite A" |
|
80 and "\<forall> a \<in> A. f a \<le> g a" |
|
81 shows "Max (f ` A) \<le> Max (g ` A)" |
|
82 proof(cases "A = {}") |
|
83 case True |
|
84 thus ?thesis by auto |
|
85 next |
|
86 case False |
|
87 show ?thesis |
|
88 proof(rule Max.boundedI) |
|
89 from assms show "finite (f ` A)" by auto |
|
90 next |
|
91 from False show "f ` A \<noteq> {}" by auto |
|
92 next |
|
93 fix fa |
|
94 assume "fa \<in> f ` A" |
|
95 then obtain a where h_fa: "a \<in> A" "fa = f a" by auto |
|
96 show "fa \<le> Max (g ` A)" |
|
97 proof(rule Max_ge_iff[THEN iffD2]) |
|
98 from assms show "finite (g ` A)" by auto |
|
99 next |
|
100 from False show "g ` A \<noteq> {}" by auto |
|
101 next |
|
102 from h_fa have "g a \<in> g ` A" by auto |
|
103 moreover have "fa \<le> g a" using h_fa assms(2) by auto |
|
104 ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto |
|
105 qed |
|
106 qed |
|
107 qed |
|
108 |
|
109 lemma Max_f_mono: |
|
110 assumes seq: "A \<subseteq> B" |
|
111 and np: "A \<noteq> {}" |
|
112 and fnt: "finite B" |
|
113 shows "Max (f ` A) \<le> Max (f ` B)" |
|
114 proof(rule Max_mono) |
|
115 from seq show "f ` A \<subseteq> f ` B" by auto |
|
116 next |
|
117 from np show "f ` A \<noteq> {}" by auto |
|
118 next |
|
119 from fnt and seq show "finite (f ` B)" by auto |
|
120 qed |
|
121 |
|
122 lemma Max_UNION: |
|
123 assumes "finite A" |
|
124 and "A \<noteq> {}" |
|
125 and "\<forall> M \<in> f ` A. finite M" |
|
126 and "\<forall> M \<in> f ` A. M \<noteq> {}" |
|
127 shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R") |
|
128 using assms[simp] |
|
129 proof - |
|
130 have "?L = Max (\<Union>(f ` A))" |
|
131 by (fold Union_image_eq, simp) |
|
132 also have "... = ?R" |
|
133 by (subst Max_Union, simp+) |
|
134 finally show ?thesis . |
|
135 qed |
|
136 |
|
137 lemma max_Max_eq: |
|
138 assumes "finite A" |
|
139 and "A \<noteq> {}" |
|
140 and "x = y" |
|
141 shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R") |
|
142 proof - |
|
143 have "?R = Max (insert y A)" by simp |
|
144 also from assms have "... = ?L" |
|
145 by (subst Max.insert, simp+) |
|
146 finally show ?thesis by simp |
|
147 qed |
|
148 |
|
149 |
78 end |
150 end |