File: theorems.tex

package info (click to toggle)
hol88 2.02.19940316-35
  • links: PTS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 65,988 kB
  • ctags: 21,623
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (587 lines) | stat: -rw-r--r-- 16,456 bytes parent folder | download | duplicates (5)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
\chapter{Pre-proved Theorems}\input{theorems-intro}\section{The type definition}\THEOREM set\_ISO\_DEF sets
|- (!a. SPEC(CHF a) = a) /\ (!r. (\p. T)r = (CHF(SPEC r) = r))
\ENDTHEOREM
\THEOREM set\_TY\_DEF sets
|- ?rep. TYPE_DEFINITION(\p. T)rep
\ENDTHEOREM
\section{Membership, equality, and set specifications}\THEOREM EXTENSION sets
|- !s t. (s = t) = (!x. x IN s = x IN t)
\ENDTHEOREM
\THEOREM GSPEC\_DEF sets
|- !f. GSPEC f = SPEC(\y. ?x. y,T = f x)
\ENDTHEOREM
\THEOREM GSPECIFICATION sets
|- !f v. v IN (GSPEC f) = (?x. v,T = f x)
\ENDTHEOREM
\THEOREM IN\_DEF sets
|- !x s. x IN s = CHF s x
\ENDTHEOREM
\THEOREM NOT\_EQUAL\_SETS sets
|- !s t. ~(s = t) = (?x. x IN t = ~x IN s)
\ENDTHEOREM
\THEOREM NUM\_SET\_WOP sets
|- !s. (?n. n IN s) = (?n. n IN s /\ (!m. m IN s ==> n <= m))
\ENDTHEOREM
\THEOREM SET\_MINIMUM sets
|- !s M. (?x. x IN s) = (?x. x IN s /\ (!y. y IN s ==> (M x) <= (M y)))
\ENDTHEOREM
\THEOREM SPECIFICATION sets
|- !P x. x IN (SPEC P) = P x
\ENDTHEOREM
\section{The empty and universal sets}\THEOREM EMPTY\_DEF sets
|- {} = SPEC(\x. F)
\ENDTHEOREM
\THEOREM EMPTY\_NOT\_UNIV sets
|- ~({} = UNIV)
\ENDTHEOREM
\THEOREM EQ\_UNIV sets
|- (!x. x IN s) = (s = UNIV)
\ENDTHEOREM
\THEOREM IN\_UNIV sets
|- !x. x IN UNIV
\ENDTHEOREM
\THEOREM MEMBER\_NOT\_EMPTY sets
|- !s. (?x. x IN s) = ~(s = {})
\ENDTHEOREM
\THEOREM NOT\_IN\_EMPTY sets
|- !x. ~x IN {}
\ENDTHEOREM
\THEOREM UNIV\_DEF sets
|- UNIV = SPEC(\x. T)
\ENDTHEOREM
\THEOREM UNIV\_NOT\_EMPTY sets
|- ~(UNIV = {})
\ENDTHEOREM
\section{Set inclusion}\THEOREM EMPTY\_SUBSET sets
|- !s. {} SUBSET s
\ENDTHEOREM
\THEOREM NOT\_PSUBSET\_EMPTY sets
|- !s. ~s PSUBSET {}
\ENDTHEOREM
\THEOREM NOT\_UNIV\_PSUBSET sets
|- !s. ~UNIV PSUBSET s
\ENDTHEOREM
\THEOREM PSUBSET\_DEF sets
|- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t)
\ENDTHEOREM
\THEOREM PSUBSET\_IRREFL sets
|- !s. ~s PSUBSET s
\ENDTHEOREM
\THEOREM PSUBSET\_MEMBER sets
|- !s t. s PSUBSET t = s SUBSET t /\ (?y. y IN t /\ ~y IN s)
\ENDTHEOREM
\THEOREM PSUBSET\_TRANS sets
|- !s t u. s PSUBSET t /\ t PSUBSET u ==> s PSUBSET u
\ENDTHEOREM
\THEOREM PSUBSET\_UNIV sets
|- !s. s PSUBSET UNIV = (?x. ~x IN s)
\ENDTHEOREM
\THEOREM SUBSET\_ANTISYM sets
|- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)
\ENDTHEOREM
\THEOREM SUBSET\_DEF sets
|- !s t. s SUBSET t = (!x. x IN s ==> x IN t)
\ENDTHEOREM
\THEOREM SUBSET\_EMPTY sets
|- !s. s SUBSET {} = (s = {})
\ENDTHEOREM
\THEOREM SUBSET\_REFL sets
|- !s. s SUBSET s
\ENDTHEOREM
\THEOREM SUBSET\_TRANS sets
|- !s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u
\ENDTHEOREM
\THEOREM SUBSET\_UNIV sets
|- !s. s SUBSET UNIV
\ENDTHEOREM
\THEOREM UNIV\_SUBSET sets
|- !s. UNIV SUBSET s = (s = UNIV)
\ENDTHEOREM
\section{Intersection and union}\THEOREM EMPTY\_UNION sets
|- !s t. (s UNION t = {}) = (s = {}) /\ (t = {})
\ENDTHEOREM
\THEOREM IN\_INTER sets
|- !s t x. x IN (s INTER t) = x IN s /\ x IN t
\ENDTHEOREM
\THEOREM INTER\_ASSOC sets
|- !s t u. (s INTER t) INTER u = s INTER (t INTER u)
\ENDTHEOREM
\THEOREM INTER\_COMM sets
|- !s t. s INTER t = t INTER s
\ENDTHEOREM
\THEOREM INTER\_DEF sets
|- !s t. s INTER t = {x | x IN s /\ x IN t}
\ENDTHEOREM
\THEOREM INTER\_EMPTY sets
|- (!s. {} INTER s = {}) /\ (!s. s INTER {} = {})
\ENDTHEOREM
\THEOREM INTER\_IDEMPOT sets
|- !s. s INTER s = s
\ENDTHEOREM
\THEOREM INTER\_OVER\_UNION sets
|- !s t u. s UNION (t INTER u) = (s UNION t) INTER (s UNION u)
\ENDTHEOREM
\THEOREM INTER\_SUBSET sets
|- (!s t. (s INTER t) SUBSET s) /\ (!s t. (t INTER s) SUBSET s)
\ENDTHEOREM
\THEOREM INTER\_UNIV sets
|- (!s. UNIV INTER s = s) /\ (!s. s INTER UNIV = s)
\ENDTHEOREM
\THEOREM IN\_UNION sets
|- !s t x. x IN (s UNION t) = x IN s \/ x IN t
\ENDTHEOREM
\THEOREM SUBSET\_INTER\_ABSORPTION sets
|- !s t. s SUBSET t = (s INTER t = s)
\ENDTHEOREM
\THEOREM SUBSET\_UNION\_ABSORPTION sets
|- !s t. s SUBSET t = (s UNION t = t)
\ENDTHEOREM
\THEOREM SUBSET\_UNION sets
|- (!s t. s SUBSET (s UNION t)) /\ (!s t. s SUBSET (t UNION s))
\ENDTHEOREM
\THEOREM UNION\_ASSOC sets
|- !s t u. (s UNION t) UNION u = s UNION (t UNION u)
\ENDTHEOREM
\THEOREM UNION\_COMM sets
|- !s t. s UNION t = t UNION s
\ENDTHEOREM
\THEOREM UNION\_DEF sets
|- !s t. s UNION t = {x | x IN s \/ x IN t}
\ENDTHEOREM
\THEOREM UNION\_EMPTY sets
|- (!s. {} UNION s = s) /\ (!s. s UNION {} = s)
\ENDTHEOREM
\THEOREM UNION\_IDEMPOT sets
|- !s. s UNION s = s
\ENDTHEOREM
\THEOREM UNION\_OVER\_INTER sets
|- !s t u. s INTER (t UNION u) = (s INTER t) UNION (s INTER u)
\ENDTHEOREM
\THEOREM UNION\_UNIV sets
|- (!s. UNIV UNION s = UNIV) /\ (!s. s UNION UNIV = UNIV)
\ENDTHEOREM
\section{Set difference}\THEOREM DIFF\_DEF sets
|- !s t. s DIFF t = {x | x IN s /\ ~x IN t}
\ENDTHEOREM
\THEOREM DIFF\_DIFF sets
|- !s t. (s DIFF t) DIFF t = s DIFF t
\ENDTHEOREM
\THEOREM DIFF\_EMPTY sets
|- !s. s DIFF {} = s
\ENDTHEOREM
\THEOREM DIFF\_EQ\_EMPTY sets
|- !s. s DIFF s = {}
\ENDTHEOREM
\THEOREM DIFF\_UNIV sets
|- !s. s DIFF UNIV = {}
\ENDTHEOREM
\THEOREM EMPTY\_DIFF sets
|- !s. {} DIFF s = {}
\ENDTHEOREM
\THEOREM IN\_DIFF sets
|- !s t x. x IN (s DIFF t) = x IN s /\ ~x IN t
\ENDTHEOREM
\section{Disjoint sets}\THEOREM DISJOINT\_DEF sets
|- !s t. DISJOINT s t = (s INTER t = {})
\ENDTHEOREM
\THEOREM DISJOINT\_DELETE\_SYM sets
|- !s t x. DISJOINT(s DELETE x)t = DISJOINT(t DELETE x)s
\ENDTHEOREM

