290 lemma SUP_mono: |
290 lemma SUP_mono: |
291 "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)" |
291 "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)" |
292 by (force intro!: Sup_mono simp: SUP_def) |
292 by (force intro!: Sup_mono simp: SUP_def) |
293 |
293 |
294 lemma INF_superset_mono: |
294 lemma INF_superset_mono: |
295 "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f" |
295 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)" |
296 by (rule INF_mono) auto |
296 -- {* The last inclusion is POSITIVE! *} |
|
297 by (blast intro: INF_mono dest: subsetD) |
297 |
298 |
298 lemma SUP_subset_mono: |
299 lemma SUP_subset_mono: |
299 "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f" |
300 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)" |
300 by (rule SUP_mono) auto |
301 by (blast intro: SUP_mono dest: subsetD) |
301 |
302 |
302 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)" |
303 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)" |
303 by (iprover intro: INF_leI le_INF_I order_trans antisym) |
304 by (iprover intro: INF_leI le_INF_I order_trans antisym) |
304 |
305 |
305 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)" |
306 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)" |
369 |
370 |
370 lemma SUP_UNIV_bool_expand: |
371 lemma SUP_UNIV_bool_expand: |
371 "(\<Squnion>b. A b) = A True \<squnion> A False" |
372 "(\<Squnion>b. A b) = A True \<squnion> A False" |
372 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute) |
373 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute) |
373 |
374 |
374 lemma INF_mono': |
|
375 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)" |
|
376 -- {* The last inclusion is POSITIVE! *} |
|
377 by (rule INF_mono) auto |
|
378 |
|
379 lemma SUP_mono': |
|
380 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)" |
|
381 -- {* The last inclusion is POSITIVE! *} |
|
382 by (blast intro: SUP_mono dest: subsetD) |
|
383 |
|
384 end |
375 end |
385 |
|
386 lemma Inf_less_iff: |
|
387 fixes a :: "'a\<Colon>{complete_lattice,linorder}" |
|
388 shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)" |
|
389 unfolding not_le [symmetric] le_Inf_iff by auto |
|
390 |
|
391 lemma less_Sup_iff: |
|
392 fixes a :: "'a\<Colon>{complete_lattice,linorder}" |
|
393 shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)" |
|
394 unfolding not_le [symmetric] Sup_le_iff by auto |
|
395 |
|
396 lemma INF_less_iff: |
|
397 fixes a :: "'a::{complete_lattice,linorder}" |
|
398 shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)" |
|
399 unfolding INF_def Inf_less_iff by auto |
|
400 |
|
401 lemma less_SUP_iff: |
|
402 fixes a :: "'a::{complete_lattice,linorder}" |
|
403 shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)" |
|
404 unfolding SUP_def less_Sup_iff by auto |
|
405 |
376 |
406 class complete_boolean_algebra = boolean_algebra + complete_lattice |
377 class complete_boolean_algebra = boolean_algebra + complete_lattice |
407 begin |
378 begin |
408 |
379 |
409 lemma uminus_Inf: |
380 lemma uminus_Inf: |
425 lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)" |
396 lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)" |
426 by (simp add: INF_def SUP_def uminus_Inf image_image) |
397 by (simp add: INF_def SUP_def uminus_Inf image_image) |
427 |
398 |
428 lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)" |
399 lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)" |
429 by (simp add: INF_def SUP_def uminus_Sup image_image) |
400 by (simp add: INF_def SUP_def uminus_Sup image_image) |
|
401 |
|
402 end |
|
403 |
|
404 class complete_linorder = linorder + complete_lattice |
|
405 begin |
|
406 |
|
407 lemma Inf_less_iff: |
|
408 "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)" |
|
409 unfolding not_le [symmetric] le_Inf_iff by auto |
|
410 |
|
411 lemma less_Sup_iff: |
|
412 "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)" |
|
413 unfolding not_le [symmetric] Sup_le_iff by auto |
|
414 |
|
415 lemma INF_less_iff: |
|
416 "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)" |
|
417 unfolding INF_def Inf_less_iff by auto |
|
418 |
|
419 lemma less_SUP_iff: |
|
420 "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)" |
|
421 unfolding SUP_def less_Sup_iff by auto |
430 |
422 |
431 end |
423 end |
432 |
424 |
433 |
425 |
434 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *} |
426 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *} |
686 by (fact INF_UNIV_bool_expand) |
678 by (fact INF_UNIV_bool_expand) |
687 |
679 |
688 lemma INT_anti_mono: |
680 lemma INT_anti_mono: |
689 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)" |
681 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)" |
690 -- {* The last inclusion is POSITIVE! *} |
682 -- {* The last inclusion is POSITIVE! *} |
691 by (fact INF_mono') |
683 by (fact INF_superset_mono) |
692 |
684 |
693 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" |
685 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" |
694 by blast |
686 by blast |
695 |
687 |
696 lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)" |
688 lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)" |
920 by blast |
912 by blast |
921 |
913 |
922 lemma UN_mono: |
914 lemma UN_mono: |
923 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> |
915 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> |
924 (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)" |
916 (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)" |
925 by (fact SUP_mono') |
917 by (fact SUP_subset_mono) |
926 |
918 |
927 lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)" |
919 lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)" |
928 by blast |
920 by blast |
929 |
921 |
930 lemma vimage_UN: "f -` (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. f -` B x)" |
922 lemma vimage_UN: "f -` (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. f -` B x)" |
1081 lemmas (in complete_lattice) INFI_def = INF_def |
1073 lemmas (in complete_lattice) INFI_def = INF_def |
1082 lemmas (in complete_lattice) SUPR_def = SUP_def |
1074 lemmas (in complete_lattice) SUPR_def = SUP_def |
1083 lemmas (in complete_lattice) le_SUPI = le_SUP_I |
1075 lemmas (in complete_lattice) le_SUPI = le_SUP_I |
1084 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2 |
1076 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2 |
1085 lemmas (in complete_lattice) le_INFI = le_INF_I |
1077 lemmas (in complete_lattice) le_INFI = le_INF_I |
1086 lemmas (in complete_lattice) INF_subset = INF_superset_mono |
1078 |
|
1079 lemma (in complete_lattice) INF_subset: |
|
1080 "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f" |
|
1081 by (rule INF_superset_mono) auto |
|
1082 |
1087 lemmas INFI_apply = INF_apply |
1083 lemmas INFI_apply = INF_apply |
1088 lemmas SUPR_apply = SUP_apply |
1084 lemmas SUPR_apply = SUP_apply |
1089 |
1085 |
1090 text {* Finally *} |
1086 text {* Finally *} |
1091 |
1087 |