571 qed |
571 qed |
572 |
572 |
573 instance bool :: complete_boolean_algebra proof |
573 instance bool :: complete_boolean_algebra proof |
574 qed (auto intro: bool_induct) |
574 qed (auto intro: bool_induct) |
575 |
575 |
|
576 |
|
577 subsection {* @{typ "_ \<Rightarrow> _"} as complete lattice *} |
|
578 |
576 instantiation "fun" :: (type, complete_lattice) complete_lattice |
579 instantiation "fun" :: (type, complete_lattice) complete_lattice |
577 begin |
580 begin |
578 |
581 |
579 definition |
582 definition |
580 "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)" |
583 "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)" |
605 |
608 |
606 instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof |
609 instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof |
607 qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image) |
610 qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image) |
608 |
611 |
609 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. |
612 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. |
|
613 |
|
614 |
|
615 subsection {* Unary and binary predicates as complete lattice *} |
|
616 |
|
617 lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)" |
|
618 by (simp add: INF_apply) |
|
619 |
|
620 lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)" |
|
621 by (simp add: INF_apply) |
|
622 |
|
623 lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b" |
|
624 by (auto simp add: INF_apply) |
|
625 |
|
626 lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c" |
|
627 by (auto simp add: INF_apply) |
|
628 |
|
629 lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b" |
|
630 by (auto simp add: INF_apply) |
|
631 |
|
632 lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c" |
|
633 by (auto simp add: INF_apply) |
|
634 |
|
635 lemma INF1_E [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R" |
|
636 by (auto simp add: INF_apply) |
|
637 |
|
638 lemma INF2_E [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R" |
|
639 by (auto simp add: INF_apply) |
|
640 |
|
641 lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)" |
|
642 by (simp add: SUP_apply) |
|
643 |
|
644 lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)" |
|
645 by (simp add: SUP_apply) |
|
646 |
|
647 lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b" |
|
648 by (auto simp add: SUP_apply) |
|
649 |
|
650 lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c" |
|
651 by (auto simp add: SUP_apply) |
|
652 |
|
653 lemma SUP1_E [elim!]: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R" |
|
654 by (auto simp add: SUP_apply) |
|
655 |
|
656 lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R" |
|
657 by (auto simp add: SUP_apply) |
|
658 |
|
659 |
|
660 subsection {* @{typ "_ set"} as complete lattice *} |
610 |
661 |
611 instantiation "set" :: (type) complete_lattice |
662 instantiation "set" :: (type) complete_lattice |
612 begin |
663 begin |
613 |
664 |
614 definition |
665 definition |
625 instance "set" :: (type) complete_boolean_algebra |
676 instance "set" :: (type) complete_boolean_algebra |
626 proof |
677 proof |
627 qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def) |
678 qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def) |
628 |
679 |
629 |
680 |
630 subsection {* Inter *} |
681 subsubsection {* Inter *} |
631 |
682 |
632 abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where |
683 abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where |
633 "Inter S \<equiv> \<Sqinter>S" |
684 "Inter S \<equiv> \<Sqinter>S" |
634 |
685 |
635 notation (xsymbols) |
686 notation (xsymbols) |
697 |
748 |
698 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B" |
749 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B" |
699 by (fact Inf_superset_mono) |
750 by (fact Inf_superset_mono) |
700 |
751 |
701 |
752 |
702 subsection {* Intersections of families *} |
753 subsubsection {* Intersections of families *} |
703 |
754 |
704 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
755 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
705 "INTER \<equiv> INFI" |
756 "INTER \<equiv> INFI" |
706 |
757 |
707 text {* |
758 text {* |
877 |
928 |
878 lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B" |
929 lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B" |
879 by (fact Sup_subset_mono) |
930 by (fact Sup_subset_mono) |
880 |
931 |
881 |
932 |
882 subsection {* Unions of families *} |
933 subsubsection {* Unions of families *} |
883 |
934 |
884 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
935 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
885 "UNION \<equiv> SUPR" |
936 "UNION \<equiv> SUPR" |
886 |
937 |
887 text {* |
938 text {* |
1082 |
1133 |
1083 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" |
1134 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" |
1084 by (fact Sup_inf_eq_bot_iff) |
1135 by (fact Sup_inf_eq_bot_iff) |
1085 |
1136 |
1086 |
1137 |
1087 subsection {* Complement *} |
1138 subsubsection {* Complement *} |
1088 |
1139 |
1089 lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)" |
1140 lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)" |
1090 by (fact uminus_INF) |
1141 by (fact uminus_INF) |
1091 |
1142 |
1092 lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)" |
1143 lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)" |
1093 by (fact uminus_SUP) |
1144 by (fact uminus_SUP) |
1094 |
1145 |
1095 |
1146 |
1096 subsection {* Miniscoping and maxiscoping *} |
1147 subsubsection {* Miniscoping and maxiscoping *} |
1097 |
1148 |
1098 text {* \medskip Miniscoping: pushing in quantifiers and big Unions |
1149 text {* \medskip Miniscoping: pushing in quantifiers and big Unions |
1099 and Intersections. *} |
1150 and Intersections. *} |
1100 |
1151 |
1101 lemma UN_simps [simp]: |
1152 lemma UN_simps [simp]: |