Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 22 Apr 1994 14:21:35 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA07044; Fri, 22 Apr 1994 06:48:56 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA07040; Fri, 22 Apr 1994 06:48:40 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA27596; Fri, 22 Apr 1994 05:48:36 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 22 Apr 1994 13:47:37 +0100 To: info-hol@cs.uidaho.edu Subject: Theory of countable sets Date: Fri, 22 Apr 94 13:47:29 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:014690:940422124743"@cl.cam.ac.uk> Here is a small theory of countable sets, which people may find useful. It's built on top of the "pred_sets" library, but it could equally well use "sets". The theory begins by defining arbitrary intersections and unions, then gives a definition of countability and a few simple theorems. If anyone has suggestions for other useful theorems, let me know and I'll consider installing a more coherent and complete version of the theory in the standard libraries. Possibly this theory should be subsumed by a more general theory about the relative sizes of sets. John. %============================================================================% % Theory of countable sets. % %============================================================================% can unlink `COUNT.th`;; new_theory `COUNT`;; load_library `pred_sets`;; let LAND_CONV = RATOR_CONV o RAND_CONV;; let IMP_RES_THEN ttac th = FIRST_ASSUM(\t. ttac (MATCH_MP th t));; %----------------------------------------------------------------------------% % Prove that we have an injective function N x N -> N (needed below). % %----------------------------------------------------------------------------% let EXP_1 = prove_thm(`EXP_1`, "!n. n EXP 1 = n", REWRITE_TAC[num_CONV "1"; EXP; MULT_CLAUSES; ADD_CLAUSES]);; let EXP_MONO = prove_thm(`EXP_MONO`, "!n m p. ((2 EXP m) * n = (2 EXP m) * p) = (n = p)", ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[num_CONV "2"; MULT_EXP_MONO]);; let EVEN_2 = prove_thm(`EVEN_2`, "EVEN 2", REWRITE_TAC[EVEN_EXISTS] THEN EXISTS_TAC "1" THEN REWRITE_TAC[MULT_CLAUSES]);; let PAIRING_INJ = prove_thm(`PAIRING_INJ`, "!x y u v. ((2 EXP x) * ((2 * y) + 1) = (2 EXP u) * ((2 * v) + 1)) = (x = u) /\ (y = v)", REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN "x:num = u" ASSUME_TAC THENL [MATCH_MP_TAC LESS_EQUAL_ANTISYM THEN POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM; NOT_LESS_EQUAL] THEN DISCH_THEN (DISJ_CASES_THEN (X_CHOOSE_TAC "d:num" o MATCH_MP LESS_ADD_1)) THEN ASM_REWRITE_TAC[EXP_ADD; GSYM MULT_ASSOC; EXP_MONO; EXP_1] THEN DISCH_THEN(MP_TAC o AP_TERM "EVEN") THEN REWRITE_TAC[EVEN_MULT; EVEN_2; GSYM ODD_EVEN; GSYM ADD1; ODD_DOUBLE]; UNDISCH_TAC "x:num = u" THEN DISCH_THEN SUBST_ALL_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[EXP_MONO; GSYM ADD1; INV_SUC_EQ] THEN REWRITE_TAC[MULT_MONO_EQ; num_CONV "2"]]);; %----------------------------------------------------------------------------% % Arbitrary union. % %----------------------------------------------------------------------------% let UNIONS = new_definition(`UNIONS`, "UNIONS (s:(*->bool)->bool) = { x | ?p. p IN s /\ x IN p }");; let UNIONS_0 = prove_thm(`UNIONS_0`, "UNIONS {} = {} :*->bool", REWRITE_TAC[UNIONS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[NOT_IN_EMPTY]);; let UNIONS_1 = prove_thm(`UNIONS_1`, "!s:*->bool. UNIONS {s} = s", REWRITE_TAC[UNIONS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_SING] THEN REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC "s:*->bool" THEN ASM_REWRITE_TAC[]);; let UNIONS_2 = prove_thm(`UNIONS_2`, "!(s:*->bool) t. UNIONS {s,t} = s UNION t", REWRITE_TAC[UNIONS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_INSERT; IN_SING; IN_UNION] THEN REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC[] THEN W(EXISTS_TAC o rand o hd o fst) THEN ASM_REWRITE_TAC[]);; let IN_UNIONS = prove_thm(`IN_UNIONS`, "!(x:*) G. x IN (UNIONS G) = ?s. x IN s /\ s IN G", REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN MATCH_ACCEPT_TAC CONJ_SYM);; %----------------------------------------------------------------------------% % Arbitrary intersection. % %----------------------------------------------------------------------------% let INTERS = new_definition(`INTERS`, "INTERS(s:(*->bool)->bool) = { x | !p. p IN s ==> x IN p }");; let INTERS_0 = prove_thm(`INTERS_0`, "INTERS {} = UNIV :*->bool", REWRITE_TAC[INTERS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_UNIV; NOT_IN_EMPTY]);; let INTERS_1 = prove_thm(`INTERS_1`, "!s:*->bool. INTERS {s} = s", REWRITE_TAC[INTERS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_SING] THEN REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN REFL_TAC);; let INTERS_2 = prove_thm(`INTERS_2`, "!(s:*->bool) t. INTERS {s,t} = s INTER t", REWRITE_TAC[INTERS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_INSERT; IN_SING; IN_INTER] THEN REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[]);; let IN_INTERS = prove_thm(`IN_INTERS`, "!(x:*) G. x IN (INTERS G) = !s. s IN G ==> x IN s", REPEAT GEN_TAC THEN REWRITE_TAC[INTERS] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC);; let INTERS_SUBSET = prove_thm(`INTERS_SUBSET`, "!X (s:*->bool). s IN X ==> (INTERS X) SUBSET s", REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET_DEF; IN_INTERS] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);; %----------------------------------------------------------------------------% % Definition of "countable" via surjection. % %----------------------------------------------------------------------------% let COUNTABLE = new_definition(`COUNTABLE`, "COUNTABLE(s) = ?f:num->*. !x. x IN s ==> ?n. f(n) = x");; %----------------------------------------------------------------------------% % Countability of finite sets. % %----------------------------------------------------------------------------% let COUNTABLE_EMPTY = prove_thm(`COUNTABLE_EMPTY`, "COUNTABLE ({}:*->bool)", REWRITE_TAC[COUNTABLE; NOT_IN_EMPTY]);; let COUNTABLE_INSERT = prove_thm(`COUNTABLE_INSERT`, "!(x:*) s. COUNTABLE(s) ==> COUNTABLE(x INSERT s)", REPEAT GEN_TAC THEN REWRITE_TAC[COUNTABLE] THEN DISCH_THEN(X_CHOOSE_TAC "f:num->*") THEN EXISTS_TAC "\n. (n = 0) => (x:*) | f(n - 1)" THEN GEN_TAC THEN REWRITE_TAC[IN_INSERT] THEN BETA_TAC THEN DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC (ANTE_RES_THEN MP_TAC)) THENL [EXISTS_TAC "0" THEN REWRITE_TAC[]; DISCH_THEN(X_CHOOSE_TAC "n:num") THEN EXISTS_TAC "SUC n" THEN ASM_REWRITE_TAC[SUC_SUB1; NOT_SUC]]);; let COUNTABLE_FINITE = prove_thm(`COUNTABLE_FINITE`, "!s:*->bool. FINITE(s) ==> COUNTABLE(s)", SET_INDUCT_TAC THEN REWRITE_TAC[COUNTABLE_EMPTY] THEN MATCH_MP_TAC COUNTABLE_INSERT THEN ASM_REWRITE_TAC[]);; %----------------------------------------------------------------------------% % Countability of the natural numbers (obviously). % %----------------------------------------------------------------------------% let COUNTABLE_NUM = prove_thm(`COUNTABLE_NUM`, "COUNTABLE(UNIV:num->bool)", REWRITE_TAC[COUNTABLE] THEN EXISTS_TAC "\x:num. x" THEN BETA_TAC THEN X_GEN_TAC "n:num" THEN DISCH_TAC THEN EXISTS_TAC "n:num" THEN REFL_TAC);; %----------------------------------------------------------------------------% % Any subset of a countable set is countable. % %----------------------------------------------------------------------------% let COUNTABLE_SUBSET = prove_thm(`COUNTABLE_SUBSET`, "!(s:*->bool) t. COUNTABLE(t) /\ s SUBSET t ==> COUNTABLE s", REPEAT GEN_TAC THEN REWRITE_TAC[COUNTABLE; SUBSET_DEF] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "f:num->*") ASSUME_TAC) THEN EXISTS_TAC "f:num->*" THEN REPEAT STRIP_TAC THEN REPEAT(FIRST_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);; %----------------------------------------------------------------------------% % Countability of N x N % %----------------------------------------------------------------------------% let COUNTABLE_NxN = prove_thm(`COUNTABLE_NxN`, "COUNTABLE(UNIV:num#num->bool)", REWRITE_TAC[COUNTABLE] THEN EXISTS_TAC "\n:num. @q. (2 EXP (FST q)) * ((2 * (SND q)) + 1) = n" THEN X_GEN_TAC "p:num#num" THEN DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC "(2 EXP (FST p)) * ((2 * (SND p)) + 1)" THEN BETA_TAC THEN REWRITE_TAC[PAIRING_INJ; GSYM PAIR_EQ; PAIR; SELECT_REFL]);; %----------------------------------------------------------------------------% % Countable union of countable sets is countable. % %----------------------------------------------------------------------------% let COUNTABLE_UNIONS = prove_thm(`COUNTABLE_UNIONS`, "!X. COUNTABLE(X) /\ (!s:*->bool. s IN X ==> COUNTABLE(s)) ==> COUNTABLE(UNIONS X)", GEN_TAC THEN REWRITE_TAC[COUNTABLE; IN_UNIONS] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "f:num->(*->bool)") MP_TAC) THEN CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV RIGHT_IMP_EXISTS_CONV)) THEN CONV_TAC(LAND_CONV SKOLEM_CONV) THEN DISCH_THEN(X_CHOOSE_TAC "g:(*->bool)->num->*") THEN MP_TAC(REWRITE_RULE[COUNTABLE; IN_UNIV] COUNTABLE_NxN) THEN DISCH_THEN (X_CHOOSE_TAC "h:num->num#num") THEN EXISTS_TAC "\n:num. (g:(*->bool)->num->*) (f(FST(h n):num)) (SND(h n))" THEN X_GEN_TAC "x:*" THEN BETA_TAC THEN DISCH_THEN(X_CHOOSE_THEN "s:*->bool" STRIP_ASSUME_TAC) THEN FIRST_ASSUM(IMP_RES_THEN (IMP_RES_THEN MP_TAC)) THEN DISCH_THEN(X_CHOOSE_THEN "k:num" (SUBST_ALL_TAC o SYM)) THEN FIRST_ASSUM(IMP_RES_THEN (X_CHOOSE_THEN "l:num" ((SUBST_ALL_TAC o SYM)))) THEN FIRST_ASSUM(X_CHOOSE_TAC "n:num" o SPEC "l:num,k:num") THEN EXISTS_TAC "n:num" THEN ASM_REWRITE_TAC[]);; %----------------------------------------------------------------------------% % And in particular the union of two. % %----------------------------------------------------------------------------% let COUNTABLE_UNION = prove_thm(`COUNTABLE_UNION`, "!(s:*->bool) t. COUNTABLE(s) /\ COUNTABLE(t) ==> COUNTABLE(s UNION t)", REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM UNIONS_2] THEN MATCH_MP_TAC COUNTABLE_UNIONS THEN CONJ_TAC THENL [REPEAT (MATCH_MP_TAC COUNTABLE_INSERT) THEN REWRITE_TAC[COUNTABLE_EMPTY]; GEN_TAC THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THEN ASM_REWRITE_TAC[]]);; %----------------------------------------------------------------------------% % Nonempty intersection of countable sets is countable. % %----------------------------------------------------------------------------% let COUNTABLE_INTERS = prove_thm(`COUNTABLE_INTERS`, "!X. ~(X = {}) /\ (!s:*->bool. s IN X ==> COUNTABLE(s)) ==> COUNTABLE(INTERS X)", GEN_TAC THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "x:*->bool") ASSUME_TAC) THEN MATCH_MP_TAC COUNTABLE_SUBSET THEN EXISTS_TAC "x:*->bool" THEN CONJ_TAC THEN TRY(FIRST_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INTERS_SUBSET THEN ASM_REWRITE_TAC[]);; %----------------------------------------------------------------------------% % And in particular the intersection of two. % %----------------------------------------------------------------------------% let COUNTABLE_INTER = prove_thm(`COUNTABLE_INTER`, "!(s:*->bool) t. COUNTABLE(s) /\ COUNTABLE(t) ==> COUNTABLE(s INTER t)", REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INTERS_2] THEN MATCH_MP_TAC COUNTABLE_INTERS THEN REWRITE_TAC[NOT_INSERT_EMPTY] THEN GEN_TAC THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THEN ASM_REWRITE_TAC[]);; close_theory();;