100/liouville.ml

   1 (* ========================================================================= *)
   2 (* Liouville approximation theorem.                                          *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/floor.ml";;
   6 needs "Library/poly.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* Definition of algebraic and transcendental.                               *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 let algebraic = new_definition
  13  `algebraic(x) <=> ?p. ALL integer p /\ ~(poly p = poly []) /\ poly p x = &0`;;
  14
  15 let transcendental = new_definition
  16  `transcendental(x) <=> ~(algebraic x)`;;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* Some trivialities.                                                        *)
  20 (* ------------------------------------------------------------------------- *)
  21
  22 let REAL_INTEGER_EQ_0 = prove
  23  (`!x. integer x /\ abs(x) < &1 ==> x = &0`,
  24   MESON_TAC[REAL_ABS_INTEGER_LEMMA; REAL_NOT_LE]);;
  25
  26 let FACT_LE_REFL = prove
  27  (`!n. n <= FACT n`,
  28   INDUCT_TAC THEN REWRITE_TAC[FACT; ARITH] THEN
  29   MATCH_MP_TAC(ARITH_RULE `x * 1 <= a ==> x <= a`) THEN
  30   REWRITE_TAC[LE_MULT_LCANCEL; NOT_SUC; FACT_LT;
  31               ARITH_RULE `1 <= n <=> 0 < n`]);;
  32
  33 let EXP_LE_REFL = prove
  34  (`!a. 1 < a ==> !n. n <= a EXP n`,
  35   GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH] THEN
  36   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
  37    `n <= x ==> 1 * x < y ==> SUC n <= y`)) THEN
  38   REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0] THEN
  39   POP_ASSUM MP_TAC THEN ARITH_TAC);;
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* Archimedian properties taken from Multivariate/misc.ml                    *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 let REAL_POW_LBOUND = prove
  46  (`!x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n`,
  47   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  48   INDUCT_TAC THEN
  49   REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_ADD_RID; REAL_LE_REFL] THEN
  50   REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
  51   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(&1 + x) * (&1 + &n * x)` THEN
  52   ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ARITH `&0 <= x ==> &0 <= &1 + x`] THEN
  53   ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ARITH
  54    `&1 + (n + &1) * x <= (&1 + x) * (&1 + n * x) <=> &0 <= n * x * x`]);;
  55
  56 let REAL_ARCH_POW = prove
  57  (`!x y. &1 < x ==> ?n. y < x pow n`,
  58   REPEAT STRIP_TAC THEN
  59   MP_TAC(SPEC `x - &1` REAL_ARCH) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
  60   DISCH_THEN(MP_TAC o SPEC `y:real`) THEN MATCH_MP_TAC MONO_EXISTS THEN
  61   X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
  62   EXISTS_TAC `&1 + &n * (x - &1)` THEN
  63   ASM_SIMP_TAC[REAL_ARITH `x < y ==> x < &1 + y`] THEN
  64   ASM_MESON_TAC[REAL_POW_LBOUND; REAL_SUB_ADD2; REAL_ARITH
  65     `&1 < x ==> &0 <= x - &1`]);;
  66
  67 (* ------------------------------------------------------------------------- *)
  68 (* Inequality variant of mean value theorem.                                 *)
  69 (* ------------------------------------------------------------------------- *)
  70
  71 let MVT_INEQ = prove
  72  (`!f f' a d M.
  73         &0 < M /\ &0 < d /\
  74         (!x. abs(x - a) <= d ==> (f diffl f'(x)) x /\ abs(f' x) < M)
  75         ==> !x. abs(x - a) <= d ==> abs(f x - f a) < M * d`,
  76   REWRITE_TAC[TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
  77   REWRITE_TAC[FORALL_AND_THM] THEN
  78   REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
  79    (REAL_ARITH `x = a \/ x < a \/ a < x`)
  80   THENL
  81    [ASM_SIMP_TAC[REAL_SUB_REFL; REAL_ABS_NUM; REAL_LT_MUL];
  82     MP_TAC(SPECL [`f:real->real`; `f':real->real`; `x:real`; `a:real`]
  83                  MVT_ALT);
  84     MP_TAC(SPECL [`f:real->real`; `f':real->real`; `a:real`; `x:real`]
  85                  MVT_ALT)] THEN
  86   (ANTS_TAC THENL
  87     [ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
  88      FIRST_X_ASSUM MATCH_MP_TAC THEN
  89      POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC;
  90      ALL_TAC]) THEN
  91   STRIP_TAC THENL
  92    [ONCE_REWRITE_TAC[REAL_ABS_SUB]; ALL_TAC] THEN
  93   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[REAL_ABS_MUL] THEN
  94   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `d * abs(f'(z:real))` THEN
  95   (CONJ_TAC THENL
  96     [MATCH_MP_TAC REAL_LE_RMUL;
  97      MATCH_MP_TAC REAL_LT_LMUL THEN
  98      ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC]) THEN
  99   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC);;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* Appropriate multiple of poly on rational is an integer.                   *)
 103 (* ------------------------------------------------------------------------- *)
 104
 105 let POLY_MULTIPLE_INTEGER = prove
 106  (`!p q l. ALL integer l ==> integer(&q pow (LENGTH l) * poly l (&p / &q))`,
 107   GEN_TAC THEN GEN_TAC THEN ASM_CASES_TAC `q = 0` THENL
 108    [LIST_INDUCT_TAC THEN REWRITE_TAC[poly; REAL_MUL_RZERO; INTEGER_CLOSED] THEN
 109     ASM_REWRITE_TAC[LENGTH; real_pow; REAL_MUL_LZERO; INTEGER_CLOSED];
 110     ALL_TAC] THEN
 111   LIST_INDUCT_TAC THEN REWRITE_TAC[poly; REAL_MUL_RZERO; INTEGER_CLOSED] THEN
 112   REWRITE_TAC[LENGTH; real_pow; ALL] THEN DISCH_TAC THEN
 113   REWRITE_TAC[REAL_ARITH
 114    `(q * qp) * (h + pq * pol) = q * h * qp + (q * pq) * (qp * pol)`] THEN
 115   ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ] THEN
 116   MATCH_MP_TAC(el 1 (CONJUNCTS INTEGER_CLOSED)) THEN
 117   ASM_SIMP_TAC[INTEGER_CLOSED]);;
 118
 119 (* ------------------------------------------------------------------------- *)
 120 (* First show any root is surrounded by an other-root-free zone.             *)
 121 (* ------------------------------------------------------------------------- *)
 122
 123 let SEPARATE_FINITE_SET = prove
 124  (`!a s. FINITE s
 125          ==> ~(a IN s) ==> ?d. &0 < d /\ !x. x IN s ==> d <= abs(x - a)`,
 126   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 127   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
 128   CONJ_TAC THENL [MESON_TAC[REAL_LT_01]; ALL_TAC] THEN
 129   REPEAT GEN_TAC THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 130   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 131   EXISTS_TAC `min d (abs(x - a))` THEN
 132   ASM_REWRITE_TAC[REAL_MIN_LE; REAL_LT_MIN; GSYM REAL_ABS_NZ; REAL_SUB_0] THEN
 133   ASM_MESON_TAC[REAL_LE_REFL]);;
 134
 135 let POLY_ROOT_SEPARATE_LE = prove
 136  (`!p x. poly p x = &0 /\ ~(poly p = poly [])
 137          ==> ?d. &0 < d /\
 138                  !x'. &0 < abs(x' - x) /\ abs(x' - x) < d
 139                       ==> ~(poly p x' = &0)`,
 140   REPEAT STRIP_TAC THEN
 141   MP_TAC(SPECL [`x:real`; `{x | poly p x = &0} DELETE x`]
 142     SEPARATE_FINITE_SET) THEN
 143   ASM_SIMP_TAC[POLY_ROOTS_FINITE_SET; FINITE_DELETE; IN_DELETE] THEN
 144   MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[IN_ELIM_THM] THEN
 145   REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_SUB_0] THEN MESON_TAC[REAL_NOT_LT]);;
 146
 147 let POLY_ROOT_SEPARATE_LT = prove
 148  (`!p x. poly p x = &0 /\ ~(poly p = poly [])
 149          ==> ?d. &0 < d /\
 150                  !x'. &0 < abs(x' - x) /\ abs(x' - x) <= d
 151                       ==> ~(poly p x' = &0)`,
 152   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP POLY_ROOT_SEPARATE_LE) THEN
 153   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 154   EXISTS_TAC `d / &2` THEN ASM_MESON_TAC[REAL_ARITH
 155    `&0 < d ==> &0 < d / &2 /\ (x <= d / &2 ==> x < d)`]);;
 156
 157 (* ------------------------------------------------------------------------- *)
 158 (* And also there is a positive bound on a polynomial in an interval.        *)
 159 (* ------------------------------------------------------------------------- *)
 160
 161 let POLY_BOUND_INTERVAL = prove
 162  (`!p d x. ?M. &0 < M /\ !x'. abs(x' - x) <= d ==> abs(poly p x') < M`,
 163   REPEAT STRIP_TAC THEN
 164   MP_TAC(SPECL [`poly p`; `x - d`; `x + d`] CONT_BOUNDED_ABS) THEN
 165   REWRITE_TAC[REWRITE_RULE[ETA_AX] (SPEC_ALL POLY_CONT)] THEN
 166   DISCH_THEN(X_CHOOSE_TAC `M:real`) THEN EXISTS_TAC `&1 + abs M` THEN
 167   CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN REPEAT STRIP_TAC THEN
 168   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `M:real` THEN CONJ_TAC THENL
 169    [FIRST_X_ASSUM MATCH_MP_TAC THEN POP_ASSUM MP_TAC; ALL_TAC] THEN
 170   REAL_ARITH_TAC);;
 171
 172 (* ------------------------------------------------------------------------- *)
 173 (* Now put these together to get the interval we need.                       *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let LIOUVILLE_INTERVAL = prove
 177  (`!p x. poly p x = &0 /\ ~(poly p = poly [])
 178          ==> ?c. &0 < c /\
 179                  (!x'. abs(x' - x) <= c
 180                        ==> abs(poly(poly_diff p) x') < &1 / c) /\
 181                  (!x'. &0 < abs(x' - x) /\ abs(x' - x) <= c
 182                        ==> ~(poly p x' = &0))`,
 183   REPEAT STRIP_TAC THEN
 184   MP_TAC(SPECL [`p:real list`; `x:real`] POLY_ROOT_SEPARATE_LT) THEN
 185   ASM_REWRITE_TAC[] THEN
 186   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 187   MP_TAC(SPECL [`poly_diff p`; `d:real`; `x:real`] POLY_BOUND_INTERVAL) THEN
 188   DISCH_THEN(X_CHOOSE_TAC `M:real`) THEN EXISTS_TAC `min d (inv M)` THEN
 189   ASM_SIMP_TAC[REAL_LT_MIN; REAL_LE_MIN; REAL_LT_INV_EQ] THEN
 190   X_GEN_TAC `y:real` THEN STRIP_TAC THEN
 191   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `M:real` THEN
 192   ASM_SIMP_TAC[] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_INV] THEN
 193   REWRITE_TAC[real_div; REAL_MUL_LID] THEN
 194   MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_MIN_LE; REAL_LT_MIN] THEN
 195   ASM_REWRITE_TAC[REAL_LT_INV_EQ; REAL_LE_REFL]);;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Liouville's approximation theorem.                                        *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let LIOUVILLE = prove
 202  (`!x. algebraic x
 203        ==> ?n c. c > &0 /\
 204                  !p q. ~(q = 0) ==> &p / &q = x \/
 205                                     abs(x - &p / &q) > c / &q pow n`,
 206   GEN_TAC THEN REWRITE_TAC[algebraic; real_gt] THEN
 207   DISCH_THEN(X_CHOOSE_THEN `l:real list` STRIP_ASSUME_TAC) THEN
 208   EXISTS_TAC `LENGTH(l:real list)` THEN
 209   MP_TAC(SPECL [`l:real list`; `x:real`] LIOUVILLE_INTERVAL) THEN
 210   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `c:real` THEN
 211   STRIP_TAC THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LE] THEN
 212   MAP_EVERY X_GEN_TAC [`p:num`; `q:num`] THEN DISCH_TAC THEN
 213   ASM_CASES_TAC `&p / &q = x` THEN ASM_REWRITE_TAC[] THEN
 214   REPEAT STRIP_TAC THEN UNDISCH_TAC
 215    `!x'. &0 < abs(x' - x) /\ abs(x' - x) <= c ==> ~(poly l x' = &0)` THEN
 216   DISCH_THEN(MP_TAC o SPEC `&p / &q`) THEN REWRITE_TAC[NOT_IMP] THEN
 217   REPEAT CONJ_TAC THENL
 218    [ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_SUB_0];
 219     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 220      `abs(x - y) <= d ==> d <= e ==> abs(y - x) <= e`)) THEN
 221     ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; REAL_LE_LDIV_EQ; LT_NZ] THEN
 222     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
 223     MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 224     MATCH_MP_TAC REAL_POW_LE_1 THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
 225     UNDISCH_TAC `~(q = 0)` THEN ARITH_TAC;
 226     ALL_TAC] THEN
 227   SUBGOAL_THEN `&q pow (LENGTH(l:real list)) * poly l (&p / &q) = &0`
 228   MP_TAC THENL
 229    [ALL_TAC; ASM_REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0; REAL_OF_NUM_EQ]] THEN
 230   MATCH_MP_TAC REAL_INTEGER_EQ_0 THEN
 231   ASM_SIMP_TAC[POLY_MULTIPLE_INTEGER] THEN
 232   MP_TAC(SPECL [`poly l`; `poly(poly_diff l)`; `x:real`;
 233                 `c / &q pow (LENGTH(l:real list))`; `&1 / c`]
 234                MVT_INEQ) THEN
 235   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; LT_NZ; REAL_POW_LT] THEN
 236   ANTS_TAC THENL
 237    [REWRITE_TAC[REWRITE_RULE[ETA_AX] (SPEC_ALL POLY_DIFF)] THEN
 238     REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 239     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
 240      `x <= d ==> d <= e ==> x <= e`)) THEN
 241     ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; REAL_LE_LDIV_EQ; LT_NZ] THEN
 242     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
 243     MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 244     MATCH_MP_TAC REAL_POW_LE_1 THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
 245     UNDISCH_TAC `~(q = 0)` THEN ARITH_TAC;
 246     ALL_TAC] THEN
 247   REWRITE_TAC[real_div; REAL_MUL_ASSOC; REAL_MUL_LID] THEN
 248   ASM_SIMP_TAC[REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN
 249   REWRITE_TAC[GSYM real_div] THEN DISCH_THEN(MP_TAC o SPEC `&p / &q`) THEN
 250   REWRITE_TAC[REAL_SUB_RZERO] THEN ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN
 251   ASM_REWRITE_TAC[] THEN
 252   ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; REAL_LT_RDIV_EQ; LT_NZ] THEN
 253   REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN
 254   REWRITE_TAC[REAL_MUL_AC]);;
 255
 256 (* ------------------------------------------------------------------------- *)
 257 (* Corollary for algebraic irrationals.                                      *)
 258 (* ------------------------------------------------------------------------- *)
 259
 260 let LIOUVILLE_IRRATIONAL = prove
 261  (`!x. algebraic x /\ ~rational x
 262        ==> ?n c. c > &0 /\ !p q. ~(q = 0) ==> abs(x - &p / &q) > c / &q pow n`,
 263   REWRITE_TAC[RATIONAL_ALT] THEN REPEAT STRIP_TAC THEN
 264   FIRST_X_ASSUM(MP_TAC o MATCH_MP LIOUVILLE) THEN
 265   REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
 266   MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN
 267   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 268   ASM_MESON_TAC[LIOUVILLE; REAL_ABS_DIV; REAL_ABS_NUM]);;
 269
 270 (* ------------------------------------------------------------------------- *)
 271 (* Liouville's constant.                                                     *)
 272 (* ------------------------------------------------------------------------- *)
 273
 274 let liouville = new_definition
 275  `liouville = suminf (\n. &1 / &10 pow (FACT n))`;;
 276
 277 (* ------------------------------------------------------------------------- *)
 278 (* Some bounds on the partial sums and hence convergence.                    *)
 279 (* ------------------------------------------------------------------------- *)
 280
 281 let LIOUVILLE_SUM_BOUND = prove
 282  (`!d n. ~(n = 0)
 283          ==> sum(n..n+d) (\k. &1 / &10 pow FACT k) <= &2 / &10 pow (FACT n)`,
 284   INDUCT_TAC THEN GEN_TAC THEN DISCH_TAC THENL
 285    [REWRITE_TAC[ADD_CLAUSES; SUM_SING_NUMSEG; real_div] THEN
 286     MATCH_MP_TAC REAL_LE_RMUL THEN
 287     SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_OF_NUM_LE; ARITH];
 288     ALL_TAC] THEN
 289   SIMP_TAC[SUM_CLAUSES_LEFT; LE_ADD] THEN REWRITE_TAC[real_div] THEN
 290   MATCH_MP_TAC(REAL_ARITH `y <= x ==> &1 * x + y <= &2 * x`) THEN
 291   REWRITE_TAC[ARITH_RULE `n + SUC d = (n + 1) + d`; GSYM real_div] THEN
 292   FIRST_X_ASSUM(MP_TAC o SPEC `n + 1`) THEN REWRITE_TAC[ADD_EQ_0; ARITH] THEN
 293   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
 294   SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
 295   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
 296   SIMP_TAC[GSYM REAL_POW_SUB; REAL_OF_NUM_EQ; ARITH; FACT_MONO; LE_ADD] THEN
 297   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&10 pow 1` THEN
 298   CONJ_TAC THENL [ALL_TAC; MATCH_MP_TAC REAL_POW_MONO] THEN
 299   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM ADD1; FACT] THEN
 300   MATCH_MP_TAC(ARITH_RULE
 301    `1 * x <= SUC n * x /\ ~(n * x = 0) ==> 1 <= SUC n * x - x`) THEN
 302   ASM_SIMP_TAC[LE_MULT_RCANCEL; MULT_EQ_0] THEN
 303   REWRITE_TAC[GSYM LT_NZ; FACT_LT] THEN ARITH_TAC);;
 304
 305 let LIOUVILLE_PSUM_BOUND = prove
 306  (`!n d. ~(n = 0)
 307          ==> sum(n,d) (\k. &1 / &10 pow FACT k) <= &2 / &10 pow (FACT n)`,
 308   REPEAT STRIP_TAC THEN ASM_CASES_TAC `d = 0` THEN
 309   ASM_SIMP_TAC[sum; REAL_LE_DIV; REAL_POW_LE; REAL_POS] THEN
 310   ASM_SIMP_TAC[PSUM_SUM_NUMSEG] THEN
 311   ASM_SIMP_TAC[ARITH_RULE `~(d = 0) ==> (n + d) - 1 = n + (d - 1)`] THEN
 312   ASM_SIMP_TAC[LIOUVILLE_SUM_BOUND]);;
 313
 314 let LIOUVILLE_SUMS = prove
 315  (`(\k. &1 / &10 pow FACT k) sums liouville`,
 316   REWRITE_TAC[liouville] THEN MATCH_MP_TAC SUMMABLE_SUM THEN
 317   REWRITE_TAC[SER_CAUCHY] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 318   MP_TAC(SPEC `inv(e)` REAL_ARCH_SIMPLE) THEN
 319   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `2 * N + 1` THEN
 320   REWRITE_TAC[GE] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 321   EXISTS_TAC `&2 / &10 pow (FACT m)` THEN CONJ_TAC THENL
 322    [MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= a ==> abs x <= a`) THEN
 323     ASM_SIMP_TAC[SUM_POS; REAL_LE_DIV; REAL_POW_LE; REAL_POS] THEN
 324     MATCH_MP_TAC LIOUVILLE_PSUM_BOUND THEN
 325     UNDISCH_TAC `2 * N + 1 <= m` THEN ARITH_TAC;
 326     ALL_TAC] THEN
 327   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
 328   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `e * &(2 * N + 1)` THEN
 329   CONJ_TAC THENL
 330    [REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 331     MATCH_MP_TAC(REAL_ARITH
 332      `&1 < (n + &1 / &2) * e ==> &2 < e * (&2 * n + &1)`) THEN
 333     ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; real_div; REAL_MUL_LID] THEN
 334     UNDISCH_TAC `inv(e) <= &N` THEN REAL_ARITH_TAC;
 335     ALL_TAC] THEN
 336   ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN
 337   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE] THEN
 338   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[] THEN
 339   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `10 EXP m` THEN
 340   REWRITE_TAC[FACT_LE_REFL; LE_EXP; ARITH] THEN SIMP_TAC[EXP_LE_REFL; ARITH]);;
 341
 342 let LIOUVILLE_PSUM_LE = prove
 343  (`!n. sum(0,n) (\k. &1 / &10 pow FACT k) <= liouville`,
 344   GEN_TAC THEN REWRITE_TAC[suminf] THEN MATCH_MP_TAC SEQ_LE THEN
 345   EXISTS_TAC `\j:num. sum(0,n) (\k. &1 / &10 pow FACT k)` THEN
 346   EXISTS_TAC `\n:num. sum(0,n) (\k. &1 / &10 pow FACT k)` THEN
 347   REWRITE_TAC[SEQ_CONST; GSYM sums; LIOUVILLE_SUMS] THEN
 348   EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN SIMP_TAC[GE; LE_EXISTS] THEN
 349   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC) THEN
 350   REWRITE_TAC[GSYM SUM_SPLIT; ADD_CLAUSES; REAL_LE_ADDR] THEN
 351   SIMP_TAC[SUM_POS; REAL_LE_DIV; REAL_POW_LE; REAL_POS]);;
 352
 353 let LIOUVILLE_PSUM_LT = prove
 354  (`!n. sum(0,n) (\k. &1 / &10 pow FACT k) < liouville`,
 355   GEN_TAC THEN MP_TAC(SPEC `SUC n` LIOUVILLE_PSUM_LE) THEN SIMP_TAC[sum] THEN
 356   MATCH_MP_TAC(REAL_ARITH `&0 < e ==> x + e <= y ==> x < y`) THEN
 357   SIMP_TAC[REAL_LT_DIV; REAL_POW_LT; REAL_OF_NUM_LT; ARITH]);;
 358
 359 let LIOVILLE_PSUM_DIFF = prove
 360  (`!n. ~(n = 0)
 361        ==> liouville
 362              <= sum(0,n) (\k. &1 / &10 pow FACT k) + &2 / &10 pow (FACT n)`,
 363   GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SEQ_LE THEN
 364   EXISTS_TAC `\n. sum(0,n) (\k. &1 / &10 pow FACT k)` THEN
 365   EXISTS_TAC
 366     `\j:num. sum (0,n) (\k. &1 / &10 pow FACT k) + &2 / &10 pow FACT n` THEN
 367   REWRITE_TAC[SEQ_CONST; GSYM sums; LIOUVILLE_SUMS] THEN
 368   EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN SIMP_TAC[GE; LE_EXISTS] THEN
 369   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC) THEN
 370   REWRITE_TAC[GSYM SUM_SPLIT; REAL_LE_LADD] THEN
 371   ASM_SIMP_TAC[ADD_CLAUSES; LIOUVILLE_PSUM_BOUND]);;
 372
 373 (* ------------------------------------------------------------------------- *)
 374 (* Main proof.                                                               *)
 375 (* ------------------------------------------------------------------------- *)
 376
 377 let TRANSCENDENTAL_LIOUVILLE = prove
 378  (`transcendental(liouville)`,
 379   REWRITE_TAC[transcendental] THEN DISCH_THEN(MP_TAC o MATCH_MP LIOUVILLE) THEN
 380   REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b) <=> a ==> ~b`] THEN
 381   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN
 382   MAP_EVERY X_GEN_TAC [`m:num`; `c:real`] THEN
 383   REWRITE_TAC[DE_MORGAN_THM; real_gt; REAL_NOT_LT] THEN DISCH_TAC THEN
 384   MP_TAC(SPECL [`&10`; `&2 / c`] REAL_ARCH_POW) THEN
 385   CONV_TAC REAL_RAT_REDUCE_CONV THEN DISCH_THEN(X_CHOOSE_TAC `k:num`) THEN
 386   ABBREV_TAC `n = m + k + 1` THEN
 387   EXISTS_TAC `nsum(0..n-1) (\i. 10 EXP (FACT(n-1) - FACT i))` THEN
 388   EXISTS_TAC `10 EXP (FACT(n-1))` THEN REWRITE_TAC[EXP_EQ_0; ARITH] THEN
 389   SUBGOAL_THEN
 390    `&(nsum(0..n-1) (\i. 10 EXP (FACT(n-1) - FACT i))) / &(10 EXP (FACT(n-1))) =
 391     sum(0..n-1) (\k. &1 / &10 pow (FACT k))`
 392   SUBST1_TAC THENL
 393    [REWRITE_TAC[real_div] THEN GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 394     REWRITE_TAC[REAL_OF_NUM_SUM_NUMSEG; GSYM SUM_LMUL] THEN
 395     SIMP_TAC[GSYM REAL_OF_NUM_POW; REAL_POW_SUB; REAL_OF_NUM_EQ; ARITH;
 396              FACT_MONO; real_div; REAL_MUL_ASSOC] THEN
 397     SIMP_TAC[REAL_MUL_LINV; REAL_OF_NUM_EQ; REAL_POW_EQ_0; ARITH] THEN
 398     REWRITE_TAC[REAL_MUL_LID];
 399     ALL_TAC] THEN
 400   MP_TAC(GEN `f:num->real`
 401    (SPECL [`f:num->real`; `0`; `m + k + 1`] PSUM_SUM_NUMSEG)) THEN
 402   REWRITE_TAC[ADD_EQ_0; ARITH; ADD_CLAUSES] THEN ASM_REWRITE_TAC[] THEN
 403   DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]) THEN
 404   SIMP_TAC[LIOUVILLE_PSUM_LT; REAL_LT_IMP_NE] THEN
 405   MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= y ==> abs x <= y`) THEN
 406   REWRITE_TAC[REAL_SUB_LE; LIOUVILLE_PSUM_LE] THEN
 407   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 / &10 pow (FACT n)` THEN
 408   REWRITE_TAC[REAL_LE_SUB_RADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
 409   CONJ_TAC THENL
 410    [MATCH_MP_TAC LIOVILLE_PSUM_DIFF THEN EXPAND_TAC "n" THEN ARITH_TAC;
 411     ALL_TAC] THEN
 412   REWRITE_TAC[LIOVILLE_PSUM_DIFF] THEN
 413   REWRITE_TAC[REAL_OF_NUM_POW; GSYM EXP_MULT] THEN
 414   SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; LT_NZ; EXP_EQ_0; ARITH] THEN
 415   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
 416   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ] THEN
 417   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&10 pow k` THEN
 418   ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 419   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
 420   SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; LT_NZ; EXP_EQ_0; ARITH] THEN
 421   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
 422   REWRITE_TAC[GSYM EXP_ADD; LE_EXP; ARITH_EQ] THEN EXPAND_TAC "n" THEN
 423   REWRITE_TAC[ARITH_RULE `(m + k + 1) - 1 = m + k`] THEN
 424   REWRITE_TAC[num_CONV `1`; ADD_CLAUSES; FACT] THEN
 425   REWRITE_TAC[ARITH_RULE
 426    `k + f * m <= SUC(m + k) * f <=> k <= (k + 1) * f`] THEN
 427   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `k = k * 1`] THEN
 428   MATCH_MP_TAC LE_MULT2 THEN REWRITE_TAC[LE_ADD] THEN
 429   REWRITE_TAC[FACT_LT; ARITH_RULE `1 <= x <=> 0 < x`]);;