\THEOREM DISJOINT\_EMPTY sets
|- !s. DISJOINT {} s /\ DISJOINT s {}
\ENDTHEOREM
\THEOREM DISJOINT\_EMPTY\_REFL sets
|- !s. (s = {}) = DISJOINT s s
\ENDTHEOREM
\THEOREM DISJOINT\_SYM sets
|- !s t. DISJOINT s t = DISJOINT t s
\ENDTHEOREM
\THEOREM DISJOINT\_UNION sets
|- !s t u. DISJOINT(s UNION t)u = DISJOINT s u /\ DISJOINT t u
\ENDTHEOREM
\THEOREM IN\_DISJOINT sets
|- !s t. DISJOINT s t = ~(?x. x IN s /\ x IN t)
\ENDTHEOREM
\section{Insertion and deletion of an element}\THEOREM ABSORPTION sets
|- !x s. x IN s = (x INSERT s = s)
\ENDTHEOREM
\THEOREM COMPONENT sets
|- !x s. x IN (x INSERT s)
\ENDTHEOREM
\THEOREM DECOMPOSITION sets
|- !s x. x IN s = (?t. (s = x INSERT t) /\ ~x IN t)
\ENDTHEOREM
\THEOREM DELETE\_COMM sets
|- !x y s. (s DELETE x) DELETE y = (s DELETE y) DELETE x
\ENDTHEOREM
\THEOREM DELETE\_DEF sets
|- !s x. s DELETE x = s DIFF {x}
\ENDTHEOREM
\THEOREM DELETE\_DELETE sets
|- !x s. (s DELETE x) DELETE x = s DELETE x
\ENDTHEOREM
\THEOREM DELETE\_INSERT sets
|- !x y s.
    (x INSERT s) DELETE y =
    ((x = y) => s DELETE y | x INSERT (s DELETE y))
