]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/SUBSETS/tbs_op.v
Added aliases and notation.
[helm.git] / helm / coq-contribs / SUBSETS / tbs_op.v
1 (** This module (Toolbox - subsets: operations) defines:
2     - subset binary intersection:     [SAnd] (subset and)
3     - subset binary union:            [SOr]  (subset or)
4     - subset implication:             [SImp] (subset implies) 
5     - subset opposite:                [SNot] (subset not) 
6     - subset infinitary intersection: [SAll] (subset all)
7     - subset infinitary union:        [SEx]  (subset exists)
8     
9     and provides:
10     - introduction and elimination rules for the defined constants
11     - standard properties (idempotency, commutativity, associativity, compatibility, distributivity) for the defined constants
12     - Cantor's diagonalization theorem: [cantor_diag]
13     
14 % \hrule %
15  
16  We require Toolbox relations and the underlying theory.
17   
18  *)
19 Require Export tbs_rel.
20
21 Section Subset_Operations_Definitions.
22
23    Section finitary_subset_operations.
24
25 (** Subset and: [(SAnd S U V)] corresponds to $ U \sand_S V $. *)
26       Definition SAnd: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
27       Intros S U V a.
28       Exact (LAnd (U a) (V a)).
29       Defined.
30
31 (** Subset or: [(SOr S U V)] corresponds to $ U \sor_S V $. *)
32       Definition SOr: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
33       Intros S U V a.
34       Exact (LOr (U a) (V a)).
35       Defined.
36    
37 (** Subset implies: [(SImp S U V)] corresponds to $ U \simp_S V $. *)
38       Definition SImp: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
39       Intros S U V a.
40       Exact (U a)->(V a).
41       Defined.
42
43 (** Subset not: [(SNot S U)] corresponds to $ \snot_S U $. *)
44       Definition SNot: (S:Set) (S -> Set) -> (S -> Set).
45       Intros S U a.
46       Exact (LNot (U a)).
47       Defined.
48
49    End finitary_subset_operations.
50    
51    Section infinitary_subset_operations.
52
53 (** Subset all: [(SAll I S F)] corresponds to $ \bigsand_S\subset{F(i) \st i \in I} $. *)
54       Definition SAll: (I,S:Set) (I -> S -> Set) -> (S -> Set).
55       Intros I S F a.
56       Exact (i:I)(F i a).
57       Defined.
58
59 (** Subset exists: [(SEx I S F)] corresponds to $ \bigsor_S\subset{F(i) \st i \in I} $. *)
60       Definition SEx: (I,S:Set) (I -> S -> Set) -> (S -> Set).
61       Intros I S F a.
62       Exact (LEx I [i](F i a)).
63       Defined.
64
65    End infinitary_subset_operations.
66
67 End Subset_Operations_Definitions.
68
69 Section Subset_Operations_Results.
70
71    Section subset_binary_intersection.
72
73 (** Subset and, epsilon introduction: $ a \e U \limp a \e V \limp a \e U \sand V $. *)
74       Theorem sand_eps_i: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a V) -> (Eps S a (SAnd S U V)).
75       Intros.
76       MApply 'eps_i.
77       Unfold SAnd.
78       MApply 'land_i.
79       MApply 'eps_e.
80       MApply 'eps_e.      
81       Qed.
82
83 (** Subset and, epsilon elimination 2: $ a \e U \sand V \limp a \e U $. *)
84       Theorem sand_eps_e2: (S:Set; V,U:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a U).
85       Intros.
86       MApply 'eps_i.
87       MApply '(land_e2 (V a)).
88       Fold (SAnd S U V a).
89       MApply 'eps_e.
90       Qed.
91
92 (** Subset and, epsilon elimination 1: $ a \e U \sand V \limp a \e V $. *)
93       Theorem sand_eps_e1: (S:Set; U,V:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a V).
94       Intros.
95       MApply 'eps_i.
96       MApply '(land_e1 (U a)).
97       Fold (SAnd S U V a).
98       MApply 'eps_e.
99       Qed.
100
101 (** Subset and, epsilon criterion: $ a \e U \land a \e V \liff a \e U \sand V $ *)
102       Theorem sand_eps: (S:Set; U,V:S->Set; a:S) (LIff (LAnd (Eps S a U) (Eps S a V)) (Eps S a (SAnd S U V))).
103       Intros.
104       MApply 'liff_i.
105       MApply 'sand_eps_i.
106       MApply '(land_e2 (Eps S a V)).
107       MApply '(land_e1 (Eps S a U)).
108       MApply 'land_i.
109       MApply '(sand_eps_e2 S V).
110       MApply '(sand_eps_e1 S U).
111       Qed.
112
113 (** Subset and, sub or equal elimination 2: $ U \sand V \sub U $. *)
114       Theorem sand_sbe_e2: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) U).
115       Intros.
116       MApply 'sbe_i.
117       MApply '(sand_eps_e2 S V).
118       Qed.
119
120 (** Subset and, sub or equal elimination 1: $ U \sand V \sub V $. *)
121       Theorem sand_sbe_e1: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) V).
122       Intros.
123       MApply 'sbe_i.
124       MApply '(sand_eps_e1 S U).
125       Qed.
126
127 (** Subset and, sub or equal introduction: $ W \sub U \limp W \sub V \limp W \sub U \sand V $. *)
128       Theorem sand_sbe_i: (S:Set; W,U,V:S->Set) (SbE S W U) -> (SbE S W V) -> (SbE S W (SAnd S U V)).
129       Intros.
130       MApply 'sbe_i.
131       MApply 'sand_eps_i.
132       MApply '(sbe_e S W).
133       MApply '(sbe_e S W).
134       Qed.
135
136 (** Subset and, sub or equal compatibility 2: $ U \sub V \limp U \sand W \sub V \sand W $. *)
137       Theorem sand_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S U W) (SAnd S V W)).
138       Intros.
139       MApply 'sand_sbe_i.
140       MApply '(sbe_t S U).
141       MApply 'sand_sbe_e2.
142       MApply 'sand_sbe_e1.
143       Qed.
144
145 (** Subset and, sub or equal subset top: $ U \sub \stop \sand U $. *)
146       Theorem sand_sbe_stop: (S:Set; U:S->Set) (SbE S U (SAnd S (STop S) U)).
147       Intros.
148       MApply 'sand_sbe_i.
149       MApply 'stop_sbe_i.
150       MApply 'sbe_r.
151       Qed.
152
153 (** Subset and, sub or equal idempotency: $ U \sub U \sand U $. *)
154       Theorem sand_sbe_r: (S:Set; U:S->Set) (SbE S U (SAnd S U U)).
155       Intros.
156       MApply 'sand_sbe_i.
157       MApply 'sbe_r.
158       MApply 'sbe_r.
159       Qed.
160
161 (** Subset and, idempotency $ U \sand U = U $. *)
162       Theorem sand_r: (S:Set; U:S->Set) (SEq S (SAnd S U U) U).
163       Intros.
164       MApply 'seq_sbe_i.
165       MApply 'sand_sbe_e2.
166       MApply 'sand_sbe_r.
167       Qed.
168
169 (** Subset and, sub or equal commutativity: $ V \sand U \sub U \sand V $. *)
170       Theorem sand_sbe_s: (S:Set; U,V:S->Set) (SbE S (SAnd S V U) (SAnd S U V)).
171       Intros.
172       MApply 'sand_sbe_i.
173       MApply 'sand_sbe_e1.
174       MApply 'sand_sbe_e2.
175       Qed.
176
177 (** Subset and, commutativity: $ V \sand U = U \sand V $. *)
178       Theorem sand_s: (S:Set; U,V:S->Set) (SEq S (SAnd S V U) (SAnd S U V)).
179       Intros.
180       MApply 'seq_sbe_i.
181       MApply 'sand_sbe_s.
182       MApply 'sand_sbe_s.
183       Qed.
184
185 (** Subset and, sub or equal associativity 1: $ U \sand (V \sand W) \sub (U \sand V) \sand W $. *)
186       Theorem sand_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
187       Intros.
188       MApply 'sand_sbe_i.
189       MApply 'sand_sbe_i.
190       MApply 'sand_sbe_e2.
191       MApply '(sbe_t S (SAnd S V W)).
192       MApply 'sand_sbe_e1.
193       MApply 'sand_sbe_e2.
194       MApply '(sbe_t S (SAnd S V W)).
195       MApply 'sand_sbe_e1.
196       MApply 'sand_sbe_e1.
197       Qed.
198
199 (** Subset and, sub or equal associativity 2: $ (U \sand V) \sand W \sub U \sand (V \sand W) $. *)
200       Theorem sand_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SAnd S (SAnd S U V) W) (SAnd S U (SAnd S V W))).
201       Intros.
202       MApply '(sbe_t S (SAnd S W (SAnd S U V))).
203       MApply 'sand_sbe_s.
204       MApply '(sbe_t S (SAnd S (SAnd S V W) U)).
205       MApply '(sbe_t S (SAnd S (SAnd S W U) V)).
206       MApply 'sand_sbe_a1.
207       MApply '(sbe_t S (SAnd S V (SAnd S W U))).
208       MApply 'sand_sbe_s.
209       MApply 'sand_sbe_a1.
210       MApply 'sand_sbe_s.
211       Qed.
212
213 (** Subset and, associativity: $ U \sand (V \sand W) = (U \sand V) \sand W $. *)
214       Theorem sand_a: (S:Set; U,V,W:S->Set) (SEq S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
215       Intros.
216       MApply 'seq_sbe_i.
217       MApply 'sand_sbe_a1.
218       MApply 'sand_sbe_a2.
219       Qed.
220
221 (** Subset and, sub or equal compatibility 1: $ U \sub V \limp W \sand U \sub W \sand V $. *)
222       Theorem sand_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S W U) (SAnd S W V)).
223       Intros.
224       MApply '(sbe_t S (SAnd S U W)).
225       MApply 'sand_sbe_s.
226       MApply '(sbe_t S (SAnd S V W)).
227       MApply 'sand_sbe_c2.
228       MApply 'sand_sbe_s.
229       Qed.
230
231 (** Subset and, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sand W \sub V \sand X $. *)
232       Theorem sand_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SAnd S U W) (SAnd S V X)).
233       Intros.
234       MApply '(sbe_t S (SAnd S V W)).
235       MApply 'sand_sbe_c2.
236       MApply 'sand_sbe_c1.
237       Qed.
238
239    End subset_binary_intersection.
240    
241    Section subset_binary_union.
242
243 (** Subset or, epsilon introduction 2: $ a \e U \limp a \e U \sor V $. *)
244       Theorem sor_eps_i2: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a (SOr S U V)).
245       Intros.
246       MApply 'eps_i.
247       Unfold SOr.
248       MApply 'in_l.
249       MApply 'eps_e.      
250       Qed.
251
252 (** Subset or, epsilon introduction 1: $ a \e V \limp a \e U \sor V $. *)
253       Theorem sor_eps_i1: (S:Set; U,V:S->Set; a:S) (Eps S a V) -> (Eps S a (SOr S U V)).
254       Intros.
255       MApply 'eps_i.
256       Unfold SOr.
257       MApply 'in_r.
258       MApply 'eps_e.      
259       Qed.
260
261 (** Subset or, epsilon elimination: $ (a \e U \limp T) \limp (a \e V \limp T) \limp a \e U \sor V \limp T $. *)
262       Theorem sor_eps_e: (S:Set; a:S; U,V:S->Set; T:Set) ((Eps S a U) -> T) -> ((Eps S a V) -> T) -> (Eps S a (SOr S U V)) -> T.
263       Intros.
264       MCut '(SOr S U V a).
265       MApply 'eps_e.
266       MApply '(lor_e (U a) (V a)).
267       MApply 'H.
268       MApply 'eps_i.
269       MApply 'H0.
270       MApply 'eps_i.
271       Qed.
272
273 (** Subset or, epsilon criterion: $ a \e U \lor a \e V \liff a \e U \sor V $. *)
274       Theorem sor_eps: (S:Set; U,V:S->Set; a:S) (LIff (LOr (Eps S a U) (Eps S a V)) (Eps S a (SOr S U V))).
275       Intros.
276       MApply 'liff_i.
277       MApply '(lor_e (Eps S a U) (Eps S a V)).
278       MApply 'sor_eps_i2.
279       MApply 'sor_eps_i1.
280       MApply '(sor_eps_e S a U V).
281       MApply 'in_l.
282       MApply 'in_r.
283       Qed.
284
285 (** Subset or, sub or equal introduction 2: $ U \sub U \sor V $. *)
286       Theorem sor_sbe_i2: (S:Set; U,V:S->Set) (SbE S U (SOr S U V)).
287       Intros.
288       MApply 'sbe_i.
289       MApply 'sor_eps_i2.
290       Qed.
291
292 (** Subset or, sub or equal introduction 1: $ V \sub U \sor V $. *)
293       Theorem sor_sbe_i1: (S:Set; U,V:S->Set) (SbE S V (SOr S U V)).
294       Intros.
295       MApply 'sbe_i.
296       MApply 'sor_eps_i1.
297       Qed.
298
299 (** Subset or, sub or equal elimination: $ U \sub W \limp V \sub W \limp U \sor V \sub W $. *)
300       Theorem sor_sbe_e: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S V W) -> (SbE S (SOr S U V) W).
301       Intros.
302       MApply 'sbe_i.
303       MApply '(sor_eps_e S a U V).
304       MApply '(sbe_e S U).
305       MApply '(sbe_e S V).
306       Qed.
307
308 (** Subset or, sub or equal compatibility 2: $ U \sub V \limp U \sor W \sub V \sor W $. *)
309       Theorem sor_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S U W) (SOr S V W)).
310       Intros.
311       MApply 'sor_sbe_e.
312       MApply '(sbe_t S V).
313       MApply 'sor_sbe_i2.
314       MApply 'sor_sbe_i1.
315       Qed.
316
317 (** Subset or, sub or equal idempotency: $ U \sor U \sub U $. *)
318       Theorem sor_sbe_r: (S:Set; U:S->Set) (SbE S (SOr S U U) U).
319       Intros.
320       MApply 'sor_sbe_e.
321       MApply 'sbe_r.
322       MApply 'sbe_r.
323       Qed.
324
325 (** Subset or, idempotency: $ U \sor U = U $. *)
326       Theorem sor_r: (S:Set; U:S->Set) (SEq S (SOr S U U) U).
327       Intros.
328       MApply 'seq_sbe_i.
329       MApply 'sor_sbe_r.
330       MApply 'sor_sbe_i2.
331       Qed.
332
333 (** Subset or, sub or equal commutativity: $ V \sor U \sub U \sor V $. *)
334       Theorem sor_sbe_s: (S:Set; U,V:S->Set) (SbE S (SOr S V U) (SOr S U V)).
335       Intros.
336       MApply 'sor_sbe_e.
337       MApply 'sor_sbe_i1.
338       MApply 'sor_sbe_i2.      
339       Qed.
340
341 (** Subset or, commutativity: $ V \sor U = U \sor V $. *)
342       Theorem sor_s: (S:Set; U,V:S->Set) (SEq S (SOr S V U) (SOr S U V)).
343       Intros.
344       MApply 'seq_sbe_i.
345       MApply 'sor_sbe_s.
346       MApply 'sor_sbe_s.
347       Qed.
348
349 (** Subset or, sub or equal associativity 1: $ U \sor (V \sor W) \sub (U \sor V) \sor W $. *)
350       Theorem sor_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
351       Intros.
352       MApply 'sor_sbe_e.
353       MApply '(sbe_t S (SOr S U V)).
354       MApply 'sor_sbe_i2.
355       MApply 'sor_sbe_i2.
356       MApply 'sor_sbe_e.
357       MApply '(sbe_t S (SOr S U V)).
358       MApply 'sor_sbe_i1.
359       MApply 'sor_sbe_i2.
360       MApply 'sor_sbe_i1.
361       Qed.
362
363 (** Subset or, sub or equal associativity 2: $ (U \sor V) \sor W \sub U \sor (V \sor W) $. *)
364       Theorem sor_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SOr S (SOr S U V) W) (SOr S U (SOr S V W))).
365       Intros.
366       MApply '(sbe_t S (SOr S W (SOr S U V))).
367       MApply 'sor_sbe_s.
368       MApply '(sbe_t S (SOr S (SOr S V W) U)).
369       MApply '(sbe_t S (SOr S (SOr S W U) V)).
370       MApply 'sor_sbe_a1.
371       MApply '(sbe_t S (SOr S V (SOr S W U))).
372       MApply 'sor_sbe_s.
373       MApply 'sor_sbe_a1.
374       MApply 'sor_sbe_s.
375       Qed.
376
377 (** Subset or, associativity: $ U \sor (V \sor W) = (U \sor V) \sor W $. *)
378       Theorem sor_a: (S:Set; U,V,W:S->Set) (SEq S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
379       Intros.
380       MApply 'seq_sbe_i.
381       MApply 'sor_sbe_a1.
382       MApply 'sor_sbe_a2.
383       Qed.
384
385 (** Subset or, sub or equal compatibility 1: $ U \sub V \limp W \sor U \sub W \sor V $. *)
386       Theorem sor_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S W U) (SOr S W V)).
387       Intros.
388       MApply '(sbe_t S (SOr S U W)).
389       MApply 'sor_sbe_s.
390       MApply '(sbe_t S (SOr S V W)).
391       MApply 'sor_sbe_c2.
392       MApply 'sor_sbe_s.
393       Qed.
394
395 (** Subset or, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sor W \sub V \sor X $. *)
396       Theorem sor_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SOr S U W) (SOr S V X)).
397       Intros.
398       MApply '(sbe_t S (SOr S V W)).
399       MApply 'sor_sbe_c2.
400       MApply 'sor_sbe_c1.
401       Qed.
402
403    End subset_binary_union.
404    
405    Section subset_implication.
406
407 (** Subset implies, epsilon introduction: $ (a \e U \limp a \e V) \limp a \e U \simp V $. *)
408       Theorem simp_eps_i: (S:Set; U,V:S->Set; a:S) ((Eps S a U) -> (Eps S a V)) -> (Eps S a (SImp S U V)).
409       Intros.
410       MApply 'eps_i.
411       Unfold SImp.
412       Intros.
413       MApply 'eps_e.
414       MApply 'H.
415       MApply 'eps_i.
416       Qed.
417
418 (** Subset implies, epsilon elimination: $ a \e U \simp V \limp a \e U \limp a \e V $. *)
419       Theorem simp_eps_e: (S:Set; U,V:S->Set; a:S) (Eps S a (SImp S U V)) -> (Eps S a U) -> (Eps S a V).
420       Intros.
421       MApply 'eps_i.
422       Apply (mcut (U a)).
423       MApply 'eps_e.
424       MApply '(eps_e S a).
425       Qed.
426
427 (** Subset implies, epsilon criterion: $ a \e U \simp V \liff (a \e U \limp a \e V) $. *)
428       Theorem simp_eps: (S:Set; U,V:S->Set; a:S) (LIff (Eps S a (SImp S U V)) (Eps S a U) -> (Eps S a V)).
429       Intros.
430       MApply 'liff_i.
431       MApply '(simp_eps_e S U).
432       MApply 'simp_eps_i.
433       MApply 'H.
434       Qed.
435
436 (** Subset implies, sub or equal elimination: $ W \sub U \simp V \limp W \sand U \sub V $. *)
437       Theorem simp_sbe_e: (S:Set; U,V,W:S->Set) (SbE S W (SImp S U V)) -> (SbE S (SAnd S W U) V).
438       Intros.
439       MApply 'sbe_i.
440       MApply '(simp_eps_e S U).
441       MApply '(sbe_e S W).
442       MApply '(sand_eps_e2 S U).
443       MApply '(sand_eps_e1 S W).
444       Qed.
445
446 (** Subset implies, sub or equal introduction: $ W \sand U \sub V \limp W \sub U \simp V $. *)
447       Theorem simp_sbe_i: (S:Set; U,V,W:S->Set) (SbE S (SAnd S W U) V) -> (SbE S W (SImp S U V)).
448       Intros.
449       MApply 'sbe_i.
450       MApply 'simp_eps_i.
451       MApply '(sbe_e S (SAnd S W U)).
452       MApply 'sand_eps_i.
453       Qed.
454
455 (** Subset implies, sub or equal compatibility 2: $ V \sub U \limp U \simp W \sub V \simp W $. *)
456       Theorem simp_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S V U) -> (SbE S (SImp S U W) (SImp S V W)).
457       Intros.
458       MApply 'simp_sbe_i.
459       MApply '(sbe_t S (SAnd S (SImp S U W) U)).
460       MApply 'sand_sbe_c1.
461       MApply 'simp_sbe_e.
462       MApply 'sbe_r.
463       Qed.
464
465 (** Subset implies, sub or equal compatibility 2: $ U \sub V \limp W \simp U \sub W \simp V $. *)
466       Theorem simp_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SImp S W U) (SImp S W V)).
467       Intros.
468       MApply 'simp_sbe_i.
469       MApply '(sbe_t S U).
470       MApply 'simp_sbe_e.
471       MApply 'sbe_r.
472       Qed.
473
474 (** Subset implies, subset top elimination: $ \stop \sub U \simp V \limp U \sub V $. *)
475       Theorem simp_stop_e: (S:Set; U,V:S->Set) (SbE S (STop S) (SImp S U V)) -> (SbE S U V).
476       Intros.
477       MApply '(sbe_t S (SAnd S (STop S) U)).
478       MApply 'sand_sbe_stop.
479       MApply 'simp_sbe_e.
480       Qed.
481
482 (** Subset implies, subset top introduction: $ U \sub V \limp \stop \sub U \simp V $. *)
483       Theorem simp_stop_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S (STop S) (SImp S U V)). 
484       Intros.
485       MApply 'simp_sbe_i.
486       MApply '(sbe_t S U).
487       MApply 'sand_sbe_e1.
488       Qed.
489
490 (** Subset implies, subset top criterion: $ \stop \sub U \simp V \liff U \sub V $. *)
491       Theorem simp_stop: (S:Set; U,V:S->Set) (LIff (SbE S (STop S) (SImp S U V)) (SbE S U V)).
492       Intros.
493       MApply 'liff_i.
494       MApply 'simp_stop_e.
495       MApply 'simp_stop_i.
496       Qed.
497
498    End subset_implication.
499    
500    Section subset_negation.
501
502 (** Subset not, epsilon introduction: $ \lnot (a \e U) \limp a \e \snot U $. *)
503       Theorem snot_eps_i: (S:Set; U:S->Set; a:S) (LNot (Eps S a U)) -> (Eps S a (SNot S U)).
504       Intros.
505       MApply 'eps_i.
506       Unfold SNot.
507       MApply 'lnot_i.
508       MApply '(lnot_e (Eps S a U)).
509       MApply 'eps_i.
510       Qed.
511
512 (** Subset not, epsilon elimination: $ a \e \snot U \limp \lnot (a \e U) $. *)
513       Theorem snot_eps_e: (S:Set; U:S->Set; a:S) (Eps S a (SNot S U)) -> (LNot (Eps S a U)).
514       Unfold SNot.
515       Intros.
516       MApply 'lnot_i.
517       MApply '(lnot_e (U a)).
518       MApply '(eps_e S a [a0:S](LNot (U a0))).
519       MApply 'eps_e.
520       Qed.
521
522 (** Subset not, epsilon criterion: $ \lnot (a \e U) \liff a \e \snot U $. *)
523       Theorem snot_eps: (S:Set; U:S->Set; a:S) (LIff (LNot (Eps S a U)) (Eps S a (SNot S U))).
524       Intros.
525       MApply 'liff_i.
526       MApply 'snot_eps_i.
527       MApply 'snot_eps_e.
528       Qed.
529
530 (** Subset not, subset implication compatibility: $ \snot U = U \simp \sbot $. *)
531       Theorem snot_simp_c: (S:Set; U:S->Set) (SEq S (SNot S U) (SImp S U (SBot S))).
532       Intros.
533       MApply 'seq_i.
534       MApply 'simp_eps_i.
535       MCut 'Empty.
536       MApply '(lnot_e (Eps S a U)).
537       MApply 'snot_eps_e.
538       MElim 'H1 'efq.
539       MApply 'snot_eps_i.
540       MApply 'lnot_i.
541       MApply '(sbot_eps_e S a).
542       MApply '(simp_eps_e S U).
543       Qed.
544
545    End subset_negation.
546
547    Section subset_infinitary_intersection.
548
549 (** Subset all, epsilon introduction: $ ((\lall i \in I)\ a \e F(i)) \limp a \e \bigsand\subset{F(i) \st i \in I} $. *)
550       Theorem sall_eps_i: (I,S:Set; F:(I->S->Set); a:S) ((i:I) (Eps S a (F i))) -> (Eps S a (SAll I S F)).
551       Intros.
552       MApply 'eps_i.
553       Unfold SAll.
554       Intros.
555       MApply 'eps_e.
556       MApply '(H i).
557       Qed.
558
559 (** Subset all, epsilon elimination: $ a \e \bigsand\subset{F(i) \st i \in I} \limp (\lall i \in I)\ a \e F(i) $. *)
560       Theorem sall_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SAll I S F)) -> (i:I) (Eps S a (F i)).
561       Intros.
562       MApply 'eps_i.
563       Apply (mcut (i:I)(F i a)).
564       MApply '(eps_e S a).
565       Intros.
566       MApply '(H0 i).
567       Qed.
568
569 (** Subset all, epsilon criterion: $ a \e \bigsand\subset{F(i) \st i \in I} \liff (\lall i \in I)\ a \e F(i) $. *)
570       Theorem sall_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SAll I S F)) (i:I) (Eps S a (F i))).
571       Intros.
572       MApply 'liff_i.
573       MApply '(sall_eps_e I).
574       MApply 'sall_eps_i.
575       MApply '(H i).
576       Qed.
577
578 (** Subset all, sub or equal elimination: $ (\lall i \in I)\ \bigsand\subset{F(i) \st i \in I} \sub F(i) $. *)
579       Theorem sall_sbe_e: (I,S:Set; F:(I->S->Set); i:I) (SbE S (SAll I S F) (F i)). 
580       Intros.
581       MApply 'sbe_i.
582       MApply '(sall_eps_e I).
583       Qed.
584
585 (** Subset all, sub or equal introduction: $ ((\lall i \in I)\ W \sub F(i)) \limp W \sub \bigsand\subset{F(i) \st i \in I} $. *)
586       Theorem sall_sbe_i: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S W (F i))) -> (SbE S W (SAll I S F)).
587       Intros.
588       MApply 'sbe_i.
589       MApply 'sall_eps_i.
590       MApply '(sbe_e S W).
591       MApply 'H.
592       Qed.
593       
594    End subset_infinitary_intersection.
595
596    Section subset_infinitary_union.
597
598 (** Subset exists, epsilon introduction: $ ((\lex i \in I)\ a \e F(i)) \limp a \e \bigsor\subset{F(i) \st i \in I} $. *)
599       Theorem sex_eps_i: (I,S:Set; F:(I->S->Set); a:S) (LEx I [i](Eps S a (F i))) -> (Eps S a (SEx I S F)).
600       Intros.
601       MApply 'eps_i.
602       Unfold SEx.
603       MElim 'H 'lex_e.
604       MApply '(lex_i I a0).
605       MApply 'eps_e.
606       Qed.
607
608 (** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \limp (\lex i \in I)\ a \e F(i) $. *)
609       Theorem sex_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SEx I S F)) -> (LEx I [i](Eps S a (F i))).
610       Intros.
611       MCut '(SEx I S F a).
612       MApply 'eps_e.
613       MElim 'H0 'lex_e.
614       MApply '(lex_i I a0).
615       MApply 'eps_i.
616       Qed.
617
618 (** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \liff (\lex i \in I)\ a \e F(i) $. *)
619       Theorem sex_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SEx I S F)) (LEx I [i](Eps S a (F i)))).
620       Intros.
621       MApply 'liff_i.
622       MApply 'sex_eps_e.
623       MApply 'sex_eps_i.
624       Qed.
625
626 (** Subset exists, sub or equal introduction: $ (\lall i \in I)\ F(i) \sub \bigsor\subset{F(i) \st i \in I} $. *)
627       Theorem sex_sbe_i: (I,S:Set; F:(I->S->Set); i:I) (SbE S (F i) (SEx I S F)). 
628       Intros.
629       MApply 'sbe_i.
630       MApply 'sex_eps_i.
631       MApply '(lex_i I i).
632       Qed.
633
634 (** Subset exists, sub or equal elimination: $ ((\lall i \in I)\ F(i) \sub W) \limp \bigsor\subset{F(i) \st i \in I} \sub W $. *)
635       Theorem sex_sbe_e: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S (F i) W)) -> (SbE S (SEx I S F) W).
636       Intros.
637       MApply 'sbe_i.
638       MCut '(LEx I [i:I](Eps S a (F i))).
639       MApply 'sex_eps_e.
640       MElim 'H1 'lex_e.
641       MApply '(sbe_e S (F a0)).
642       MApply 'H.
643       Qed.
644       
645    End subset_infinitary_union.
646
647    Section subset_frame.
648
649 (** Frame, subset and introduction: $ U \sub V \limp U \sand V = U $. *)
650       Theorem frame_sand_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SAnd S U V) U).
651       Intros.
652       MApply 'seq_sbe_i.
653       MApply 'sand_sbe_e2.
654       MApply '(sbe_t S (SAnd S U U)).
655       MApply 'sand_sbe_r.
656       MApply 'sand_sbe_c1.
657       Qed.
658
659 (** Frame, subset and elimination: $ U \sand V = U \limp U \sub V $. *)
660       Theorem frame_sand_e: (S:Set; U,V:S->Set) (SEq S (SAnd S U V) U) -> (SbE S U V).
661       Intros.
662       MApply '(sbe_t S (SAnd S U V)).
663       MApply '(land_e1 (SbE S (SAnd S U V) U)).
664       MApply 'seq_sbe_e.
665       MApply 'sand_sbe_e1.
666       Qed.
667
668 (** Frame, subset or introduction: $ U \sub V \limp U \sor V = V $. *)
669       Theorem frame_sor_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SOr S U V) V).
670       Intros.
671       MApply 'seq_sbe_i.
672       MApply '(sbe_t S (SOr S V V)).
673       MApply 'sor_sbe_c2.
674       MApply 'sor_sbe_r.
675       MApply 'sor_sbe_i1.
676       Qed.
677
678 (** Frame, subset or elimination: $ U \sor V = V \limp U \sub V $. *)
679       Theorem frame_sor_e: (S:Set; U,V:S->Set) (SEq S (SOr S U V) V) -> (SbE S U V).
680       Intros.
681       MApply '(sbe_t S (SOr S U V)).
682       MApply 'sor_sbe_i2.      
683       MApply '(land_e2 (SbE S V (SOr S U V))).
684       MApply 'seq_sbe_e.
685       Qed.
686
687 (** Frame, subset exists introduction: $ \bigsor\subset{F(i) \st i \in I} \sand W \sub \bigsor\subset{F(i) \sand W \st i \in I} $. *)
688       Theorem frame_sex_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
689       Intros.
690       MApply 'sbe_i.
691       MApply 'sex_eps_i.
692       MCut '(Eps S a (SEx I S F)).
693       MApply '(sand_eps_e2 S W).
694       MCut '(LEx I [i:I](Eps S a (F i))).
695       MApply 'sex_eps_e.
696       MElim 'H1 'lex_e.
697       MApply '(lex_i I a0).
698       MApply 'sand_eps_i.
699       MApply '(sand_eps_e1 S (SEx I S F)).
700       Qed.
701
702 (** Frame, subset exists elimination: $ \bigsor\subset{F(i) \sand W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \sand W $. *)
703       Theorem frame_sex_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SEx I S [i]
704 (SAnd S (F i) W)) (SAnd S (SEx I S F) W)).
705       Intros.
706       MApply 'sand_sbe_i.
707       MApply 'sex_sbe_e.
708       MApply '(sbe_t S (F i)).
709       MApply 'sand_sbe_e2.
710       MApply 'sex_sbe_i.
711       MApply 'sex_sbe_e.
712       MApply 'sand_sbe_e1.
713       Qed.
714
715 (** Frame, subset exists distributivity: $ \bigsor\subset{F(i) \st i \in I} \sand W = \bigsor\subset{F(i) \sand W \st i \in I} $. *)
716       Theorem frame_sex_d: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
717       Intros.
718       MApply 'seq_sbe_i.
719       MApply 'frame_sex_i.
720       MApply 'frame_sex_e.
721       Qed.
722
723 (** Frame, subset implies elimination: $ \bigsor\subset{F(i) \st i \in I} \simp W \sub \bigsand\subset{F(i) \simp W \st i \in I} $. *)
724       Theorem frame_simp_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
725       Intros.
726       MApply 'sall_sbe_i.
727       MApply 'simp_sbe_c2.
728       MApply 'sex_sbe_i.
729       Qed.
730
731 (** Frame, subset implies introduction: $ \bigsand\subset{F(i) \simp W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \simp W $. *)
732       Theorem frame_simp_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAll I S [i](SImp S (F i) W)) (SImp S (SEx I S F) W)).
733       Intros.
734       MApply 'sbe_i.
735       MApply 'simp_eps_i.
736       MCut '(LEx I [i:I](Eps S a (F i))).
737       MApply 'sex_eps_e.
738       MElim 'H1 'lex_e.
739       MApply '(simp_eps_e S (F a0)).
740       MApply '(sall_eps_e I S [i:I](SImp S (F i) W)).
741       Qed.
742
743 (** Frame, subset implies compatibility: $ \bigsor\subset{F(i) \st i \in I} \simp W = \bigsand\subset{F(i) \simp W \st i \in I} $. *)
744       Theorem frame_simp_c: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
745       Intros.
746       MApply 'seq_sbe_i.
747       MApply 'frame_simp_e.
748       MApply 'frame_simp_i.
749       Qed.
750       
751    End subset_frame.
752
753    Section cantor_diagonalization.
754
755 (** [(D S F)] is Cantor's subset $ D_F $. *)
756       Local D: (S:Set) (S -> S -> Set) -> (S -> Set).
757       Intros S F.
758       Exact (SNot S [a:S](F a a)).
759       Defined.
760
761 (** Cantor's diagonalization: $ (\lall b \in S)\ \lnot (F(b) = D_F) $. *)
762       Theorem cantor_diag: (S:Set; F:S->S->Set) (b:S) (LNot (SEq S (F b) (D S F))).
763       Intros.
764       MApply 'lnot_i.   
765       MCut '(LIff (Eps S b (F b)) (LNot (Eps S b (F b)))).
766       MApply 'liff_i.
767       MApply 'snot_eps_e.
768       Change (Eps S b (D S F)).
769       MApply '(seq_e1 S (F b)).
770       MApply '(seq_e2 S (D S F)).
771       Change (Eps S b (SNot S (F b))).
772       MApply 'snot_eps_i.
773       MApply '(lnot_liff_lbot (Eps S b (F b))).
774       Qed.
775    
776    End cantor_diagonalization.
777
778 End Subset_Operations_Results.