1 (* ========================================================================= *)
2 (* Theorem 3: countability of rational numbers. *)
3 (* ========================================================================= *)
5 needs "Library/card.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* Definition of rational and countable. *)
11 (* ------------------------------------------------------------------------- *)
13 let rational = new_definition
14 `rational(r) <=> ?p q. ~(q = 0) /\ (abs(r) = &p / &q)`;;
16 let countable = new_definition
17 `countable s <=> s <=_c (UNIV:num->bool)`;;
19 (* ------------------------------------------------------------------------- *)
20 (* Proof of the main result. *)
21 (* ------------------------------------------------------------------------- *)
23 let COUNTABLE_RATIONALS = prove
24 (`countable { x:real | rational(x)}`,
25 REWRITE_TAC[countable] THEN TRANS_TAC CARD_LE_TRANS
26 `{ x:real | ?p q. x = &p / &q } *_c (UNIV:num->bool)` THEN
28 [REWRITE_TAC[LE_C; EXISTS_PAIR_THM; mul_c] THEN
29 EXISTS_TAC `\(x,b). if b = 0 then x else --x` THEN
30 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
31 REWRITE_TAC[IN_ELIM_THM; rational; IN_UNIV; PAIR_EQ] THEN
32 MESON_TAC[REAL_ARITH `(abs(x) = a) ==> (x = a) \/ x = --a`];
34 MATCH_MP_TAC CARD_MUL_ABSORB_LE THEN REWRITE_TAC[num_INFINITE] THEN
35 TRANS_TAC CARD_LE_TRANS `(UNIV *_c UNIV):num#num->bool` THEN CONJ_TAC THENL
36 [REWRITE_TAC[LE_C; EXISTS_PAIR_THM; mul_c; IN_UNIV] THEN
37 EXISTS_TAC `\(p,q). &p / &q` THEN
38 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
39 REWRITE_TAC[IN_ELIM_THM; rational] THEN MESON_TAC[];
40 MESON_TAC[CARD_MUL_ABSORB_LE; CARD_LE_REFL; num_INFINITE]]);;
42 (* ------------------------------------------------------------------------- *)
43 (* Maybe I should actually prove equality? *)
44 (* ------------------------------------------------------------------------- *)
46 let denumerable = new_definition
47 `denumerable s <=> s =_c (UNIV:num->bool)`;;
49 let DENUMERABLE_RATIONALS = prove
50 (`denumerable { x:real | rational(x)}`,
51 REWRITE_TAC[denumerable; GSYM CARD_LE_ANTISYM] THEN
52 REWRITE_TAC[GSYM countable; COUNTABLE_RATIONALS] THEN
53 REWRITE_TAC[le_c] THEN EXISTS_TAC `&` THEN
54 SIMP_TAC[IN_ELIM_THM; IN_UNIV; REAL_OF_NUM_EQ; rational] THEN
55 X_GEN_TAC `p:num` THEN MAP_EVERY EXISTS_TAC [`p:num`; `1`] THEN
56 REWRITE_TAC[REAL_DIV_1; REAL_ABS_NUM; ARITH_EQ]);;
58 (* ------------------------------------------------------------------------- *)
59 (* Expand out the cardinal comparison definitions for explicitness. *)
60 (* ------------------------------------------------------------------------- *)
62 let DENUMERABLE_RATIONALS_EXPAND = prove
63 (`?rat:num->real. (!n. rational(rat n)) /\
64 (!x. rational x ==> ?!n. x = rat n)`,
65 MP_TAC DENUMERABLE_RATIONALS THEN REWRITE_TAC[denumerable] THEN
66 ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[eq_c] THEN
67 REWRITE_TAC[IN_UNIV; IN_ELIM_THM] THEN
68 MATCH_MP_TAC MONO_EXISTS THEN MESON_TAC[]);;