\ENDTHEOREM
\THEOREM DELETE\_INTER sets
|- !s t x. (s DELETE x) INTER t = (s INTER t) DELETE x
\ENDTHEOREM
\THEOREM DELETE\_NON\_ELEMENT sets
|- !x s. ~x IN s = (s DELETE x = s)
\ENDTHEOREM
\THEOREM DELETE\_SUBSET sets
|- !x s. (s DELETE x) SUBSET s
\ENDTHEOREM
\THEOREM DIFF\_INSERT sets
|- !s t x. s DIFF (x INSERT t) = (s DELETE x) DIFF t
\ENDTHEOREM
\THEOREM DISJOINT\_INSERT sets
|- !x s t. DISJOINT(x INSERT s)t = DISJOINT s t /\ ~x IN t
\ENDTHEOREM
\THEOREM EMPTY\_DELETE sets
|- !x. {} DELETE x = {}
\ENDTHEOREM
\THEOREM IN\_DELETE sets
|- !s x y. x IN (s DELETE y) = x IN s /\ ~(x = y)
\ENDTHEOREM
\THEOREM IN\_DELETE\_EQ sets
|- !s x x'.
    (x IN s = x' IN s) = (x IN (s DELETE x') = x' IN (s DELETE x))
\ENDTHEOREM
\THEOREM IN\_INSERT sets
|- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s
\ENDTHEOREM
\THEOREM INSERT\_COMM sets
|- !x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)
\ENDTHEOREM
\THEOREM INSERT\_DEF sets
|- !x s. x INSERT s = {y | (y = x) \/ y IN s}
\ENDTHEOREM
\THEOREM INSERT\_DELETE sets
|- !x s. x IN s ==> (x INSERT (s DELETE x) = s)
\ENDTHEOREM
\THEOREM INSERT\_DIFF sets
|- !s t x.
    (x INSERT s) DIFF t = (x IN t => s DIFF t | x INSERT (s DIFF t))
