5 *) |
5 *) |
6 |
6 |
7 header {* Conditionally-complete Lattices *} |
7 header {* Conditionally-complete Lattices *} |
8 |
8 |
9 theory Conditionally_Complete_Lattices |
9 theory Conditionally_Complete_Lattices |
10 imports Main Lubs |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X" |
13 lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X" |
14 by (induct X rule: finite_ne_induct) (simp_all add: sup_max) |
14 by (induct X rule: finite_ne_induct) (simp_all add: sup_max) |
15 |
15 |
25 lemma bdd_aboveI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> M) \<Longrightarrow> bdd_above A" |
25 lemma bdd_aboveI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> M) \<Longrightarrow> bdd_above A" |
26 by (auto simp: bdd_above_def) |
26 by (auto simp: bdd_above_def) |
27 |
27 |
28 lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A" |
28 lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A" |
29 by (auto simp: bdd_below_def) |
29 by (auto simp: bdd_below_def) |
|
30 |
|
31 lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)" |
|
32 by force |
|
33 |
|
34 lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)" |
|
35 by force |
30 |
36 |
31 lemma bdd_above_empty [simp, intro]: "bdd_above {}" |
37 lemma bdd_above_empty [simp, intro]: "bdd_above {}" |
32 unfolding bdd_above_def by auto |
38 unfolding bdd_above_def by auto |
33 |
39 |
34 lemma bdd_below_empty [simp, intro]: "bdd_below {}" |
40 lemma bdd_below_empty [simp, intro]: "bdd_below {}" |
296 by (metis cINF_greatest cINF_lower assms order_trans) |
302 by (metis cINF_greatest cINF_lower assms order_trans) |
297 |
303 |
298 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)" |
304 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)" |
299 by (metis cSUP_least cSUP_upper assms order_trans) |
305 by (metis cSUP_least cSUP_upper assms order_trans) |
300 |
306 |
|
307 lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i" |
|
308 by (metis cINF_lower less_le_trans) |
|
309 |
|
310 lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y" |
|
311 by (metis cSUP_upper le_less_trans) |
|
312 |
301 lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)" |
313 lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)" |
302 by (metis INF_def cInf_insert assms empty_is_image image_insert) |
314 by (metis INF_def cInf_insert assms empty_is_image image_insert) |
303 |
315 |
304 lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)" |
316 lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)" |
305 by (metis SUP_def cSup_insert assms empty_is_image image_insert) |
317 by (metis SUP_def cSup_insert assms empty_is_image image_insert) |
344 |
356 |
345 end |
357 end |
346 |
358 |
347 instance complete_lattice \<subseteq> conditionally_complete_lattice |
359 instance complete_lattice \<subseteq> conditionally_complete_lattice |
348 by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) |
360 by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) |
349 |
|
350 lemma isLub_cSup: |
|
351 "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)" |
|
352 by (auto simp add: isLub_def setle_def leastP_def isUb_def |
|
353 intro!: setgeI cSup_upper cSup_least) |
|
354 |
361 |
355 lemma cSup_eq: |
362 lemma cSup_eq: |
356 fixes a :: "'a :: {conditionally_complete_lattice, no_bot}" |
363 fixes a :: "'a :: {conditionally_complete_lattice, no_bot}" |
357 assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" |
364 assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" |
358 assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" |
365 assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" |
368 shows "Inf X = a" |
375 shows "Inf X = a" |
369 proof cases |
376 proof cases |
370 assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) |
377 assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) |
371 qed (intro cInf_eq_non_empty assms) |
378 qed (intro cInf_eq_non_empty assms) |
372 |
379 |
373 lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b" |
|
374 by (metis cSup_least setle_def) |
|
375 |
|
376 lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b" |
|
377 by (metis cInf_greatest setge_def) |
|
378 |
|
379 class conditionally_complete_linorder = conditionally_complete_lattice + linorder |
380 class conditionally_complete_linorder = conditionally_complete_lattice + linorder |
380 begin |
381 begin |
381 |
382 |
382 lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*) |
383 lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*) |
383 "X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)" |
384 "X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)" |
384 by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) |
385 by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) |
385 |
386 |
386 lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)" |
387 lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)" |
387 by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) |
388 by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) |
|
389 |
|
390 lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" |
|
391 unfolding INF_def using cInf_less_iff[of "f`A"] by auto |
|
392 |
|
393 lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" |
|
394 unfolding SUP_def using less_cSup_iff[of "f`A"] by auto |
388 |
395 |
389 lemma less_cSupE: |
396 lemma less_cSupE: |
390 assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x" |
397 assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x" |
391 by (metis cSup_least assms not_le that) |
398 by (metis cSup_least assms not_le that) |
392 |
399 |
435 using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp |
442 using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp |
436 |
443 |
437 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X" |
444 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X" |
438 using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp |
445 using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp |
439 |
446 |
440 lemma cSup_bounds: |
|
441 fixes S :: "'a :: conditionally_complete_lattice set" |
|
442 assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b" |
|
443 shows "a \<le> Sup S \<and> Sup S \<le> b" |
|
444 proof- |
|
445 from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast |
|
446 hence b: "Sup S \<le> b" using u |
|
447 by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) |
|
448 from Se obtain y where y: "y \<in> S" by blast |
|
449 from lub l have "a \<le> Sup S" |
|
450 by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) |
|
451 (metis le_iff_sup le_sup_iff y) |
|
452 with b show ?thesis by blast |
|
453 qed |
|
454 |
|
455 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" |
|
456 by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) |
|
457 |
|
458 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" |
|
459 by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) |
|
460 |
|
461 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
447 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
462 by (auto intro!: cSup_eq_non_empty intro: dense_le) |
448 by (auto intro!: cSup_eq_non_empty intro: dense_le) |
463 |
449 |
464 lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
450 lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" |
465 by (auto intro!: cSup_eq intro: dense_le_bounded) |
451 by (auto intro!: cSup_eq intro: dense_le_bounded) |