100/ratcountable.ml

   1 (* ========================================================================= *)
   2 (* Theorem 3: countability of rational numbers.                              *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/card.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Definition of rational and countable.                                     *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let rational = new_definition
  14   `rational(r) <=> ?p q. ~(q = 0) /\ (abs(r) = &p / &q)`;;
  15
  16 let countable = new_definition
  17   `countable s <=> s <=_c (UNIV:num->bool)`;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Proof of the main result.                                                 *)
  21 (* ------------------------------------------------------------------------- *)
  22
  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
  27   CONJ_TAC THENL
  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`];
  33     ALL_TAC] THEN
  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]]);;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* Maybe I should actually prove equality?                                   *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let denumerable = new_definition
  47   `denumerable s <=> s =_c (UNIV:num->bool)`;;
  48
  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]);;
  57
  58 (* ------------------------------------------------------------------------- *)
  59 (* Expand out the cardinal comparison definitions for explicitness.          *)
  60 (* ------------------------------------------------------------------------- *)
  61
  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[]);;