\ENDTHEOREM
\THEOREM INSERT\_INSERT sets
|- !x s. x INSERT (x INSERT s) = x INSERT s
\ENDTHEOREM
\THEOREM INSERT\_INTER sets
|- !x s t.
    (x INSERT s) INTER t = (x IN t => x INSERT (s INTER t) | s INTER t)
\ENDTHEOREM
\THEOREM INSERT\_SUBSET sets
|- !x s t. (x INSERT s) SUBSET t = x IN t /\ s SUBSET t
\ENDTHEOREM
\THEOREM INSERT\_UNION sets
|- !x s t.
    (x INSERT s) UNION t = (x IN t => s UNION t | x INSERT (s UNION t))
\ENDTHEOREM
\THEOREM INSERT\_UNION\_EQ sets
|- !x s t. (x INSERT s) UNION t = x INSERT (s UNION t)
\ENDTHEOREM
\THEOREM INSERT\_UNIV sets
|- !x. x INSERT UNIV = UNIV
\ENDTHEOREM
\THEOREM NOT\_EMPTY\_INSERT sets
|- !x s. ~({} = x INSERT s)
\ENDTHEOREM
\THEOREM NOT\_INSERT\_EMPTY sets
|- !x s. ~(x INSERT s = {})
\ENDTHEOREM
\THEOREM PSUBSET\_INSERT\_SUBSET sets
|- !s t. s PSUBSET t = (?x. ~x IN s /\ (x INSERT s) SUBSET t)
\ENDTHEOREM
\THEOREM SET\_CASES sets
|- !s. (s = {}) \/ (?x t. (s = x INSERT t) /\ ~x IN t)
\ENDTHEOREM
\THEOREM SUBSET\_DELETE sets
|- !x s t. s SUBSET (t DELETE x) = ~x IN s /\ s SUBSET t
\ENDTHEOREM
\THEOREM SUBSET\_INSERT\_DELETE sets
|- !x s t. s SUBSET (x INSERT t) = (s DELETE x) SUBSET t
\ENDTHEOREM
\THEOREM SUBSET\_INSERT sets
|- !x s. ~x IN s ==> (!t. s SUBSET (x INSERT t) = s SUBSET t)
\ENDTHEOREM
\section{The {\tt CHOICE} and {\tt REST} functions}\THEOREM CHOICE\_DEF sets
|- !s. ~(s = {}) ==> (CHOICE s) IN s
\ENDTHEOREM
\THEOREM CHOICE\_INSERT\_REST sets
|- !s. ~(s = {}) ==> ((CHOICE s) INSERT (REST s) = s)
\ENDTHEOREM
\THEOREM CHOICE\_NOT\_IN\_REST sets
|- !s. ~(CHOICE s) IN (REST s)
\ENDTHEOREM
\THEOREM CHOICE\_SING sets
|- !x. CHOICE{x} = x
\ENDTHEOREM
\THEOREM REST\_DEF sets
|- !s. REST s = s DELETE (CHOICE s)
\ENDTHEOREM
\THEOREM REST\_PSUBSET sets
|- !s. ~(s = {}) ==> (REST s) PSUBSET s
\ENDTHEOREM
\THEOREM REST\_SING sets
|- !x. REST{x} = {}
\ENDTHEOREM
\THEOREM REST\_SUBSET sets
|- !s. (REST s) SUBSET s
\ENDTHEOREM
\THEOREM SING\_IFF\_EMPTY\_REST sets
|- !s. SING s = ~(s = {}) /\ (REST s = {})
\ENDTHEOREM
\section{Image of a function on a set}\THEOREM IMAGE\_COMPOSE sets
|- !f g s. IMAGE(f o g)s = IMAGE f(IMAGE g s)
\ENDTHEOREM
\THEOREM IMAGE\_DEF sets
|- !f s. IMAGE f s = {f x | x IN s}
\ENDTHEOREM
\THEOREM IMAGE\_DELETE sets
|- !f x s. ~x IN s ==> (IMAGE f(s DELETE x) = IMAGE f s)
\ENDTHEOREM
\THEOREM IMAGE\_EMPTY sets
|- !f. IMAGE f{} = {}
\ENDTHEOREM
\THEOREM IMAGE\_EQ\_EMPTY sets
|- !s f. (IMAGE f s = {}) = (s = {})
\ENDTHEOREM
\THEOREM IMAGE\_ID sets
|- !s. IMAGE(\x. x)s = s
\ENDTHEOREM
\THEOREM IMAGE\_IN sets
|- !x s. x IN s ==> (!f. (f x) IN (IMAGE f s))
\ENDTHEOREM
\THEOREM IMAGE\_INSERT sets
|- !f x s. IMAGE f(x INSERT s) = (f x) INSERT (IMAGE f s)
\ENDTHEOREM
\THEOREM IMAGE\_INTER sets
|- !f s t. (IMAGE f(s INTER t)) SUBSET ((IMAGE f s) INTER (IMAGE f t))
\ENDTHEOREM
\THEOREM IMAGE\_SUBSET sets
|- !s t. s SUBSET t ==> (!f. (IMAGE f s) SUBSET (IMAGE f t))
\ENDTHEOREM
\THEOREM IMAGE\_UNION sets
|- !f s t. IMAGE f(s UNION t) = (IMAGE f s) UNION (IMAGE f t)
\ENDTHEOREM
\THEOREM IN\_IMAGE sets
|- !y s f. y IN (IMAGE f s) = (?x. (y = f x) /\ x IN s)
\ENDTHEOREM
\section{Mappings between sets}\THEOREM BIJ\_COMPOSE sets
|- !f g s t u. BIJ f s t /\ BIJ g t u ==> BIJ(g o f)s u
\ENDTHEOREM
\THEOREM BIJ\_DEF sets
|- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t
\ENDTHEOREM
\THEOREM BIJ\_EMPTY sets
|- !f. (!s. BIJ f{}s = (s = {})) /\ (!s. BIJ f s{} = (s = {}))
\ENDTHEOREM
\THEOREM BIJ\_ID sets
|- !s. BIJ(\x. x)s s
\ENDTHEOREM
\THEOREM IMAGE\_SURJ sets
|- !f s t. SURJ f s t = (IMAGE f s = t)
\ENDTHEOREM
\THEOREM INJ\_COMPOSE sets
|- !f g s t u. INJ f s t /\ INJ g t u ==> INJ(g o f)s u
\ENDTHEOREM
\THEOREM INJ\_DEF sets
|- !f s t.
    INJ f s t =
    (!x. x IN s ==> (f x) IN t) /\
    (!x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y))
