140 and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" |
146 and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" |
141 assumes cSup_upper: "x \<in> X \<Longrightarrow> bdd_above X \<Longrightarrow> x \<le> Sup X" |
147 assumes cSup_upper: "x \<in> X \<Longrightarrow> bdd_above X \<Longrightarrow> x \<le> Sup X" |
142 and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" |
148 and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" |
143 begin |
149 begin |
144 |
150 |
|
151 lemma cSup_upper2: "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> bdd_above X \<Longrightarrow> y \<le> Sup X" |
|
152 by (metis cSup_upper order_trans) |
|
153 |
|
154 lemma cInf_lower2: "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> y" |
|
155 by (metis cInf_lower order_trans) |
|
156 |
|
157 lemma cSup_mono: "B \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. b \<le> a) \<Longrightarrow> Sup B \<le> Sup A" |
|
158 by (metis cSup_least cSup_upper2) |
|
159 |
|
160 lemma cInf_mono: "B \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b) \<Longrightarrow> Inf A \<le> Inf B" |
|
161 by (metis cInf_greatest cInf_lower2) |
|
162 |
|
163 lemma cSup_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Sup A \<le> Sup B" |
|
164 by (metis cSup_least cSup_upper subsetD) |
|
165 |
|
166 lemma cInf_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Inf B \<le> Inf A" |
|
167 by (metis cInf_greatest cInf_lower subsetD) |
|
168 |
145 lemma cSup_eq_maximum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z" |
169 lemma cSup_eq_maximum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z" |
146 by (intro antisym cSup_upper[of z X] cSup_least[of X z]) auto |
170 by (intro antisym cSup_upper[of z X] cSup_least[of X z]) auto |
147 |
171 |
148 lemma cInf_eq_minimum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z" |
172 lemma cInf_eq_minimum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z" |
149 by (intro antisym cInf_lower[of z X] cInf_greatest[of X z]) auto |
173 by (intro antisym cInf_lower[of z X] cInf_greatest[of X z]) auto |
151 lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)" |
175 lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)" |
152 by (metis order_trans cSup_upper cSup_least) |
176 by (metis order_trans cSup_upper cSup_least) |
153 |
177 |
154 lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)" |
178 lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)" |
155 by (metis order_trans cInf_lower cInf_greatest) |
179 by (metis order_trans cInf_lower cInf_greatest) |
156 |
|
157 lemma cSup_singleton [simp]: "Sup {x} = x" |
|
158 by (intro cSup_eq_maximum) auto |
|
159 |
|
160 lemma cInf_singleton [simp]: "Inf {x} = x" |
|
161 by (intro cInf_eq_minimum) auto |
|
162 |
|
163 lemma cSup_upper2: "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> bdd_above X \<Longrightarrow> y \<le> Sup X" |
|
164 by (metis cSup_upper order_trans) |
|
165 |
|
166 lemma cInf_lower2: "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> y" |
|
167 by (metis cInf_lower order_trans) |
|
168 |
180 |
169 lemma cSup_eq_non_empty: |
181 lemma cSup_eq_non_empty: |
170 assumes 1: "X \<noteq> {}" |
182 assumes 1: "X \<noteq> {}" |
171 assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" |
183 assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" |
172 assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" |
184 assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" |
190 by (intro cSup_eq_non_empty) (auto intro: le_supI2 cSup_upper cSup_least) |
202 by (intro cSup_eq_non_empty) (auto intro: le_supI2 cSup_upper cSup_least) |
191 |
203 |
192 lemma cInf_insert: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf (insert a X) = inf a (Inf X)" |
204 lemma cInf_insert: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf (insert a X) = inf a (Inf X)" |
193 by (intro cInf_eq_non_empty) (auto intro: le_infI2 cInf_lower cInf_greatest) |
205 by (intro cInf_eq_non_empty) (auto intro: le_infI2 cInf_lower cInf_greatest) |
194 |
206 |
|
207 lemma cSup_singleton [simp]: "Sup {x} = x" |
|
208 by (intro cSup_eq_maximum) auto |
|
209 |
|
210 lemma cInf_singleton [simp]: "Inf {x} = x" |
|
211 by (intro cInf_eq_minimum) auto |
|
212 |
195 lemma cSup_insert_If: "bdd_above X \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))" |
213 lemma cSup_insert_If: "bdd_above X \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))" |
196 using cSup_insert[of X] by simp |
214 using cSup_insert[of X] by simp |
197 |
215 |
198 lemma cInf_insert_if: "bdd_below X \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))" |
216 lemma cInf_insert_If: "bdd_below X \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))" |
199 using cInf_insert[of X] by simp |
217 using cInf_insert[of X] by simp |
200 |
218 |
201 lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X" |
219 lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X" |
202 proof (induct X arbitrary: x rule: finite_induct) |
220 proof (induct X arbitrary: x rule: finite_induct) |
203 case (insert x X y) then show ?case |
221 case (insert x X y) then show ?case |
231 lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y" |
249 lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y" |
232 by (auto intro!: cInf_eq_minimum) |
250 by (auto intro!: cInf_eq_minimum) |
233 |
251 |
234 lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y" |
252 lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y" |
235 by (auto intro!: cInf_eq_minimum) |
253 by (auto intro!: cInf_eq_minimum) |
|
254 |
|
255 lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x" |
|
256 unfolding INF_def by (rule cInf_lower) auto |
|
257 |
|
258 lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f" |
|
259 unfolding INF_def by (rule cInf_greatest) auto |
|
260 |
|
261 lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f" |
|
262 unfolding SUP_def by (rule cSup_upper) auto |
|
263 |
|
264 lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M" |
|
265 unfolding SUP_def by (rule cSup_least) auto |
|
266 |
|
267 lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u" |
|
268 by (auto intro: cINF_lower assms order_trans) |
|
269 |
|
270 lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f" |
|
271 by (auto intro: cSUP_upper assms order_trans) |
|
272 |
|
273 lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)" |
|
274 by (metis cINF_greatest cINF_lower assms order_trans) |
|
275 |
|
276 lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)" |
|
277 by (metis cSUP_least cSUP_upper assms order_trans) |
|
278 |
|
279 lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)" |
|
280 by (metis INF_def cInf_insert assms empty_is_image image_insert) |
|
281 |
|
282 lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)" |
|
283 by (metis SUP_def cSup_insert assms empty_is_image image_insert) |
|
284 |
|
285 lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFI A f \<le> INFI B g" |
|
286 unfolding INF_def by (auto intro: cInf_mono) |
|
287 |
|
288 lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPR A f \<le> SUPR B g" |
|
289 unfolding SUP_def by (auto intro: cSup_mono) |
|
290 |
|
291 lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFI B g \<le> INFI A f" |
|
292 by (rule cINF_mono) auto |
|
293 |
|
294 lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPR A f \<le> SUPR B g" |
|
295 by (rule cSUP_mono) auto |
|
296 |
|
297 lemma less_eq_cInf_inter: "bdd_below A \<Longrightarrow> bdd_below B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> inf (Inf A) (Inf B) \<le> Inf (A \<inter> B)" |
|
298 by (metis cInf_superset_mono lattice_class.inf_sup_ord(1) le_infI1) |
|
299 |
|
300 lemma cSup_inter_less_eq: "bdd_above A \<Longrightarrow> bdd_above B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> Sup (A \<inter> B) \<le> sup (Sup A) (Sup B) " |
|
301 by (metis cSup_subset_mono lattice_class.inf_sup_ord(1) le_supI1) |
|
302 |
|
303 lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)" |
|
304 by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower) |
|
305 |
|
306 lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFI (A \<union> B) f = inf (INFI A f) (INFI B f)" |
|
307 unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib) |
|
308 |
|
309 lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)" |
|
310 by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper) |
|
311 |
|
312 lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPR (A \<union> B) f = sup (SUPR A f) (SUPR B f)" |
|
313 unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib) |
|
314 |
|
315 lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))" |
|
316 by (intro antisym le_infI cINF_greatest cINF_lower2) |
|
317 (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI) |
|
318 |
|
319 lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPR A f) (SUPR A g) = (SUP a:A. sup (f a) (g a))" |
|
320 by (intro antisym le_supI cSUP_least cSUP_upper2) |
|
321 (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI) |
236 |
322 |
237 end |
323 end |
238 |
324 |
239 instance complete_lattice \<subseteq> conditionally_complete_lattice |
325 instance complete_lattice \<subseteq> conditionally_complete_lattice |
240 by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) |
326 by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) |
321 (metis `a<b` `~ P b` linear less_le) |
407 (metis `a<b` `~ P b` linear less_le) |
322 qed |
408 qed |
323 |
409 |
324 end |
410 end |
325 |
411 |
326 class linear_continuum = conditionally_complete_linorder + dense_linorder + |
412 lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X" |
327 assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b" |
413 using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp |
328 begin |
414 |
329 |
415 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X" |
330 lemma ex_gt_or_lt: "\<exists>b. a < b \<or> b < a" |
416 using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp |
331 by (metis UNIV_not_singleton neq_iff) |
|
332 |
|
333 end |
|
334 |
417 |
335 lemma cSup_bounds: |
418 lemma cSup_bounds: |
336 fixes S :: "'a :: conditionally_complete_lattice set" |
419 fixes S :: "'a :: conditionally_complete_lattice set" |
337 assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b" |
420 assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b" |
338 shows "a \<le> Sup S \<and> Sup S \<le> b" |
421 shows "a \<le> Sup S \<and> Sup S \<le> b" |
345 by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) |
428 by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) |
346 (metis le_iff_sup le_sup_iff y) |
429 (metis le_iff_sup le_sup_iff y) |
347 with b show ?thesis by blast |
430 with b show ?thesis by blast |
348 qed |
431 qed |
349 |
432 |
350 |
|
351 lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b" |
433 lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b" |
352 by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) |
434 by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) |
353 |
435 |
354 lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b" |
436 lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b" |
355 by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) |
437 by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) |
356 |
438 |
357 lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X" |
|
358 using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp |
|
359 |
|
360 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X" |
|
361 using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp |
|
362 |
|
363 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
439 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
364 by (auto intro!: cSup_eq_non_empty intro: dense_le) |
440 by (auto intro!: cSup_eq_non_empty intro: dense_le) |
365 |
441 |
366 lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
442 lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
367 by (auto intro!: cSup_eq intro: dense_le_bounded) |
443 by (auto intro!: cSup_eq intro: dense_le_bounded) |