author | bulwahn |
Tue, 31 May 2011 18:13:00 +0200 | |
changeset 43115 | 6773d8a9e351 |
parent 42156 | df219e736a5d |
child 48475 | 02dd825f5a4e |
permissions | -rw-r--r-- |
17456 | 1 |
header {* Extending FOL by a modified version of HOL set theory *} |
2 |
||
3 |
theory Set |
|
4 |
imports FOL |
|
5 |
begin |
|
0 | 6 |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38499
diff
changeset
|
7 |
declare [[eta_contract]] |
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38499
diff
changeset
|
8 |
|
17456 | 9 |
typedecl 'a set |
10 |
arities set :: ("term") "term" |
|
0 | 11 |
|
12 |
consts |
|
13 |
Collect :: "['a => o] => 'a set" (*comprehension*) |
|
14 |
Compl :: "('a set) => 'a set" (*complement*) |
|
24825 | 15 |
Int :: "['a set, 'a set] => 'a set" (infixl "Int" 70) |
16 |
Un :: "['a set, 'a set] => 'a set" (infixl "Un" 65) |
|
17456 | 17 |
Union :: "(('a set)set) => 'a set" (*...of a set*) |
18 |
Inter :: "(('a set)set) => 'a set" (*...of a set*) |
|
19 |
UNION :: "['a set, 'a => 'b set] => 'b set" (*general*) |
|
20 |
INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) |
|
21 |
Ball :: "['a set, 'a => o] => o" (*bounded quants*) |
|
22 |
Bex :: "['a set, 'a => o] => o" (*bounded quants*) |
|
0 | 23 |
mono :: "['a set => 'b set] => o" (*monotonicity*) |
24825 | 24 |
mem :: "['a, 'a set] => o" (infixl ":" 50) (*membership*) |
25 |
subset :: "['a set, 'a set] => o" (infixl "<=" 50) |
|
0 | 26 |
singleton :: "'a => 'a set" ("{_}") |
27 |
empty :: "'a set" ("{}") |
|
28 |
||
3935 | 29 |
syntax |
35113 | 30 |
"_Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) |
0 | 31 |
|
32 |
(* Big Intersection / Union *) |
|
33 |
||
35113 | 34 |
"_INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) |
35 |
"_UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) |
|
0 | 36 |
|
37 |
(* Bounded Quantifiers *) |
|
38 |
||
35113 | 39 |
"_Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10) |
40 |
"_Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10) |
|
0 | 41 |
|
42 |
translations |
|
35054 | 43 |
"{x. P}" == "CONST Collect(%x. P)" |
44 |
"INT x:A. B" == "CONST INTER(A, %x. B)" |
|
45 |
"UN x:A. B" == "CONST UNION(A, %x. B)" |
|
46 |
"ALL x:A. P" == "CONST Ball(A, %x. P)" |
|
47 |
"EX x:A. P" == "CONST Bex(A, %x. P)" |
|
0 | 48 |
|
42156 | 49 |
axiomatization where |
50 |
mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" and |
|
51 |
set_extension: "A = B <-> (ALL x. x:A <-> x:B)" |
|
0 | 52 |
|
17456 | 53 |
defs |
54 |
Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)" |
|
55 |
Bex_def: "Bex(A, P) == EX x. x:A & P(x)" |
|
56 |
mono_def: "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))" |
|
57 |
subset_def: "A <= B == ALL x:A. x:B" |
|
58 |
singleton_def: "{a} == {x. x=a}" |
|
59 |
empty_def: "{} == {x. False}" |
|
60 |
Un_def: "A Un B == {x. x:A | x:B}" |
|
61 |
Int_def: "A Int B == {x. x:A & x:B}" |
|
62 |
Compl_def: "Compl(A) == {x. ~x:A}" |
|
63 |
INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}" |
|
64 |
UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}" |
|
65 |
Inter_def: "Inter(S) == (INT x:S. x)" |
|
66 |
Union_def: "Union(S) == (UN x:S. x)" |
|
67 |
||
20140 | 68 |
|
69 |
lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}" |
|
70 |
apply (rule mem_Collect_iff [THEN iffD2]) |
|
71 |
apply assumption |
|
72 |
done |
|
73 |
||
74 |
lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)" |
|
75 |
apply (erule mem_Collect_iff [THEN iffD1]) |
|
76 |
done |
|
77 |
||
78 |
lemmas CollectE = CollectD [elim_format] |
|
79 |
||
80 |
lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B" |
|
81 |
apply (rule set_extension [THEN iffD2]) |
|
82 |
apply simp |
|
83 |
done |
|
84 |
||
85 |
||
86 |
subsection {* Bounded quantifiers *} |
|
87 |
||
88 |
lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)" |
|
89 |
by (simp add: Ball_def) |
|
90 |
||
91 |
lemma bspec: "[| ALL x:A. P(x); x:A |] ==> P(x)" |
|
92 |
by (simp add: Ball_def) |
|
93 |
||
94 |
lemma ballE: "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q" |
|
95 |
unfolding Ball_def by blast |
|
96 |
||
97 |
lemma bexI: "[| P(x); x:A |] ==> EX x:A. P(x)" |
|
98 |
unfolding Bex_def by blast |
|
99 |
||
100 |
lemma bexCI: "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" |
|
101 |
unfolding Bex_def by blast |
|
102 |
||
103 |
lemma bexE: "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q" |
|
104 |
unfolding Bex_def by blast |
|
105 |
||
106 |
(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
|
107 |
lemma ball_rew: "(ALL x:A. True) <-> True" |
|
108 |
by (blast intro: ballI) |
|
109 |
||
110 |
||
111 |
subsection {* Congruence rules *} |
|
112 |
||
113 |
lemma ball_cong: |
|
114 |
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
115 |
(ALL x:A. P(x)) <-> (ALL x:A'. P'(x))" |
|
116 |
by (blast intro: ballI elim: ballE) |
|
117 |
||
118 |
lemma bex_cong: |
|
119 |
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> |
|
120 |
(EX x:A. P(x)) <-> (EX x:A'. P'(x))" |
|
121 |
by (blast intro: bexI elim: bexE) |
|
122 |
||
123 |
||
124 |
subsection {* Rules for subsets *} |
|
125 |
||
126 |
lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B" |
|
127 |
unfolding subset_def by (blast intro: ballI) |
|
128 |
||
129 |
(*Rule in Modus Ponens style*) |
|
130 |
lemma subsetD: "[| A <= B; c:A |] ==> c:B" |
|
131 |
unfolding subset_def by (blast elim: ballE) |
|
132 |
||
133 |
(*Classical elimination rule*) |
|
134 |
lemma subsetCE: "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P" |
|
135 |
by (blast dest: subsetD) |
|
136 |
||
137 |
lemma subset_refl: "A <= A" |
|
138 |
by (blast intro: subsetI) |
|
139 |
||
140 |
lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C" |
|
141 |
by (blast intro: subsetI dest: subsetD) |
|
142 |
||
143 |
||
144 |
subsection {* Rules for equality *} |
|
145 |
||
146 |
(*Anti-symmetry of the subset relation*) |
|
147 |
lemma subset_antisym: "[| A <= B; B <= A |] ==> A = B" |
|
148 |
by (blast intro: set_ext dest: subsetD) |
|
149 |
||
150 |
lemmas equalityI = subset_antisym |
|
151 |
||
152 |
(* Equality rules from ZF set theory -- are they appropriate here? *) |
|
153 |
lemma equalityD1: "A = B ==> A<=B" |
|
154 |
and equalityD2: "A = B ==> B<=A" |
|
155 |
by (simp_all add: subset_refl) |
|
156 |
||
157 |
lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" |
|
158 |
by (simp add: subset_refl) |
|
159 |
||
160 |
lemma equalityCE: |
|
161 |
"[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P" |
|
162 |
by (blast elim: equalityE subsetCE) |
|
163 |
||
164 |
lemma trivial_set: "{x. x:A} = A" |
|
165 |
by (blast intro: equalityI subsetI CollectI dest: CollectD) |
|
166 |
||
167 |
||
168 |
subsection {* Rules for binary union *} |
|
169 |
||
170 |
lemma UnI1: "c:A ==> c : A Un B" |
|
171 |
and UnI2: "c:B ==> c : A Un B" |
|
172 |
unfolding Un_def by (blast intro: CollectI)+ |
|
173 |
||
174 |
(*Classical introduction rule: no commitment to A vs B*) |
|
175 |
lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B" |
|
176 |
by (blast intro: UnI1 UnI2) |
|
177 |
||
178 |
lemma UnE: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" |
|
179 |
unfolding Un_def by (blast dest: CollectD) |
|
180 |
||
181 |
||
182 |
subsection {* Rules for small intersection *} |
|
183 |
||
184 |
lemma IntI: "[| c:A; c:B |] ==> c : A Int B" |
|
185 |
unfolding Int_def by (blast intro: CollectI) |
|
186 |
||
187 |
lemma IntD1: "c : A Int B ==> c:A" |
|
188 |
and IntD2: "c : A Int B ==> c:B" |
|
189 |
unfolding Int_def by (blast dest: CollectD)+ |
|
190 |
||
191 |
lemma IntE: "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" |
|
192 |
by (blast dest: IntD1 IntD2) |
|
193 |
||
194 |
||
195 |
subsection {* Rules for set complement *} |
|
196 |
||
197 |
lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)" |
|
198 |
unfolding Compl_def by (blast intro: CollectI) |
|
199 |
||
200 |
(*This form, with negated conclusion, works well with the Classical prover. |
|
201 |
Negated assumptions behave like formulae on the right side of the notional |
|
202 |
turnstile...*) |
|
203 |
lemma ComplD: "[| c : Compl(A) |] ==> ~c:A" |
|
204 |
unfolding Compl_def by (blast dest: CollectD) |
|
205 |
||
206 |
lemmas ComplE = ComplD [elim_format] |
|
207 |
||
208 |
||
209 |
subsection {* Empty sets *} |
|
210 |
||
211 |
lemma empty_eq: "{x. False} = {}" |
|
212 |
by (simp add: empty_def) |
|
213 |
||
214 |
lemma emptyD: "a : {} ==> P" |
|
215 |
unfolding empty_def by (blast dest: CollectD) |
|
216 |
||
217 |
lemmas emptyE = emptyD [elim_format] |
|
218 |
||
219 |
lemma not_emptyD: |
|
220 |
assumes "~ A={}" |
|
221 |
shows "EX x. x:A" |
|
222 |
proof - |
|
223 |
have "\<not> (EX x. x:A) \<Longrightarrow> A = {}" |
|
224 |
by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+ |
|
41526 | 225 |
with assms show ?thesis by blast |
20140 | 226 |
qed |
227 |
||
228 |
||
229 |
subsection {* Singleton sets *} |
|
230 |
||
231 |
lemma singletonI: "a : {a}" |
|
232 |
unfolding singleton_def by (blast intro: CollectI) |
|
233 |
||
234 |
lemma singletonD: "b : {a} ==> b=a" |
|
235 |
unfolding singleton_def by (blast dest: CollectD) |
|
236 |
||
237 |
lemmas singletonE = singletonD [elim_format] |
|
238 |
||
239 |
||
240 |
subsection {* Unions of families *} |
|
241 |
||
242 |
(*The order of the premises presupposes that A is rigid; b may be flexible*) |
|
243 |
lemma UN_I: "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))" |
|
244 |
unfolding UNION_def by (blast intro: bexI CollectI) |
|
245 |
||
246 |
lemma UN_E: "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R" |
|
247 |
unfolding UNION_def by (blast dest: CollectD elim: bexE) |
|
248 |
||
249 |
lemma UN_cong: |
|
250 |
"[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> |
|
251 |
(UN x:A. C(x)) = (UN x:B. D(x))" |
|
252 |
by (simp add: UNION_def cong: bex_cong) |
|
253 |
||
254 |
||
255 |
subsection {* Intersections of families *} |
|
256 |
||
257 |
lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))" |
|
258 |
unfolding INTER_def by (blast intro: CollectI ballI) |
|
259 |
||
260 |
lemma INT_D: "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)" |
|
261 |
unfolding INTER_def by (blast dest: CollectD bspec) |
|
262 |
||
263 |
(*"Classical" elimination rule -- does not require proving X:C *) |
|
264 |
lemma INT_E: "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R" |
|
265 |
unfolding INTER_def by (blast dest: CollectD bspec) |
|
266 |
||
267 |
lemma INT_cong: |
|
268 |
"[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> |
|
269 |
(INT x:A. C(x)) = (INT x:B. D(x))" |
|
270 |
by (simp add: INTER_def cong: ball_cong) |
|
271 |
||
272 |
||
273 |
subsection {* Rules for Unions *} |
|
274 |
||
275 |
(*The order of the premises presupposes that C is rigid; A may be flexible*) |
|
276 |
lemma UnionI: "[| X:C; A:X |] ==> A : Union(C)" |
|
277 |
unfolding Union_def by (blast intro: UN_I) |
|
278 |
||
279 |
lemma UnionE: "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R" |
|
280 |
unfolding Union_def by (blast elim: UN_E) |
|
281 |
||
282 |
||
283 |
subsection {* Rules for Inter *} |
|
284 |
||
285 |
lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)" |
|
286 |
unfolding Inter_def by (blast intro: INT_I) |
|
287 |
||
288 |
(*A "destruct" rule -- every X in C contains A as an element, but |
|
289 |
A:X can hold when X:C does not! This rule is analogous to "spec". *) |
|
290 |
lemma InterD: "[| A : Inter(C); X:C |] ==> A:X" |
|
291 |
unfolding Inter_def by (blast dest: INT_D) |
|
292 |
||
293 |
(*"Classical" elimination rule -- does not require proving X:C *) |
|
294 |
lemma InterE: "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R" |
|
295 |
unfolding Inter_def by (blast elim: INT_E) |
|
296 |
||
297 |
||
298 |
section {* Derived rules involving subsets; Union and Intersection as lattice operations *} |
|
299 |
||
300 |
subsection {* Big Union -- least upper bound of a set *} |
|
301 |
||
302 |
lemma Union_upper: "B:A ==> B <= Union(A)" |
|
303 |
by (blast intro: subsetI UnionI) |
|
304 |
||
305 |
lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C" |
|
306 |
by (blast intro: subsetI dest: subsetD elim: UnionE) |
|
307 |
||
308 |
||
309 |
subsection {* Big Intersection -- greatest lower bound of a set *} |
|
310 |
||
311 |
lemma Inter_lower: "B:A ==> Inter(A) <= B" |
|
312 |
by (blast intro: subsetI dest: InterD) |
|
313 |
||
314 |
lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)" |
|
315 |
by (blast intro: subsetI InterI dest: subsetD) |
|
316 |
||
317 |
||
318 |
subsection {* Finite Union -- the least upper bound of 2 sets *} |
|
319 |
||
320 |
lemma Un_upper1: "A <= A Un B" |
|
321 |
by (blast intro: subsetI UnI1) |
|
322 |
||
323 |
lemma Un_upper2: "B <= A Un B" |
|
324 |
by (blast intro: subsetI UnI2) |
|
325 |
||
326 |
lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C" |
|
327 |
by (blast intro: subsetI elim: UnE dest: subsetD) |
|
328 |
||
329 |
||
330 |
subsection {* Finite Intersection -- the greatest lower bound of 2 sets *} |
|
331 |
||
332 |
lemma Int_lower1: "A Int B <= A" |
|
333 |
by (blast intro: subsetI elim: IntE) |
|
334 |
||
335 |
lemma Int_lower2: "A Int B <= B" |
|
336 |
by (blast intro: subsetI elim: IntE) |
|
337 |
||
338 |
lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B" |
|
339 |
by (blast intro: subsetI IntI dest: subsetD) |
|
340 |
||
341 |
||
342 |
subsection {* Monotonicity *} |
|
343 |
||
344 |
lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)" |
|
345 |
unfolding mono_def by blast |
|
346 |
||
347 |
lemma monoD: "[| mono(f); A <= B |] ==> f(A) <= f(B)" |
|
348 |
unfolding mono_def by blast |
|
349 |
||
350 |
lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)" |
|
351 |
by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2) |
|
352 |
||
353 |
lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)" |
|
354 |
by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2) |
|
355 |
||
356 |
||
357 |
subsection {* Automated reasoning setup *} |
|
358 |
||
359 |
lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI |
|
360 |
and [intro] = bexI UnionI UN_I |
|
361 |
and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE |
|
362 |
and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE |
|
363 |
||
364 |
lemma mem_rews: |
|
365 |
"(a : A Un B) <-> (a:A | a:B)" |
|
366 |
"(a : A Int B) <-> (a:A & a:B)" |
|
367 |
"(a : Compl(B)) <-> (~a:B)" |
|
368 |
"(a : {b}) <-> (a=b)" |
|
369 |
"(a : {}) <-> False" |
|
370 |
"(a : {x. P(x)}) <-> P(a)" |
|
371 |
by blast+ |
|
372 |
||
373 |
lemmas [simp] = trivial_set empty_eq mem_rews |
|
374 |
and [cong] = ball_cong bex_cong INT_cong UN_cong |
|
375 |
||
376 |
||
377 |
section {* Equalities involving union, intersection, inclusion, etc. *} |
|
378 |
||
379 |
subsection {* Binary Intersection *} |
|
380 |
||
381 |
lemma Int_absorb: "A Int A = A" |
|
382 |
by (blast intro: equalityI) |
|
383 |
||
384 |
lemma Int_commute: "A Int B = B Int A" |
|
385 |
by (blast intro: equalityI) |
|
386 |
||
387 |
lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)" |
|
388 |
by (blast intro: equalityI) |
|
389 |
||
390 |
lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)" |
|
391 |
by (blast intro: equalityI) |
|
392 |
||
393 |
lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)" |
|
394 |
by (blast intro: equalityI elim: equalityE) |
|
395 |
||
396 |
||
397 |
subsection {* Binary Union *} |
|
398 |
||
399 |
lemma Un_absorb: "A Un A = A" |
|
400 |
by (blast intro: equalityI) |
|
401 |
||
402 |
lemma Un_commute: "A Un B = B Un A" |
|
403 |
by (blast intro: equalityI) |
|
404 |
||
405 |
lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)" |
|
406 |
by (blast intro: equalityI) |
|
407 |
||
408 |
lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" |
|
409 |
by (blast intro: equalityI) |
|
410 |
||
411 |
lemma Un_Int_crazy: |
|
412 |
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" |
|
413 |
by (blast intro: equalityI) |
|
414 |
||
415 |
lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)" |
|
416 |
by (blast intro: equalityI elim: equalityE) |
|
417 |
||
418 |
||
419 |
subsection {* Simple properties of @{text "Compl"} -- complement of a set *} |
|
420 |
||
421 |
lemma Compl_disjoint: "A Int Compl(A) = {x. False}" |
|
422 |
by (blast intro: equalityI) |
|
423 |
||
424 |
lemma Compl_partition: "A Un Compl(A) = {x. True}" |
|
425 |
by (blast intro: equalityI) |
|
426 |
||
427 |
lemma double_complement: "Compl(Compl(A)) = A" |
|
428 |
by (blast intro: equalityI) |
|
429 |
||
430 |
lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)" |
|
431 |
by (blast intro: equalityI) |
|
432 |
||
433 |
lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)" |
|
434 |
by (blast intro: equalityI) |
|
435 |
||
436 |
lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))" |
|
437 |
by (blast intro: equalityI) |
|
438 |
||
439 |
lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))" |
|
440 |
by (blast intro: equalityI) |
|
441 |
||
442 |
(*Halmos, Naive Set Theory, page 16.*) |
|
443 |
lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)" |
|
444 |
by (blast intro: equalityI elim: equalityE) |
|
445 |
||
446 |
||
447 |
subsection {* Big Union and Intersection *} |
|
448 |
||
449 |
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" |
|
450 |
by (blast intro: equalityI) |
|
451 |
||
452 |
lemma Union_disjoint: |
|
453 |
"(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})" |
|
454 |
by (blast intro: equalityI elim: equalityE) |
|
455 |
||
456 |
lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)" |
|
457 |
by (blast intro: equalityI) |
|
458 |
||
459 |
||
460 |
subsection {* Unions and Intersections of Families *} |
|
461 |
||
462 |
lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})" |
|
463 |
by (blast intro: equalityI) |
|
464 |
||
465 |
(*Look: it has an EXISTENTIAL quantifier*) |
|
466 |
lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})" |
|
467 |
by (blast intro: equalityI) |
|
468 |
||
469 |
lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)" |
|
470 |
by (blast intro: equalityI) |
|
471 |
||
472 |
lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)" |
|
473 |
by (blast intro: equalityI) |
|
474 |
||
475 |
||
476 |
section {* Monotonicity of various operations *} |
|
477 |
||
478 |
lemma Union_mono: "A<=B ==> Union(A) <= Union(B)" |
|
479 |
by blast |
|
480 |
||
481 |
lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)" |
|
482 |
by blast |
|
483 |
||
484 |
lemma UN_mono: |
|
485 |
"[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> |
|
486 |
(UN x:A. f(x)) <= (UN x:B. g(x))" |
|
487 |
by blast |
|
488 |
||
489 |
lemma INT_anti_mono: |
|
490 |
"[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> |
|
491 |
(INT x:A. f(x)) <= (INT x:A. g(x))" |
|
492 |
by blast |
|
493 |
||
494 |
lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D" |
|
495 |
by blast |
|
496 |
||
497 |
lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D" |
|
498 |
by blast |
|
499 |
||
500 |
lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)" |
|
501 |
by blast |
|
0 | 502 |
|
503 |
end |