\ENDTHEOREM
\THEOREM INJ\_EMPTY sets
|- !f. (!s. INJ f{}s) /\ (!s. INJ f s{} = (s = {}))
\ENDTHEOREM
\THEOREM INJ\_ID sets
|- !s. INJ(\x. x)s s
\ENDTHEOREM
\THEOREM LINV\_DEF sets
|- !f s t. INJ f s t ==> (!x. x IN s ==> (LINV f s(f x) = x))
\ENDTHEOREM
\THEOREM RINV\_DEF sets
|- !f s t. SURJ f s t ==> (!x. x IN t ==> (f(RINV f s x) = x))
\ENDTHEOREM
\THEOREM SURJ\_COMPOSE sets
|- !f g s t u. SURJ f s t /\ SURJ g t u ==> SURJ(g o f)s u
\ENDTHEOREM
\THEOREM SURJ\_DEF sets
|- !f s t.
    SURJ f s t =
    (!x. x IN s ==> (f x) IN t) /\
    (!x. x IN t ==> (?y. y IN s /\ (f y = x)))
\ENDTHEOREM
\THEOREM SURJ\_EMPTY sets
|- !f. (!s. SURJ f{}s = (s = {})) /\ (!s. SURJ f s{} = (s = {}))
\ENDTHEOREM
\THEOREM SURJ\_ID sets
|- !s. SURJ(\x. x)s s
\ENDTHEOREM
\section{Singleton sets}\THEOREM DELETE\_EQ\_SING sets
|- !s x. x IN s ==> ((s DELETE x = {}) = (s = {x}))
\ENDTHEOREM
\THEOREM DISJOINT\_SING\_EMPTY sets
|- !x. DISJOINT{x}{}
\ENDTHEOREM
\THEOREM EQUAL\_SING sets
|- !x y. ({x} = {y}) = (x = y)
\ENDTHEOREM
\THEOREM FINITE\_SING sets
|- !x. FINITE{x}
\ENDTHEOREM
\THEOREM INSERT\_SING\_UNION sets
|- !s x. x INSERT s = {x} UNION s
\ENDTHEOREM
\THEOREM IN\_SING sets
|- !x y. x IN {y} = (x = y)
\ENDTHEOREM
\THEOREM NOT\_EMPTY\_SING sets
|- !x. ~({} = {x})
\ENDTHEOREM
\THEOREM NOT\_SING\_EMPTY sets
|- !x. ~({x} = {})
\ENDTHEOREM
\THEOREM SING\_DEF sets
|- !s. SING s = (?x. s = {x})
\ENDTHEOREM
\THEOREM SING\_DELETE sets
|- !x. {x} DELETE x = {}
\ENDTHEOREM
\THEOREM SING sets
|- !x. SING{x}
\ENDTHEOREM
\THEOREM SING\_FINITE sets
|- !s. SING s ==> FINITE s
\ENDTHEOREM
\section{Finite and infinite sets}\THEOREM FINITE\_DEF sets
|- !s.
    FINITE s = (!P. P{} /\ (!s'. P s' ==> (!e. P(e INSERT s'))) ==> P s)
\ENDTHEOREM
\THEOREM FINITE\_DELETE sets
|- !x s. FINITE(s DELETE x) = FINITE s
\ENDTHEOREM
\THEOREM FINITE\_DIFF sets
|- !s. FINITE s ==> (!t. FINITE(s DIFF t))
\ENDTHEOREM
\THEOREM FINITE\_EMPTY sets
|- FINITE{}
\ENDTHEOREM
\THEOREM FINITE\_INDUCT sets
|- !P.
    P{} /\ (!s. FINITE s /\ P s ==> (!e. ~e IN s ==> P(e INSERT s))) ==>
    (!s. FINITE s ==> P s)
\ENDTHEOREM
\THEOREM FINITE\_INSERT sets
|- !x s. FINITE(x INSERT s) = FINITE s
\ENDTHEOREM
\THEOREM FINITE\_ISO\_NUM sets
|- !s.
    FINITE s ==>
    (?f.
      (!n m. n < (CARD s) /\ m < (CARD s) ==> (f n = f m) ==> (n = m)) /\
      (s = {f n | n < (CARD s)}))
\ENDTHEOREM
\THEOREM FINITE\_PSUBSET\_INFINITE sets
|- !s. INFINITE s = (!t. FINITE t ==> t SUBSET s ==> t PSUBSET s)
\ENDTHEOREM
\THEOREM FINITE\_PSUBSET\_UNIV sets
|- INFINITE UNIV = (!s. FINITE s ==> s PSUBSET UNIV)
\ENDTHEOREM
\THEOREM FINITE\_UNION sets
|- !s t. FINITE(s UNION t) = FINITE s /\ FINITE t
\ENDTHEOREM
\THEOREM IMAGE\_11\_INFINITE sets
|- !f.
    (!x y. (f x = f y) ==> (x = y)) ==>
    (!s. INFINITE s ==> INFINITE(IMAGE f s))
\ENDTHEOREM
\THEOREM IMAGE\_FINITE sets
|- !s. FINITE s ==> (!f. FINITE(IMAGE f s))
\ENDTHEOREM
\THEOREM INFINITE\_DEF sets
|- !s. INFINITE s = ~FINITE s
\ENDTHEOREM
\THEOREM INFINITE\_DIFF\_FINITE sets
|- !s t. INFINITE s /\ FINITE t ==> ~(s DIFF t = {})
\ENDTHEOREM
\THEOREM INFINITE\_SUBSET sets
|- !s. INFINITE s ==> (!t. s SUBSET t ==> INFINITE t)
\ENDTHEOREM
\THEOREM INFINITE\_UNIV sets
|- INFINITE (UNIV:(*)set) =
   (?f:*->*. (!x y. (f x = f y) ==> (x = y)) /\ (?y. !x. ~(f x = y)))
\ENDTHEOREM
\THEOREM IN\_INFINITE\_NOT\_FINITE sets
|- !s t. INFINITE s /\ FINITE t ==> (?x. x IN s /\ ~x IN t)
\ENDTHEOREM
\THEOREM INTER\_FINITE sets
|- !s. FINITE s ==> (!t. FINITE(s INTER t))
\ENDTHEOREM
\THEOREM NOT\_IN\_FINITE sets
|- INFINITE UNIV = (!s. FINITE s ==> (?x. ~x IN s))
\ENDTHEOREM
\THEOREM PSUBSET\_FINITE sets
|- !s. FINITE s ==> (!t. t PSUBSET s ==> FINITE t)
\ENDTHEOREM
\THEOREM SUBSET\_FINITE sets
|- !s. FINITE s ==> (!t. t SUBSET s ==> FINITE t)
\ENDTHEOREM
\section{Cardinality of sets}\THEOREM CARD\_DEF sets
|- (CARD{} = 0) /\
   (!s.
     FINITE s ==>
     (!x. CARD(x INSERT s) = (x IN s => CARD s | SUC(CARD s))))
\ENDTHEOREM
\THEOREM CARD\_DELETE sets
|- !s.
    FINITE s ==>
    (!x. CARD(s DELETE x) = (x IN s => (CARD s) - 1 | CARD s))
\ENDTHEOREM
\THEOREM CARD\_DIFF sets
|- !t.
    FINITE t ==>
    (!s. FINITE s ==> (CARD(s DIFF t) = (CARD s) - (CARD(s INTER t))))
\ENDTHEOREM
\THEOREM CARD\_EMPTY sets
|- CARD{} = 0
\ENDTHEOREM
\THEOREM CARD\_EQ\_0 sets
|- !s. FINITE s ==> ((CARD s = 0) = (s = {}))
\ENDTHEOREM
\THEOREM CARD\_INSERT sets
|- !s.
    FINITE s ==>
    (!x. CARD(x INSERT s) = (x IN s => CARD s | SUC(CARD s)))
\ENDTHEOREM
\THEOREM CARD\_INTER\_LESS\_EQ sets
|- !s. FINITE s ==> (!t. (CARD(s INTER t)) <= (CARD s))
\ENDTHEOREM
\THEOREM CARD\_PSUBSET sets
|- !s. FINITE s ==> (!t. t PSUBSET s ==> (CARD t) < (CARD s))
\ENDTHEOREM
\THEOREM CARD\_SING sets
|- !x. CARD{x} = 1
\ENDTHEOREM
\THEOREM CARD\_SUBSET sets
|- !s. FINITE s ==> (!t. t SUBSET s ==> (CARD t) <= (CARD s))
\ENDTHEOREM
\THEOREM CARD\_UNION sets
|- !s.
    FINITE s ==>
    (!t.
      FINITE t ==>
      ((CARD(s UNION t)) + (CARD(s INTER t)) = (CARD s) + (CARD t)))
\ENDTHEOREM
\THEOREM LESS\_CARD\_DIFF sets
|- !t.
    FINITE t ==>
    (!s. FINITE s ==> (CARD t) < (CARD s) ==> 0 < (CARD(s DIFF t)))
\ENDTHEOREM
\THEOREM SING\_IFF\_CARD1 sets
|- !s. SING s = (CARD s = 1) /\ FINITE s
\ENDTHEOREM