85 lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)" |
85 lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)" |
86 by (auto intro: Inf_greatest dest: Inf_lower) |
86 by (auto intro: Inf_greatest dest: Inf_lower) |
87 |
87 |
88 lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)" |
88 lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)" |
89 by (auto intro: Sup_least dest: Sup_upper) |
89 by (auto intro: Sup_least dest: Sup_upper) |
|
90 |
|
91 lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
|
92 by (auto intro: Inf_greatest Inf_lower) |
|
93 |
|
94 lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B" |
|
95 by (auto intro: Sup_least Sup_upper) |
90 |
96 |
91 lemma Inf_mono: |
97 lemma Inf_mono: |
92 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b" |
98 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b" |
93 shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
99 shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
94 proof (rule Inf_greatest) |
100 proof (rule Inf_greatest) |
132 from `A \<noteq> {}` obtain v where "v \<in> A" by blast |
138 from `A \<noteq> {}` obtain v where "v \<in> A" by blast |
133 moreover with assms have "u \<sqsubseteq> v" by blast |
139 moreover with assms have "u \<sqsubseteq> v" by blast |
134 ultimately show ?thesis by (rule Sup_upper2) |
140 ultimately show ?thesis by (rule Sup_upper2) |
135 qed |
141 qed |
136 |
142 |
137 lemma Inf_inter_less_eq: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)" |
143 lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)" |
138 by (auto intro: Inf_greatest Inf_lower) |
144 by (auto intro: Inf_greatest Inf_lower) |
139 |
145 |
140 lemma Sup_inter_greater_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B " |
146 lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B " |
141 by (auto intro: Sup_least Sup_upper) |
147 by (auto intro: Sup_least Sup_upper) |
142 |
148 |
143 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" |
149 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B" |
144 by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) |
150 by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2) |
145 |
151 |
175 interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom> |
181 interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom> |
176 by (fact dual_complete_lattice) |
182 by (fact dual_complete_lattice) |
177 from dual.Inf_top_conv show ?P and ?Q by simp_all |
183 from dual.Inf_top_conv show ?P and ?Q by simp_all |
178 qed |
184 qed |
179 |
185 |
180 lemma Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B" |
|
181 by (auto intro: Inf_greatest Inf_lower) |
|
182 |
|
183 lemma Sup_anti_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B" |
|
184 by (auto intro: Sup_least Sup_upper) |
|
185 |
|
186 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
186 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
187 INF_def: "INFI A f = \<Sqinter> (f ` A)" |
187 INF_def: "INFI A f = \<Sqinter> (f ` A)" |
188 |
188 |
189 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
189 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
190 SUP_def: "SUPR A f = \<Squnion> (f ` A)" |
190 SUP_def: "SUPR A f = \<Squnion> (f ` A)" |
283 |
283 |
284 lemma SUP_mono: |
284 lemma SUP_mono: |
285 "(\<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)" |
285 "(\<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)" |
286 by (force intro!: Sup_mono simp: SUP_def) |
286 by (force intro!: Sup_mono simp: SUP_def) |
287 |
287 |
288 lemma INF_subset: |
288 lemma INF_superset_mono: |
289 "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f" |
289 "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f" |
290 by (intro INF_mono) auto |
290 by (rule INF_mono) auto |
291 |
291 |
292 lemma SUP_subset: |
292 lemma SUPO_subset_mono: |
293 "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f" |
293 "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f" |
294 by (intro SUP_mono) auto |
294 by (rule SUP_mono) auto |
295 |
295 |
296 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)" |
296 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)" |
297 by (iprover intro: INF_leI le_INF_I order_trans antisym) |
297 by (iprover intro: INF_leI le_INF_I order_trans antisym) |
298 |
298 |
299 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)" |
299 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)" |
363 |
363 |
364 lemma SUP_UNIV_bool_expand: |
364 lemma SUP_UNIV_bool_expand: |
365 "(\<Squnion>b. A b) = A True \<squnion> A False" |
365 "(\<Squnion>b. A b) = A True \<squnion> A False" |
366 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute) |
366 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute) |
367 |
367 |
368 lemma INF_anti_mono: |
368 lemma INF_mono': |
369 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)" |
369 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)" |
370 -- {* The last inclusion is POSITIVE! *} |
370 -- {* The last inclusion is POSITIVE! *} |
371 by (blast intro: INF_mono dest: subsetD) |
371 by (rule INF_mono) auto |
372 |
372 |
373 lemma SUP_anti_mono: |
373 lemma SUP_mono': |
374 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<sqsubseteq> f x) \<Longrightarrow> (\<Squnion>x\<in>B. g x) \<sqsubseteq> (\<Squnion>x\<in>B. f x)" |
374 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>B. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)" |
375 -- {* The last inclusion is POSITIVE! *} |
375 -- {* The last inclusion is POSITIVE! *} |
376 by (blast intro: SUP_mono dest: subsetD) |
376 by (blast intro: SUP_mono dest: subsetD) |
377 |
377 |
378 end |
378 end |
379 |
379 |
552 |
552 |
553 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B" |
553 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B" |
554 by (fact Inf_insert) |
554 by (fact Inf_insert) |
555 |
555 |
556 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)" |
556 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)" |
557 by (fact Inf_inter_less_eq) |
557 by (fact less_eq_Inf_inter) |
558 |
558 |
559 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B" |
559 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B" |
560 by (fact Inf_union_distrib) |
560 by (fact Inf_union_distrib) |
561 |
561 |
562 lemma Inter_UNIV_conv [simp, no_atp]: |
562 lemma Inter_UNIV_conv [simp, no_atp]: |
563 "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)" |
563 "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)" |
564 "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)" |
564 "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)" |
565 by (fact Inf_top_conv)+ |
565 by (fact Inf_top_conv)+ |
566 |
566 |
567 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B" |
567 lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B" |
568 by (fact Inf_anti_mono) |
568 by (fact Inf_superset_mono) |
569 |
569 |
570 |
570 |
571 subsection {* Intersections of families *} |
571 subsection {* Intersections of families *} |
572 |
572 |
573 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
573 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
680 by (fact INF_UNIV_bool_expand) |
680 by (fact INF_UNIV_bool_expand) |
681 |
681 |
682 lemma INT_anti_mono: |
682 lemma INT_anti_mono: |
683 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)" |
683 "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)" |
684 -- {* The last inclusion is POSITIVE! *} |
684 -- {* The last inclusion is POSITIVE! *} |
685 by (fact INF_anti_mono) |
685 by (fact INF_mono') |
686 |
686 |
687 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" |
687 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" |
688 by blast |
688 by blast |
689 |
689 |
690 lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)" |
690 lemma vimage_INT: "f -` (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. f -` B x)" |
1075 lemmas (in complete_lattice) INFI_def = INF_def |
1075 lemmas (in complete_lattice) INFI_def = INF_def |
1076 lemmas (in complete_lattice) SUPR_def = SUP_def |
1076 lemmas (in complete_lattice) SUPR_def = SUP_def |
1077 lemmas (in complete_lattice) le_SUPI = le_SUP_I |
1077 lemmas (in complete_lattice) le_SUPI = le_SUP_I |
1078 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2 |
1078 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2 |
1079 lemmas (in complete_lattice) le_INFI = le_INF_I |
1079 lemmas (in complete_lattice) le_INFI = le_INF_I |
|
1080 lemmas (in complete_lattice) INF_subset = INF_superset_mono |
1080 lemmas INFI_apply = INF_apply |
1081 lemmas INFI_apply = INF_apply |
1081 lemmas SUPR_apply = SUP_apply |
1082 lemmas SUPR_apply = SUP_apply |
1082 |
1083 |
1083 text {* Finally *} |
1084 text {* Finally *} |
1084 |
1085 |