1 (* ========================================================================= *)
2 (* Very basic set theory (using predicates as sets). *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* (c) Copyright, Marco Maggesi 2012 *)
9 (* ========================================================================= *)
13 (* ------------------------------------------------------------------------- *)
14 (* Infix symbols for set operations. *)
15 (* ------------------------------------------------------------------------- *)
17 parse_as_infix("IN",(11,"right"));;
18 parse_as_infix("SUBSET",(12,"right"));;
19 parse_as_infix("PSUBSET",(12,"right"));;
20 parse_as_infix("INTER",(20,"right"));;
21 parse_as_infix("UNION",(16,"right"));;
22 parse_as_infix("DIFF",(18,"left"));;
23 parse_as_infix("INSERT",(21,"right"));;
24 parse_as_infix("DELETE",(21,"left"));;
26 parse_as_infix("HAS_SIZE",(12,"right"));;
27 parse_as_infix("<=_c",(12,"right"));;
28 parse_as_infix("<_c",(12,"right"));;
29 parse_as_infix(">=_c",(12,"right"));;
30 parse_as_infix(">_c",(12,"right"));;
31 parse_as_infix("=_c",(12,"right"));;
33 (* ------------------------------------------------------------------------- *)
35 (* ------------------------------------------------------------------------- *)
37 let IN = new_definition
38 `!P:A->bool. !x. x IN P <=> P x`;;
40 (* ------------------------------------------------------------------------- *)
41 (* Axiom of extensionality in this framework. *)
42 (* ------------------------------------------------------------------------- *)
45 (`!s t. (s = t) <=> !x:A. x IN s <=> x IN t`,
46 REWRITE_TAC[IN; FUN_EQ_THM]);;
48 (* ------------------------------------------------------------------------- *)
49 (* General specification. *)
50 (* ------------------------------------------------------------------------- *)
52 let GSPEC = new_definition
53 `GSPEC (p:A->bool) = p`;;
55 let SETSPEC = new_definition
56 `SETSPEC v P t <=> P /\ (v = t)`;;
58 (* ------------------------------------------------------------------------- *)
59 (* Rewrite rule for eliminating set-comprehension membership assertions. *)
60 (* ------------------------------------------------------------------------- *)
62 let IN_ELIM_THM = prove
63 (`(!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ (x = t))) /\
64 (!p x. x IN GSPEC (\v. ?y. SETSPEC v (p y) y) <=> p x) /\
65 (!P x. GSPEC (\v. P (SETSPEC v)) x <=> P (\p t. p /\ (x = t))) /\
66 (!p x. GSPEC (\v. ?y. SETSPEC v (p y) y) x <=> p x) /\
67 (!p x. x IN (\y. p y) <=> p x)`,
68 REPEAT STRIP_TAC THEN REWRITE_TAC[IN; GSPEC] THEN
69 TRY(AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM]) THEN
70 REWRITE_TAC[SETSPEC] THEN MESON_TAC[]);;
72 (* ------------------------------------------------------------------------- *)
73 (* These two definitions are needed first, for the parsing of enumerations. *)
74 (* ------------------------------------------------------------------------- *)
76 let EMPTY = new_definition
79 let INSERT_DEF = new_definition
80 `x INSERT s = \y:A. y IN s \/ (y = x)`;;
82 (* ------------------------------------------------------------------------- *)
83 (* The other basic operations. *)
84 (* ------------------------------------------------------------------------- *)
86 let UNIV = new_definition
89 let UNION = new_definition
90 `s UNION t = {x:A | x IN s \/ x IN t}`;;
92 let UNIONS = new_definition
93 `UNIONS s = {x:A | ?u. u IN s /\ x IN u}`;;
95 let INTER = new_definition
96 `s INTER t = {x:A | x IN s /\ x IN t}`;;
98 let INTERS = new_definition
99 `INTERS s = {x:A | !u. u IN s ==> x IN u}`;;
101 let DIFF = new_definition
102 `s DIFF t = {x:A | x IN s /\ ~(x IN t)}`;;
105 (`x INSERT s = {y:A | y IN s \/ (y = x)}`,
106 REWRITE_TAC[EXTENSION; INSERT_DEF; IN_ELIM_THM]);;
108 let DELETE = new_definition
109 `s DELETE x = {y:A | y IN s /\ ~(y = x)}`;;
111 (* ------------------------------------------------------------------------- *)
112 (* Other basic predicates. *)
113 (* ------------------------------------------------------------------------- *)
115 let SUBSET = new_definition
116 `s SUBSET t <=> !x:A. x IN s ==> x IN t`;;
118 let PSUBSET = new_definition
119 `(s:A->bool) PSUBSET t <=> s SUBSET t /\ ~(s = t)`;;
121 let DISJOINT = new_definition
122 `DISJOINT (s:A->bool) t <=> (s INTER t = EMPTY)`;;
124 let SING = new_definition
125 `SING s = ?x:A. s = {x}`;;
127 (* ------------------------------------------------------------------------- *)
129 (* ------------------------------------------------------------------------- *)
131 let FINITE_RULES,FINITE_INDUCT,FINITE_CASES =
132 new_inductive_definition
133 `FINITE (EMPTY:A->bool) /\
134 !(x:A) s. FINITE s ==> FINITE (x INSERT s)`;;
136 let INFINITE = new_definition
137 `INFINITE (s:A->bool) <=> ~(FINITE s)`;;
139 (* ------------------------------------------------------------------------- *)
140 (* Stuff concerned with functions. *)
141 (* ------------------------------------------------------------------------- *)
143 let IMAGE = new_definition
144 `IMAGE (f:A->B) s = { y | ?x. x IN s /\ (y = f x)}`;;
146 let INJ = new_definition
147 `INJ (f:A->B) s t <=>
148 (!x. x IN s ==> (f x) IN t) /\
149 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))`;;
151 let SURJ = new_definition
152 `SURJ (f:A->B) s t <=>
153 (!x. x IN s ==> (f x) IN t) /\
154 (!x. (x IN t) ==> ?y. y IN s /\ (f y = x))`;;
156 let BIJ = new_definition
157 `BIJ (f:A->B) s t <=> INJ f s t /\ SURJ f s t`;;
159 (* ------------------------------------------------------------------------- *)
160 (* Another funny thing. *)
161 (* ------------------------------------------------------------------------- *)
163 let CHOICE = new_definition
164 `CHOICE s = @x:A. x IN s`;;
166 let REST = new_definition
167 `REST (s:A->bool) = s DELETE (CHOICE s)`;;
169 (* ------------------------------------------------------------------------- *)
170 (* Basic membership properties. *)
171 (* ------------------------------------------------------------------------- *)
173 let NOT_IN_EMPTY = prove
174 (`!x:A. ~(x IN EMPTY)`,
175 REWRITE_TAC[IN; EMPTY]);;
179 REWRITE_TAC[UNIV; IN]);;
182 (`!s t (x:A). x IN (s UNION t) <=> x IN s \/ x IN t`,
183 REWRITE_TAC[IN_ELIM_THM; UNION]);;
185 let IN_UNIONS = prove
186 (`!s (x:A). x IN (UNIONS s) <=> ?t. t IN s /\ x IN t`,
187 REWRITE_TAC[IN_ELIM_THM; UNIONS]);;
190 (`!s t (x:A). x IN (s INTER t) <=> x IN s /\ x IN t`,
191 REWRITE_TAC[IN_ELIM_THM; INTER]);;
193 let IN_INTERS = prove
194 (`!s (x:A). x IN (INTERS s) <=> !t. t IN s ==> x IN t`,
195 REWRITE_TAC[IN_ELIM_THM; INTERS]);;
198 (`!(s:A->bool) t x. x IN (s DIFF t) <=> x IN s /\ ~(x IN t)`,
199 REWRITE_TAC[IN_ELIM_THM; DIFF]);;
201 let IN_INSERT = prove
202 (`!x:A. !y s. x IN (y INSERT s) <=> (x = y) \/ x IN s`,
203 ONCE_REWRITE_TAC[DISJ_SYM] THEN REWRITE_TAC[IN_ELIM_THM; INSERT]);;
205 let IN_DELETE = prove
206 (`!s. !x:A. !y. x IN (s DELETE y) <=> x IN s /\ ~(x = y)`,
207 REWRITE_TAC[IN_ELIM_THM; DELETE]);;
210 (`!x y. x IN {y:A} <=> (x = y)`,
211 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]);;
214 (`!y:B. !s f. (y IN (IMAGE f s)) <=> ?x:A. (y = f x) /\ x IN s`,
215 ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[IN_ELIM_THM; IMAGE]);;
218 (`!x:A. !s. x IN (REST s) <=> x IN s /\ ~(x = CHOICE s)`,
219 REWRITE_TAC[REST; IN_DELETE]);;
221 let FORALL_IN_INSERT = prove
222 (`!P a s. (!x. x IN (a INSERT s) ==> P x) <=> P a /\ (!x. x IN s ==> P x)`,
223 REWRITE_TAC[IN_INSERT] THEN MESON_TAC[]);;
225 let EXISTS_IN_INSERT = prove
226 (`!P a s. (?x. x IN (a INSERT s) /\ P x) <=> P a \/ ?x. x IN s /\ P x`,
227 REWRITE_TAC[IN_INSERT] THEN MESON_TAC[]);;
229 let FORALL_IN_UNION = prove
231 (!x. x IN s UNION t ==> P x) <=>
232 (!x. x IN s ==> P x) /\ (!x. x IN t ==> P x)`,
233 REWRITE_TAC[IN_UNION] THEN MESON_TAC[]);;
235 let EXISTS_IN_UNION = prove
237 (?x. x IN s UNION t /\ P x) <=>
238 (?x. x IN s /\ P x) \/ (?x. x IN t /\ P x)`,
239 REWRITE_TAC[IN_UNION] THEN MESON_TAC[]);;
241 (* ------------------------------------------------------------------------- *)
242 (* Basic property of the choice function. *)
243 (* ------------------------------------------------------------------------- *)
245 let CHOICE_DEF = prove
246 (`!s:A->bool. ~(s = EMPTY) ==> (CHOICE s) IN s`,
247 REWRITE_TAC[CHOICE; EXTENSION; NOT_IN_EMPTY; NOT_FORALL_THM; EXISTS_THM]);;
249 (* ------------------------------------------------------------------------- *)
250 (* Tactic to automate some routine set theory by reduction to FOL. *)
251 (* ------------------------------------------------------------------------- *)
255 POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT COND_CASES_TAC THEN
256 REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
257 REWRITE_TAC[NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
258 IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE;
261 (if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
265 let SET_RULE tm = prove(tm,SET_TAC[]);;
267 (* ------------------------------------------------------------------------- *)
268 (* Misc. theorems. *)
269 (* ------------------------------------------------------------------------- *)
271 let NOT_EQUAL_SETS = prove
272 (`!s:A->bool. !t. ~(s = t) <=> ?x. x IN t <=> ~(x IN s)`,
275 (* ------------------------------------------------------------------------- *)
277 (* ------------------------------------------------------------------------- *)
279 let MEMBER_NOT_EMPTY = prove
280 (`!s:A->bool. (?x. x IN s) <=> ~(s = EMPTY)`,
283 (* ------------------------------------------------------------------------- *)
284 (* The universal set. *)
285 (* ------------------------------------------------------------------------- *)
287 let UNIV_NOT_EMPTY = prove
288 (`~(UNIV:A->bool = EMPTY)`,
291 let EMPTY_NOT_UNIV = prove
292 (`~(EMPTY:A->bool = UNIV)`,
296 (`(!x:A. x IN s) <=> (s = UNIV)`,
299 (* ------------------------------------------------------------------------- *)
301 (* ------------------------------------------------------------------------- *)
303 let SUBSET_TRANS = prove
304 (`!(s:A->bool) t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u`,
307 let SUBSET_REFL = prove
308 (`!s:A->bool. s SUBSET s`,
311 let SUBSET_ANTISYM = prove
312 (`!(s:A->bool) t. s SUBSET t /\ t SUBSET s ==> s = t`,
315 let SUBSET_ANTISYM_EQ = prove
316 (`!(s:A->bool) t. s SUBSET t /\ t SUBSET s <=> s = t`,
319 let EMPTY_SUBSET = prove
320 (`!s:A->bool. EMPTY SUBSET s`,
323 let SUBSET_EMPTY = prove
324 (`!s:A->bool. s SUBSET EMPTY <=> (s = EMPTY)`,
327 let SUBSET_UNIV = prove
328 (`!s:A->bool. s SUBSET UNIV`,
331 let UNIV_SUBSET = prove
332 (`!s:A->bool. UNIV SUBSET s <=> (s = UNIV)`,
335 let SING_SUBSET = prove
336 (`!s x. {x} SUBSET s <=> x IN s`,
339 let SUBSET_RESTRICT = prove
340 (`!s P. {x | x IN s /\ P x} SUBSET s`,
341 SIMP_TAC[SUBSET; IN_ELIM_THM]);;
343 (* ------------------------------------------------------------------------- *)
345 (* ------------------------------------------------------------------------- *)
347 let PSUBSET_TRANS = prove
348 (`!(s:A->bool) t u. s PSUBSET t /\ t PSUBSET u ==> s PSUBSET u`,
351 let PSUBSET_SUBSET_TRANS = prove
352 (`!(s:A->bool) t u. s PSUBSET t /\ t SUBSET u ==> s PSUBSET u`,
355 let SUBSET_PSUBSET_TRANS = prove
356 (`!(s:A->bool) t u. s SUBSET t /\ t PSUBSET u ==> s PSUBSET u`,
359 let PSUBSET_IRREFL = prove
360 (`!s:A->bool. ~(s PSUBSET s)`,
363 let NOT_PSUBSET_EMPTY = prove
364 (`!s:A->bool. ~(s PSUBSET EMPTY)`,
367 let NOT_UNIV_PSUBSET = prove
368 (`!s:A->bool. ~(UNIV PSUBSET s)`,
371 let PSUBSET_UNIV = prove
372 (`!s:A->bool. s PSUBSET UNIV <=> ?x. ~(x IN s)`,
375 let PSUBSET_ALT = prove
376 (`!s t:A->bool. s PSUBSET t <=> s SUBSET t /\ (?a. a IN t /\ ~(a IN s))`,
377 REWRITE_TAC[PSUBSET] THEN SET_TAC[]);;
379 (* ------------------------------------------------------------------------- *)
381 (* ------------------------------------------------------------------------- *)
383 let UNION_ASSOC = prove
384 (`!(s:A->bool) t u. (s UNION t) UNION u = s UNION (t UNION u)`,
387 let UNION_IDEMPOT = prove
388 (`!s:A->bool. s UNION s = s`,
391 let UNION_COMM = prove
392 (`!(s:A->bool) t. s UNION t = t UNION s`,
395 let SUBSET_UNION = prove
396 (`(!s:A->bool. !t. s SUBSET (s UNION t)) /\
397 (!s:A->bool. !t. s SUBSET (t UNION s))`,
400 let SUBSET_UNION_ABSORPTION = prove
401 (`!s:A->bool. !t. s SUBSET t <=> (s UNION t = t)`,
404 let UNION_EMPTY = prove
405 (`(!s:A->bool. EMPTY UNION s = s) /\
406 (!s:A->bool. s UNION EMPTY = s)`,
409 let UNION_UNIV = prove
410 (`(!s:A->bool. UNIV UNION s = UNIV) /\
411 (!s:A->bool. s UNION UNIV = UNIV)`,
414 let EMPTY_UNION = prove
415 (`!s:A->bool. !t. (s UNION t = EMPTY) <=> (s = EMPTY) /\ (t = EMPTY)`,
418 let UNION_SUBSET = prove
419 (`!s t u. (s UNION t) SUBSET u <=> s SUBSET u /\ t SUBSET u`,
422 let FORALL_SUBSET_UNION = prove
424 (!s. s SUBSET t UNION u ==> P s) <=>
425 (!t' u'. t' SUBSET t /\ u' SUBSET u ==> P(t' UNION u'))`,
426 REPEAT GEN_TAC THEN EQ_TAC THENL
427 [REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[];
428 DISCH_TAC THEN X_GEN_TAC `s:A->bool` THEN DISCH_TAC THEN
429 FIRST_ASSUM(MP_TAC o SPECL [`s INTER t:A->bool`; `s INTER u:A->bool`]) THEN
430 ANTS_TAC THENL [ALL_TAC; MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC] THEN
433 let EXISTS_SUBSET_UNION = prove
435 (?s. s SUBSET t UNION u /\ P s) <=>
436 (?t' u'. t' SUBSET t /\ u' SUBSET u /\ P(t' UNION u'))`,
437 REWRITE_TAC[MESON[] `(?x. P x /\ Q x) <=> ~(!x. P x ==> ~Q x)`] THEN
438 REWRITE_TAC[FORALL_SUBSET_UNION] THEN MESON_TAC[]);;
440 (* ------------------------------------------------------------------------- *)
442 (* ------------------------------------------------------------------------- *)
444 let INTER_ASSOC = prove
445 (`!(s:A->bool) t u. (s INTER t) INTER u = s INTER (t INTER u)`,
448 let INTER_IDEMPOT = prove
449 (`!s:A->bool. s INTER s = s`,
452 let INTER_COMM = prove
453 (`!(s:A->bool) t. s INTER t = t INTER s`,
456 let INTER_SUBSET = prove
457 (`(!s:A->bool. !t. (s INTER t) SUBSET s) /\
458 (!s:A->bool. !t. (t INTER s) SUBSET s)`,
461 let SUBSET_INTER_ABSORPTION = prove
462 (`!s:A->bool. !t. s SUBSET t <=> (s INTER t = s)`,
465 let INTER_EMPTY = prove
466 (`(!s:A->bool. EMPTY INTER s = EMPTY) /\
467 (!s:A->bool. s INTER EMPTY = EMPTY)`,
470 let INTER_UNIV = prove
471 (`(!s:A->bool. UNIV INTER s = s) /\
472 (!s:A->bool. s INTER UNIV = s)`,
475 let SUBSET_INTER = prove
476 (`!s t u. s SUBSET (t INTER u) <=> s SUBSET t /\ s SUBSET u`,
479 (* ------------------------------------------------------------------------- *)
480 (* Distributivity. *)
481 (* ------------------------------------------------------------------------- *)
483 let UNION_OVER_INTER = prove
484 (`!s:A->bool. !t u. s INTER (t UNION u) = (s INTER t) UNION (s INTER u)`,
487 let INTER_OVER_UNION = prove
488 (`!s:A->bool. !t u. s UNION (t INTER u) = (s UNION t) INTER (s UNION u)`,
491 (* ------------------------------------------------------------------------- *)
493 (* ------------------------------------------------------------------------- *)
495 let IN_DISJOINT = prove
496 (`!s:A->bool. !t. DISJOINT s t <=> ~(?x. x IN s /\ x IN t)`,
499 let DISJOINT_SYM = prove
500 (`!s:A->bool. !t. DISJOINT s t <=> DISJOINT t s`,
503 let DISJOINT_EMPTY = prove
504 (`!s:A->bool. DISJOINT EMPTY s /\ DISJOINT s EMPTY`,
507 let DISJOINT_EMPTY_REFL = prove
508 (`!s:A->bool. (s = EMPTY) <=> (DISJOINT s s)`,
511 let DISJOINT_UNION = prove
512 (`!s:A->bool. !t u. DISJOINT (s UNION t) u <=> DISJOINT s u /\ DISJOINT t u`,
515 (* ------------------------------------------------------------------------- *)
516 (* Set difference. *)
517 (* ------------------------------------------------------------------------- *)
519 let DIFF_EMPTY = prove
520 (`!s:A->bool. s DIFF EMPTY = s`,
523 let EMPTY_DIFF = prove
524 (`!s:A->bool. EMPTY DIFF s = EMPTY`,
527 let DIFF_UNIV = prove
528 (`!s:A->bool. s DIFF UNIV = EMPTY`,
531 let DIFF_DIFF = prove
532 (`!s:A->bool. !t. (s DIFF t) DIFF t = s DIFF t`,
535 let DIFF_EQ_EMPTY = prove
536 (`!s:A->bool. s DIFF s = EMPTY`,
539 let SUBSET_DIFF = prove
540 (`!s t. (s DIFF t) SUBSET s`,
543 (* ------------------------------------------------------------------------- *)
544 (* Insertion and deletion. *)
545 (* ------------------------------------------------------------------------- *)
547 let COMPONENT = prove
548 (`!x:A. !s. x IN (x INSERT s)`,
551 let DECOMPOSITION = prove
552 (`!s:A->bool. !x. x IN s <=> ?t. (s = x INSERT t) /\ ~(x IN t)`,
553 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
554 ASM_REWRITE_TAC[IN_INSERT] THEN EXISTS_TAC `s DELETE x:A` THEN
555 POP_ASSUM MP_TAC THEN SET_TAC[]);;
557 let SET_CASES = prove
558 (`!s:A->bool. (s = EMPTY) \/ ?x:A. ?t. (s = x INSERT t) /\ ~(x IN t)`,
559 MESON_TAC[MEMBER_NOT_EMPTY; DECOMPOSITION]);;
561 let ABSORPTION = prove
562 (`!x:A. !s. x IN s <=> (x INSERT s = s)`,
565 let INSERT_INSERT = prove
566 (`!x:A. !s. x INSERT (x INSERT s) = x INSERT s`,
569 let INSERT_COMM = prove
570 (`!x:A. !y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)`,
573 let INSERT_UNIV = prove
574 (`!x:A. x INSERT UNIV = UNIV`,
577 let NOT_INSERT_EMPTY = prove
578 (`!x:A. !s. ~(x INSERT s = EMPTY)`,
581 let NOT_EMPTY_INSERT = prove
582 (`!x:A. !s. ~(EMPTY = x INSERT s)`,
585 let INSERT_UNION = prove
586 (`!x:A. !s t. (x INSERT s) UNION t =
587 if x IN t then s UNION t else x INSERT (s UNION t)`,
588 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
589 POP_ASSUM MP_TAC THEN SET_TAC[]);;
591 let INSERT_UNION_EQ = prove
592 (`!x:A. !s t. (x INSERT s) UNION t = x INSERT (s UNION t)`,
595 let INSERT_INTER = prove
596 (`!x:A. !s t. (x INSERT s) INTER t =
597 if x IN t then x INSERT (s INTER t) else s INTER t`,
598 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
599 POP_ASSUM MP_TAC THEN SET_TAC[]);;
601 let DISJOINT_INSERT = prove
602 (`!(x:A) s t. DISJOINT (x INSERT s) t <=> (DISJOINT s t) /\ ~(x IN t)`,
605 let INSERT_SUBSET = prove
606 (`!x:A. !s t. (x INSERT s) SUBSET t <=> (x IN t /\ s SUBSET t)`,
609 let SUBSET_INSERT = prove
610 (`!x:A. !s. ~(x IN s) ==> !t. s SUBSET (x INSERT t) <=> s SUBSET t`,
613 let INSERT_DIFF = prove
614 (`!s t. !x:A. (x INSERT s) DIFF t =
615 if x IN t then s DIFF t else x INSERT (s DIFF t)`,
616 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
617 POP_ASSUM MP_TAC THEN SET_TAC[]);;
619 let INSERT_AC = prove
620 (`(x INSERT (y INSERT s) = y INSERT (x INSERT s)) /\
621 (x INSERT (x INSERT s) = x INSERT s)`,
622 REWRITE_TAC[INSERT_COMM; INSERT_INSERT]);;
624 let INTER_ACI = prove
625 (`(p INTER q = q INTER p) /\
626 ((p INTER q) INTER r = p INTER q INTER r) /\
627 (p INTER q INTER r = q INTER p INTER r) /\
629 (p INTER p INTER q = p INTER q)`,
632 let UNION_ACI = prove
633 (`(p UNION q = q UNION p) /\
634 ((p UNION q) UNION r = p UNION q UNION r) /\
635 (p UNION q UNION r = q UNION p UNION r) /\
637 (p UNION p UNION q = p UNION q)`,
640 let DELETE_NON_ELEMENT = prove
641 (`!x:A. !s. ~(x IN s) <=> (s DELETE x = s)`,
644 let IN_DELETE_EQ = prove
646 (x IN s <=> x' IN s) <=> (x IN (s DELETE x') <=> x' IN (s DELETE x))`,
649 let EMPTY_DELETE = prove
650 (`!x:A. EMPTY DELETE x = EMPTY`,
653 let DELETE_DELETE = prove
654 (`!x:A. !s. (s DELETE x) DELETE x = s DELETE x`,
657 let DELETE_COMM = prove
658 (`!x:A. !y. !s. (s DELETE x) DELETE y = (s DELETE y) DELETE x`,
661 let DELETE_SUBSET = prove
662 (`!x:A. !s. (s DELETE x) SUBSET s`,
665 let SUBSET_DELETE = prove
666 (`!x:A. !s t. s SUBSET (t DELETE x) <=> ~(x IN s) /\ (s SUBSET t)`,
669 let SUBSET_INSERT_DELETE = prove
670 (`!x:A. !s t. s SUBSET (x INSERT t) <=> ((s DELETE x) SUBSET t)`,
673 let DIFF_INSERT = prove
674 (`!s t. !x:A. s DIFF (x INSERT t) = (s DELETE x) DIFF t`,
677 let PSUBSET_INSERT_SUBSET = prove
678 (`!s t. s PSUBSET t <=> ?x:A. ~(x IN s) /\ (x INSERT s) SUBSET t`,
681 let PSUBSET_MEMBER = prove
682 (`!s:A->bool. !t. s PSUBSET t <=> (s SUBSET t /\ ?y. y IN t /\ ~(y IN s))`,
685 let DELETE_INSERT = prove
687 (x INSERT s) DELETE y =
688 if x = y then s DELETE y else x INSERT (s DELETE y)`,
689 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
690 POP_ASSUM MP_TAC THEN SET_TAC[]);;
692 let INSERT_DELETE = prove
693 (`!x:A. !s. x IN s ==> (x INSERT (s DELETE x) = s)`,
696 let DELETE_INTER = prove
697 (`!s t. !x:A. (s DELETE x) INTER t = (s INTER t) DELETE x`,
700 let DISJOINT_DELETE_SYM = prove
701 (`!s t. !x:A. DISJOINT (s DELETE x) t = DISJOINT (t DELETE x) s`,
704 (* ------------------------------------------------------------------------- *)
705 (* Multiple union. *)
706 (* ------------------------------------------------------------------------- *)
717 (`UNIONS {s,t} = s UNION t`,
720 let UNIONS_INSERT = prove
721 (`UNIONS (s INSERT u) = s UNION (UNIONS u)`,
724 let FORALL_IN_UNIONS = prove
725 (`!P s. (!x. x IN UNIONS s ==> P x) <=> !t x. t IN s /\ x IN t ==> P x`,
728 let EXISTS_IN_UNIONS = prove
729 (`!P s. (?x. x IN UNIONS s /\ P x) <=> (?t x. t IN s /\ x IN t /\ P x)`,
732 let EMPTY_UNIONS = prove
733 (`!s. (UNIONS s = {}) <=> !t. t IN s ==> t = {}`,
736 let INTER_UNIONS = prove
737 (`(!s t. UNIONS s INTER t = UNIONS {x INTER t | x IN s}) /\
738 (!s t. t INTER UNIONS s = UNIONS {t INTER x | x IN s})`,
739 ONCE_REWRITE_TAC[EXTENSION] THEN
740 REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_INTER] THEN
741 MESON_TAC[IN_INTER]);;
743 let UNIONS_SUBSET = prove
744 (`!f t. UNIONS f SUBSET t <=> !s. s IN f ==> s SUBSET t`,
747 let SUBSET_UNIONS = prove
748 (`!f g. f SUBSET g ==> UNIONS f SUBSET UNIONS g`,
751 let UNIONS_UNION = prove
752 (`!s t. UNIONS(s UNION t) = (UNIONS s) UNION (UNIONS t)`,
755 let INTERS_UNION = prove
756 (`!s t. INTERS (s UNION t) = INTERS s INTER INTERS t`,
759 let UNIONS_MONO = prove
760 (`(!x. x IN s ==> ?y. y IN t /\ x SUBSET y) ==> UNIONS s SUBSET UNIONS t`,
763 let UNIONS_MONO_IMAGE = prove
764 (`(!x. x IN s ==> f x SUBSET g x)
765 ==> UNIONS(IMAGE f s) SUBSET UNIONS(IMAGE g s)`,
768 (* ------------------------------------------------------------------------- *)
769 (* Multiple intersection. *)
770 (* ------------------------------------------------------------------------- *)
781 (`INTERS {s,t} = s INTER t`,
784 let INTERS_INSERT = prove
785 (`INTERS (s INSERT u) = s INTER (INTERS u)`,
788 let SUBSET_INTERS = prove
789 (`!s f. s SUBSET INTERS f <=> (!t. t IN f ==> s SUBSET t)`,
792 (* ------------------------------------------------------------------------- *)
794 (* ------------------------------------------------------------------------- *)
796 let IMAGE_CLAUSES = prove
797 (`(IMAGE f {} = {}) /\
798 (IMAGE f (x INSERT s) = (f x) INSERT (IMAGE f s))`,
799 REWRITE_TAC[IMAGE; IN_ELIM_THM; NOT_IN_EMPTY; IN_INSERT; EXTENSION] THEN
802 let IMAGE_UNION = prove
803 (`!f s t. IMAGE f (s UNION t) = (IMAGE f s) UNION (IMAGE f t)`,
804 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_UNION] THEN MESON_TAC[]);;
807 (`!s. IMAGE (\x. x) s = s`,
808 REWRITE_TAC[EXTENSION; IN_IMAGE; UNWIND_THM1]);;
811 (`!s. IMAGE I s = s`,
812 REWRITE_TAC[I_DEF; IMAGE_ID]);;
815 (`!f g s. IMAGE (f o g) s = IMAGE f (IMAGE g s)`,
816 REWRITE_TAC[EXTENSION; IN_IMAGE; o_THM] THEN MESON_TAC[]);;
818 let IMAGE_SUBSET = prove
819 (`!f s t. s SUBSET t ==> (IMAGE f s) SUBSET (IMAGE f t)`,
820 REWRITE_TAC[SUBSET; IN_IMAGE] THEN MESON_TAC[]);;
822 let IMAGE_INTER_INJ = prove
823 (`!f s t. (!x y. (f(x) = f(y)) ==> (x = y))
824 ==> (IMAGE f (s INTER t) = (IMAGE f s) INTER (IMAGE f t))`,
825 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_INTER] THEN MESON_TAC[]);;
827 let IMAGE_DIFF_INJ = prove
828 (`!f s t. (!x y. (f(x) = f(y)) ==> (x = y))
829 ==> (IMAGE f (s DIFF t) = (IMAGE f s) DIFF (IMAGE f t))`,
830 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_DIFF] THEN MESON_TAC[]);;
832 let IMAGE_DELETE_INJ = prove
833 (`!f s a. (!x. (f(x) = f(a)) ==> (x = a))
834 ==> (IMAGE f (s DELETE a) = (IMAGE f s) DELETE (f a))`,
835 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_DELETE] THEN MESON_TAC[]);;
837 let IMAGE_EQ_EMPTY = prove
838 (`!f s. (IMAGE f s = {}) <=> (s = {})`,
839 REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_IMAGE] THEN MESON_TAC[]);;
841 let FORALL_IN_IMAGE = prove
842 (`!f s. (!y. y IN IMAGE f s ==> P y) <=> (!x. x IN s ==> P(f x))`,
843 REWRITE_TAC[IN_IMAGE] THEN MESON_TAC[]);;
845 let EXISTS_IN_IMAGE = prove
846 (`!f s. (?y. y IN IMAGE f s /\ P y) <=> ?x. x IN s /\ P(f x)`,
847 REWRITE_TAC[IN_IMAGE] THEN MESON_TAC[]);;
849 let SUBSET_IMAGE = prove
850 (`!f:A->B s t. s SUBSET (IMAGE f t) <=> ?u. u SUBSET t /\ (s = IMAGE f u)`,
851 REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[IMAGE_SUBSET]] THEN
852 DISCH_TAC THEN EXISTS_TAC `{x | x IN t /\ (f:A->B) x IN s}` THEN
853 POP_ASSUM MP_TAC THEN
854 REWRITE_TAC[EXTENSION; SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
857 let FORALL_SUBSET_IMAGE = prove
858 (`!P f s. (!t. t SUBSET IMAGE f s ==> P t) <=>
859 (!t. t SUBSET s ==> P(IMAGE f t))`,
860 REWRITE_TAC[SUBSET_IMAGE] THEN MESON_TAC[]);;
862 let EXISTS_SUBSET_IMAGE = prove
864 (?t. t SUBSET IMAGE f s /\ P t) <=> (?t. t SUBSET s /\ P (IMAGE f t))`,
865 REWRITE_TAC[SUBSET_IMAGE] THEN MESON_TAC[]);;
867 let IMAGE_CONST = prove
868 (`!s c. IMAGE (\x. c) s = if s = {} then {} else {c}`,
869 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
870 ASM_REWRITE_TAC[IMAGE_CLAUSES] THEN
871 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_SING] THEN
872 ASM_MESON_TAC[MEMBER_NOT_EMPTY]);;
874 let SIMPLE_IMAGE = prove
875 (`!f s. {f x | x IN s} = IMAGE f s`,
876 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN MESON_TAC[]);;
878 let SIMPLE_IMAGE_GEN = prove
879 (`!f P. {f x | P x} = IMAGE f {x | P x}`,
882 let IMAGE_UNIONS = prove
883 (`!f s. IMAGE f (UNIONS s) = UNIONS (IMAGE (IMAGE f) s)`,
884 ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IN_UNIONS; IN_IMAGE] THEN
885 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
886 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
887 REWRITE_TAC[GSYM CONJ_ASSOC; UNWIND_THM2; IN_IMAGE] THEN
890 let FUN_IN_IMAGE = prove
891 (`!f s x. x IN s ==> f(x) IN IMAGE f s`,
894 let SURJECTIVE_IMAGE_EQ = prove
895 (`!s t. (!y. y IN t ==> ?x. f x = y) /\ (!x. (f x) IN t <=> x IN s)
899 (* ------------------------------------------------------------------------- *)
901 (* ------------------------------------------------------------------------- *)
903 let EMPTY_GSPEC = prove
907 let UNIV_GSPEC = prove
911 let SING_GSPEC = prove
912 (`(!a. {x | x = a} = {a}) /\
913 (!a. {x | a = x} = {a})`,
916 let IN_ELIM_PAIR_THM = prove
917 (`!P a b. (a,b) IN {(x,y) | P x y} <=> P a b`,
918 REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[PAIR_EQ]);;
920 let SET_PAIR_THM = prove
921 (`!P. {p | P p} = {(a,b) | P(a,b)}`,
922 REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_ELIM_THM; IN_ELIM_PAIR_THM]);;
924 let FORALL_IN_GSPEC = prove
925 (`(!P f. (!z. z IN {f x | P x} ==> Q z) <=> (!x. P x ==> Q(f x))) /\
926 (!P f. (!z. z IN {f x y | P x y} ==> Q z) <=>
927 (!x y. P x y ==> Q(f x y))) /\
928 (!P f. (!z. z IN {f w x y | P w x y} ==> Q z) <=>
929 (!w x y. P w x y ==> Q(f w x y))) /\
930 (!P f. (!z. z IN {f v w x y | P v w x y} ==> Q z) <=>
931 (!v w x y. P v w x y ==> Q(f v w x y)))`,
934 let EXISTS_IN_GSPEC = prove
935 (`(!P f. (?z. z IN {f x | P x} /\ Q z) <=> (?x. P x /\ Q(f x))) /\
936 (!P f. (?z. z IN {f x y | P x y} /\ Q z) <=>
937 (?x y. P x y /\ Q(f x y))) /\
938 (!P f. (?z. z IN {f w x y | P w x y} /\ Q z) <=>
939 (?w x y. P w x y /\ Q(f w x y))) /\
940 (!P f. (?z. z IN {f v w x y | P v w x y} /\ Q z) <=>
941 (?v w x y. P v w x y /\ Q(f v w x y)))`,
944 let SET_PROVE_CASES = prove
945 (`!P:(A->bool)->bool.
946 P {} /\ (!a s. ~(a IN s) ==> P(a INSERT s))
948 MESON_TAC[SET_CASES]);;
950 let UNIONS_IMAGE = prove
951 (`!f s. UNIONS (IMAGE f s) = {y | ?x. x IN s /\ y IN f x}`,
952 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
953 REWRITE_TAC[IN_UNIONS; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]);;
955 let INTERS_IMAGE = prove
956 (`!f s. INTERS (IMAGE f s) = {y | !x. x IN s ==> y IN f x}`,
957 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
958 REWRITE_TAC[IN_INTERS; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]);;
960 let UNIONS_GSPEC = prove
961 (`(!P f. UNIONS {f x | P x} = {a | ?x. P x /\ a IN (f x)}) /\
962 (!P f. UNIONS {f x y | P x y} = {a | ?x y. P x y /\ a IN (f x y)}) /\
963 (!P f. UNIONS {f x y z | P x y z} =
964 {a | ?x y z. P x y z /\ a IN (f x y z)})`,
965 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
966 REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN MESON_TAC[]);;
968 let INTERS_GSPEC = prove
969 (`(!P f. INTERS {f x | P x} = {a | !x. P x ==> a IN (f x)}) /\
970 (!P f. INTERS {f x y | P x y} = {a | !x y. P x y ==> a IN (f x y)}) /\
971 (!P f. INTERS {f x y z | P x y z} =
972 {a | !x y z. P x y z ==> a IN (f x y z)})`,
973 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
974 REWRITE_TAC[IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
976 let DIFF_INTERS = prove
977 (`!u s. u DIFF INTERS s = UNIONS {u DIFF t | t IN s}`,
978 REWRITE_TAC[UNIONS_GSPEC] THEN SET_TAC[]);;
980 let INTERS_UNIONS = prove
981 (`!s. INTERS s = UNIV DIFF (UNIONS {UNIV DIFF t | t IN s})`,
982 REWRITE_TAC[GSYM DIFF_INTERS] THEN SET_TAC[]);;
984 let UNIONS_INTERS = prove
985 (`!s. UNIONS s = UNIV DIFF (INTERS {UNIV DIFF t | t IN s})`,
986 GEN_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
987 REWRITE_TAC[IN_UNIONS; IN_UNIV; IN_DIFF; INTERS_GSPEC; IN_ELIM_THM] THEN
990 let UNIONS_DIFF = prove
991 (`!s t. UNIONS s DIFF t = UNIONS {x DIFF t | x IN s}`,
992 REWRITE_TAC[UNIONS_GSPEC] THEN SET_TAC[]);;
994 let DIFF_UNIONS = prove
995 (`!u s. u DIFF UNIONS s = u INTER INTERS {u DIFF t | t IN s}`,
996 REWRITE_TAC[INTERS_GSPEC] THEN SET_TAC[]);;
998 let DIFF_UNIONS_NONEMPTY = prove
999 (`!u s. ~(s = {}) ==> u DIFF UNIONS s = INTERS {u DIFF t | t IN s}`,
1000 REWRITE_TAC[INTERS_GSPEC] THEN SET_TAC[]);;
1002 let INTERS_OVER_UNIONS = prove
1003 (`!f:A->(B->bool)->bool s.
1004 INTERS { UNIONS(f x) | x IN s} =
1005 UNIONS { INTERS {g x | x IN s} |g| !x. x IN s ==> g x IN f x}`,
1006 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
1007 REWRITE_TAC[SIMPLE_IMAGE; INTERS_IMAGE; UNIONS_IMAGE; UNIONS_GSPEC] THEN
1008 REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN
1009 X_GEN_TAC `b:B` THEN REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
1012 (* ------------------------------------------------------------------------- *)
1013 (* Stronger form of induction is sometimes handy. *)
1014 (* ------------------------------------------------------------------------- *)
1016 let FINITE_INDUCT_STRONG = prove
1017 (`!P:(A->bool)->bool.
1018 P {} /\ (!x s. P s /\ ~(x IN s) /\ FINITE s ==> P(x INSERT s))
1019 ==> !s. FINITE s ==> P s`,
1020 GEN_TAC THEN STRIP_TAC THEN
1021 SUBGOAL_THEN `!s:A->bool. FINITE s ==> FINITE s /\ P s` MP_TAC THENL
1022 [ALL_TAC; MESON_TAC[]] THEN
1023 MATCH_MP_TAC FINITE_INDUCT THEN ASM_SIMP_TAC[FINITE_RULES] THEN
1024 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `x:A IN s` THENL
1025 [SUBGOAL_THEN `x:A INSERT s = s` (fun th -> ASM_REWRITE_TAC[th]) THEN
1026 UNDISCH_TAC `x:A IN s` THEN SET_TAC[];
1027 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);;
1029 (* ------------------------------------------------------------------------- *)
1030 (* Useful general properties of functions. *)
1031 (* ------------------------------------------------------------------------- *)
1033 let INJECTIVE_ON_ALT = prove
1034 (`!P f. (!x y. P x /\ P y /\ f x = f y ==> x = y) <=>
1035 (!x y. P x /\ P y ==> (f x = f y <=> x = y))`,
1038 let INJECTIVE_ALT = prove
1039 (`!f. (!x y. f x = f y ==> x = y) <=> (!x y. f x = f y <=> x = y)`,
1042 let SURJECTIVE_ON_RIGHT_INVERSE = prove
1043 (`!f t. (!y. y IN t ==> ?x. x IN s /\ (f(x) = y)) <=>
1044 (?g. !y. y IN t ==> g(y) IN s /\ (f(g(y)) = y))`,
1045 REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM]);;
1047 let INJECTIVE_ON_LEFT_INVERSE = prove
1048 (`!f s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)) <=>
1049 (?g. !x. x IN s ==> (g(f(x)) = x))`,
1051 `(!x. x IN s ==> (g(f(x)) = x)) <=>
1052 (!y x. x IN s /\ (y = f x) ==> (g y = x))` in
1053 REWRITE_TAC[lemma; GSYM SKOLEM_THM] THEN MESON_TAC[]);;
1055 let BIJECTIVE_ON_LEFT_RIGHT_INVERSE = prove
1057 (!x. x IN s ==> f(x) IN t)
1058 ==> ((!x y. x IN s /\ y IN s /\ f(x) = f(y) ==> x = y) /\
1059 (!y. y IN t ==> ?x. x IN s /\ f x = y) <=>
1060 ?g. (!y. y IN t ==> g(y) IN s) /\
1061 (!y. y IN t ==> (f(g(y)) = y)) /\
1062 (!x. x IN s ==> (g(f(x)) = x)))`,
1063 REPEAT GEN_TAC THEN DISCH_TAC THEN
1064 REWRITE_TAC[INJECTIVE_ON_LEFT_INVERSE; SURJECTIVE_ON_RIGHT_INVERSE] THEN
1065 REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN
1066 EQ_TAC THEN ASM_MESON_TAC[]);;
1068 let SURJECTIVE_RIGHT_INVERSE = prove
1069 (`(!y. ?x. f(x) = y) <=> (?g. !y. f(g(y)) = y)`,
1070 MESON_TAC[SURJECTIVE_ON_RIGHT_INVERSE; IN_UNIV]);;
1072 let INJECTIVE_LEFT_INVERSE = prove
1073 (`(!x y. (f x = f y) ==> (x = y)) <=> (?g. !x. g(f(x)) = x)`,
1074 let th = REWRITE_RULE[IN_UNIV]
1075 (ISPECL [`f:A->B`; `UNIV:A->bool`] INJECTIVE_ON_LEFT_INVERSE) in
1078 let BIJECTIVE_LEFT_RIGHT_INVERSE = prove
1080 (!x y. f(x) = f(y) ==> x = y) /\ (!y. ?x. f x = y) <=>
1081 ?g. (!y. f(g(y)) = y) /\ (!x. g(f(x)) = x)`,
1083 MP_TAC(ISPECL [`f:A->B`; `(:A)`; `(:B)`] BIJECTIVE_ON_LEFT_RIGHT_INVERSE) THEN
1084 REWRITE_TAC[IN_UNIV]);;
1086 let FUNCTION_FACTORS_LEFT_GEN = prove
1087 (`!P f g. (!x y. P x /\ P y /\ g x = g y ==> f x = f y) <=>
1088 (?h. !x. P x ==> f(x) = h(g x))`,
1089 ONCE_REWRITE_TAC[MESON[]
1090 `(!x. P x ==> f(x) = g(k x)) <=> (!y x. P x /\ y = k x ==> f x = g y)`] THEN
1091 REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[]);;
1093 let FUNCTION_FACTORS_LEFT = prove
1094 (`!f g. (!x y. (g x = g y) ==> (f x = f y)) <=> ?h. f = h o g`,
1095 REWRITE_TAC[FUN_EQ_THM; o_THM;
1096 GSYM(REWRITE_RULE[] (ISPEC `\x. T` FUNCTION_FACTORS_LEFT_GEN))]);;
1098 let FUNCTION_FACTORS_RIGHT_GEN = prove
1099 (`!P f g. (!x. P x ==> ?y. g(y) = f(x)) <=>
1100 (?h. !x. P x ==> f(x) = g(h x))`,
1101 REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[]);;
1103 let FUNCTION_FACTORS_RIGHT = prove
1104 (`!f g. (!x. ?y. g(y) = f(x)) <=> ?h. f = g o h`,
1105 REWRITE_TAC[FUN_EQ_THM; o_THM; GSYM SKOLEM_THM] THEN MESON_TAC[]);;
1107 let SURJECTIVE_FORALL_THM = prove
1108 (`!f:A->B. (!y. ?x. f x = y) <=> (!P. (!x. P(f x)) <=> (!y. P y))`,
1109 GEN_TAC THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
1110 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN MESON_TAC[]);;
1112 let SURJECTIVE_EXISTS_THM = prove
1113 (`!f:A->B. (!y. ?x. f x = y) <=> (!P. (?x. P(f x)) <=> (?y. P y))`,
1114 GEN_TAC THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
1115 DISCH_THEN(MP_TAC o SPEC `\y:B. !x:A. ~(f x = y)`) THEN MESON_TAC[]);;
1117 let SURJECTIVE_IMAGE_THM = prove
1118 (`!f:A->B. (!y. ?x. f x = y) <=> (!P. IMAGE f {x | P(f x)} = {x | P x})`,
1119 GEN_TAC THEN REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
1120 EQ_TAC THENL [ALL_TAC; DISCH_THEN(MP_TAC o SPEC `\y:B. T`)] THEN
1123 let IMAGE_INJECTIVE_IMAGE_OF_SUBSET = prove
1126 IMAGE f s = IMAGE f t /\
1127 (!x y. x IN t /\ y IN t /\ f x = f y ==> x = y)`,
1130 `?g. !y. y IN IMAGE (f:A->B) s ==> g(y) IN s /\ f(g(y)) = y`
1131 STRIP_ASSUME_TAC THENL
1132 [REWRITE_TAC[GSYM SURJECTIVE_ON_RIGHT_INVERSE] THEN SET_TAC[];
1133 EXISTS_TAC `IMAGE (g:B->A) (IMAGE (f:A->B) s)` THEN ASM SET_TAC[]]);;
1135 (* ------------------------------------------------------------------------- *)
1136 (* Basic combining theorems for finite sets. *)
1137 (* ------------------------------------------------------------------------- *)
1139 let FINITE_EMPTY = prove
1141 REWRITE_TAC[FINITE_RULES]);;
1143 let FINITE_SUBSET = prove
1144 (`!(s:A->bool) t. FINITE t /\ s SUBSET t ==> FINITE s`,
1145 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1146 REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1147 MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
1148 [MESON_TAC[SUBSET_EMPTY; FINITE_RULES]; ALL_TAC] THEN
1149 X_GEN_TAC `x:A` THEN X_GEN_TAC `u:A->bool` THEN DISCH_TAC THEN
1150 X_GEN_TAC `t:A->bool` THEN DISCH_TAC THEN
1151 SUBGOAL_THEN `FINITE((x:A) INSERT (t DELETE x))` ASSUME_TAC THENL
1152 [MATCH_MP_TAC(CONJUNCT2 FINITE_RULES) THEN
1153 FIRST_ASSUM MATCH_MP_TAC THEN
1154 UNDISCH_TAC `t SUBSET (x:A INSERT u)` THEN SET_TAC[];
1155 ASM_CASES_TAC `x:A IN t` THENL
1156 [SUBGOAL_THEN `x:A INSERT (t DELETE x) = t` SUBST_ALL_TAC THENL
1157 [UNDISCH_TAC `x:A IN t` THEN SET_TAC[]; ASM_REWRITE_TAC[]];
1158 FIRST_ASSUM MATCH_MP_TAC THEN
1159 UNDISCH_TAC `t SUBSET x:A INSERT u` THEN
1160 UNDISCH_TAC `~(x:A IN t)` THEN SET_TAC[]]]);;
1162 let FINITE_RESTRICT = prove
1163 (`!s:A->bool P. FINITE s ==> FINITE {x | x IN s /\ P x}`,
1164 MESON_TAC[SUBSET_RESTRICT; FINITE_SUBSET]);;
1166 let FINITE_UNION_IMP = prove
1167 (`!(s:A->bool) t. FINITE s /\ FINITE t ==> FINITE (s UNION t)`,
1168 REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1169 MATCH_MP_TAC FINITE_INDUCT THEN REWRITE_TAC[UNION_EMPTY] THEN
1170 SUBGOAL_THEN `!x s t. (x:A INSERT s) UNION t = x INSERT (s UNION t)`
1171 (fun th -> REWRITE_TAC[th]) THENL
1173 MESON_TAC[FINITE_RULES]]);;
1175 let FINITE_UNION = prove
1176 (`!(s:A->bool) t. FINITE(s UNION t) <=> FINITE(s) /\ FINITE(t)`,
1177 REPEAT GEN_TAC THEN EQ_TAC THENL
1178 [REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
1179 EXISTS_TAC `(s:A->bool) UNION t` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
1180 MATCH_ACCEPT_TAC FINITE_UNION_IMP]);;
1182 let FINITE_INTER = prove
1183 (`!(s:A->bool) t. FINITE s \/ FINITE t ==> FINITE (s INTER t)`,
1184 MESON_TAC[INTER_SUBSET; FINITE_SUBSET]);;
1186 let FINITE_INSERT = prove
1187 (`!(s:A->bool) x. FINITE (x INSERT s) <=> FINITE s`,
1188 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
1189 [MATCH_MP_TAC FINITE_SUBSET THEN
1190 EXISTS_TAC `x:A INSERT s` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
1191 MATCH_MP_TAC(CONJUNCT2 FINITE_RULES) THEN
1192 ASM_REWRITE_TAC[]]);;
1194 let FINITE_SING = prove
1196 REWRITE_TAC[FINITE_INSERT; FINITE_RULES]);;
1198 let FINITE_DELETE_IMP = prove
1199 (`!(s:A->bool) x. FINITE s ==> FINITE (s DELETE x)`,
1200 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
1201 ASM_REWRITE_TAC[] THEN ASM SET_TAC[]);;
1203 let FINITE_DELETE = prove
1204 (`!(s:A->bool) x. FINITE (s DELETE x) <=> FINITE s`,
1205 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[FINITE_DELETE_IMP] THEN
1206 ASM_CASES_TAC `x:A IN s` THENL
1207 [SUBGOAL_THEN `s = x INSERT (s DELETE x:A)`
1208 (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THEN
1209 REWRITE_TAC[FINITE_INSERT] THEN POP_ASSUM MP_TAC THEN SET_TAC[];
1210 SUBGOAL_THEN `s DELETE x:A = s` (fun th -> REWRITE_TAC[th]) THEN
1211 POP_ASSUM MP_TAC THEN SET_TAC[]]);;
1213 let FINITE_FINITE_UNIONS = prove
1214 (`!s. FINITE(s) ==> (FINITE(UNIONS s) <=> (!t. t IN s ==> FINITE(t)))`,
1215 MATCH_MP_TAC FINITE_INDUCT THEN
1216 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; UNIONS_0; UNIONS_INSERT] THEN
1217 REWRITE_TAC[FINITE_UNION; FINITE_RULES] THEN MESON_TAC[]);;
1219 let FINITE_IMAGE_EXPAND = prove
1220 (`!(f:A->B) s. FINITE s ==> FINITE {y | ?x. x IN s /\ (y = f x)}`,
1221 GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT THEN
1222 REWRITE_TAC[NOT_IN_EMPTY; REWRITE_RULE[] EMPTY_GSPEC; FINITE_RULES] THEN
1224 SUBGOAL_THEN `{y | ?z. z IN (x INSERT s) /\ (y = (f:A->B) z)} =
1225 {y | ?z. z IN s /\ (y = f z)} UNION {(f x)}`
1226 (fun th -> REWRITE_TAC[th]) THENL
1227 [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; IN_UNION; NOT_IN_EMPTY] THEN
1229 REWRITE_TAC[FINITE_UNION; FINITE_INSERT; FINITE_RULES]]);;
1231 let FINITE_IMAGE = prove
1232 (`!(f:A->B) s. FINITE s ==> FINITE (IMAGE f s)`,
1233 REWRITE_TAC[IMAGE; FINITE_IMAGE_EXPAND]);;
1235 let FINITE_IMAGE_INJ_GENERAL = prove
1237 (!x y. x IN s /\ y IN s /\ f(x) = f(y) ==> x = y) /\
1239 ==> FINITE {x | x IN s /\ f(x) IN A}`,
1240 REPEAT STRIP_TAC THEN
1241 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
1242 DISCH_THEN(X_CHOOSE_TAC `g:B->A`) THEN
1243 MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `IMAGE (g:B->A) A` THEN
1244 ASM_SIMP_TAC[FINITE_IMAGE] THEN ASM SET_TAC[]);;
1246 let FINITE_FINITE_PREIMAGE_GENERAL = prove
1249 (!y. y IN t ==> FINITE {x | x IN s /\ f(x) = y})
1250 ==> FINITE {x | x IN s /\ f(x) IN t}`,
1251 REPEAT STRIP_TAC THEN
1253 `{x | x IN s /\ (f:A->B)(x) IN t} =
1254 UNIONS (IMAGE (\a. {x | x IN s /\ f x = a}) t)`
1256 [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM; IN_UNIONS] THEN
1257 REWRITE_TAC[EXISTS_IN_IMAGE] THEN SET_TAC[];
1258 ASM_SIMP_TAC[FINITE_FINITE_UNIONS; FINITE_IMAGE; FORALL_IN_IMAGE]]);;
1260 let FINITE_FINITE_PREIMAGE = prove
1263 (!y. y IN t ==> FINITE {x | f(x) = y})
1264 ==> FINITE {x | f(x) IN t}`,
1265 REPEAT GEN_TAC THEN MP_TAC
1266 (ISPECL [`f:A->B`; `(:A)`; `t:B->bool`] FINITE_FINITE_PREIMAGE_GENERAL) THEN
1267 REWRITE_TAC[IN_UNIV]);;
1269 let FINITE_IMAGE_INJ_EQ = prove
1270 (`!(f:A->B) s. (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y))
1271 ==> (FINITE(IMAGE f s) <=> FINITE s)`,
1272 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[FINITE_IMAGE] THEN
1273 POP_ASSUM MP_TAC THEN REWRITE_TAC[IMP_IMP] THEN
1274 DISCH_THEN(MP_TAC o MATCH_MP FINITE_IMAGE_INJ_GENERAL) THEN
1275 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN SET_TAC[]);;
1277 let FINITE_IMAGE_INJ = prove
1278 (`!(f:A->B) A. (!x y. (f(x) = f(y)) ==> (x = y)) /\
1279 FINITE A ==> FINITE {x | f(x) IN A}`,
1281 MP_TAC(SPECL [`f:A->B`; `A:B->bool`; `UNIV:A->bool`]
1282 FINITE_IMAGE_INJ_GENERAL) THEN REWRITE_TAC[IN_UNIV]);;
1284 let INFINITE_IMAGE_INJ = prove
1285 (`!f:A->B. (!x y. (f x = f y) ==> (x = y))
1286 ==> !s. INFINITE s ==> INFINITE(IMAGE f s)`,
1287 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
1288 REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN DISCH_TAC THEN
1289 MATCH_MP_TAC FINITE_SUBSET THEN
1290 EXISTS_TAC `{x | f(x) IN IMAGE (f:A->B) s}` THEN CONJ_TAC THENL
1291 [MATCH_MP_TAC FINITE_IMAGE_INJ THEN ASM_REWRITE_TAC[];
1292 REWRITE_TAC[SUBSET; IN_ELIM_THM; IMAGE] THEN MESON_TAC[]]);;
1294 let INFINITE_NONEMPTY = prove
1295 (`!s. INFINITE(s) ==> ~(s = EMPTY)`,
1296 MESON_TAC[INFINITE; FINITE_RULES]);;
1298 let INFINITE_DIFF_FINITE = prove
1299 (`!s:A->bool t. INFINITE(s) /\ FINITE(t) ==> INFINITE(s DIFF t)`,
1301 MATCH_MP_TAC(TAUT `(b /\ ~c ==> ~a) ==> a /\ b ==> c`) THEN
1302 REWRITE_TAC[INFINITE] THEN STRIP_TAC THEN
1303 MATCH_MP_TAC FINITE_SUBSET THEN
1304 EXISTS_TAC `(t:A->bool) UNION (s DIFF t)` THEN
1305 ASM_REWRITE_TAC[FINITE_UNION] THEN SET_TAC[]);;
1307 let FINITE_SUBSET_IMAGE = prove
1309 FINITE(t) /\ t SUBSET (IMAGE f s) <=>
1310 ?s'. FINITE s' /\ s' SUBSET s /\ (t = IMAGE f s')`,
1311 REPEAT GEN_TAC THEN EQ_TAC THENL
1312 [ALL_TAC; ASM_MESON_TAC[FINITE_IMAGE; IMAGE_SUBSET]] THEN
1314 EXISTS_TAC `IMAGE (\y. @x. x IN s /\ ((f:A->B)(x) = y)) t` THEN
1315 ASM_SIMP_TAC[FINITE_IMAGE] THEN
1316 REWRITE_TAC[EXTENSION; SUBSET; FORALL_IN_IMAGE] THEN CONJ_TAC THENL
1317 [ASM_MESON_TAC[SUBSET; IN_IMAGE]; ALL_TAC] THEN
1318 REWRITE_TAC[IN_IMAGE] THEN X_GEN_TAC `y:B` THEN
1319 REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
1320 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
1321 REWRITE_TAC[UNWIND_THM2; GSYM CONJ_ASSOC] THEN
1322 ASM_MESON_TAC[SUBSET; IN_IMAGE]);;
1324 let EXISTS_FINITE_SUBSET_IMAGE = prove
1326 (?t. FINITE t /\ t SUBSET IMAGE f s /\ P t) <=>
1327 (?t. FINITE t /\ t SUBSET s /\ P (IMAGE f t))`,
1328 REWRITE_TAC[FINITE_SUBSET_IMAGE; CONJ_ASSOC] THEN MESON_TAC[]);;
1330 let FORALL_FINITE_SUBSET_IMAGE = prove
1331 (`!P f s. (!t. FINITE t /\ t SUBSET IMAGE f s ==> P t) <=>
1332 (!t. FINITE t /\ t SUBSET s ==> P(IMAGE f t))`,
1334 ONCE_REWRITE_TAC[MESON[] `(!x. P x) <=> ~(?x. ~P x)`] THEN
1335 REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; EXISTS_FINITE_SUBSET_IMAGE]);;
1337 let FINITE_SUBSET_IMAGE_IMP = prove
1339 FINITE(t) /\ t SUBSET (IMAGE f s)
1340 ==> ?s'. FINITE s' /\ s' SUBSET s /\ t SUBSET (IMAGE f s')`,
1341 MESON_TAC[SUBSET_REFL; FINITE_SUBSET_IMAGE]);;
1343 let FINITE_DIFF = prove
1344 (`!s t. FINITE s ==> FINITE(s DIFF t)`,
1345 MESON_TAC[FINITE_SUBSET; SUBSET_DIFF]);;
1347 let INFINITE_SUPERSET = prove
1348 (`!s t. INFINITE s /\ s SUBSET t ==> INFINITE t`,
1349 REWRITE_TAC[INFINITE] THEN MESON_TAC[FINITE_SUBSET]);;
1351 let FINITE_TRANSITIVITY_CHAIN = prove
1355 (!x y z. R x y /\ R y z ==> R x z) /\
1356 (!x. x IN s ==> ?y. y IN s /\ R x y)
1358 GEN_TAC THEN ONCE_REWRITE_TAC[IMP_CONJ] THEN
1359 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[NOT_IN_EMPTY] THEN
1362 let UNIONS_MAXIMAL_SETS = prove
1364 ==> UNIONS {t:A->bool | t IN f /\ !u. u IN f ==> ~(t PSUBSET u)} =
1366 SIMP_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET_UNIONS; SUBSET_RESTRICT] THEN
1367 REPEAT STRIP_TAC THEN MATCH_MP_TAC UNIONS_MONO THEN
1368 X_GEN_TAC `s:A->bool` THEN DISCH_TAC THEN REWRITE_TAC[EXISTS_IN_GSPEC] THEN
1369 GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN DISCH_TAC THEN
1370 MP_TAC(ISPECL [`\t u:A->bool. s SUBSET t /\ t PSUBSET u`;
1371 `{t:A->bool | t IN f /\ s SUBSET t}`]FINITE_TRANSITIVITY_CHAIN) THEN
1372 ASM_SIMP_TAC[NOT_IMP; FINITE_RESTRICT; FORALL_IN_GSPEC; EXISTS_IN_GSPEC] THEN
1373 REPEAT CONJ_TAC THENL [SET_TAC[]; SET_TAC[]; ALL_TAC; ASM SET_TAC[]] THEN
1374 ASM_MESON_TAC[PSUBSET_TRANS; SUBSET_PSUBSET_TRANS; PSUBSET]);;
1376 (* ------------------------------------------------------------------------- *)
1377 (* Recursion over finite sets; based on Ching-Tsun's code (archive 713). *)
1378 (* ------------------------------------------------------------------------- *)
1380 let FINREC = new_recursive_definition num_RECURSION
1381 `(FINREC (f:A->B->B) b s a 0 <=> (s = {}) /\ (a = b)) /\
1382 (FINREC (f:A->B->B) b s a (SUC n) <=>
1384 FINREC f b (s DELETE x) c n /\
1387 let FINREC_1_LEMMA = prove
1388 (`!f b s a. FINREC f b s a (SUC 0) <=> ?x. (s = {x}) /\ (a = f x b)`,
1389 REWRITE_TAC[FINREC] THEN
1390 REPEAT GEN_TAC THEN AP_TERM_TAC THEN ABS_TAC THEN SET_TAC[]);;
1392 let FINREC_SUC_LEMMA = prove
1394 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
1396 FINREC f b s z (SUC n)
1397 ==> !x. x IN s ==> ?w. FINREC f b (s DELETE x) w n /\
1399 let lem = prove(`s DELETE (x:A) DELETE y = s DELETE y DELETE x`,SET_TAC[]) in
1400 REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
1401 [REWRITE_TAC[FINREC_1_LEMMA] THEN REWRITE_TAC[FINREC] THEN
1402 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
1403 ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
1404 DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `b:B` THEN
1405 ASM_REWRITE_TAC[] THEN SET_TAC[];
1407 GEN_REWRITE_TAC LAND_CONV [FINREC] THEN
1408 DISCH_THEN(X_CHOOSE_THEN `y:A` MP_TAC) THEN
1409 DISCH_THEN(X_CHOOSE_THEN `c:B` STRIP_ASSUME_TAC) THEN
1410 X_GEN_TAC `x:A` THEN DISCH_TAC THEN
1411 ASM_CASES_TAC `x:A = y` THEN ASM_REWRITE_TAC[] THENL
1412 [EXISTS_TAC `c:B` THEN ASM_REWRITE_TAC[];
1413 UNDISCH_TAC `FINREC (f:A->B->B) b (s DELETE y) c (SUC n)` THEN
1414 DISCH_THEN(ANTE_RES_THEN (MP_TAC o SPEC `x:A`)) THEN
1415 ASM_REWRITE_TAC[IN_DELETE] THEN
1416 DISCH_THEN(X_CHOOSE_THEN `v:B` STRIP_ASSUME_TAC) THEN
1417 EXISTS_TAC `(f:A->B->B) y v` THEN ASM_REWRITE_TAC[FINREC] THEN
1419 [MAP_EVERY EXISTS_TAC [`y:A`; `v:B`] THEN
1420 ONCE_REWRITE_TAC[lem] THEN ASM_REWRITE_TAC[IN_DELETE];
1421 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]]]);;
1423 let FINREC_UNIQUE_LEMMA = prove
1425 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
1427 FINREC f b s a1 n1 /\ FINREC f b s a2 n2
1428 ==> (a1 = a2) /\ (n1 = n2)`,
1429 REPEAT GEN_TAC THEN DISCH_TAC THEN
1430 INDUCT_TAC THEN INDUCT_TAC THENL
1431 [REWRITE_TAC[FINREC] THEN MESON_TAC[NOT_IN_EMPTY];
1432 REWRITE_TAC[FINREC] THEN MESON_TAC[NOT_IN_EMPTY];
1433 REWRITE_TAC[FINREC] THEN MESON_TAC[NOT_IN_EMPTY];
1434 IMP_RES_THEN ASSUME_TAC FINREC_SUC_LEMMA THEN REPEAT GEN_TAC THEN
1435 DISCH_THEN(fun th -> MP_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN
1436 DISCH_THEN(CONJUNCTS_THEN (ANTE_RES_THEN ASSUME_TAC)) THEN
1437 REWRITE_TAC[FINREC] THEN STRIP_TAC THEN ASM_MESON_TAC[]]);;
1439 let FINREC_EXISTS_LEMMA = prove
1440 (`!(f:A->B->B) b s. FINITE s ==> ?a n. FINREC f b s a n`,
1441 let lem = prove(`~(x IN s ) ==> ((x:A INSERT s) DELETE x = s)`,SET_TAC[]) in
1442 GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1443 REPEAT STRIP_TAC THENL
1444 [MAP_EVERY EXISTS_TAC [`b:B`; `0`] THEN REWRITE_TAC[FINREC];
1445 MAP_EVERY EXISTS_TAC [`(f:A->B->B) x a`; `SUC n`] THEN
1446 REWRITE_TAC[FINREC] THEN MAP_EVERY EXISTS_TAC [`x:A`; `a:B`] THEN
1447 FIRST_ASSUM(fun th -> ASM_REWRITE_TAC[MATCH_MP lem th; IN_INSERT])]);;
1449 let FINREC_FUN_LEMMA = prove
1450 (`!P (R:A->B->C->bool).
1451 (!s. P s ==> ?a n. R s a n) /\
1452 (!n1 n2 s a1 a2. R s a1 n1 /\ R s a2 n2 ==> (a1 = a2) /\ (n1 = n2))
1453 ==> ?f. !s a. P s ==> ((?n. R s a n) <=> (f s = a))`,
1454 REPEAT STRIP_TAC THEN EXISTS_TAC `\s:A. @a:B. ?n:C. R s a n` THEN
1455 REPEAT STRIP_TAC THEN BETA_TAC THEN EQ_TAC THENL
1456 [STRIP_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN ASM_MESON_TAC[];
1457 DISCH_THEN(SUBST1_TAC o SYM) THEN CONV_TAC SELECT_CONV THEN
1460 let FINREC_FUN = prove
1462 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
1463 ==> ?g. (g {} = b) /\
1464 !s x. FINITE s /\ x IN s
1465 ==> (g s = f x (g (s DELETE x)))`,
1466 REPEAT STRIP_TAC THEN IMP_RES_THEN MP_TAC FINREC_UNIQUE_LEMMA THEN
1467 DISCH_THEN(MP_TAC o SPEC `b:B`) THEN DISCH_THEN
1468 (MP_TAC o CONJ (SPECL [`f:A->B->B`; `b:B`] FINREC_EXISTS_LEMMA)) THEN
1469 DISCH_THEN(MP_TAC o MATCH_MP FINREC_FUN_LEMMA) THEN
1470 DISCH_THEN(X_CHOOSE_TAC `g:(A->bool)->B`) THEN
1471 EXISTS_TAC `g:(A->bool)->B` THEN CONJ_TAC THENL
1472 [SUBGOAL_THEN `FINITE(EMPTY:A->bool)`
1473 (ANTE_RES_THEN (fun th -> GEN_REWRITE_TAC I [GSYM th])) THENL
1474 [REWRITE_TAC[FINITE_RULES];
1475 EXISTS_TAC `0` THEN REWRITE_TAC[FINREC]];
1476 REPEAT STRIP_TAC THEN
1477 ANTE_RES_THEN MP_TAC (ASSUME `FINITE(s:A->bool)`) THEN
1478 DISCH_THEN(ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC[] THEN
1479 FIRST_ASSUM(MP_TAC o SPEC `(g:(A->bool)->B) s`) THEN
1480 REWRITE_TAC[] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
1482 [ASM_REWRITE_TAC[FINREC] THEN DISCH_TAC THEN UNDISCH_TAC `x:A IN s` THEN
1483 ASM_REWRITE_TAC[NOT_IN_EMPTY];
1484 IMP_RES_THEN ASSUME_TAC FINREC_SUC_LEMMA THEN
1485 DISCH_THEN(ANTE_RES_THEN (MP_TAC o SPEC `x:A`)) THEN
1486 ASM_REWRITE_TAC[] THEN
1487 DISCH_THEN(X_CHOOSE_THEN `w:B` (CONJUNCTS_THEN ASSUME_TAC)) THEN
1488 SUBGOAL_THEN `(g (s DELETE x:A) = w:B)` SUBST1_TAC THENL
1489 [SUBGOAL_THEN `FINITE(s DELETE x:A)` MP_TAC THENL
1490 [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:A->bool` THEN
1491 ASM_REWRITE_TAC[] THEN SET_TAC[];
1492 DISCH_THEN(ANTE_RES_THEN (MP_TAC o GSYM)) THEN
1493 DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
1494 EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[]];
1495 ASM_REWRITE_TAC[]]]]);;
1497 let SET_RECURSION_LEMMA = prove
1499 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
1500 ==> ?g. (g {} = b) /\
1502 ==> (g (x INSERT s) =
1503 if x IN s then g s else f x (g s))`,
1505 DISCH_THEN(MP_TAC o SPEC `b:B` o MATCH_MP FINREC_FUN) THEN
1506 DISCH_THEN(X_CHOOSE_THEN `g:(A->bool)->B` STRIP_ASSUME_TAC) THEN
1507 EXISTS_TAC `g:(A->bool)->B` THEN ASM_REWRITE_TAC[] THEN
1508 REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1510 [AP_TERM_TAC THEN REWRITE_TAC[GSYM ABSORPTION] THEN ASM_REWRITE_TAC[];
1511 SUBGOAL_THEN `FINITE(x:A INSERT s) /\ x IN (x INSERT s)` MP_TAC THENL
1512 [REWRITE_TAC[IN_INSERT] THEN ASM_MESON_TAC[FINITE_RULES];
1513 DISCH_THEN(ANTE_RES_THEN SUBST1_TAC) THEN
1514 REPEAT AP_TERM_TAC THEN UNDISCH_TAC `~(x:A IN s)` THEN SET_TAC[]]]);;
1516 let ITSET = new_definition
1520 ==> (g (x INSERT s) = if x IN s then g s else f x (g s)))
1523 let FINITE_RECURSION = prove
1525 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
1526 ==> (ITSET f {} b = b) /\
1528 ==> (ITSET f (x INSERT s) b =
1529 if x IN s then ITSET f s b
1530 else f x (ITSET f s b))`,
1531 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[ITSET] THEN
1532 CONV_TAC SELECT_CONV THEN MATCH_MP_TAC SET_RECURSION_LEMMA THEN
1533 ASM_REWRITE_TAC[]);;
1535 let FINITE_RECURSION_DELETE = prove
1537 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
1538 ==> (ITSET f {} b = b) /\
1541 if x IN s then f x (ITSET f (s DELETE x) b)
1542 else ITSET f (s DELETE x) b)`,
1543 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP FINITE_RECURSION) THEN
1544 DISCH_THEN(STRIP_ASSUME_TAC o SPEC `b:B`) THEN ASM_REWRITE_TAC[] THEN
1545 REPEAT GEN_TAC THEN ASM_CASES_TAC `x:A IN s` THEN ASM_REWRITE_TAC[] THENL
1546 [DISCH_THEN(MP_TAC o MATCH_MP FINITE_DELETE_IMP) THEN
1547 DISCH_THEN(ANTE_RES_THEN MP_TAC o SPEC `x:A`) THEN
1548 DISCH_THEN(MP_TAC o SPEC `x:A`) THEN
1549 REWRITE_TAC[IN_DELETE] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
1550 AP_THM_TAC THEN AP_TERM_TAC THEN UNDISCH_TAC `x:A IN s` THEN SET_TAC[];
1551 DISCH_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1552 UNDISCH_TAC `~(x:A IN s)` THEN SET_TAC[]]);;
1554 let ITSET_EQ = prove
1555 (`!s f g b. FINITE(s) /\ (!x. x IN s ==> (f x = g x)) /\
1556 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s))) /\
1557 (!x y s. ~(x = y) ==> (g x (g y s) = g y (g x s)))
1558 ==> (ITSET f s b = ITSET g s b)`,
1559 ONCE_REWRITE_TAC[IMP_CONJ] THEN
1560 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1561 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1562 SIMP_TAC[FINITE_RECURSION; NOT_IN_EMPTY; IN_INSERT] THEN
1563 REPEAT STRIP_TAC THEN AP_TERM_TAC THEN
1564 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[RIGHT_IMP_FORALL_THM]) THEN
1567 (* ------------------------------------------------------------------------- *)
1569 (* ------------------------------------------------------------------------- *)
1571 let CARD = new_definition
1572 `CARD s = ITSET (\x n. SUC n) s 0`;;
1574 let CARD_CLAUSES = prove
1575 (`(CARD ({}:A->bool) = 0) /\
1576 (!(x:A) s. FINITE s ==>
1577 (CARD (x INSERT s) =
1578 if x IN s then CARD s else SUC(CARD s)))`,
1579 MP_TAC(ISPECL [`\(x:A) n. SUC n`; `0`] FINITE_RECURSION) THEN
1580 REWRITE_TAC[CARD]);;
1582 let CARD_UNION = prove
1583 (`!(s:A->bool) t. FINITE(s) /\ FINITE(t) /\ (s INTER t = EMPTY)
1584 ==> (CARD (s UNION t) = CARD s + CARD t)`,
1585 REWRITE_TAC[TAUT `a /\ b /\ c ==> d <=> a ==> b /\ c ==> d`] THEN
1586 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1587 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1588 REWRITE_TAC[UNION_EMPTY; CARD_CLAUSES; INTER_EMPTY; ADD_CLAUSES] THEN
1589 X_GEN_TAC `x:A` THEN X_GEN_TAC `s:A->bool` THEN REPEAT STRIP_TAC THEN
1590 SUBGOAL_THEN `(x:A INSERT s) UNION t = x INSERT (s UNION t)`
1591 SUBST1_TAC THENL [SET_TAC[]; ALL_TAC] THEN
1592 SUBGOAL_THEN `FINITE ((s:A->bool) UNION t) /\ FINITE s`
1593 STRIP_ASSUME_TAC THENL
1594 [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FINITE_UNION_IMP THEN
1595 ASM_REWRITE_TAC[]; ALL_TAC] THEN
1596 MP_TAC(ISPECL [`x:A`; `s:A->bool`] (CONJUNCT2 CARD_CLAUSES)) THEN
1597 MP_TAC(ISPECL [`x:A`; `s:A->bool UNION t`] (CONJUNCT2 CARD_CLAUSES)) THEN
1598 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1599 SUBGOAL_THEN `~(x:A IN (s UNION t))` ASSUME_TAC THENL
1600 [ASM_REWRITE_TAC[IN_UNION] THEN
1601 UNDISCH_TAC `(x:A INSERT s) INTER t = EMPTY` THEN
1602 REWRITE_TAC[EXTENSION; IN_INSERT; IN_INTER; NOT_IN_EMPTY] THEN
1604 ASM_REWRITE_TAC[SUC_INJ; ADD_CLAUSES] THEN
1605 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1606 UNDISCH_TAC `x:A INSERT s INTER t = EMPTY` THEN SET_TAC[]]);;
1608 let CARD_DELETE = prove
1610 ==> (CARD(s DELETE x) = if x IN s then CARD(s) - 1 else CARD(s))`,
1611 REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
1612 [SUBGOAL_THEN `s = x:A INSERT (s DELETE x)`
1613 (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th])
1614 THENL [UNDISCH_TAC `x:A IN s` THEN SET_TAC[]; ALL_TAC] THEN
1615 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; IN_DELETE; SUC_SUB1];
1616 AP_TERM_TAC THEN UNDISCH_TAC `~(x:A IN s)` THEN SET_TAC[]]);;
1618 let CARD_UNION_EQ = prove
1619 (`!s t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
1620 ==> (CARD s + CARD t = CARD u)`,
1621 MESON_TAC[CARD_UNION; FINITE_SUBSET; SUBSET_UNION]);;
1623 let CARD_DIFF = prove
1624 (`!s t. FINITE s /\ t SUBSET s ==> CARD(s DIFF t) = CARD s - CARD t`,
1625 REPEAT STRIP_TAC THEN
1626 MATCH_MP_TAC(ARITH_RULE `a + b:num = c ==> a = c - b`) THEN
1627 MATCH_MP_TAC CARD_UNION_EQ THEN ASM_SIMP_TAC[] THEN ASM SET_TAC[]);;
1629 let CARD_EQ_0 = prove
1630 (`!s. FINITE s ==> ((CARD s = 0) <=> (s = {}))`,
1631 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1632 SIMP_TAC[CARD_CLAUSES; NOT_INSERT_EMPTY; NOT_SUC]);;
1634 let CARD_SING = prove
1635 (`!a:A. CARD {a} = 1`,
1636 SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; NOT_IN_EMPTY; ARITH]);;
1638 (* ------------------------------------------------------------------------- *)
1639 (* A stronger still form of induction where we get to choose the element. *)
1640 (* ------------------------------------------------------------------------- *)
1642 let FINITE_INDUCT_DELETE = prove
1644 (!s. FINITE s /\ ~(s = {}) ==> ?x. x IN s /\ (P(s DELETE x) ==> P s))
1645 ==> !s:A->bool. FINITE s ==> P s`,
1646 GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `CARD(s:A->bool)` THEN
1647 ASM_CASES_TAC `s:A->bool = {}` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1649 `!s. FINITE s /\ ~(s = {}) ==> ?x:A. x IN s /\ (P(s DELETE x) ==> P s)` THEN
1650 DISCH_THEN(MP_TAC o SPEC `s:A->bool`) THEN ASM_REWRITE_TAC[] THEN
1651 DISCH_THEN(X_CHOOSE_THEN `x:A` (CONJUNCTS_THEN2 ASSUME_TAC MATCH_MP_TAC)) THEN
1652 FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (x:A)`) THEN
1653 ASM_SIMP_TAC[FINITE_DELETE; CARD_DELETE; CARD_EQ_0;
1654 ARITH_RULE `n - 1 < n <=> ~(n = 0)`]);;
1656 (* ------------------------------------------------------------------------- *)
1657 (* Relational form is often more useful. *)
1658 (* ------------------------------------------------------------------------- *)
1660 let HAS_SIZE = new_definition
1661 `s HAS_SIZE n <=> FINITE s /\ (CARD s = n)`;;
1663 let HAS_SIZE_CARD = prove
1664 (`!s n. s HAS_SIZE n ==> (CARD s = n)`,
1665 SIMP_TAC[HAS_SIZE]);;
1667 let HAS_SIZE_0 = prove
1668 (`!(s:A->bool). s HAS_SIZE 0 <=> (s = {})`,
1669 REPEAT GEN_TAC THEN REWRITE_TAC[HAS_SIZE] THEN
1670 EQ_TAC THEN DISCH_TAC THEN
1671 ASM_REWRITE_TAC[FINITE_RULES; CARD_CLAUSES] THEN
1672 FIRST_ASSUM(MP_TAC o CONJUNCT2) THEN
1673 FIRST_ASSUM(MP_TAC o CONJUNCT1) THEN
1674 SPEC_TAC(`s:A->bool`,`s:A->bool`) THEN
1675 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1676 REWRITE_TAC[NOT_INSERT_EMPTY] THEN
1677 REPEAT GEN_TAC THEN STRIP_TAC THEN
1678 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP (CONJUNCT2 CARD_CLAUSES) th]) THEN
1679 ASM_REWRITE_TAC[NOT_SUC]);;
1681 let HAS_SIZE_SUC = prove
1682 (`!(s:A->bool) n. s HAS_SIZE (SUC n) <=>
1683 ~(s = {}) /\ !a. a IN s ==> (s DELETE a) HAS_SIZE n`,
1684 REPEAT GEN_TAC THEN REWRITE_TAC[HAS_SIZE] THEN
1685 ASM_CASES_TAC `s:A->bool = {}` THEN
1686 ASM_REWRITE_TAC[CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; NOT_SUC] THEN
1687 REWRITE_TAC[FINITE_DELETE] THEN
1688 ASM_CASES_TAC `FINITE(s:A->bool)` THEN
1689 ASM_REWRITE_TAC[NOT_FORALL_THM; MEMBER_NOT_EMPTY] THEN
1690 EQ_TAC THEN REPEAT STRIP_TAC THENL
1691 [MP_TAC(ISPECL [`a:A`; `s DELETE a:A`] (CONJUNCT2 CARD_CLAUSES)) THEN
1692 ASM_REWRITE_TAC[FINITE_DELETE; IN_DELETE] THEN
1693 SUBGOAL_THEN `a INSERT (s DELETE a:A) = s` SUBST1_TAC THENL
1694 [UNDISCH_TAC `a:A IN s` THEN SET_TAC[];
1695 ASM_REWRITE_TAC[SUC_INJ] THEN MESON_TAC[]];
1696 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
1697 DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
1698 MP_TAC(ISPECL [`a:A`; `s DELETE a:A`] (CONJUNCT2 CARD_CLAUSES)) THEN
1699 ASM_REWRITE_TAC[FINITE_DELETE; IN_DELETE] THEN
1700 SUBGOAL_THEN `a INSERT (s DELETE a:A) = s` SUBST1_TAC THENL
1701 [UNDISCH_TAC `a:A IN s` THEN SET_TAC[];
1702 ASM_MESON_TAC[]]]);;
1704 let HAS_SIZE_UNION = prove
1705 (`!s t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ DISJOINT s t
1706 ==> (s UNION t) HAS_SIZE (m + n)`,
1707 SIMP_TAC[HAS_SIZE; FINITE_UNION; DISJOINT; CARD_UNION]);;
1709 let HAS_SIZE_DIFF = prove
1710 (`!s t m n. s HAS_SIZE m /\ t HAS_SIZE n /\ t SUBSET s
1711 ==> (s DIFF t) HAS_SIZE (m - n)`,
1712 SIMP_TAC[HAS_SIZE; FINITE_DIFF; CARD_DIFF]);;
1714 let HAS_SIZE_UNIONS = prove
1715 (`!s t:A->B->bool m n.
1717 (!x. x IN s ==> t(x) HAS_SIZE n) /\
1718 (!x y. x IN s /\ y IN s /\ ~(x = y) ==> DISJOINT (t x) (t y))
1719 ==> UNIONS {t(x) | x IN s} HAS_SIZE (m * n)`,
1720 GEN_REWRITE_TAC (funpow 4 BINDER_CONV o funpow 2 LAND_CONV) [HAS_SIZE] THEN
1721 REWRITE_TAC[GSYM CONJ_ASSOC] THEN
1722 ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1723 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
1724 [REPEAT GEN_TAC THEN REWRITE_TAC[CARD_CLAUSES] THEN
1725 DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) (K ALL_TAC)) THEN
1726 REWRITE_TAC[MULT_CLAUSES; HAS_SIZE_0; EMPTY_UNIONS] THEN
1727 REWRITE_TAC[IN_ELIM_THM; NOT_IN_EMPTY];
1729 MAP_EVERY X_GEN_TAC [`x:A`; `s:A->bool`] THEN STRIP_TAC THEN
1730 MAP_EVERY X_GEN_TAC [`t:A->B->bool`; `m:num`; `n:num`] THEN
1731 ASM_SIMP_TAC[CARD_CLAUSES] THEN
1732 DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) STRIP_ASSUME_TAC) THEN
1733 REWRITE_TAC[SET_RULE
1734 `UNIONS {t y | y IN x INSERT s} = t x UNION UNIONS {t y | y IN s}`] THEN
1735 REWRITE_TAC[ARITH_RULE `SUC a * b = b + a * b`] THEN
1736 MATCH_MP_TAC HAS_SIZE_UNION THEN ASM_SIMP_TAC[IN_INSERT] THEN
1737 REWRITE_TAC[SET_RULE
1738 `DISJOINT a (UNIONS s) <=> !x. x IN s ==> DISJOINT a x`] THEN
1739 ASM_SIMP_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
1740 ASM_MESON_TAC[IN_INSERT]);;
1742 let FINITE_HAS_SIZE = prove
1743 (`!s. FINITE s <=> s HAS_SIZE CARD s`,
1744 REWRITE_TAC[HAS_SIZE]);;
1746 (* ------------------------------------------------------------------------- *)
1747 (* This is often more useful as a rewrite. *)
1748 (* ------------------------------------------------------------------------- *)
1750 let HAS_SIZE_CLAUSES = prove
1751 (`(s HAS_SIZE 0 <=> (s = {})) /\
1752 (s HAS_SIZE (SUC n) <=>
1753 ?a t. t HAS_SIZE n /\ ~(a IN t) /\ (s = a INSERT t))`,
1754 let lemma = SET_RULE `a IN s ==> (s = a INSERT (s DELETE a))` in
1755 REWRITE_TAC[HAS_SIZE_0] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL
1756 [REWRITE_TAC[HAS_SIZE_SUC; GSYM MEMBER_NOT_EMPTY] THEN
1757 MESON_TAC[lemma; IN_DELETE];
1758 SIMP_TAC[LEFT_IMP_EXISTS_THM; HAS_SIZE; CARD_CLAUSES; FINITE_INSERT]]);;
1760 (* ------------------------------------------------------------------------- *)
1761 (* Produce an explicit expansion for "s HAS_SIZE n" for numeral n. *)
1762 (* ------------------------------------------------------------------------- *)
1766 (`(~(a IN {}) /\ P <=> P) /\
1767 (~(a IN {b}) /\ P <=> ~(a = b) /\ P) /\
1768 (~(a IN (b INSERT cs)) /\ P <=> ~(a = b) /\ ~(a IN cs) /\ P)`,
1771 (`((?s. s HAS_SIZE 0 /\ P s) <=> P {}) /\
1772 ((?s. s HAS_SIZE (SUC n) /\ P s) <=>
1773 (?a s. s HAS_SIZE n /\ ~(a IN s) /\ P(a INSERT s)))`,
1774 REWRITE_TAC[HAS_SIZE_CLAUSES] THEN MESON_TAC[]) in
1775 let qconv_0 = GEN_REWRITE_CONV I [CONJUNCT1 qth]
1776 and qconv_1 = GEN_REWRITE_CONV I [CONJUNCT2 qth]
1777 and rconv_0 = GEN_REWRITE_CONV I [CONJUNCT1 pth]
1778 and rconv_1 = GEN_REWRITE_CONV I [CONJUNCT2 pth] in
1779 let rec EXISTS_HAS_SIZE_AND_CONV tm =
1781 (BINDER_CONV(LAND_CONV(RAND_CONV num_CONV)) THENC
1783 BINDER_CONV EXISTS_HAS_SIZE_AND_CONV)) tm in
1784 let rec NOT_IN_INSERT_CONV tm =
1785 ((rconv_0 THENC NOT_IN_INSERT_CONV) ORELSEC
1786 (rconv_1 THENC RAND_CONV NOT_IN_INSERT_CONV) ORELSEC
1789 GEN_REWRITE_CONV I [CONJUNCT1 HAS_SIZE_CLAUSES] ORELSEC
1790 (RAND_CONV num_CONV THENC
1791 GEN_REWRITE_CONV I [CONJUNCT2 HAS_SIZE_CLAUSES] THENC
1792 BINDER_CONV EXISTS_HAS_SIZE_AND_CONV) in
1794 let th = HAS_SIZE_CONV tm in
1795 let tm' = rand(concl th) in
1796 let evs,bod = strip_exists tm' in
1797 if evs = [] then th else
1798 let th' = funpow (length evs) BINDER_CONV NOT_IN_INSERT_CONV tm' in
1801 (* ------------------------------------------------------------------------- *)
1802 (* Various useful lemmas about cardinalities of unions etc. *)
1803 (* ------------------------------------------------------------------------- *)
1805 let CARD_SUBSET_EQ = prove
1806 (`!(a:A->bool) b. FINITE b /\ a SUBSET b /\ (CARD a = CARD b) ==> (a = b)`,
1807 REPEAT STRIP_TAC THEN
1808 MP_TAC(SPECL [`a:A->bool`; `b DIFF (a:A->bool)`] CARD_UNION) THEN
1809 SUBGOAL_THEN `FINITE(a:A->bool)` ASSUME_TAC THENL
1810 [ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
1811 SUBGOAL_THEN `FINITE(b:A->bool DIFF a)` ASSUME_TAC THENL
1812 [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `b:A->bool` THEN
1813 ASM_REWRITE_TAC[] THEN SET_TAC[]; ALL_TAC] THEN
1814 SUBGOAL_THEN `a:A->bool INTER (b DIFF a) = EMPTY` ASSUME_TAC THENL
1815 [SET_TAC[]; ALL_TAC] THEN
1816 ASM_REWRITE_TAC[] THEN
1817 SUBGOAL_THEN `a UNION (b:A->bool DIFF a) = b` ASSUME_TAC THENL
1818 [UNDISCH_TAC `a:A->bool SUBSET b` THEN SET_TAC[]; ALL_TAC] THEN
1819 ASM_REWRITE_TAC[] THEN
1820 REWRITE_TAC[ARITH_RULE `(a = a + b) <=> (b = 0)`] THEN DISCH_TAC THEN
1821 SUBGOAL_THEN `b:A->bool DIFF a = EMPTY` MP_TAC THENL
1822 [REWRITE_TAC[GSYM HAS_SIZE_0] THEN
1823 ASM_REWRITE_TAC[HAS_SIZE];
1824 UNDISCH_TAC `a:A->bool SUBSET b` THEN SET_TAC[]]);;
1826 let CARD_SUBSET = prove
1827 (`!(a:A->bool) b. a SUBSET b /\ FINITE(b) ==> CARD(a) <= CARD(b)`,
1828 REPEAT STRIP_TAC THEN
1829 SUBGOAL_THEN `b:A->bool = a UNION (b DIFF a)` SUBST1_TAC THENL
1830 [UNDISCH_TAC `a:A->bool SUBSET b` THEN SET_TAC[]; ALL_TAC] THEN
1832 `CARD (a UNION b DIFF a) = CARD(a:A->bool) + CARD(b DIFF a)`
1834 [MATCH_MP_TAC CARD_UNION THEN REPEAT CONJ_TAC THENL
1835 [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `b:A->bool` THEN
1837 MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `b:A->bool` THEN
1838 ASM_REWRITE_TAC[] THEN SET_TAC[];
1842 let CARD_SUBSET_LE = prove
1843 (`!(a:A->bool) b. FINITE b /\ a SUBSET b /\ (CARD b <= CARD a) ==> (a = b)`,
1844 MESON_TAC[CARD_SUBSET; CARD_SUBSET_EQ; LE_ANTISYM]);;
1846 let SUBSET_CARD_EQ = prove
1847 (`!s t. FINITE t /\ s SUBSET t ==> (CARD s = CARD t <=> s = t)`,
1848 MESON_TAC[CARD_SUBSET_EQ; LE_ANTISYM; CARD_SUBSET]);;
1850 let CARD_PSUBSET = prove
1851 (`!(a:A->bool) b. a PSUBSET b /\ FINITE(b) ==> CARD(a) < CARD(b)`,
1852 REPEAT GEN_TAC THEN REWRITE_TAC[SET_RULE
1853 `a PSUBSET b <=> ?x. x IN b /\ ~(x IN a) /\ a SUBSET (b DELETE x)` ] THEN
1854 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1855 DISCH_THEN(X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC) THEN
1856 MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `CARD(b DELETE (x:A))` THEN
1857 ASM_SIMP_TAC[CARD_SUBSET; FINITE_DELETE] THEN
1858 ASM_SIMP_TAC[CARD_DELETE; ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN
1859 ASM_MESON_TAC[CARD_EQ_0; MEMBER_NOT_EMPTY]);;
1861 let CARD_UNION_LE = prove
1863 FINITE s /\ FINITE t ==> CARD(s UNION t) <= CARD(s) + CARD(t)`,
1864 REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
1865 EXISTS_TAC `CARD(s:A->bool) + CARD(t DIFF s)` THEN
1866 ASM_SIMP_TAC[LE_ADD_LCANCEL; CARD_SUBSET; SUBSET_DIFF; FINITE_DIFF] THEN
1867 MATCH_MP_TAC EQ_IMP_LE THEN
1868 ONCE_REWRITE_TAC[SET_RULE `s UNION t = s UNION (t DIFF s)`] THEN
1869 MATCH_MP_TAC CARD_UNION THEN ASM_SIMP_TAC[FINITE_DIFF] THEN SET_TAC[]);;
1871 let CARD_UNIONS_LE = prove
1872 (`!s t:A->B->bool m n.
1873 s HAS_SIZE m /\ (!x. x IN s ==> FINITE(t x) /\ CARD(t x) <= n)
1874 ==> CARD(UNIONS {t(x) | x IN s}) <= m * n`,
1875 GEN_REWRITE_TAC (funpow 4 BINDER_CONV o funpow 2 LAND_CONV) [HAS_SIZE] THEN
1876 REWRITE_TAC[GSYM CONJ_ASSOC] THEN
1877 ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1878 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THEN
1879 REWRITE_TAC[SET_RULE `UNIONS {t x | x IN {}} = {}`; CARD_CLAUSES; LE_0] THEN
1880 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
1881 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THEN
1882 DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) ASSUME_TAC) THEN
1883 REWRITE_TAC[SET_RULE
1884 `UNIONS {t x | x IN a INSERT s} = t(a) UNION UNIONS {t x | x IN s}`] THEN
1885 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC
1886 `CARD((t:A->B->bool) x) + CARD(UNIONS {(t:A->B->bool) y | y IN s})` THEN
1888 [MATCH_MP_TAC CARD_UNION_LE THEN ASM_SIMP_TAC[IN_INSERT] THEN
1889 REWRITE_TAC[SET_RULE `{t x | x IN s} = IMAGE t s`] THEN
1890 ASM_SIMP_TAC[FINITE_FINITE_UNIONS; FINITE_IMAGE; FORALL_IN_IMAGE;
1892 MATCH_MP_TAC(ARITH_RULE `a <= n /\ b <= x * n ==> a + b <= SUC x * n`) THEN
1893 ASM_SIMP_TAC[IN_INSERT]]);;
1895 let CARD_UNION_GEN = prove
1896 (`!s t. FINITE s /\ FINITE t
1897 ==> CARD(s UNION t) = (CARD(s) + CARD(t)) - CARD(s INTER t)`,
1898 REPEAT STRIP_TAC THEN
1899 ONCE_REWRITE_TAC[SET_RULE `s UNION t = s UNION (t DIFF s)`] THEN
1900 ASM_SIMP_TAC[ARITH_RULE `x:num <= y ==> (a + y) - x = a + (y - x)`;
1901 CARD_SUBSET; INTER_SUBSET; GSYM CARD_DIFF] THEN
1902 REWRITE_TAC[SET_RULE `t DIFF (s INTER t) = t DIFF s`] THEN
1903 MATCH_MP_TAC CARD_UNION THEN ASM_SIMP_TAC[FINITE_DIFF] THEN SET_TAC[]);;
1905 let CARD_UNION_OVERLAP_EQ = prove
1906 (`!s t. FINITE s /\ FINITE t
1907 ==> (CARD(s UNION t) = CARD s + CARD t <=> s INTER t = {})`,
1908 REPEAT GEN_TAC THEN STRIP_TAC THEN
1909 ASM_SIMP_TAC[CARD_UNION_GEN] THEN
1910 REWRITE_TAC[ARITH_RULE `a - b = a <=> b = 0 \/ a = 0`] THEN
1911 ASM_SIMP_TAC[ADD_EQ_0; CARD_EQ_0; FINITE_INTER] THEN SET_TAC[]);;
1913 let CARD_UNION_OVERLAP = prove
1914 (`!s t. FINITE s /\ FINITE t /\ CARD(s UNION t) < CARD(s) + CARD(t)
1915 ==> ~(s INTER t = {})`,
1916 SIMP_TAC[GSYM CARD_UNION_OVERLAP_EQ] THEN ARITH_TAC);;
1918 (* ------------------------------------------------------------------------- *)
1919 (* Cardinality of image under maps, injective or general. *)
1920 (* ------------------------------------------------------------------------- *)
1922 let CARD_IMAGE_INJ = prove
1923 (`!(f:A->B) s. (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\
1924 FINITE s ==> (CARD (IMAGE f s) = CARD s)`,
1926 REWRITE_TAC[TAUT `a /\ b ==> c <=> b ==> a ==> c`] THEN
1927 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1928 REWRITE_TAC[NOT_IN_EMPTY; IMAGE_CLAUSES] THEN
1929 REPEAT STRIP_TAC THEN
1930 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_IMAGE; IN_IMAGE] THEN
1931 COND_CASES_TAC THEN ASM_MESON_TAC[IN_INSERT]);;
1933 let HAS_SIZE_IMAGE_INJ = prove
1935 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\ s HAS_SIZE n
1936 ==> (IMAGE f s) HAS_SIZE n`,
1937 SIMP_TAC[HAS_SIZE; FINITE_IMAGE] THEN MESON_TAC[CARD_IMAGE_INJ]);;
1939 let CARD_IMAGE_LE = prove
1940 (`!(f:A->B) s. FINITE s ==> CARD(IMAGE f s) <= CARD s`,
1941 GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1942 SIMP_TAC[IMAGE_CLAUSES; CARD_CLAUSES; FINITE_IMAGE; LE_REFL] THEN
1943 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
1944 DISCH_THEN(MP_TAC o CONJUNCT1) THEN ARITH_TAC);;
1946 let CARD_IMAGE_INJ_EQ = prove
1949 (!x. x IN s ==> f(x) IN t) /\
1950 (!y. y IN t ==> ?!x. x IN s /\ f(x) = y)
1951 ==> CARD t = CARD s`,
1952 REPEAT STRIP_TAC THEN
1953 SUBGOAL_THEN `t = IMAGE (f:A->B) s` SUBST1_TAC THENL
1954 [REWRITE_TAC[EXTENSION; IN_IMAGE] THEN ASM_MESON_TAC[];
1955 MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_MESON_TAC[]]);;
1957 let CARD_SUBSET_IMAGE = prove
1958 (`!f s t. FINITE t /\ s SUBSET IMAGE f t ==> CARD s <= CARD t`,
1959 MESON_TAC[LE_TRANS; FINITE_IMAGE; CARD_IMAGE_LE; CARD_SUBSET]);;
1961 let HAS_SIZE_IMAGE_INJ_EQ = prove
1963 (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)
1964 ==> ((IMAGE f s) HAS_SIZE n <=> s HAS_SIZE n)`,
1965 REPEAT STRIP_TAC THEN REWRITE_TAC[HAS_SIZE] THEN
1967 `(a' <=> a) /\ (a ==> (b' <=> b)) ==> (a' /\ b' <=> a /\ b)`) THEN
1969 [MATCH_MP_TAC FINITE_IMAGE_INJ_EQ;
1970 DISCH_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1971 MATCH_MP_TAC CARD_IMAGE_INJ] THEN
1972 ASM_REWRITE_TAC[]);;
1974 let CARD_IMAGE_EQ_INJ = prove
1977 ==> (CARD(IMAGE f s) = CARD s <=>
1978 !x y. x IN s /\ y IN s /\ f x = f y ==> x = y)`,
1979 REPEAT STRIP_TAC THEN EQ_TAC THENL
1980 [DISCH_TAC; ASM_MESON_TAC[CARD_IMAGE_INJ]] THEN
1981 MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN STRIP_TAC THEN
1982 ASM_CASES_TAC `x:A = y` THEN ASM_REWRITE_TAC[] THEN
1983 UNDISCH_TAC `CARD(IMAGE (f:A->B) s) = CARD s` THEN
1984 SUBGOAL_THEN `IMAGE (f:A->B) s = IMAGE f (s DELETE y)` SUBST1_TAC THENL
1985 [ASM SET_TAC[]; REWRITE_TAC[]] THEN
1986 MATCH_MP_TAC(ARITH_RULE `!n. m <= n /\ n < p ==> ~(m:num = p)`) THEN
1987 EXISTS_TAC `CARD(s DELETE (y:A))` THEN
1988 ASM_SIMP_TAC[CARD_IMAGE_LE; FINITE_DELETE] THEN
1989 ASM_SIMP_TAC[CARD_DELETE; CARD_EQ_0;
1990 ARITH_RULE `n - 1 < n <=> ~(n = 0)`] THEN
1993 (* ------------------------------------------------------------------------- *)
1994 (* Choosing a smaller subset of a given size. *)
1995 (* ------------------------------------------------------------------------- *)
1997 let CHOOSE_SUBSET_STRONG = prove
1999 (FINITE s ==> n <= CARD s) ==> ?t. t SUBSET s /\ t HAS_SIZE n`,
2000 INDUCT_TAC THEN REWRITE_TAC[HAS_SIZE_0; HAS_SIZE_SUC] THENL
2001 [MESON_TAC[EMPTY_SUBSET]; ALL_TAC] THEN
2002 MATCH_MP_TAC SET_PROVE_CASES THEN
2003 REWRITE_TAC[FINITE_EMPTY; CARD_CLAUSES; ARITH_RULE `~(SUC n <= 0)`] THEN
2004 MAP_EVERY X_GEN_TAC [`a:A`; `s:A->bool`] THEN DISCH_TAC THEN
2005 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; LE_SUC] THEN DISCH_TAC THEN
2006 FIRST_X_ASSUM(MP_TAC o SPEC `s:A->bool`) THEN ASM_REWRITE_TAC[] THEN
2007 DISCH_THEN(X_CHOOSE_THEN `t:A->bool` STRIP_ASSUME_TAC) THEN
2008 EXISTS_TAC `(a:A) INSERT t` THEN
2009 REPEAT(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
2010 RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
2011 ASM_SIMP_TAC[HAS_SIZE; CARD_DELETE; FINITE_INSERT; FINITE_DELETE;
2013 GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[SUC_SUB1] THEN
2016 let CHOOSE_SUBSET = prove
2017 (`!s:A->bool. FINITE s ==> !n. n <= CARD s ==> ?t. t SUBSET s /\ t HAS_SIZE n`,
2018 MESON_TAC[CHOOSE_SUBSET_STRONG]);;
2020 let CHOOSE_SUBSET_BETWEEN = prove
2022 s SUBSET u /\ FINITE s /\ CARD s <= n /\ (FINITE u ==> n <= CARD u)
2023 ==> ?t. s SUBSET t /\ t SUBSET u /\ t HAS_SIZE n`,
2024 REPEAT STRIP_TAC THEN
2025 MP_TAC(ISPECL [`n - CARD(s:A->bool)`; `u DIFF s:A->bool`]
2026 CHOOSE_SUBSET_STRONG) THEN
2028 [ASM_CASES_TAC `FINITE(u:A->bool)` THEN
2029 ASM_SIMP_TAC[CARD_DIFF; ARITH_RULE `n:num <= m ==> n - x <= m - x`] THEN
2030 MATCH_MP_TAC(TAUT `~p ==> p ==> q`) THEN
2031 ASM_MESON_TAC[FINITE_UNION; FINITE_SUBSET; SET_RULE
2032 `u SUBSET (u DIFF s) UNION s`];
2033 DISCH_THEN(X_CHOOSE_THEN `t:A->bool` STRIP_ASSUME_TAC) THEN
2034 EXISTS_TAC `s UNION t:A->bool` THEN
2035 REPEAT(CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
2036 SUBGOAL_THEN `n:num = CARD(s) + (n - CARD(s:A->bool))` SUBST1_TAC THENL
2038 MATCH_MP_TAC HAS_SIZE_UNION] THEN
2039 ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[HAS_SIZE] THEN ASM SET_TAC[]]);;
2041 (* ------------------------------------------------------------------------- *)
2042 (* Cardinality of product. *)
2043 (* ------------------------------------------------------------------------- *)
2045 let HAS_SIZE_PRODUCT_DEPENDENT = prove
2047 s HAS_SIZE m /\ (!x. x IN s ==> t(x) HAS_SIZE n)
2048 ==> {(x:A,y:B) | x IN s /\ y IN t(x)} HAS_SIZE (m * n)`,
2049 GEN_REWRITE_TAC (funpow 4 BINDER_CONV o funpow 2 LAND_CONV) [HAS_SIZE] THEN
2050 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
2051 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2052 SIMP_TAC[CARD_CLAUSES; NOT_IN_EMPTY; IN_INSERT] THEN CONJ_TAC THENL
2053 [GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
2054 REWRITE_TAC[MULT_CLAUSES; HAS_SIZE_0] THEN SET_TAC[];
2056 MAP_EVERY X_GEN_TAC [`x:A`; `s:A->bool`] THEN STRIP_TAC THEN
2057 X_GEN_TAC `m:num` THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
2058 MAP_EVERY X_GEN_TAC [`t:A->B->bool`; `n:num`] THEN
2059 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
2060 SIMP_TAC[FORALL_AND_THM; LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
2061 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `CARD(s:A->bool)`) THEN
2062 ASM_REWRITE_TAC[MULT_CLAUSES] THEN DISCH_TAC THEN
2063 REWRITE_TAC[SET_RULE
2064 `{(x,y) | (x = a \/ x IN s) /\ y IN t(x)} =
2065 {(x,y) | x IN s /\ y IN t(x)} UNION
2066 IMAGE (\y. (a,y)) (t a)`] THEN
2067 MATCH_MP_TAC HAS_SIZE_UNION THEN
2068 ASM_SIMP_TAC[HAS_SIZE_IMAGE_INJ; PAIR_EQ] THEN
2069 REWRITE_TAC[DISJOINT; IN_IMAGE; IN_ELIM_THM; IN_INTER; EXTENSION;
2070 NOT_IN_EMPTY; EXISTS_PAIR_THM; PAIR_EQ] THEN
2071 REPEAT STRIP_TAC THEN ASM_MESON_TAC[PAIR_EQ]);;
2073 let FINITE_PRODUCT_DEPENDENT = prove
2075 FINITE s /\ (!x. x IN s ==> FINITE(t x))
2076 ==> FINITE {f x y | x IN s /\ y IN (t x)}`,
2077 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
2078 EXISTS_TAC `IMAGE (\(x,y). (f:A->B->C) x y) {x,y | x IN s /\ y IN t x}` THEN
2079 REWRITE_TAC[SUBSET; IN_IMAGE; EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
2080 REWRITE_TAC[FORALL_IN_GSPEC] THEN
2081 CONJ_TAC THENL [MATCH_MP_TAC FINITE_IMAGE; MESON_TAC[]] THEN
2082 MAP_EVERY UNDISCH_TAC
2083 [`!x:A. x IN s ==> FINITE(t x :B->bool)`; `FINITE(s:A->bool)`] THEN
2084 MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`t:A->B->bool`; `s:A->bool`] THEN
2085 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
2086 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
2087 [GEN_TAC THEN SUBGOAL_THEN `{(x:A,y:B) | x IN {} /\ y IN (t x)} = {}`
2088 (fun th -> REWRITE_TAC[th; FINITE_RULES]) THEN
2089 REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY];
2091 MAP_EVERY X_GEN_TAC [`a:A`; `s:A->bool`] THEN STRIP_TAC THEN
2092 X_GEN_TAC `t:A->B->bool` THEN
2094 `{(x:A,y:B) | x IN (a INSERT s) /\ y IN (t x)} =
2095 IMAGE (\y. a,y) (t a) UNION {(x,y) | x IN s /\ y IN (t x)}`
2096 (fun th -> ASM_SIMP_TAC[IN_INSERT; FINITE_IMAGE; FINITE_UNION; th]) THEN
2097 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM; IN_INSERT; IN_UNION] THEN
2100 let FINITE_PRODUCT = prove
2101 (`!s t. FINITE s /\ FINITE t ==> FINITE {(x:A,y:B) | x IN s /\ y IN t}`,
2102 SIMP_TAC[FINITE_PRODUCT_DEPENDENT]);;
2104 let CARD_PRODUCT = prove
2105 (`!s t. FINITE s /\ FINITE t
2106 ==> (CARD {(x:A,y:B) | x IN s /\ y IN t} = CARD s * CARD t)`,
2107 REPEAT STRIP_TAC THEN
2108 MP_TAC(SPECL [`s:A->bool`; `CARD(s:A->bool)`; `\x:A. t:B->bool`;
2109 `CARD(t:B->bool)`] HAS_SIZE_PRODUCT_DEPENDENT) THEN
2110 ASM_SIMP_TAC[HAS_SIZE]);;
2112 let HAS_SIZE_PRODUCT = prove
2113 (`!s m t n. s HAS_SIZE m /\ t HAS_SIZE n
2114 ==> {(x:A,y:B) | x IN s /\ y IN t} HAS_SIZE (m * n)`,
2115 SIMP_TAC[HAS_SIZE; CARD_PRODUCT; FINITE_PRODUCT]);;
2117 (* ------------------------------------------------------------------------- *)
2118 (* Actually introduce a Cartesian product operation. *)
2119 (* ------------------------------------------------------------------------- *)
2121 parse_as_infix("CROSS",(22,"right"));;
2123 let CROSS = new_definition
2124 `s CROSS t = {x,y | x IN s /\ y IN t}`;;
2126 let IN_CROSS = prove
2127 (`!x y s t. (x,y) IN (s CROSS t) <=> x IN s /\ y IN t`,
2128 REWRITE_TAC[CROSS; IN_ELIM_PAIR_THM]);;
2130 let HAS_SIZE_CROSS = prove
2131 (`!s t m n. s HAS_SIZE m /\ t HAS_SIZE n ==> (s CROSS t) HAS_SIZE (m * n)`,
2132 REWRITE_TAC[CROSS; HAS_SIZE_PRODUCT]);;
2134 let FINITE_CROSS = prove
2135 (`!s t. FINITE s /\ FINITE t ==> FINITE(s CROSS t)`,
2136 SIMP_TAC[CROSS; FINITE_PRODUCT]);;
2138 let CARD_CROSS = prove
2139 (`!s t. FINITE s /\ FINITE t ==> CARD(s CROSS t) = CARD s * CARD t`,
2140 SIMP_TAC[CROSS; CARD_PRODUCT]);;
2142 let CROSS_EQ_EMPTY = prove
2143 (`!s t. s CROSS t = {} <=> s = {} \/ t = {}`,
2144 REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; IN_CROSS; NOT_IN_EMPTY] THEN
2147 (* ------------------------------------------------------------------------- *)
2148 (* Cardinality of functions with bounded domain (support) and range. *)
2149 (* ------------------------------------------------------------------------- *)
2151 let HAS_SIZE_FUNSPACE = prove
2152 (`!d n t:B->bool m s:A->bool.
2153 s HAS_SIZE m /\ t HAS_SIZE n
2154 ==> {f | (!x. x IN s ==> f(x) IN t) /\ (!x. ~(x IN s) ==> (f x = d))}
2155 HAS_SIZE (n EXP m)`,
2156 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
2157 REWRITE_TAC[HAS_SIZE_CLAUSES] THENL
2158 [REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[NOT_IN_EMPTY; EXP] THEN
2159 CONV_TAC HAS_SIZE_CONV THEN EXISTS_TAC `(\x. d):A->B` THEN
2160 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING] THEN REWRITE_TAC[FUN_EQ_THM];
2161 REWRITE_TAC[LEFT_IMP_EXISTS_THM; LEFT_AND_EXISTS_THM]] THEN
2162 MAP_EVERY X_GEN_TAC [`s0:A->bool`; `a:A`; `s:A->bool`] THEN
2163 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `s:A->bool`) THEN
2164 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2166 `{f:A->B | (!x. x IN a INSERT s ==> f x IN t) /\
2167 (!x. ~(x IN a INSERT s) ==> (f x = d))} =
2168 IMAGE (\(b,g) x. if x = a then b else g(x))
2170 g IN {f | (!x. x IN s ==> f x IN t) /\
2171 (!x. ~(x IN s) ==> (f x = d))}}`
2173 [REWRITE_TAC[EXTENSION; IN_IMAGE; FORALL_PAIR_THM; IN_ELIM_THM;
2174 EXISTS_PAIR_THM] THEN
2175 REWRITE_TAC[PAIR_EQ; CONJ_ASSOC; ONCE_REWRITE_RULE[CONJ_SYM]
2177 X_GEN_TAC `f:A->B` THEN REWRITE_TAC[IN_INSERT] THEN EQ_TAC THENL
2178 [STRIP_TAC THEN MAP_EVERY EXISTS_TAC
2179 [`(f:A->B) a`; `\x. if x IN s then (f:A->B) x else d`] THEN
2180 REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[];
2181 DISCH_THEN(X_CHOOSE_THEN `b:B` (X_CHOOSE_THEN `g:A->B`
2182 STRIP_ASSUME_TAC)) THEN
2183 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]];
2185 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_SIMP_TAC[EXP; HAS_SIZE_PRODUCT] THEN
2186 REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM; PAIR_EQ; CONJ_ASSOC] THEN
2187 REWRITE_TAC[ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1] THEN
2188 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
2189 REWRITE_TAC[FUN_EQ_THM] THEN REPEAT GEN_TAC THEN
2190 STRIP_TAC THEN CONJ_TAC THENL
2191 [FIRST_X_ASSUM(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[];
2192 X_GEN_TAC `x:A` THEN FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN
2195 let CARD_FUNSPACE = prove
2196 (`!s t. FINITE s /\ FINITE t
2197 ==> (CARD {f | (!x. x IN s ==> f(x) IN t) /\
2198 (!x. ~(x IN s) ==> (f x = d))} =
2199 (CARD t) EXP (CARD s))`,
2200 MESON_TAC[HAS_SIZE_FUNSPACE; HAS_SIZE]);;
2202 let FINITE_FUNSPACE = prove
2203 (`!s t. FINITE s /\ FINITE t
2204 ==> FINITE {f | (!x. x IN s ==> f(x) IN t) /\
2205 (!x. ~(x IN s) ==> (f x = d))}`,
2206 MESON_TAC[HAS_SIZE_FUNSPACE; HAS_SIZE]);;
2208 let HAS_SIZE_FUNSPACE_UNIV = prove
2209 (`!m n. (:A) HAS_SIZE m /\ (:B) HAS_SIZE n ==> (:A->B) HAS_SIZE (n EXP m)`,
2211 DISCH_THEN(MP_TAC o MATCH_MP HAS_SIZE_FUNSPACE) THEN
2212 REWRITE_TAC[IN_UNIV; UNIV_GSPEC]);;
2214 let CARD_FUNSPACE_UNIV = prove
2215 (`FINITE(:A) /\ FINITE(:B) ==> CARD(:A->B) = CARD(:B) EXP CARD(:A)`,
2216 MESON_TAC[HAS_SIZE_FUNSPACE_UNIV; HAS_SIZE]);;
2218 let FINITE_FUNSPACE_UNIV = prove
2219 (`FINITE(:A) /\ FINITE(:B) ==> FINITE(:A->B)`,
2220 MESON_TAC[HAS_SIZE_FUNSPACE_UNIV; HAS_SIZE]);;
2222 (* ------------------------------------------------------------------------- *)
2223 (* Cardinality of type bool. *)
2224 (* ------------------------------------------------------------------------- *)
2226 let HAS_SIZE_BOOL = prove
2227 (`(:bool) HAS_SIZE 2`,
2228 SUBGOAL_THEN `(:bool) = {F,T}` SUBST1_TAC THENL
2229 [REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT] THEN CONV_TAC TAUT;
2230 SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; ARITH;
2231 IN_SING; NOT_IN_EMPTY]]);;
2233 let CARD_BOOL = prove
2235 MESON_TAC[HAS_SIZE_BOOL; HAS_SIZE]);;
2237 let FINITE_BOOL = prove
2239 MESON_TAC[HAS_SIZE_BOOL; HAS_SIZE]);;
2241 (* ------------------------------------------------------------------------- *)
2242 (* Hence cardinality of powerset. *)
2243 (* ------------------------------------------------------------------------- *)
2245 let HAS_SIZE_POWERSET = prove
2246 (`!(s:A->bool) n. s HAS_SIZE n ==> {t | t SUBSET s} HAS_SIZE (2 EXP n)`,
2247 REPEAT STRIP_TAC THEN SUBGOAL_THEN
2249 {f | (!x:A. x IN s ==> f(x) IN UNIV) /\ (!x. ~(x IN s) ==> (f x = F))}`
2251 [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_UNIV; SUBSET; IN; CONTRAPOS_THM];
2252 MATCH_MP_TAC HAS_SIZE_FUNSPACE THEN ASM_REWRITE_TAC[] THEN
2253 CONV_TAC HAS_SIZE_CONV THEN MAP_EVERY EXISTS_TAC [`T`; `F`] THEN
2254 REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
2257 let CARD_POWERSET = prove
2258 (`!s:A->bool. FINITE s ==> (CARD {t | t SUBSET s} = 2 EXP (CARD s))`,
2259 MESON_TAC[HAS_SIZE_POWERSET; HAS_SIZE]);;
2261 let FINITE_POWERSET = prove
2262 (`!s:A->bool. FINITE s ==> FINITE {t | t SUBSET s}`,
2263 MESON_TAC[HAS_SIZE_POWERSET; HAS_SIZE]);;
2265 let FINITE_UNIONS = prove
2266 (`!s:(A->bool)->bool.
2267 FINITE(UNIONS s) <=> FINITE s /\ (!t. t IN s ==> FINITE t)`,
2268 GEN_TAC THEN ASM_CASES_TAC `FINITE(s:(A->bool)->bool)` THEN
2269 ASM_SIMP_TAC[FINITE_FINITE_UNIONS] THEN
2270 DISCH_THEN(MP_TAC o MATCH_MP FINITE_POWERSET) THEN
2271 POP_ASSUM MP_TAC THEN REWRITE_TAC[CONTRAPOS_THM] THEN
2272 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] FINITE_SUBSET) THEN SET_TAC[]);;
2274 let POWERSET_CLAUSES = prove
2275 (`{s | s SUBSET {}} = {{}} /\
2276 (!a:A t. {s | s SUBSET (a INSERT t)} =
2277 {s | s SUBSET t} UNION IMAGE (\s. a INSERT s) {s | s SUBSET t})`,
2278 REWRITE_TAC[SUBSET_INSERT_DELETE; SUBSET_EMPTY; SING_GSPEC] THEN
2279 MAP_EVERY X_GEN_TAC [`a:A`; `t:A->bool`] THEN
2280 MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[UNION_SUBSET] THEN
2281 ONCE_REWRITE_TAC[SUBSET] THEN
2282 REWRITE_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
2283 REWRITE_TAC[IN_ELIM_THM; IN_UNION; IN_IMAGE] THEN
2284 CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
2285 X_GEN_TAC `s:A->bool` THEN
2286 ASM_CASES_TAC `(a:A) IN s` THENL [ALL_TAC; ASM SET_TAC[]] THEN
2287 STRIP_TAC THEN DISJ2_TAC THEN EXISTS_TAC `s DELETE (a:A)` THEN
2290 (* ------------------------------------------------------------------------- *)
2291 (* Set of numbers is infinite. *)
2292 (* ------------------------------------------------------------------------- *)
2294 let HAS_SIZE_NUMSEG_LT = prove
2295 (`!n. {m | m < n} HAS_SIZE n`,
2297 [SUBGOAL_THEN `{m | m < 0} = {}`
2298 (fun th -> REWRITE_TAC[HAS_SIZE_0; th]) THEN
2299 REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM; LT];
2300 SUBGOAL_THEN `{m | m < SUC n} = n INSERT {m | m < n}` SUBST1_TAC THENL
2301 [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT] THEN ARITH_TAC;
2303 RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
2304 ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT] THEN
2305 REWRITE_TAC[IN_ELIM_THM; LT_REFL]]);;
2307 let CARD_NUMSEG_LT = prove
2308 (`!n. CARD {m | m < n} = n`,
2309 REWRITE_TAC[REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_LT]);;
2311 let FINITE_NUMSEG_LT = prove
2312 (`!n:num. FINITE {m | m < n}`,
2313 REWRITE_TAC[REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_LT]);;
2315 let HAS_SIZE_NUMSEG_LE = prove
2316 (`!n. {m | m <= n} HAS_SIZE (n + 1)`,
2317 REWRITE_TAC[GSYM LT_SUC_LE; HAS_SIZE_NUMSEG_LT; ADD1]);;
2319 let FINITE_NUMSEG_LE = prove
2320 (`!n. FINITE {m | m <= n}`,
2321 REWRITE_TAC[REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_LE]);;
2323 let CARD_NUMSEG_LE = prove
2324 (`!n. CARD {m | m <= n} = n + 1`,
2325 REWRITE_TAC[REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_LE]);;
2327 let num_FINITE = prove
2328 (`!s:num->bool. FINITE s <=> ?a. !x. x IN s ==> x <= a`,
2329 GEN_TAC THEN EQ_TAC THENL
2330 [SPEC_TAC(`s:num->bool`,`s:num->bool`) THEN
2331 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2332 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[LE_CASES; LE_TRANS];
2333 DISCH_THEN(X_CHOOSE_TAC `n:num`) THEN MATCH_MP_TAC FINITE_SUBSET THEN
2334 EXISTS_TAC `{m:num | m <= n}` THEN REWRITE_TAC[FINITE_NUMSEG_LE] THEN
2335 ASM_SIMP_TAC[SUBSET; IN_ELIM_THM]]);;
2337 let num_FINITE_AVOID = prove
2338 (`!s:num->bool. FINITE(s) ==> ?a. ~(a IN s)`,
2339 MESON_TAC[num_FINITE; LT; NOT_LT]);;
2341 let num_INFINITE = prove
2343 REWRITE_TAC[INFINITE] THEN MESON_TAC[num_FINITE_AVOID; IN_UNIV]);;
2345 (* ------------------------------------------------------------------------- *)
2346 (* Set of strings is infinite. *)
2347 (* ------------------------------------------------------------------------- *)
2349 let string_INFINITE = prove
2350 (`INFINITE(:string)`,
2351 MP_TAC num_INFINITE THEN REWRITE_TAC[INFINITE; CONTRAPOS_THM] THEN
2352 DISCH_THEN(MP_TAC o ISPEC `LENGTH:string->num` o MATCH_MP FINITE_IMAGE) THEN
2353 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
2354 REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN MESON_TAC[LENGTH_REPLICATE]);;
2356 (* ------------------------------------------------------------------------- *)
2357 (* Non-trivial intervals of reals are infinite. *)
2358 (* ------------------------------------------------------------------------- *)
2360 let FINITE_REAL_INTERVAL = prove
2361 (`(!a. ~FINITE {x:real | a < x}) /\
2362 (!a. ~FINITE {x:real | a <= x}) /\
2363 (!b. ~FINITE {x:real | x < b}) /\
2364 (!b. ~FINITE {x:real | x <= b}) /\
2365 (!a b. FINITE {x:real | a < x /\ x < b} <=> b <= a) /\
2366 (!a b. FINITE {x:real | a <= x /\ x < b} <=> b <= a) /\
2367 (!a b. FINITE {x:real | a < x /\ x <= b} <=> b <= a) /\
2368 (!a b. FINITE {x:real | a <= x /\ x <= b} <=> b <= a)`,
2369 SUBGOAL_THEN `!a b. FINITE {x:real | a < x /\ x < b} <=> b <= a`
2371 [REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN
2372 ASM_CASES_TAC `a:real < b` THEN
2373 ASM_SIMP_TAC[REAL_ARITH `~(a:real < b) ==> ~(a < x /\ x < b)`] THEN
2374 REWRITE_TAC[EMPTY_GSPEC; FINITE_EMPTY] THEN
2375 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
2376 DISCH_THEN(MP_TAC o SPEC `IMAGE (\n. a + (b - a) / (&n + &2)) (:num)`) THEN
2377 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
2378 SIMP_TAC[REAL_LT_ADDR; REAL_ARITH `a + x / y < b <=> x / y < b - a`] THEN
2379 ASM_SIMP_TAC[REAL_LT_DIV; REAL_SUB_LT; REAL_LT_LDIV_EQ; NOT_IMP;
2380 REAL_ARITH `&0:real < &n + &2`] THEN
2381 REWRITE_TAC[REAL_ARITH `x:real < x * (n + &2) <=> &0 < x * (n + &1)`] THEN
2382 ASM_SIMP_TAC[REAL_SUB_LT; REAL_LT_MUL; REAL_ARITH `&0:real < &n + &1`] THEN
2383 MP_TAC num_INFINITE THEN REWRITE_TAC[INFINITE] THEN
2384 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
2385 MATCH_MP_TAC FINITE_IMAGE_INJ_EQ THEN
2386 ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
2387 `a < b ==> (a + (b - a) / (&n + &2) = a + (b - a) / (&m + &2) <=>
2390 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THENL
2391 [DISCH_THEN(MP_TAC o SPEC `{x:real | a < x /\ x < a + &1}` o
2392 MATCH_MP(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
2393 ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN REAL_ARITH_TAC;
2394 DISCH_THEN(MP_TAC o SPEC `{x:real | a < x /\ x < a + &1}` o
2395 MATCH_MP(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
2396 ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN REAL_ARITH_TAC;
2397 DISCH_THEN(MP_TAC o SPEC `{x:real | b - &1 < x /\ x < b}` o
2398 MATCH_MP(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
2399 ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN REAL_ARITH_TAC;
2400 DISCH_THEN(MP_TAC o SPEC `{x:real | b - &1 < x /\ x < b}` o
2401 MATCH_MP(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
2402 ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN REAL_ARITH_TAC;
2403 REWRITE_TAC[REAL_ARITH
2404 `a:real <= x /\ x < b <=> (a < x /\ x < b) \/ ~(b <= a) /\ x = a`];
2405 REWRITE_TAC[REAL_ARITH
2406 `a:real < x /\ x <= b <=> (a < x /\ x < b) \/ ~(b <= a) /\ x = b`];
2407 ASM_CASES_TAC `b:real = a` THEN
2408 ASM_SIMP_TAC[REAL_LE_ANTISYM; REAL_LE_REFL; SING_GSPEC; FINITE_SING] THEN
2409 ASM_SIMP_TAC[REAL_ARITH
2411 (a <= x /\ x <= b <=> (a < x /\ x < b) \/ ~(b <= a) /\ x = a \/
2412 ~(b <= a) /\ x = b)`]] THEN
2413 ASM_REWRITE_TAC[FINITE_UNION; SET_RULE
2414 `{x | p x \/ q x} = {x | p x} UNION {x | q x}`] THEN
2415 ASM_CASES_TAC `b:real <= a` THEN
2416 ASM_REWRITE_TAC[EMPTY_GSPEC; FINITE_EMPTY]);;
2418 let real_INFINITE = prove
2420 REWRITE_TAC[INFINITE] THEN
2421 DISCH_THEN(MP_TAC o SPEC `{x:real | &0 <= x}` o
2422 MATCH_MP(REWRITE_RULE[IMP_CONJ] FINITE_SUBSET)) THEN
2423 REWRITE_TAC[FINITE_REAL_INTERVAL; SUBSET_UNIV]);;
2425 (* ------------------------------------------------------------------------- *)
2426 (* Indexing of finite sets and enumeration of subsets of N in order. *)
2427 (* ------------------------------------------------------------------------- *)
2429 let HAS_SIZE_INDEX = prove
2430 (`!s n. s HAS_SIZE n
2431 ==> ?f:num->A. (!m. m < n ==> f(m) IN s) /\
2432 (!x. x IN s ==> ?!m. m < n /\ (f m = x))`,
2433 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THEN
2434 SIMP_TAC[HAS_SIZE_0; HAS_SIZE_SUC; LT; NOT_IN_EMPTY] THEN
2435 X_GEN_TAC `s:A->bool` THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN
2436 REWRITE_TAC[NOT_FORALL_THM] THEN
2437 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:A`) (MP_TAC o SPEC `a:A`)) THEN
2438 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2439 FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (a:A)`) THEN ASM_REWRITE_TAC[] THEN
2440 DISCH_THEN(X_CHOOSE_THEN `f:num->A` STRIP_ASSUME_TAC) THEN
2441 EXISTS_TAC `\m:num. if m < n then f(m) else a:A` THEN CONJ_TAC THENL
2442 [GEN_TAC THEN REWRITE_TAC[] THEN COND_CASES_TAC THEN
2443 ASM_MESON_TAC[IN_DELETE]; ALL_TAC] THEN
2444 X_GEN_TAC `x:A` THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
2445 FIRST_X_ASSUM(MP_TAC o SPEC `x:A`) THEN
2446 ASM_REWRITE_TAC[IN_DELETE] THEN
2447 CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV) THEN
2448 ASM_CASES_TAC `a:A = x` THEN ASM_SIMP_TAC[] THEN
2449 ASM_MESON_TAC[LT_REFL; IN_DELETE]);;
2451 let INFINITE_ENUMERATE = prove
2454 ==> ?r:num->num. (!m n. m < n ==> r(m) < r(n)) /\
2455 IMAGE r (:num) = s`,
2456 REPEAT STRIP_TAC THEN
2457 SUBGOAL_THEN `!n:num. ?x. n <= x /\ x IN s` MP_TAC THENL
2458 [ASM_MESON_TAC[INFINITE; num_FINITE; LT_IMP_LE; NOT_LE];
2459 GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [num_WOP]] THEN
2460 REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM; FORALL_AND_THM] THEN
2461 REWRITE_TAC[TAUT `p ==> ~(q /\ r) <=> q /\ p ==> ~r`] THEN
2462 X_GEN_TAC `next:num->num` THEN STRIP_TAC THEN
2463 (MP_TAC o prove_recursive_functions_exist num_RECURSION)
2464 `(f(0) = next 0) /\ (!n. f(SUC n) = next(f n + 1))` THEN
2465 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:num->num` THEN STRIP_TAC THEN
2466 MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
2467 [GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LT] THEN
2468 ASM_MESON_TAC[ARITH_RULE `m <= n /\ n + 1 <= p ==> m < p`; LE_LT];
2470 ASM_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; FORALL_IN_IMAGE; SUBSET] THEN
2471 REWRITE_TAC[IN_IMAGE; IN_UNIV] THEN CONJ_TAC THENL
2472 [INDUCT_TAC THEN ASM_MESON_TAC[]; ALL_TAC] THEN
2473 MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN REPEAT STRIP_TAC THEN
2474 ASM_CASES_TAC `?m:num. m < n /\ m IN s` THENL
2475 [MP_TAC(SPEC `\m:num. m < n /\ m IN s` num_MAX) THEN
2476 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT
2477 `p /\ (q ==> r) ==> (p <=> q) ==> r`) THEN
2478 CONJ_TAC THENL [MESON_TAC[LT_IMP_LE]; ALL_TAC] THEN
2479 DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
2480 SUBGOAL_THEN `?q. p = (r:num->num) q` (CHOOSE_THEN SUBST_ALL_TAC) THENL
2481 [ASM_MESON_TAC[]; EXISTS_TAC `SUC q`] THEN
2482 ASM_REWRITE_TAC[GSYM LE_ANTISYM; GSYM NOT_LT] THEN
2483 ASM_MESON_TAC[NOT_LE; ARITH_RULE `r < p <=> r + 1 <= p`];
2484 EXISTS_TAC `0` THEN ASM_REWRITE_TAC[GSYM LE_ANTISYM; GSYM NOT_LT] THEN
2485 ASM_MESON_TAC[LE_0]]);;
2487 (* ------------------------------------------------------------------------- *)
2488 (* Mapping between finite sets and lists. *)
2489 (* ------------------------------------------------------------------------- *)
2491 let set_of_list = new_recursive_definition list_RECURSION
2492 `(set_of_list ([]:A list) = {}) /\
2493 (set_of_list (CONS (h:A) t) = h INSERT (set_of_list t))`;;
2495 let list_of_set = new_definition
2496 `list_of_set s = @l. (set_of_list l = s) /\ (LENGTH l = CARD s)`;;
2498 let LIST_OF_SET_PROPERTIES = prove
2499 (`!s:A->bool. FINITE(s)
2500 ==> (set_of_list(list_of_set s) = s) /\
2501 (LENGTH(list_of_set s) = CARD s)`,
2502 REWRITE_TAC[list_of_set] THEN
2503 CONV_TAC(BINDER_CONV(RAND_CONV SELECT_CONV)) THEN
2504 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REPEAT STRIP_TAC THENL
2505 [EXISTS_TAC `[]:A list` THEN REWRITE_TAC[CARD_CLAUSES; LENGTH; set_of_list];
2506 EXISTS_TAC `CONS (x:A) l` THEN ASM_REWRITE_TAC[LENGTH] THEN
2507 ASM_REWRITE_TAC[set_of_list] THEN
2508 FIRST_ASSUM(fun th -> REWRITE_TAC
2509 [MATCH_MP (CONJUNCT2 CARD_CLAUSES) th]) THEN
2510 ASM_REWRITE_TAC[]]);;
2512 let SET_OF_LIST_OF_SET = prove
2513 (`!s. FINITE(s) ==> (set_of_list(list_of_set s) = s)`,
2514 MESON_TAC[LIST_OF_SET_PROPERTIES]);;
2516 let LENGTH_LIST_OF_SET = prove
2517 (`!s. FINITE(s) ==> (LENGTH(list_of_set s) = CARD s)`,
2518 MESON_TAC[LIST_OF_SET_PROPERTIES]);;
2520 let MEM_LIST_OF_SET = prove
2521 (`!s:A->bool. FINITE(s) ==> !x. MEM x (list_of_set s) <=> x IN s`,
2522 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP SET_OF_LIST_OF_SET) THEN
2523 DISCH_THEN(fun th -> GEN_REWRITE_TAC (BINDER_CONV o funpow 2 RAND_CONV)
2525 SPEC_TAC(`list_of_set(s:A->bool)`,`l:A list`) THEN
2526 LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; set_of_list; NOT_IN_EMPTY] THEN
2527 ASM_REWRITE_TAC[IN_INSERT]);;
2529 let FINITE_SET_OF_LIST = prove
2530 (`!l. FINITE(set_of_list l)`,
2531 LIST_INDUCT_TAC THEN ASM_SIMP_TAC[set_of_list; FINITE_RULES]);;
2533 let IN_SET_OF_LIST = prove
2534 (`!x l. x IN (set_of_list l) <=> MEM x l`,
2535 GEN_TAC THEN LIST_INDUCT_TAC THEN
2536 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; MEM; set_of_list] THEN
2539 let SET_OF_LIST_APPEND = prove
2540 (`!l1 l2. set_of_list(APPEND l1 l2) = set_of_list(l1) UNION set_of_list(l2)`,
2541 REWRITE_TAC[EXTENSION; IN_SET_OF_LIST; IN_UNION; MEM_APPEND]);;
2543 let SET_OF_LIST_MAP = prove
2544 (`!f l. set_of_list(MAP f l) = IMAGE f (set_of_list l)`,
2545 GEN_TAC THEN LIST_INDUCT_TAC THEN
2546 ASM_REWRITE_TAC[set_of_list; MAP; IMAGE_CLAUSES]);;
2548 let SET_OF_LIST_EQ_EMPTY = prove
2549 (`!l. set_of_list l = {} <=> l = []`,
2550 LIST_INDUCT_TAC THEN
2551 REWRITE_TAC[set_of_list; NOT_CONS_NIL; NOT_INSERT_EMPTY]);;
2553 let LIST_OF_SET_EMPTY = prove
2554 (`list_of_set {} = []`,
2555 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
2556 SIMP_TAC[LENGTH_LIST_OF_SET; FINITE_EMPTY; CARD_CLAUSES]);;
2558 let LIST_OF_SET_SING = prove
2559 (`!x:A. list_of_set {a} = [a]`,
2560 GEN_TAC THEN REWRITE_TAC[list_of_set] THEN
2561 MATCH_MP_TAC SELECT_UNIQUE THEN
2562 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[NOT_CONS_NIL] THEN
2563 SIMP_TAC[LENGTH; CARD_CLAUSES; FINITE_EMPTY; NOT_IN_EMPTY; NOT_SUC] THEN
2564 GEN_TAC THEN LIST_INDUCT_TAC THEN DISCH_THEN(K ALL_TAC) THEN
2565 SIMP_TAC[LENGTH; set_of_list; CONS_11; SUC_INJ; NOT_CONS_NIL; NOT_SUC] THEN
2568 (* ------------------------------------------------------------------------- *)
2569 (* Mappings from finite set enumerations to lists (no "setification"). *)
2570 (* ------------------------------------------------------------------------- *)
2573 let fn = splitlist (dest_binary "INSERT") in
2574 fun tm -> let l,n = fn tm in
2575 if is_const n & fst(dest_const n) = "EMPTY" then l
2576 else failwith "dest_setenum: not a finite set enumeration";;
2578 let is_setenum = can dest_setenum;;
2581 let insert_atm = `(INSERT):A->(A->bool)->(A->bool)`
2582 and nil_atm = `(EMPTY):A->bool` in
2584 let insert_tm = inst [ty,aty] insert_atm
2585 and nil_tm = inst [ty,aty] nil_atm in
2586 itlist (mk_binop insert_tm) l nil_tm;;
2588 let mk_fset l = mk_setenum(l,type_of(hd l));;
2590 (* ------------------------------------------------------------------------- *)
2591 (* Pairwise property over sets and lists. *)
2592 (* ------------------------------------------------------------------------- *)
2594 let pairwise = new_definition
2595 `pairwise r s <=> !x y. x IN s /\ y IN s /\ ~(x = y) ==> r x y`;;
2597 let PAIRWISE = new_recursive_definition list_RECURSION
2598 `(PAIRWISE (r:A->A->bool) [] <=> T) /\
2599 (PAIRWISE (r:A->A->bool) (CONS h t) <=> ALL (r h) t /\ PAIRWISE r t)`;;
2601 let PAIRWISE_EMPTY = prove
2602 (`!r. pairwise r {} <=> T`,
2603 REWRITE_TAC[pairwise; NOT_IN_EMPTY] THEN MESON_TAC[]);;
2605 let PAIRWISE_SING = prove
2606 (`!r x. pairwise r {x} <=> T`,
2607 REWRITE_TAC[pairwise; IN_SING] THEN MESON_TAC[]);;
2609 let PAIRWISE_MONO = prove
2610 (`!r s t. pairwise r s /\ t SUBSET s ==> pairwise r t`,
2611 REWRITE_TAC[pairwise] THEN SET_TAC[]);;
2613 let PAIRWISE_INSERT = prove
2615 pairwise r (x INSERT s) <=>
2616 (!y. y IN s /\ ~(y = x) ==> r x y /\ r y x) /\
2618 REWRITE_TAC[pairwise; IN_INSERT] THEN MESON_TAC[]);;
2620 let PAIRWISE_IMAGE = prove
2621 (`!r f. pairwise r (IMAGE f s) <=>
2622 pairwise (\x y. ~(f x = f y) ==> r (f x) (f y)) s`,
2623 REWRITE_TAC[pairwise; IN_IMAGE] THEN MESON_TAC[]);;
2625 (* ------------------------------------------------------------------------- *)
2626 (* Some additional properties of "set_of_list". *)
2627 (* ------------------------------------------------------------------------- *)
2629 let CARD_SET_OF_LIST_LE = prove
2630 (`!l. CARD(set_of_list l) <= LENGTH l`,
2631 LIST_INDUCT_TAC THEN
2632 SIMP_TAC[LENGTH; set_of_list; CARD_CLAUSES; FINITE_SET_OF_LIST] THEN
2635 let HAS_SIZE_SET_OF_LIST = prove
2636 (`!l. (set_of_list l) HAS_SIZE (LENGTH l) <=> PAIRWISE (\x y. ~(x = y)) l`,
2637 REWRITE_TAC[HAS_SIZE; FINITE_SET_OF_LIST] THEN LIST_INDUCT_TAC THEN
2638 ASM_SIMP_TAC[CARD_CLAUSES; LENGTH; set_of_list; PAIRWISE; ALL;
2639 FINITE_SET_OF_LIST; GSYM ALL_MEM; IN_SET_OF_LIST] THEN
2640 COND_CASES_TAC THEN ASM_REWRITE_TAC[SUC_INJ] THEN
2641 ASM_MESON_TAC[CARD_SET_OF_LIST_LE; ARITH_RULE `~(SUC n <= n)`]);;
2643 (* ------------------------------------------------------------------------- *)
2644 (* Classic result on function of finite set into itself. *)
2645 (* ------------------------------------------------------------------------- *)
2647 let SURJECTIVE_IFF_INJECTIVE_GEN = prove
2649 FINITE s /\ FINITE t /\ (CARD s = CARD t) /\ (IMAGE f s) SUBSET t
2650 ==> ((!y. y IN t ==> ?x. x IN s /\ (f x = y)) <=>
2651 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)))`,
2652 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
2653 [ASM_CASES_TAC `x:A = y` THEN ASM_REWRITE_TAC[] THEN
2654 SUBGOAL_THEN `CARD s <= CARD (IMAGE (f:A->B) (s DELETE y))` MP_TAC THENL
2655 [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CARD_SUBSET THEN
2656 ASM_SIMP_TAC[FINITE_IMAGE; FINITE_DELETE] THEN
2657 REWRITE_TAC[SUBSET; IN_IMAGE; IN_DELETE] THEN ASM_MESON_TAC[];
2658 REWRITE_TAC[NOT_LE] THEN MATCH_MP_TAC LET_TRANS THEN
2659 EXISTS_TAC `CARD(s DELETE (y:A))` THEN
2660 ASM_SIMP_TAC[CARD_IMAGE_LE; FINITE_DELETE] THEN
2661 ASM_SIMP_TAC[CARD_DELETE; ARITH_RULE `x - 1 < x <=> ~(x = 0)`] THEN
2662 ASM_MESON_TAC[CARD_EQ_0; MEMBER_NOT_EMPTY]];
2663 SUBGOAL_THEN `IMAGE (f:A->B) s = t` MP_TAC THENL
2664 [ALL_TAC; ASM_MESON_TAC[EXTENSION; IN_IMAGE]] THEN
2665 ASM_MESON_TAC[CARD_SUBSET_EQ; CARD_IMAGE_INJ]]);;
2667 let SURJECTIVE_IFF_INJECTIVE = prove
2669 FINITE s /\ (IMAGE f s) SUBSET s
2670 ==> ((!y. y IN s ==> ?x. x IN s /\ (f x = y)) <=>
2671 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)))`,
2672 SIMP_TAC[SURJECTIVE_IFF_INJECTIVE_GEN]);;
2674 let IMAGE_IMP_INJECTIVE_GEN = prove
2676 FINITE s /\ (CARD s = CARD t) /\ (IMAGE f s = t)
2677 ==> !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)`,
2678 REPEAT GEN_TAC THEN DISCH_THEN(ASSUME_TAC o GSYM) THEN
2679 MP_TAC(ISPECL [`s:A->bool`; `t:B->bool`; `f:A->B`]
2680 SURJECTIVE_IFF_INJECTIVE_GEN) THEN
2681 ASM_SIMP_TAC[SUBSET_REFL; FINITE_IMAGE] THEN
2682 ASM_MESON_TAC[EXTENSION; IN_IMAGE]);;
2684 let IMAGE_IMP_INJECTIVE = prove
2685 (`!s f. FINITE s /\ (IMAGE f s = s)
2686 ==> !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)`,
2687 MESON_TAC[IMAGE_IMP_INJECTIVE_GEN]);;
2689 (* ------------------------------------------------------------------------- *)
2690 (* Converse relation between cardinality and injection. *)
2691 (* ------------------------------------------------------------------------- *)
2693 let CARD_LE_INJ = prove
2694 (`!s t. FINITE s /\ FINITE t /\ CARD s <= CARD t
2695 ==> ?f:A->B. (IMAGE f s) SUBSET t /\
2696 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)`,
2697 REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
2698 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2699 REWRITE_TAC[IMAGE_CLAUSES; EMPTY_SUBSET; NOT_IN_EMPTY] THEN
2700 SIMP_TAC[CARD_CLAUSES] THEN
2701 MAP_EVERY X_GEN_TAC [`x:A`; `s:A->bool`] THEN STRIP_TAC THEN
2702 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2703 REWRITE_TAC[CARD_CLAUSES; LE; NOT_SUC] THEN
2704 MAP_EVERY X_GEN_TAC [`y:B`; `t:B->bool`] THEN
2705 SIMP_TAC[CARD_CLAUSES] THEN
2706 DISCH_THEN(CONJUNCTS_THEN2 (K ALL_TAC) STRIP_ASSUME_TAC) THEN
2707 REWRITE_TAC[LE_SUC] THEN STRIP_TAC THEN
2708 FIRST_X_ASSUM(MP_TAC o SPEC `t:B->bool`) THEN ASM_REWRITE_TAC[] THEN
2709 DISCH_THEN(X_CHOOSE_THEN `f:A->B` STRIP_ASSUME_TAC) THEN
2710 EXISTS_TAC `\z:A. if z = x then (y:B) else f(z)` THEN
2711 REWRITE_TAC[IN_INSERT; SUBSET; IN_IMAGE] THEN
2712 ASM_MESON_TAC[SUBSET; IN_IMAGE]);;
2714 (* ------------------------------------------------------------------------- *)
2715 (* Occasionally handy rewrites. *)
2716 (* ------------------------------------------------------------------------- *)
2718 let FORALL_IN_CLAUSES = prove
2719 (`(!P. (!x. x IN {} ==> P x) <=> T) /\
2720 (!P a s. (!x. x IN (a INSERT s) ==> P x) <=> P a /\ (!x. x IN s ==> P x))`,
2721 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[]);;
2723 let EXISTS_IN_CLAUSES = prove
2724 (`(!P. (?x. x IN {} /\ P x) <=> F) /\
2725 (!P a s. (?x. x IN (a INSERT s) /\ P x) <=> P a \/ (?x. x IN s /\ P x))`,
2726 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[]);;
2728 (* ------------------------------------------------------------------------- *)
2729 (* Injectivity and surjectivity of image under a function. *)
2730 (* ------------------------------------------------------------------------- *)
2732 let INJECTIVE_ON_IMAGE = prove
2734 (!s t. s SUBSET u /\ t SUBSET u /\ IMAGE f s = IMAGE f t ==> s = t) <=>
2735 (!x y. x IN u /\ y IN u /\ f x = f y ==> x = y)`,
2736 REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_TAC; SET_TAC[]] THEN
2737 MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN STRIP_TAC THEN
2738 FIRST_X_ASSUM(MP_TAC o SPECL [`{x:A}`; `{y:A}`]) THEN
2739 ASM_REWRITE_TAC[SING_SUBSET; IMAGE_CLAUSES] THEN SET_TAC[]);;
2741 let INJECTIVE_IMAGE = prove
2743 (!s t. IMAGE f s = IMAGE f t ==> s = t) <=> (!x y. f x = f y ==> x = y)`,
2744 GEN_TAC THEN MP_TAC(ISPECL [`f:A->B`; `(:A)`] INJECTIVE_ON_IMAGE) THEN
2745 REWRITE_TAC[IN_UNIV; SUBSET_UNIV]);;
2747 let SURJECTIVE_ON_IMAGE = prove
2749 (!t. t SUBSET v ==> ?s. s SUBSET u /\ IMAGE f s = t) <=>
2750 (!y. y IN v ==> ?x. x IN u /\ f x = y)`,
2751 REPEAT GEN_TAC THEN EQ_TAC THENL
2752 [DISCH_TAC THEN X_GEN_TAC `y:B` THEN DISCH_TAC THEN
2753 FIRST_X_ASSUM(MP_TAC o SPEC `{y:B}`) THEN ASM SET_TAC[];
2754 DISCH_TAC THEN X_GEN_TAC `t:B->bool` THEN DISCH_TAC THEN
2755 EXISTS_TAC `{x | x IN u /\ (f:A->B) x IN t}` THEN ASM SET_TAC[]]);;
2757 let SURJECTIVE_IMAGE = prove
2758 (`!f:A->B. (!t. ?s. IMAGE f s = t) <=> (!y. ?x. f x = y)`,
2760 MP_TAC(ISPECL [`f:A->B`; `(:A)`; `(:B)`] SURJECTIVE_ON_IMAGE) THEN
2761 REWRITE_TAC[IN_UNIV; SUBSET_UNIV]);;
2763 (* ------------------------------------------------------------------------- *)
2764 (* Existence of bijections between two finite sets of same size. *)
2765 (* ------------------------------------------------------------------------- *)
2767 let CARD_EQ_BIJECTION = prove
2768 (`!s t. FINITE s /\ FINITE t /\ CARD s = CARD t
2769 ==> ?f:A->B. (!x. x IN s ==> f(x) IN t) /\
2770 (!y. y IN t ==> ?x. x IN s /\ f x = y) /\
2771 !x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y)`,
2772 MP_TAC CARD_LE_INJ THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
2773 DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
2774 ASM_REWRITE_TAC[LE_REFL] THEN MATCH_MP_TAC MONO_EXISTS THEN
2775 ASM_SIMP_TAC[SURJECTIVE_IFF_INJECTIVE_GEN] THEN
2776 MESON_TAC[SUBSET; IN_IMAGE]);;
2778 let CARD_EQ_BIJECTIONS = prove
2779 (`!s t. FINITE s /\ FINITE t /\ CARD s = CARD t
2780 ==> ?f:A->B g. (!x. x IN s ==> f(x) IN t /\ g(f x) = x) /\
2781 (!y. y IN t ==> g(y) IN s /\ f(g y) = y)`,
2782 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CARD_EQ_BIJECTION) THEN
2783 MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[SURJECTIVE_ON_RIGHT_INVERSE] THEN
2784 GEN_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
2785 MATCH_MP_TAC MONO_EXISTS THEN MESON_TAC[]);;
2787 let BIJECTIONS_HAS_SIZE = prove
2789 (!x. x IN s ==> f(x) IN t /\ g(f x) = x) /\
2790 (!y. y IN t ==> g(y) IN s /\ f(g y) = y) /\
2793 REPEAT STRIP_TAC THEN SUBGOAL_THEN `t = IMAGE (f:A->B) s` SUBST_ALL_TAC THENL
2795 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_MESON_TAC[]]);;
2797 let BIJECTIONS_HAS_SIZE_EQ = prove
2799 (!x. x IN s ==> f(x) IN t /\ g(f x) = x) /\
2800 (!y. y IN t ==> g(y) IN s /\ f(g y) = y)
2801 ==> !n. s HAS_SIZE n <=> t HAS_SIZE n`,
2802 REPEAT STRIP_TAC THEN EQ_TAC THEN
2803 MATCH_MP_TAC(ONCE_REWRITE_RULE
2804 [TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`] BIJECTIONS_HAS_SIZE) THENL
2805 [MAP_EVERY EXISTS_TAC [`f:A->B`; `g:B->A`];
2806 MAP_EVERY EXISTS_TAC [`g:B->A`; `f:A->B`]] THEN
2809 let BIJECTIONS_CARD_EQ = prove
2811 (FINITE s \/ FINITE t) /\
2812 (!x. x IN s ==> f(x) IN t /\ g(f x) = x) /\
2813 (!y. y IN t ==> g(y) IN s /\ f(g y) = y)
2814 ==> CARD s = CARD t`,
2815 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
2816 MP_TAC (MP_TAC o MATCH_MP BIJECTIONS_HAS_SIZE_EQ)) THEN
2817 MESON_TAC[HAS_SIZE]);;
2819 (* ------------------------------------------------------------------------- *)
2820 (* Transitive relation with finitely many predecessors is wellfounded. *)
2821 (* ------------------------------------------------------------------------- *)
2823 let WF_FINITE = prove
2824 (`!(<<). (!x. ~(x << x)) /\ (!x y z. x << y /\ y << z ==> x << z) /\
2825 (!x:A. FINITE {y | y << x})
2827 REPEAT STRIP_TAC THEN REWRITE_TAC[WF_DCHAIN] THEN
2828 DISCH_THEN(X_CHOOSE_THEN `s:num->A` STRIP_ASSUME_TAC) THEN
2829 SUBGOAL_THEN `!m n. m < n ==> (s:num->A) n << s m` ASSUME_TAC THENL
2830 [MATCH_MP_TAC TRANSITIVE_STEPWISE_LT THEN ASM_MESON_TAC[]; ALL_TAC] THEN
2831 MP_TAC(ISPEC `s:num->A` INFINITE_IMAGE_INJ) THEN ANTS_TAC THENL
2832 [ASM_MESON_TAC[LT_CASES]; ALL_TAC] THEN
2833 DISCH_THEN(MP_TAC o SPEC `(:num)`) THEN
2834 REWRITE_TAC[num_INFINITE] THEN REWRITE_TAC[INFINITE] THEN
2835 MATCH_MP_TAC FINITE_SUBSET THEN
2836 EXISTS_TAC `s(0) INSERT {y:A | y << s(0)}` THEN
2837 ASM_REWRITE_TAC[FINITE_INSERT] THEN
2838 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_INSERT] THEN
2839 INDUCT_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[LT_0]);;
2841 (* ------------------------------------------------------------------------- *)
2842 (* Cardinal comparisons (more theory in Examples/card.ml) *)
2843 (* ------------------------------------------------------------------------- *)
2845 let le_c = new_definition
2846 `s <=_c t <=> ?f. (!x. x IN s ==> f(x) IN t) /\
2847 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y))`;;
2849 let lt_c = new_definition
2850 `s <_c t <=> s <=_c t /\ ~(t <=_c s)`;;
2852 let eq_c = new_definition
2853 `s =_c t <=> ?f. (!x. x IN s ==> f(x) IN t) /\
2854 !y. y IN t ==> ?!x. x IN s /\ (f x = y)`;;
2856 let ge_c = new_definition
2857 `s >=_c t <=> t <=_c s`;;
2859 let gt_c = new_definition
2860 `s >_c t <=> t <_c s`;;
2863 (`!s t. s <=_c t <=> ?g. !x. x IN s ==> ?y. y IN t /\ (g y = x)`,
2864 REWRITE_TAC[le_c; INJECTIVE_ON_LEFT_INVERSE; SURJECTIVE_ON_RIGHT_INVERSE;
2865 RIGHT_IMP_EXISTS_THM; SKOLEM_THM; RIGHT_AND_EXISTS_THM] THEN
2869 (`!s t. s >=_c t <=> ?f. !y. y IN t ==> ?x. x IN s /\ (y = f x)`,
2870 REWRITE_TAC[ge_c; LE_C] THEN MESON_TAC[]);;
2872 let COUNTABLE = new_definition
2873 `COUNTABLE t <=> (:num) >=_c t`;;
2875 (* ------------------------------------------------------------------------- *)
2876 (* Supremum and infimum. *)
2877 (* ------------------------------------------------------------------------- *)
2879 let sup = new_definition
2880 `sup s = @a:real. (!x. x IN s ==> x <= a) /\
2881 !b. (!x. x IN s ==> x <= b) ==> a <= b`;;
2884 (`!s t. (!b. (!x. x IN s ==> x <= b) <=> (!x. x IN t ==> x <= b))
2889 (`!s. ~(s = {}) /\ (?b. !x. x IN s ==> x <= b)
2890 ==> (!x. x IN s ==> x <= sup s) /\
2891 !b. (!x. x IN s ==> x <= b) ==> sup s <= b`,
2892 REWRITE_TAC[sup] THEN CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN
2893 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_COMPLETE THEN
2894 ASM_MESON_TAC[MEMBER_NOT_EMPTY]);;
2896 let SUP_FINITE_LEMMA = prove
2897 (`!s. FINITE s /\ ~(s = {}) ==> ?b:real. b IN s /\ !x. x IN s ==> x <= b`,
2898 REWRITE_TAC[IMP_CONJ] THEN
2899 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2900 REWRITE_TAC[NOT_INSERT_EMPTY; IN_INSERT] THEN
2901 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2902 MESON_TAC[REAL_LE_TOTAL; REAL_LE_TRANS]);;
2904 let SUP_FINITE = prove
2905 (`!s. FINITE s /\ ~(s = {}) ==> (sup s) IN s /\ !x. x IN s ==> x <= sup s`,
2906 GEN_TAC THEN DISCH_TAC THEN
2907 FIRST_ASSUM(MP_TAC o MATCH_MP SUP_FINITE_LEMMA) THEN
2908 ASM_MESON_TAC[REAL_LE_ANTISYM; REAL_LE_TOTAL; SUP]);;
2910 let REAL_LE_SUP_FINITE = prove
2911 (`!s a. FINITE s /\ ~(s = {}) ==> (a <= sup s <=> ?x. x IN s /\ a <= x)`,
2912 MESON_TAC[SUP_FINITE; REAL_LE_TRANS]);;
2914 let REAL_SUP_LE_FINITE = prove
2915 (`!s a. FINITE s /\ ~(s = {}) ==> (sup s <= a <=> !x. x IN s ==> x <= a)`,
2916 MESON_TAC[SUP_FINITE; REAL_LE_TRANS]);;
2918 let REAL_LT_SUP_FINITE = prove
2919 (`!s a. FINITE s /\ ~(s = {}) ==> (a < sup s <=> ?x. x IN s /\ a < x)`,
2920 MESON_TAC[SUP_FINITE; REAL_LTE_TRANS]);;
2922 let REAL_SUP_LT_FINITE = prove
2923 (`!s a. FINITE s /\ ~(s = {}) ==> (sup s < a <=> !x. x IN s ==> x < a)`,
2924 MESON_TAC[SUP_FINITE; REAL_LET_TRANS]);;
2926 let REAL_SUP_UNIQUE = prove
2927 (`!s b. (!x. x IN s ==> x <= b) /\
2928 (!b'. b' < b ==> ?x. x IN s /\ b' < x)
2930 REPEAT STRIP_TAC THEN REWRITE_TAC[sup] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
2931 ASM_MESON_TAC[REAL_NOT_LE; REAL_LE_ANTISYM]);;
2933 let REAL_SUP_LE = prove
2934 (`!b. ~(s = {}) /\ (!x. x IN s ==> x <= b) ==> sup s <= b`,
2937 let REAL_SUP_LE_SUBSET = prove
2938 (`!s t. ~(s = {}) /\ s SUBSET t /\ (?b. !x. x IN t ==> x <= b)
2939 ==> sup s <= sup t`,
2940 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_SUP_LE THEN
2941 MP_TAC(SPEC `t:real->bool` SUP) THEN ASM SET_TAC[]);;
2943 let REAL_SUP_BOUNDS = prove
2944 (`!s a b. ~(s = {}) /\ (!x. x IN s ==> a <= x /\ x <= b)
2945 ==> a <= sup s /\ sup s <= b`,
2946 REPEAT GEN_TAC THEN STRIP_TAC THEN
2947 MP_TAC(SPEC `s:real->bool` SUP) THEN ANTS_TAC THENL
2948 [ASM_MESON_TAC[]; ALL_TAC] THEN
2949 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
2950 ASM_MESON_TAC[REAL_LE_TRANS]);;
2952 let REAL_ABS_SUP_LE = prove
2953 (`!s a. ~(s = {}) /\ (!x. x IN s ==> abs(x) <= a) ==> abs(sup s) <= a`,
2954 REWRITE_TAC[GSYM REAL_BOUNDS_LE; REAL_SUP_BOUNDS]);;
2956 let REAL_SUP_ASCLOSE = prove
2957 (`!s l e. ~(s = {}) /\ (!x. x IN s ==> abs(x - l) <= e)
2958 ==> abs(sup s - l) <= e`,
2959 SIMP_TAC[REAL_ARITH `abs(x - l):real <= e <=> l - e <= x /\ x <= l + e`] THEN
2960 REWRITE_TAC[REAL_SUP_BOUNDS]);;
2962 let inf = new_definition
2963 `inf s = @a:real. (!x. x IN s ==> a <= x) /\
2964 !b. (!x. x IN s ==> b <= x) ==> b <= a`;;
2967 (`!s t. (!a. (!x. x IN s ==> a <= x) <=> (!x. x IN t ==> a <= x))
2972 (`!s. ~(s = {}) /\ (?b. !x. x IN s ==> b <= x)
2973 ==> (!x. x IN s ==> inf s <= x) /\
2974 !b. (!x. x IN s ==> b <= x) ==> b <= inf s`,
2975 GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[inf] THEN
2976 CONV_TAC(ONCE_DEPTH_CONV SELECT_CONV) THEN
2977 ONCE_REWRITE_TAC[GSYM REAL_LE_NEG2] THEN
2978 EXISTS_TAC `--(sup (IMAGE (--) s))` THEN
2979 MP_TAC(SPEC `IMAGE (--) (s:real->bool)` SUP) THEN
2980 REWRITE_TAC[REAL_NEG_NEG] THEN
2981 ABBREV_TAC `a = sup (IMAGE (--) s)` THEN
2982 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_IMAGE] THEN
2983 ASM_MESON_TAC[REAL_NEG_NEG; MEMBER_NOT_EMPTY; REAL_LE_NEG2]);;
2985 let INF_FINITE_LEMMA = prove
2986 (`!s. FINITE s /\ ~(s = {}) ==> ?b:real. b IN s /\ !x. x IN s ==> b <= x`,
2987 REWRITE_TAC[IMP_CONJ] THEN
2988 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2989 REWRITE_TAC[NOT_INSERT_EMPTY; IN_INSERT] THEN
2990 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN
2991 MESON_TAC[REAL_LE_TOTAL; REAL_LE_TRANS]);;
2993 let INF_FINITE = prove
2994 (`!s. FINITE s /\ ~(s = {}) ==> (inf s) IN s /\ !x. x IN s ==> inf s <= x`,
2995 GEN_TAC THEN DISCH_TAC THEN
2996 FIRST_ASSUM(MP_TAC o MATCH_MP INF_FINITE_LEMMA) THEN
2997 ASM_MESON_TAC[REAL_LE_ANTISYM; REAL_LE_TOTAL; INF]);;
2999 let REAL_LE_INF_FINITE = prove
3000 (`!s a. FINITE s /\ ~(s = {}) ==> (a <= inf s <=> !x. x IN s ==> a <= x)`,
3001 MESON_TAC[INF_FINITE; REAL_LE_TRANS]);;
3003 let REAL_INF_LE_FINITE = prove
3004 (`!s a. FINITE s /\ ~(s = {}) ==> (inf s <= a <=> ?x. x IN s /\ x <= a)`,
3005 MESON_TAC[INF_FINITE; REAL_LE_TRANS]);;
3007 let REAL_LT_INF_FINITE = prove
3008 (`!s a. FINITE s /\ ~(s = {}) ==> (a < inf s <=> !x. x IN s ==> a < x)`,
3009 MESON_TAC[INF_FINITE; REAL_LTE_TRANS]);;
3011 let REAL_INF_LT_FINITE = prove
3012 (`!s a. FINITE s /\ ~(s = {}) ==> (inf s < a <=> ?x. x IN s /\ x < a)`,
3013 MESON_TAC[INF_FINITE; REAL_LET_TRANS]);;
3015 let REAL_INF_UNIQUE = prove
3016 (`!s b. (!x. x IN s ==> b <= x) /\
3017 (!b'. b < b' ==> ?x. x IN s /\ x < b')
3019 REPEAT STRIP_TAC THEN REWRITE_TAC[inf] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
3020 ASM_MESON_TAC[REAL_NOT_LE; REAL_LE_ANTISYM]);;
3022 let REAL_LE_INF = prove
3023 (`!b. ~(s = {}) /\ (!x. x IN s ==> b <= x) ==> b <= inf s`,
3026 let REAL_LE_INF_SUBSET = prove
3027 (`!s t. ~(t = {}) /\ t SUBSET s /\ (?b. !x. x IN s ==> b <= x)
3028 ==> inf s <= inf t`,
3029 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_INF THEN
3030 MP_TAC(SPEC `s:real->bool` INF) THEN ASM SET_TAC[]);;
3032 let REAL_INF_BOUNDS = prove
3033 (`!s a b. ~(s = {}) /\ (!x. x IN s ==> a <= x /\ x <= b)
3034 ==> a <= inf s /\ inf s <= b`,
3035 REPEAT GEN_TAC THEN STRIP_TAC THEN
3036 MP_TAC(SPEC `s:real->bool` INF) THEN ANTS_TAC THENL
3037 [ASM_MESON_TAC[]; ALL_TAC] THEN
3038 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
3039 ASM_MESON_TAC[REAL_LE_TRANS]);;
3041 let REAL_ABS_INF_LE = prove
3042 (`!s a. ~(s = {}) /\ (!x. x IN s ==> abs(x) <= a) ==> abs(inf s) <= a`,
3043 REWRITE_TAC[GSYM REAL_BOUNDS_LE; REAL_INF_BOUNDS]);;
3045 let REAL_INF_ASCLOSE = prove
3046 (`!s l e. ~(s = {}) /\ (!x. x IN s ==> abs(x - l) <= e)
3047 ==> abs(inf s - l) <= e`,
3048 SIMP_TAC[REAL_ARITH `abs(x - l):real <= e <=> l - e <= x /\ x <= l + e`] THEN
3049 REWRITE_TAC[REAL_INF_BOUNDS]);;
3051 let SUP_UNIQUE_FINITE = prove
3052 (`!s. FINITE s /\ ~(s = {})
3053 ==> (sup s = a <=> a IN s /\ !y. y IN s ==> y <= a)`,
3054 ASM_SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_LE_SUP_FINITE; REAL_SUP_LE_FINITE;
3055 NOT_INSERT_EMPTY; FINITE_INSERT; FINITE_EMPTY] THEN
3056 MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS; REAL_LE_ANTISYM]);;
3058 let INF_UNIQUE_FINITE = prove
3059 (`!s. FINITE s /\ ~(s = {})
3060 ==> (inf s = a <=> a IN s /\ !y. y IN s ==> a <= y)`,
3061 ASM_SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_LE_INF_FINITE; REAL_INF_LE_FINITE;
3062 NOT_INSERT_EMPTY; FINITE_INSERT; FINITE_EMPTY] THEN
3063 MESON_TAC[REAL_LE_REFL; REAL_LE_TRANS; REAL_LE_ANTISYM]);;
3065 let SUP_INSERT_FINITE = prove
3066 (`!x s. FINITE s ==> sup(x INSERT s) = if s = {} then x else max x (sup s)`,
3067 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
3068 ASM_SIMP_TAC[SUP_UNIQUE_FINITE; FINITE_INSERT; FINITE_EMPTY;
3069 NOT_INSERT_EMPTY; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
3070 REWRITE_TAC[IN_SING; REAL_LE_REFL] THEN
3071 REWRITE_TAC[real_max] THEN COND_CASES_TAC THEN
3072 ASM_SIMP_TAC[SUP_FINITE; IN_INSERT; REAL_LE_REFL] THEN
3073 ASM_MESON_TAC[SUP_FINITE; REAL_LE_TOTAL; REAL_LE_TRANS]);;
3075 let SUP_SING = prove
3077 SIMP_TAC[SUP_INSERT_FINITE; FINITE_EMPTY]);;
3079 let INF_INSERT_FINITE = prove
3080 (`!x s. FINITE s ==> inf(x INSERT s) = if s = {} then x else min x (inf s)`,
3081 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
3082 ASM_SIMP_TAC[INF_UNIQUE_FINITE; FINITE_INSERT; FINITE_EMPTY;
3083 NOT_INSERT_EMPTY; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
3084 REWRITE_TAC[IN_SING; REAL_LE_REFL] THEN
3085 REWRITE_TAC[real_min] THEN COND_CASES_TAC THEN
3086 ASM_SIMP_TAC[INF_FINITE; IN_INSERT; REAL_LE_REFL] THEN
3087 ASM_MESON_TAC[INF_FINITE; REAL_LE_TOTAL; REAL_LE_TRANS]);;
3089 let INF_SING = prove
3091 SIMP_TAC[INF_INSERT_FINITE; FINITE_EMPTY]);;
3093 let REAL_SUP_EQ_INF = prove
3094 (`!s. ~(s = {}) /\ (?B. !x. x IN s ==> abs(x) <= B)
3095 ==> (sup s = inf s <=> ?a. s = {a})`,
3096 REPEAT STRIP_TAC THEN EQ_TAC THENL
3097 [DISCH_TAC THEN EXISTS_TAC `sup s` THEN MATCH_MP_TAC
3098 (SET_RULE `~(s = {}) /\ (!x. x IN s ==> x = a) ==> s = {a}`) THEN
3099 ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
3100 ASM_MESON_TAC[SUP; REAL_ABS_BOUNDS; INF];
3102 ASM_SIMP_TAC[SUP_INSERT_FINITE; INF_INSERT_FINITE; FINITE_EMPTY]]);;
3104 let REAL_LE_SUP = prove
3105 (`!s a b y. y IN s /\ a <= y /\ (!x. x IN s ==> x <= b) ==> a <= sup s`,
3106 MESON_TAC[SUP; MEMBER_NOT_EMPTY; REAL_LE_TRANS]);;
3108 let REAL_INF_LE = prove
3109 (`!s a b y. y IN s /\ y <= b /\ (!x. x IN s ==> a <= x) ==> inf s <= b`,
3110 MESON_TAC[INF; MEMBER_NOT_EMPTY; REAL_LE_TRANS]);;
3112 let REAL_SUP_LE_EQ = prove
3113 (`!s y. ~(s = {}) /\ (?b. !x. x IN s ==> x <= b)
3114 ==> (sup s <= y <=> !x. x IN s ==> x <= y)`,
3115 MESON_TAC[SUP; REAL_LE_TRANS]);;
3117 let REAL_LE_INF_EQ = prove
3118 (`!s t. ~(s = {}) /\ (?b. !x. x IN s ==> b <= x)
3119 ==> (y <= inf s <=> !x. x IN s ==> y <= x)`,
3120 MESON_TAC[INF; REAL_LE_TRANS]);;
3122 let SUP_UNIQUE = prove
3123 (`!s b. (!c. (!x. x IN s ==> x <= c) <=> b <= c) ==> sup s = b`,
3124 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM SUP_SING] THEN
3125 MATCH_MP_TAC SUP_EQ THEN ASM SET_TAC[]);;
3127 let INF_UNIQUE = prove
3128 (`!s b. (!c. (!x. x IN s ==> c <= x) <=> c <= b) ==> inf s = b`,
3129 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM INF_SING] THEN
3130 MATCH_MP_TAC INF_EQ THEN ASM SET_TAC[]);;
3132 let SUP_UNION = prove
3133 (`!s t. ~(s = {}) /\ ~(t = {}) /\
3134 (?b. !x. x IN s ==> x <= b) /\ (?c. !x. x IN t ==> x <= c)
3135 ==> sup(s UNION t) = max (sup s) (sup t)`,
3136 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUP_UNIQUE THEN
3137 REWRITE_TAC[FORALL_IN_UNION; REAL_MAX_LE] THEN
3138 ASM_MESON_TAC[SUP; REAL_LE_TRANS]);;
3140 let INF_UNION = prove
3141 (`!s t. ~(s = {}) /\ ~(t = {}) /\
3142 (?b. !x. x IN s ==> b <= x) /\ (?c. !x. x IN t ==> c <= x)
3143 ==> inf(s UNION t) = min (inf s) (inf t)`,
3144 REPEAT STRIP_TAC THEN MATCH_MP_TAC INF_UNIQUE THEN
3145 REWRITE_TAC[FORALL_IN_UNION; REAL_LE_MIN] THEN
3146 ASM_MESON_TAC[INF; REAL_LE_TRANS]);;
3148 (* ------------------------------------------------------------------------- *)
3149 (* Inductive definition of sets, by reducing them to inductive relations. *)
3150 (* ------------------------------------------------------------------------- *)
3152 let new_inductive_set =
3153 let const_of_var v = mk_mconst(name_of v,type_of v) in
3155 let rec f (n:int) (tm:term) : hol_type list -> term = function
3158 let v = variant (variables tm) (mk_var("x"^string_of_int n,ty)) in
3159 f (n+1) (mk_comb(tm,v)) tys in
3160 fun tm -> let tys = fst (splitlist dest_fun_ty (type_of tm)) in
3162 let mk_eqin = REWR_CONV (GSYM IN) o comb_all in
3163 let transf conv = rhs o concl o conv in
3164 let remove_in_conv ptm : conv =
3165 let rconv = REWR_CONV(SYM(mk_eqin ptm)) in
3166 fun tm -> let htm = fst(strip_comb(snd(dest_binary "IN" tm))) in
3167 if htm = ptm then rconv tm else fail() in
3168 let remove_in_transf =
3169 transf o ONCE_DEPTH_CONV o FIRST_CONV o map remove_in_conv in
3171 let tm = snd(strip_forall tm) in
3172 let tm = snd(splitlist(dest_binop `(==>)`) tm) in
3173 let tm = snd(dest_binary "IN" tm) in
3174 fst(strip_comb tm) in
3175 let find_pvars = setify o map rule_head o binops `(/\)` in
3177 let pvars = find_pvars tm in
3178 let dtm = remove_in_transf pvars tm in
3179 let th_rules, th_induct, th_cases = new_inductive_definition dtm in
3180 let insert_in_rule = REWRITE_RULE(map (mk_eqin o const_of_var) pvars) in
3181 insert_in_rule th_rules,
3182 insert_in_rule th_induct,
3183 insert_in_rule th_cases;;