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