(* ========================================================================= *)
(* #22: non-denumerability of continuum (= uncountability of the reals).     *)
(* ========================================================================= *)

needs "Library/card.ml";;

prioritize_real();;

(* ------------------------------------------------------------------------- *)
(* Definition of countability.                                               *)
(* ------------------------------------------------------------------------- *)

let countable = new_definition
  `countable s <=> s <=_c (UNIV:num->bool)`;;
(* ------------------------------------------------------------------------- *)
(* Set of repeating digits and its countability.                             *)
(* ------------------------------------------------------------------------- *)

let repeating = new_definition
 `repeating = {s:num->bool | ?n. !m. m >= n ==> s m}`;;
let BINARY_BOUND = 
prove
(`!n. nsum(0..n) (\i. if b(i) then 2 EXP i else 0) < 2 EXP (n + 1)`,

  INDUCT_TAC THEN REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THENL
   [COND_CASES_TAC THEN REWRITE_TAC[ARITH]; ALL_TAC] THEN
  POP_ASSUM MP_TAC THEN REWRITE_TAC[LE_0; EXP_ADD; EXP_1; EXP] THEN
  ARITH_TAC);;
let BINARY_DIV_POW2 = 
prove
 (`!n. (nsum(0..n) (\i. if b(i) then 2 EXP i else 0)) DIV (2 EXP (SUC n)) = 0`,

  SIMP_TAC[ADD1; DIV_LT; BINARY_BOUND]);;
let PLUS_MOD_REFL = 
prove
 (`!a b. ~(b = 0) ==> (a + b) MOD b = a MOD b`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC MOD_EQ THEN MESON_TAC[MULT_CLAUSES]);;
let BINARY_PLUS_DIV_POW2 = 
prove
 (`!n. (nsum(0..n) (\i. if b(i) then 2 EXP i else 0) + 2 EXP (SUC n))
       DIV (2 EXP (SUC n)) = 1`,

  GEN_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN
  EXISTS_TAC `nsum(0..n) (\i. if b(i) then 2 EXP i else 0)` THEN
  ASM_REWRITE_TAC[BINARY_BOUND; ADD1] THEN
  REWRITE_TAC[ADD_AC; MULT_CLAUSES]);;
let BINARY_UNIQUE_LEMMA = 
prove
 (`!n. nsum(0..n) (\i. if b(i) then 2 EXP i else 0) =
       nsum(0..n) (\i. if c(i) then 2 EXP i else 0)
       ==> !i. i <= n ==> (b(i) <=> c(i))`,

  INDUCT_TAC THEN REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THENL
   [SIMP_TAC[LE] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH]);
    REWRITE_TAC[LE_0]] THEN
  REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THENL
   [UNDISCH_THEN `i = SUC n` SUBST_ALL_TAC THEN
    FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x DIV (2 EXP (SUC n))`) THEN
    REPEAT COND_CASES_TAC THEN
    ASM_REWRITE_TAC[ADD_CLAUSES; BINARY_DIV_POW2; BINARY_PLUS_DIV_POW2] THEN
    REWRITE_TAC[ARITH_EQ];
    FIRST_X_ASSUM(MP_TAC o AP_TERM `\x. x MOD (2 EXP (SUC n))`) THEN
    REPEAT COND_CASES_TAC THEN
    SIMP_TAC[ADD_CLAUSES; BINARY_BOUND; MOD_LT; PLUS_MOD_REFL; EXP_EQ_0; ARITH;
             ADD1] THEN
    ASM_MESON_TAC[LE_REFL]]);;
let COUNTABLE_REPEATING = 
prove
 (`countable repeating`,

  REWRITE_TAC[countable] THEN
  TRANS_TAC CARD_LE_TRANS `(UNIV:num->bool) *_c (UNIV:num->bool)` THEN
  CONJ_TAC THENL
    [ALL_TAC;
     MATCH_MP_TAC CARD_EQ_IMP_LE THEN REWRITE_TAC[CARD_SQUARE_NUM]] THEN
  REWRITE_TAC[le_c] THEN EXISTS_TAC
   `\s:num->bool. let n = minimal n. !m. m >= n ==> s m in
                  n,nsum(0..n) (\i. if s(i) then 2 EXP i else 0)` THEN
  REWRITE_TAC[repeating; IN_ELIM_THM] THEN CONJ_TAC THENL
   [GEN_TAC THEN LET_TAC THEN REWRITE_TAC[mul_c; IN_ELIM_THM; IN_UNIV] THEN
    MESON_TAC[];
    ALL_TAC] THEN
  MAP_EVERY X_GEN_TAC [`s:num->bool`; `t:num->bool`] THEN
  ONCE_REWRITE_TAC[MINIMAL] THEN
  ABBREV_TAC `k = minimal n. !m. m >= n ==> s m` THEN
  ABBREV_TAC `l = minimal n. !m. m >= n ==> t m` THEN
  ASM_REWRITE_TAC[LET_DEF; LET_END_DEF; PAIR_EQ] THEN
  REPEAT(POP_ASSUM(K ALL_TAC)) THEN
  ASM_CASES_TAC `l:num = k` THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[FUN_EQ_THM; GE] THEN
  STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP BINARY_UNIQUE_LEMMA) THEN
  ASM_MESON_TAC[LE_CASES]);;
(* ------------------------------------------------------------------------- *)
(* Canonical digits and their uncountability.                                *)
(* ------------------------------------------------------------------------- *)

let canonical = new_definition
 `canonical = {s:num->bool | !n. ?m. m >= n /\ ~(s m)}`;;
let UNCOUNTABLE_CANONICAL = 
prove
 (`~countable canonical`,

  REWRITE_TAC[countable] THEN STRIP_TAC THEN
  MP_TAC (INST_TYPE [`:num`,`:A`] CANTOR_THM_UNIV) THEN
  REWRITE_TAC[CARD_NOT_LT] THEN
  MP_TAC(ISPECL [`canonical`; `repeating`] CARD_DISJOINT_UNION) THEN
  ANTS_TAC THENL
   [REWRITE_TAC[EXTENSION; IN_INTER; NOT_IN_EMPTY; IN_ELIM_THM;
                canonical; repeating; GE] THEN
    MESON_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN `canonical UNION repeating = UNIV` SUBST1_TAC THENL
   [REWRITE_TAC[EXTENSION; IN_UNION; IN_ELIM_THM;
                canonical; repeating; GE; IN_UNIV] THEN
    MESON_TAC[];
    ALL_TAC] THEN
  DISCH_TAC THEN TRANS_TAC CARD_LE_TRANS `canonical +_c repeating` THEN
  ASM_SIMP_TAC[CARD_EQ_IMP_LE] THEN
  TRANS_TAC CARD_LE_TRANS `(UNIV:num->bool) +_c (UNIV:num->bool)` THEN
  CONJ_TAC THENL
   [ASM_MESON_TAC[countable; COUNTABLE_REPEATING; CARD_LE_ADD];
    MATCH_MP_TAC CARD_ADD_ABSORB_LE THEN
    REWRITE_TAC[num_INFINITE; CARD_LE_REFL]]);;
(* ------------------------------------------------------------------------- *)
(* Injection of canonical digits into the reals.                             *)
(* ------------------------------------------------------------------------- *)

needs "Library/analysis.ml";;

prioritize_real();;

let SUM_BINSEQUENCE_LBOUND = 
prove
 (`!m n. &0 <= sum(m,n) (\i. if s(i) then inv(&2 pow i) else &0)`,

  MATCH_MP_TAC SUM_POS THEN GEN_TAC THEN REWRITE_TAC[] THEN
  COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL; REAL_LE_INV_EQ] THEN
  SIMP_TAC[REAL_POW_LE; REAL_POS]);;
let SUM_BINSEQUENCE_UBOUND_SHARP = 
prove
 (`!s m n. sum(m,n) (\i. if s(i) then inv(&2 pow i) else &0)
             <= &2 / &2 pow m - &2 / &2 pow (m + n)`,

  GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN
  REWRITE_TAC[ADD_CLAUSES; REAL_SUB_REFL; REAL_LE_REFL] THEN
  MATCH_MP_TAC(REAL_ARITH
   `&0 <= y /\ x + y <= a ==> x + (if b then y else &0) <= a`) THEN
  SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
   `x <= a ==> a + y <= b ==> x + y <= b`)) THEN
  REWRITE_TAC[real_pow; real_div; REAL_INV_MUL] THEN REAL_ARITH_TAC);;
let SUMMABLE_BINSEQUENCE = 
prove
 (`!s. summable (\i. if s(i) then inv(&2 pow i) else &0)`,

  GEN_TAC THEN REWRITE_TAC[summable; sums; GSYM convergent] THEN
  MATCH_MP_TAC SEQ_ICONV THEN REWRITE_TAC[MR1_BOUNDED] THEN CONJ_TAC THENL
   [MAP_EVERY EXISTS_TAC [`&2`; `0`] THEN
    REWRITE_TAC[GE; LE_0; LE_REFL] THEN X_GEN_TAC `n:num` THEN
    MP_TAC(SPECL [`s:num->bool`; `0`; `n:num`]
         SUM_BINSEQUENCE_UBOUND_SHARP) THEN
    MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ a < b ==> x <= a ==> abs x < b`) THEN
    REWRITE_TAC[SUM_BINSEQUENCE_LBOUND; real_pow; REAL_DIV_1; ADD_CLAUSES] THEN
    REWRITE_TAC[REAL_ARITH `a - x < a <=> &0 < x`] THEN
    SIMP_TAC[REAL_LT_DIV; REAL_POW_LT; REAL_OF_NUM_LT; ARITH];
    GEN_TAC THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[GE; LE_EXISTS] THEN
    DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[GSYM SUM_SPLIT] THEN
    MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> a + x >= a`) THEN
    REWRITE_TAC[SUM_BINSEQUENCE_LBOUND]]);;
let SUMS_BINSEQUENCE = 
prove
 (`!s. (\i. if s(i) then inv(&2 pow i) else &0) sums
       (suminf (\i. if s(i) then inv(&2 pow i) else &0))`,

  SIMP_TAC[SUMMABLE_SUM; SUMMABLE_BINSEQUENCE]);;
let SUM_BINSEQUENCE_UBOUND_LE = 
prove
 (`!s m n. sum(m,n) (\i. if s(i) then inv(&2 pow i) else &0) <= &2 / &2 pow m`,

  MP_TAC SUM_BINSEQUENCE_UBOUND_SHARP THEN
  REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  MATCH_MP_TAC(REAL_ARITH `&0 <= b ==> x <= a - b ==> x <= a`) THEN
  SIMP_TAC[REAL_LE_DIV; REAL_POW_LE; REAL_POS]);;
(* ------------------------------------------------------------------------- *)
(* The main injection and hence main theorem.                                *)
(* ------------------------------------------------------------------------- *)

let SUMINF_INJ_LEMMA = 
prove
 (`!s t n. ~(s n) /\ t n /\
           (!m. m < n ==> (s(m) <=> t(m))) /\
           (!n. ?m. m >= n /\ ~(s m))
           ==> suminf(\n. if s n then inv (&2 pow n) else &0)
                < suminf(\n. if t n then inv (&2 pow n) else &0)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
  EXISTS_TAC `sum(0,n+1) (\n. if t n then inv (&2 pow n) else &0)` THEN
  CONJ_TAC THENL
   [ALL_TAC;
    MATCH_MP_TAC SEQ_LE THEN MAP_EVERY EXISTS_TAC
     [`\k:num. sum(0,n+1) (\n. if t n then inv (&2 pow n) else &0)`;
      `\n:num. sum(0,n) (\n. if t n then inv (&2 pow n) else &0)`] THEN
    REWRITE_TAC[SEQ_CONST; GSYM sums; SUMS_BINSEQUENCE] THEN
    EXISTS_TAC `n + 1` THEN X_GEN_TAC `m:num` THEN
    REWRITE_TAC[GE; LE_EXISTS] THEN DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
    REWRITE_TAC[GSYM ADD1] THEN
    REWRITE_TAC[GSYM SUM_SPLIT; REAL_LE_ADDR; SUM_BINSEQUENCE_LBOUND]] THEN
  ASM_REWRITE_TAC[GSYM SUM_SPLIT; SUM_1; ADD_CLAUSES] THEN
  UNDISCH_THEN `!n:num. ?m. m >= n /\ ~s m` (MP_TAC o SPEC `n + 1`) THEN
  REWRITE_TAC[GE] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
  MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC
    `sum(0,m) (\n. if s n then inv (&2 pow n) else &0) + inv(&2 pow m)` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC SEQ_LE THEN MAP_EVERY EXISTS_TAC
     [`\n:num. sum(0,n) (\n. if s n then inv (&2 pow n) else &0)`;
      `\k:num. sum(0,m) (\n. if s n then inv(&2 pow n) else &0) +
               inv(&2 pow m)`] THEN
    REWRITE_TAC[SEQ_CONST; GSYM sums; SUMS_BINSEQUENCE] THEN
    EXISTS_TAC `m:num` THEN REWRITE_TAC[GE; LE_REFL] THEN
    X_GEN_TAC `r:num` THEN REWRITE_TAC[LE_EXISTS] THEN
    DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
    REWRITE_TAC[GSYM SUM_SPLIT; REAL_LE_LADD; ADD_CLAUSES] THEN
    DISJ_CASES_THEN SUBST_ALL_TAC (ARITH_RULE `p = 0 \/ p = 1 + PRE p`) THEN
    SIMP_TAC[sum; REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
    ONCE_REWRITE_TAC[GSYM SUM_SPLIT] THEN
    ASM_REWRITE_TAC[SUM_1; REAL_ADD_LID] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 / &2 pow (m + 1)` THEN
    REWRITE_TAC[SUM_BINSEQUENCE_UBOUND_LE] THEN
    REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN CONV_TAC REAL_FIELD;
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
  DISCH_THEN(X_CHOOSE_THEN `r:num` SUBST_ALL_TAC) THEN
  REWRITE_TAC[GSYM SUM_SPLIT] THEN
  ASM_REWRITE_TAC[ADD_CLAUSES; SUM_1; REAL_ADD_RID] THEN
  MATCH_MP_TAC(REAL_ARITH `a = b /\ c < e - d ==> (a + c) + d < b + e`) THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC SUM_EQ THEN ASM_SIMP_TAC[LE_0; ADD_CLAUSES]; ALL_TAC] THEN
  MATCH_MP_TAC REAL_LET_TRANS THEN
  EXISTS_TAC `&2 / &2 pow (n + 1) - &2 / &2 pow ((n + 1) + r)` THEN
  REWRITE_TAC[SUM_BINSEQUENCE_UBOUND_SHARP] THEN
  MATCH_MP_TAC(REAL_ARITH `a = b /\ d < c ==> a - c < b - d`) THEN
  CONJ_TAC THENL
   [REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN CONV_TAC REAL_FIELD;
    MATCH_MP_TAC(REAL_FIELD `&0 < inv(x) ==> inv(x) < &2 / x`) THEN
    SIMP_TAC[REAL_LT_INV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH]]);;
let UNCOUNTABLE_REALS = 
prove
 (`~countable(UNIV:real->bool)`,

  MP_TAC UNCOUNTABLE_CANONICAL THEN REWRITE_TAC[CONTRAPOS_THM] THEN
  REWRITE_TAC[countable] THEN DISCH_TAC THEN
  TRANS_TAC CARD_LE_TRANS `UNIV:real->bool` THEN
  ASM_REWRITE_TAC[] THEN POP_ASSUM(K ALL_TAC) THEN REWRITE_TAC[le_c] THEN
  EXISTS_TAC `\s. suminf(\n. if s(n) then inv(&2 pow n) else &0)` THEN
  REWRITE_TAC[IN_UNIV] THEN
  MAP_EVERY X_GEN_TAC [`s:num->bool`; `t:num->bool`] THEN
  REWRITE_TAC[canonical; IN_ELIM_THM] THEN STRIP_TAC THEN
  REWRITE_TAC[FUN_EQ_THM] THEN
  GEN_REWRITE_TAC I [MESON[] `(!x. P x) <=> ~(?x. ~P x)`] THEN
  ONCE_REWRITE_TAC[MINIMAL] THEN
  ABBREV_TAC `n = minimal x. ~(s x <=> t x)` THEN
  FIRST_X_ASSUM(K ALL_TAC o check (is_var o rhs o concl)) THEN
  ASM_CASES_TAC `(t:num->bool) n` THEN ASM_REWRITE_TAC[] THEN
  STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SYM) THENL
   [MATCH_MP_TAC(REAL_ARITH `b < a ==> a = b ==> F`);
    MATCH_MP_TAC(REAL_ARITH `a < b ==> a = b ==> F`)] THEN
  MATCH_MP_TAC SUMINF_INJ_LEMMA THEN ASM_MESON_TAC[]);;