80 |
80 |
81 lemma Sup_binary: |
81 lemma Sup_binary: |
82 "\<Squnion>{a, b} = a \<squnion> b" |
82 "\<Squnion>{a, b} = a \<squnion> b" |
83 by (simp add: Sup_empty Sup_insert) |
83 by (simp add: Sup_empty Sup_insert) |
84 |
84 |
|
85 lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)" |
|
86 by (auto intro: Inf_greatest dest: Inf_lower) |
|
87 |
85 lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)" |
88 lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)" |
86 by (auto intro: Sup_least dest: Sup_upper) |
89 by (auto intro: Sup_least dest: Sup_upper) |
87 |
90 |
88 lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)" |
91 lemma Inf_mono: |
89 by (auto intro: Inf_greatest dest: Inf_lower) |
92 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b" |
|
93 shows "Inf A \<le> Inf B" |
|
94 proof (rule Inf_greatest) |
|
95 fix b assume "b \<in> B" |
|
96 with assms obtain a where "a \<in> A" and "a \<le> b" by blast |
|
97 from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower) |
|
98 with `a \<le> b` show "Inf A \<le> b" by auto |
|
99 qed |
90 |
100 |
91 lemma Sup_mono: |
101 lemma Sup_mono: |
92 assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b" |
102 assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b" |
93 shows "Sup A \<le> Sup B" |
103 shows "Sup A \<le> Sup B" |
94 proof (rule Sup_least) |
104 proof (rule Sup_least) |
96 with assms obtain b where "b \<in> B" and "a \<le> b" by blast |
106 with assms obtain b where "b \<in> B" and "a \<le> b" by blast |
97 from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper) |
107 from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper) |
98 with `a \<le> b` show "a \<le> Sup B" by auto |
108 with `a \<le> b` show "a \<le> Sup B" by auto |
99 qed |
109 qed |
100 |
110 |
101 lemma Inf_mono: |
111 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
102 assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b" |
112 "INFI A f = \<Sqinter> (f ` A)" |
103 shows "Inf A \<le> Inf B" |
|
104 proof (rule Inf_greatest) |
|
105 fix b assume "b \<in> B" |
|
106 with assms obtain a where "a \<in> A" and "a \<le> b" by blast |
|
107 from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower) |
|
108 with `a \<le> b` show "Inf A \<le> b" by auto |
|
109 qed |
|
110 |
113 |
111 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
114 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
112 "SUPR A f = \<Squnion> (f ` A)" |
115 "SUPR A f = \<Squnion> (f ` A)" |
113 |
116 |
114 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
115 "INFI A f = \<Sqinter> (f ` A)" |
|
116 |
|
117 end |
117 end |
118 |
118 |
119 syntax |
119 syntax |
|
120 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10) |
|
121 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10) |
120 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10) |
122 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10) |
121 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10) |
123 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10) |
122 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10) |
|
123 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10) |
|
124 |
124 |
125 syntax (xsymbols) |
125 syntax (xsymbols) |
|
126 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
127 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
126 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
128 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
127 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
129 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
128 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
129 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
|
130 |
130 |
131 translations |
131 translations |
|
132 "INF x y. B" == "INF x. INF y. B" |
|
133 "INF x. B" == "CONST INFI CONST UNIV (%x. B)" |
|
134 "INF x. B" == "INF x:CONST UNIV. B" |
|
135 "INF x:A. B" == "CONST INFI A (%x. B)" |
132 "SUP x y. B" == "SUP x. SUP y. B" |
136 "SUP x y. B" == "SUP x. SUP y. B" |
133 "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)" |
137 "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)" |
134 "SUP x. B" == "SUP x:CONST UNIV. B" |
138 "SUP x. B" == "SUP x:CONST UNIV. B" |
135 "SUP x:A. B" == "CONST SUPR A (%x. B)" |
139 "SUP x:A. B" == "CONST SUPR A (%x. B)" |
136 "INF x y. B" == "INF x. INF y. B" |
|
137 "INF x. B" == "CONST INFI CONST UNIV (%x. B)" |
|
138 "INF x. B" == "INF x:CONST UNIV. B" |
|
139 "INF x:A. B" == "CONST INFI A (%x. B)" |
|
140 |
140 |
141 print_translation {* |
141 print_translation {* |
142 [Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}, |
142 [Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, |
143 Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}] |
143 Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] |
144 *} -- {* to avoid eta-contraction of body *} |
144 *} -- {* to avoid eta-contraction of body *} |
145 |
145 |
146 context complete_lattice |
146 context complete_lattice |
147 begin |
147 begin |
148 |
148 |
162 unfolding SUPR_def by (auto simp add: Sup_le_iff) |
162 unfolding SUPR_def by (auto simp add: Sup_le_iff) |
163 |
163 |
164 lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)" |
164 lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)" |
165 unfolding INFI_def by (auto simp add: le_Inf_iff) |
165 unfolding INFI_def by (auto simp add: le_Inf_iff) |
166 |
166 |
|
167 lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M" |
|
168 by (auto intro: antisym INF_leI le_INFI) |
|
169 |
167 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M" |
170 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M" |
168 by (auto intro: antisym SUP_leI le_SUPI) |
171 by (auto intro: antisym SUP_leI le_SUPI) |
169 |
172 |
170 lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M" |
173 lemma INF_mono: |
171 by (auto intro: antisym INF_leI le_INFI) |
174 "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)" |
|
175 by (force intro!: Inf_mono simp: INFI_def) |
172 |
176 |
173 lemma SUP_mono: |
177 lemma SUP_mono: |
174 "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)" |
178 "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)" |
175 by (force intro!: Sup_mono simp: SUPR_def) |
179 by (force intro!: Sup_mono simp: SUPR_def) |
176 |
180 |
177 lemma INF_mono: |
181 lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f" |
178 "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)" |
182 by (intro INF_mono) auto |
179 by (force intro!: Inf_mono simp: INFI_def) |
|
180 |
183 |
181 lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f" |
184 lemma SUP_subset: "A \<subseteq> B \<Longrightarrow> SUPR A f \<le> SUPR B f" |
182 by (intro SUP_mono) auto |
185 by (intro SUP_mono) auto |
183 |
186 |
184 lemma INF_subset: "A \<subseteq> B \<Longrightarrow> INFI B f \<le> INFI A f" |
187 lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)" |
185 by (intro INF_mono) auto |
188 by (iprover intro: INF_leI le_INFI order_trans antisym) |
186 |
189 |
187 lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" |
190 lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" |
188 by (iprover intro: SUP_leI le_SUPI order_trans antisym) |
191 by (iprover intro: SUP_leI le_SUPI order_trans antisym) |
189 |
192 |
190 lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)" |
|
191 by (iprover intro: INF_leI le_INFI order_trans antisym) |
|
192 |
|
193 end |
193 end |
|
194 |
|
195 lemma Inf_less_iff: |
|
196 fixes a :: "'a\<Colon>{complete_lattice,linorder}" |
|
197 shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)" |
|
198 unfolding not_le[symmetric] le_Inf_iff by auto |
194 |
199 |
195 lemma less_Sup_iff: |
200 lemma less_Sup_iff: |
196 fixes a :: "'a\<Colon>{complete_lattice,linorder}" |
201 fixes a :: "'a\<Colon>{complete_lattice,linorder}" |
197 shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)" |
202 shows "a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)" |
198 unfolding not_le[symmetric] Sup_le_iff by auto |
203 unfolding not_le[symmetric] Sup_le_iff by auto |
199 |
204 |
200 lemma Inf_less_iff: |
205 lemma INF_less_iff: |
201 fixes a :: "'a\<Colon>{complete_lattice,linorder}" |
206 fixes a :: "'a::{complete_lattice,linorder}" |
202 shows "Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)" |
207 shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" |
203 unfolding not_le[symmetric] le_Inf_iff by auto |
208 unfolding INFI_def Inf_less_iff by auto |
204 |
209 |
205 lemma less_SUP_iff: |
210 lemma less_SUP_iff: |
206 fixes a :: "'a::{complete_lattice,linorder}" |
211 fixes a :: "'a::{complete_lattice,linorder}" |
207 shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" |
212 shows "a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" |
208 unfolding SUPR_def less_Sup_iff by auto |
213 unfolding SUPR_def less_Sup_iff by auto |
209 |
|
210 lemma INF_less_iff: |
|
211 fixes a :: "'a::{complete_lattice,linorder}" |
|
212 shows "(INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" |
|
213 unfolding INFI_def Inf_less_iff by auto |
|
214 |
214 |
215 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *} |
215 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *} |
216 |
216 |
217 instantiation bool :: complete_lattice |
217 instantiation bool :: complete_lattice |
218 begin |
218 begin |
274 by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply) |
274 by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply) |
275 |
275 |
276 lemma SUPR_apply: |
276 lemma SUPR_apply: |
277 "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)" |
277 "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)" |
278 by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply) |
278 by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply) |
|
279 |
|
280 |
|
281 subsection {* Inter *} |
|
282 |
|
283 abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where |
|
284 "Inter S \<equiv> \<Sqinter>S" |
|
285 |
|
286 notation (xsymbols) |
|
287 Inter ("\<Inter>_" [90] 90) |
|
288 |
|
289 lemma Inter_eq: |
|
290 "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}" |
|
291 proof (rule set_eqI) |
|
292 fix x |
|
293 have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)" |
|
294 by auto |
|
295 then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}" |
|
296 by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def) |
|
297 qed |
|
298 |
|
299 lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)" |
|
300 by (unfold Inter_eq) blast |
|
301 |
|
302 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" |
|
303 by (simp add: Inter_eq) |
|
304 |
|
305 text {* |
|
306 \medskip A ``destruct'' rule -- every @{term X} in @{term C} |
|
307 contains @{term A} as an element, but @{prop "A:X"} can hold when |
|
308 @{prop "X:C"} does not! This rule is analogous to @{text spec}. |
|
309 *} |
|
310 |
|
311 lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X" |
|
312 by auto |
|
313 |
|
314 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" |
|
315 -- {* ``Classical'' elimination rule -- does not require proving |
|
316 @{prop "X:C"}. *} |
|
317 by (unfold Inter_eq) blast |
|
318 |
|
319 lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B" |
|
320 by blast |
|
321 |
|
322 lemma Inter_subset: |
|
323 "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B" |
|
324 by blast |
|
325 |
|
326 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A" |
|
327 by (iprover intro: InterI subsetI dest: subsetD) |
|
328 |
|
329 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}" |
|
330 by blast |
|
331 |
|
332 lemma Inter_empty [simp]: "\<Inter>{} = UNIV" |
|
333 by (fact Inf_empty) |
|
334 |
|
335 lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}" |
|
336 by blast |
|
337 |
|
338 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B" |
|
339 by blast |
|
340 |
|
341 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)" |
|
342 by blast |
|
343 |
|
344 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B" |
|
345 by blast |
|
346 |
|
347 lemma Inter_UNIV_conv [simp,no_atp]: |
|
348 "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)" |
|
349 "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)" |
|
350 by blast+ |
|
351 |
|
352 lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B" |
|
353 by blast |
|
354 |
|
355 |
|
356 subsection {* Intersections of families *} |
|
357 |
|
358 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
|
359 "INTER \<equiv> INFI" |
|
360 |
|
361 syntax |
|
362 "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10) |
|
363 "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10) |
|
364 |
|
365 syntax (xsymbols) |
|
366 "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10) |
|
367 "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10) |
|
368 |
|
369 syntax (latex output) |
|
370 "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) |
|
371 "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10) |
|
372 |
|
373 translations |
|
374 "INT x y. B" == "INT x. INT y. B" |
|
375 "INT x. B" == "CONST INTER CONST UNIV (%x. B)" |
|
376 "INT x. B" == "INT x:CONST UNIV. B" |
|
377 "INT x:A. B" == "CONST INTER A (%x. B)" |
|
378 |
|
379 print_translation {* |
|
380 [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}] |
|
381 *} -- {* to avoid eta-contraction of body *} |
|
382 |
|
383 lemma INTER_eq_Inter_image: |
|
384 "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)" |
|
385 by (fact INFI_def) |
|
386 |
|
387 lemma Inter_def: |
|
388 "\<Inter>S = (\<Inter>x\<in>S. x)" |
|
389 by (simp add: INTER_eq_Inter_image image_def) |
|
390 |
|
391 lemma INTER_def: |
|
392 "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}" |
|
393 by (auto simp add: INTER_eq_Inter_image Inter_eq) |
|
394 |
|
395 lemma Inter_image_eq [simp]: |
|
396 "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)" |
|
397 by (rule sym) (fact INTER_eq_Inter_image) |
|
398 |
|
399 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" |
|
400 by (unfold INTER_def) blast |
|
401 |
|
402 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" |
|
403 by (unfold INTER_def) blast |
|
404 |
|
405 lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" |
|
406 by auto |
|
407 |
|
408 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" |
|
409 -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *} |
|
410 by (unfold INTER_def) blast |
|
411 |
|
412 lemma INT_cong [cong]: |
|
413 "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" |
|
414 by (simp add: INTER_def) |
|
415 |
|
416 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})" |
|
417 by blast |
|
418 |
|
419 lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})" |
|
420 by blast |
|
421 |
|
422 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a" |
|
423 by (fact INF_leI) |
|
424 |
|
425 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)" |
|
426 by (fact le_INFI) |
|
427 |
|
428 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV" |
|
429 by blast |
|
430 |
|
431 lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)" |
|
432 by blast |
|
433 |
|
434 lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)" |
|
435 by (fact le_INF_iff) |
|
436 |
|
437 lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B" |
|
438 by blast |
|
439 |
|
440 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)" |
|
441 by blast |
|
442 |
|
443 lemma INT_insert_distrib: |
|
444 "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)" |
|
445 by blast |
|
446 |
|
447 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)" |
|
448 by auto |
|
449 |
|
450 lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})" |
|
451 -- {* Look: it has an \emph{existential} quantifier *} |
|
452 by blast |
|
453 |
|
454 lemma INTER_UNIV_conv[simp]: |
|
455 "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)" |
|
456 "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)" |
|
457 by blast+ |
|
458 |
|
459 lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)" |
|
460 by (auto intro: bool_induct) |
|
461 |
|
462 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" |
|
463 by blast |
|
464 |
|
465 lemma INT_anti_mono: |
|
466 "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==> |
|
467 (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)" |
|
468 -- {* The last inclusion is POSITIVE! *} |
|
469 by (blast dest: subsetD) |
|
470 |
|
471 lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)" |
|
472 by blast |
279 |
473 |
280 |
474 |
281 subsection {* Union *} |
475 subsection {* Union *} |
282 |
476 |
283 abbreviation Union :: "'a set set \<Rightarrow> 'a set" where |
477 abbreviation Union :: "'a set set \<Rightarrow> 'a set" where |
510 -- {* NOT suitable for rewriting *} |
704 -- {* NOT suitable for rewriting *} |
511 by blast |
705 by blast |
512 |
706 |
513 lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))" |
707 lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))" |
514 by blast |
708 by blast |
515 |
|
516 |
|
517 subsection {* Inter *} |
|
518 |
|
519 abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where |
|
520 "Inter S \<equiv> \<Sqinter>S" |
|
521 |
|
522 notation (xsymbols) |
|
523 Inter ("\<Inter>_" [90] 90) |
|
524 |
|
525 lemma Inter_eq: |
|
526 "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}" |
|
527 proof (rule set_eqI) |
|
528 fix x |
|
529 have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)" |
|
530 by auto |
|
531 then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}" |
|
532 by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def) |
|
533 qed |
|
534 |
|
535 lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)" |
|
536 by (unfold Inter_eq) blast |
|
537 |
|
538 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" |
|
539 by (simp add: Inter_eq) |
|
540 |
|
541 text {* |
|
542 \medskip A ``destruct'' rule -- every @{term X} in @{term C} |
|
543 contains @{term A} as an element, but @{prop "A:X"} can hold when |
|
544 @{prop "X:C"} does not! This rule is analogous to @{text spec}. |
|
545 *} |
|
546 |
|
547 lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X" |
|
548 by auto |
|
549 |
|
550 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" |
|
551 -- {* ``Classical'' elimination rule -- does not require proving |
|
552 @{prop "X:C"}. *} |
|
553 by (unfold Inter_eq) blast |
|
554 |
|
555 lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B" |
|
556 by blast |
|
557 |
|
558 lemma Inter_subset: |
|
559 "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B" |
|
560 by blast |
|
561 |
|
562 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A" |
|
563 by (iprover intro: InterI subsetI dest: subsetD) |
|
564 |
|
565 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}" |
|
566 by blast |
|
567 |
|
568 lemma Inter_empty [simp]: "\<Inter>{} = UNIV" |
|
569 by (fact Inf_empty) |
|
570 |
|
571 lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}" |
|
572 by blast |
|
573 |
|
574 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B" |
|
575 by blast |
|
576 |
|
577 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)" |
|
578 by blast |
|
579 |
|
580 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B" |
|
581 by blast |
|
582 |
|
583 lemma Inter_UNIV_conv [simp,no_atp]: |
|
584 "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)" |
|
585 "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)" |
|
586 by blast+ |
|
587 |
|
588 lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B" |
|
589 by blast |
|
590 |
|
591 |
|
592 subsection {* Intersections of families *} |
|
593 |
|
594 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where |
|
595 "INTER \<equiv> INFI" |
|
596 |
|
597 syntax |
|
598 "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10) |
|
599 "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10) |
|
600 |
|
601 syntax (xsymbols) |
|
602 "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10) |
|
603 "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10) |
|
604 |
|
605 syntax (latex output) |
|
606 "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) |
|
607 "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10) |
|
608 |
|
609 translations |
|
610 "INT x y. B" == "INT x. INT y. B" |
|
611 "INT x. B" == "CONST INTER CONST UNIV (%x. B)" |
|
612 "INT x. B" == "INT x:CONST UNIV. B" |
|
613 "INT x:A. B" == "CONST INTER A (%x. B)" |
|
614 |
|
615 print_translation {* |
|
616 [Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}] |
|
617 *} -- {* to avoid eta-contraction of body *} |
|
618 |
|
619 lemma INTER_eq_Inter_image: |
|
620 "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)" |
|
621 by (fact INFI_def) |
|
622 |
|
623 lemma Inter_def: |
|
624 "\<Inter>S = (\<Inter>x\<in>S. x)" |
|
625 by (simp add: INTER_eq_Inter_image image_def) |
|
626 |
|
627 lemma INTER_def: |
|
628 "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}" |
|
629 by (auto simp add: INTER_eq_Inter_image Inter_eq) |
|
630 |
|
631 lemma Inter_image_eq [simp]: |
|
632 "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)" |
|
633 by (rule sym) (fact INTER_eq_Inter_image) |
|
634 |
|
635 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" |
|
636 by (unfold INTER_def) blast |
|
637 |
|
638 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" |
|
639 by (unfold INTER_def) blast |
|
640 |
|
641 lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" |
|
642 by auto |
|
643 |
|
644 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" |
|
645 -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *} |
|
646 by (unfold INTER_def) blast |
|
647 |
|
648 lemma INT_cong [cong]: |
|
649 "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" |
|
650 by (simp add: INTER_def) |
|
651 |
|
652 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})" |
|
653 by blast |
|
654 |
|
655 lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})" |
|
656 by blast |
|
657 |
|
658 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a" |
|
659 by (fact INF_leI) |
|
660 |
|
661 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)" |
|
662 by (fact le_INFI) |
|
663 |
|
664 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV" |
|
665 by blast |
|
666 |
|
667 lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)" |
|
668 by blast |
|
669 |
|
670 lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)" |
|
671 by (fact le_INF_iff) |
|
672 |
|
673 lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B" |
|
674 by blast |
|
675 |
|
676 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)" |
|
677 by blast |
|
678 |
|
679 lemma INT_insert_distrib: |
|
680 "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)" |
|
681 by blast |
|
682 |
|
683 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)" |
|
684 by auto |
|
685 |
|
686 lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})" |
|
687 -- {* Look: it has an \emph{existential} quantifier *} |
|
688 by blast |
|
689 |
|
690 lemma INTER_UNIV_conv[simp]: |
|
691 "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)" |
|
692 "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)" |
|
693 by blast+ |
|
694 |
|
695 lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)" |
|
696 by (auto intro: bool_induct) |
|
697 |
|
698 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))" |
|
699 by blast |
|
700 |
|
701 lemma INT_anti_mono: |
|
702 "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==> |
|
703 (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)" |
|
704 -- {* The last inclusion is POSITIVE! *} |
|
705 by (blast dest: subsetD) |
|
706 |
|
707 lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)" |
|
708 by blast |
|
709 |
709 |
710 |
710 |
711 subsection {* Distributive laws *} |
711 subsection {* Distributive laws *} |
712 |
712 |
713 lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)" |
713 lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)" |
856 |
856 |
857 |
857 |
858 no_notation |
858 no_notation |
859 less_eq (infix "\<sqsubseteq>" 50) and |
859 less_eq (infix "\<sqsubseteq>" 50) and |
860 less (infix "\<sqsubset>" 50) and |
860 less (infix "\<sqsubset>" 50) and |
|
861 bot ("\<bottom>") and |
|
862 top ("\<top>") and |
861 inf (infixl "\<sqinter>" 70) and |
863 inf (infixl "\<sqinter>" 70) and |
862 sup (infixl "\<squnion>" 65) and |
864 sup (infixl "\<squnion>" 65) and |
863 Inf ("\<Sqinter>_" [900] 900) and |
865 Inf ("\<Sqinter>_" [900] 900) and |
864 Sup ("\<Squnion>_" [900] 900) and |
866 Sup ("\<Squnion>_" [900] 900) |
865 top ("\<top>") and |
|
866 bot ("\<bottom>") |
|
867 |
867 |
868 no_syntax (xsymbols) |
868 no_syntax (xsymbols) |
|
869 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
870 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
869 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
871 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
870 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
872 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
871 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
|
872 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
|
873 |
873 |
874 lemmas mem_simps = |
874 lemmas mem_simps = |
875 insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff |
875 insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff |
876 mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff |
876 mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff |
877 -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} |
877 -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} |