100/piseries.ml

   1 (* ========================================================================= *)
   2 (* Taylor series for tan and cot, via partial fractions expansion of cot.    *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/analysis.ml";;
   6 needs "Library/transc.ml";;
   7 needs "Library/floor.ml";;
   8 needs "Library/poly.ml";;
   9 needs "Examples/machin.ml";;
  10 needs "Library/iter.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Compatibility stuff for some old proofs.                                  *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let REAL_LE_1_POW2 = prove
  17  (`!n. &1 <= &2 pow n`,
  18   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> 0 < n`;
  19               EXP_LT_0; ARITH]);;
  20
  21 let REAL_LT_1_POW2 = prove
  22  (`!n. &1 < &2 pow n <=> ~(n = 0)`,
  23   GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
  24   CONV_TAC REAL_RAT_REDUCE_CONV THEN
  25   SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&2 pow 0`)) THEN
  26   MATCH_MP_TAC REAL_POW_MONO_LT THEN
  27   REWRITE_TAC[REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
  28
  29 let REAL_POW2_CLAUSES = prove
  30  (`(!n. &0 <= &2 pow n) /\
  31    (!n. &0 < &2 pow n) /\
  32    (!n. &0 <= inv(&2 pow n)) /\
  33    (!n. &0 < inv(&2 pow n)) /\
  34    (!n. inv(&2 pow n) <= &1) /\
  35    (!n. &1 - inv(&2 pow n) <= &1) /\
  36    (!n. &1 <= &2 pow n) /\
  37    (!n. &1 < &2 pow n <=> ~(n = 0)) /\
  38    (!n. &0 <= &1 - inv(&2 pow n)) /\
  39    (!n. &0 <= &2 pow n - &1) /\
  40    (!n. &0 < &1 - inv(&2 pow n) <=> ~(n = 0))`,
  41   SIMP_TAC[REAL_LE_1_POW2; REAL_LT_1_POW2; REAL_SUB_LE; REAL_SUB_LT;
  42            REAL_INV_LE_1] THEN
  43   SIMP_TAC[REAL_LE_INV_EQ; REAL_LT_INV_EQ; REAL_POW_LT; REAL_POW_LE;
  44            REAL_OF_NUM_LE; REAL_OF_NUM_LT; ARITH;
  45            REAL_ARITH `&1 - x <= &1 <=> &0 <= x`] THEN
  46   GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
  47   CONV_TAC REAL_RAT_REDUCE_CONV THEN
  48   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv(&2 pow 1)` THEN
  49   ASM_SIMP_TAC[REAL_LE_INV2; REAL_POW_MONO; REAL_POW_LT; REAL_OF_NUM_LT; ARITH;
  50                REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
  51   CONV_TAC REAL_RAT_REDUCE_CONV);;
  52
  53 let REAL_INTEGER_CLOSURES = prove
  54  (`(!n. ?p. abs(&n) = &p) /\
  55    (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x + y) = &p) /\
  56    (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x - y) = &p) /\
  57    (!x y. (?m. abs(x) = &m) /\ (?n. abs(y) = &n) ==> ?p. abs(x * y) = &p) /\
  58    (!x r. (?n. abs(x) = &n) ==> ?p. abs(x pow r) = &p) /\
  59    (!x. (?n. abs(x) = &n) ==> ?p. abs(--x) = &p) /\
  60    (!x. (?n. abs(x) = &n) ==> ?p. abs(abs x) = &p)`,
  61   REWRITE_TAC[GSYM integer; INTEGER_CLOSED]);;
  62
  63 let PI_APPROX_25_BITS = time PI_APPROX_BINARY_RULE 25;;
  64
  65 (* ------------------------------------------------------------------------- *)
  66 (* Convert a polynomial into a "canonical" list-based form.                  *)
  67 (* ------------------------------------------------------------------------- *)
  68
  69 let POLYMERIZE_CONV =
  70   let pth = prove
  71    (`a = poly [a] x`,
  72     REWRITE_TAC[poly; REAL_MUL_RZERO; REAL_ADD_RID])
  73   and qth = prove
  74    (`x * poly p x = poly (CONS (&0) p) x`,
  75     REWRITE_TAC[poly; REAL_ADD_LID]) in
  76   let conv_base = GEN_REWRITE_CONV I [pth]
  77   and conv_zero = GEN_REWRITE_CONV I [qth]
  78   and conv_step = GEN_REWRITE_CONV I [GSYM(CONJUNCT2 poly)] in
  79   let is_add = is_binop `(+):real->real->real`
  80   and is_mul = is_binop `(*):real->real->real` in
  81   let rec conv tm =
  82     if is_add tm then
  83       let l,r = dest_comb tm in
  84       let r1,r2 = dest_comb r in
  85       let th1 = AP_TERM l (AP_TERM r1 (conv r2)) in
  86       TRANS th1 (conv_step(rand(concl th1)))
  87     else if is_mul tm then
  88       let th1 = AP_TERM (rator tm) (conv (rand tm)) in
  89       TRANS th1 (conv_zero(rand(concl th1)))
  90     else conv_base tm in
  91   conv;;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* Basic definition of cotangent.                                            *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 let cot = new_definition
  98   `cot x = cos x / sin x`;;
  99
 100 let COT_TAN = prove
 101  (`cot(x) = inv(tan(x))`,
 102   REWRITE_TAC[cot; tan; REAL_INV_DIV]);;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* We need to reverse sums to prove the grisly lemma below.                  *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let SUM_PERMUTE_0 = prove
 109  (`!n p. (!y. y < n ==> ?!x. x < n /\ (p(x) = y))
 110         ==> !f. sum(0,n)(\n. f(p n)) = sum(0,n) f`,
 111   INDUCT_TAC THEN GEN_TAC THEN TRY(REWRITE_TAC[sum] THEN NO_TAC) THEN
 112   DISCH_TAC THEN GEN_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `n:num`) THEN
 113   REWRITE_TAC[LESS_SUC_REFL] THEN
 114   CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) THEN
 115   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 116   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
 117   GEN_REWRITE_TAC RAND_CONV [sum] THEN REWRITE_TAC[ADD_CLAUSES] THEN
 118   ABBREV_TAC `q:num->num = \r. if r < k then p(r) else p(SUC r)` THEN
 119   SUBGOAL_THEN `!y:num. y < n ==> ?!x. x < n /\ (q x = y)` MP_TAC THENL
 120    [X_GEN_TAC `y:num` THEN DISCH_TAC THEN (MP_TAC o ASSUME)
 121       `!y. y < (SUC n) ==> ?!x. x < (SUC n) /\ (p x = y)` THEN
 122     DISCH_THEN(MP_TAC o SPEC `y:num`) THEN
 123     W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
 124      [MATCH_MP_TAC LT_TRANS THEN EXISTS_TAC `n:num` THEN
 125       ASM_REWRITE_TAC[LESS_SUC_REFL];
 126       DISCH_THEN(fun th -> DISCH_THEN(MP_TAC o C MP th))] THEN
 127     CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) THEN
 128     DISCH_THEN(X_CHOOSE_THEN `x:num` STRIP_ASSUME_TAC o CONJUNCT1) THEN
 129     CONJ_TAC THENL
 130      [DISJ_CASES_TAC(SPECL [`x:num`; `k:num`] LTE_CASES) THENL
 131        [EXISTS_TAC `x:num` THEN EXPAND_TAC "q" THEN BETA_TAC THEN
 132         ASM_REWRITE_TAC[] THEN
 133         REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
 134         EXISTS_TAC `&k` THEN
 135         ASM_REWRITE_TAC[REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
 136         UNDISCH_TAC `k < (SUC n)` THEN
 137         REWRITE_TAC[GSYM LT_SUC_LE; LE_ADD2];
 138         MP_TAC(ASSUME `k <= x:num`) THEN REWRITE_TAC[LE_LT] THEN
 139         DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC SUBST_ALL_TAC) THENL
 140          [EXISTS_TAC `x - 1` THEN EXPAND_TAC "q" THEN BETA_TAC THEN
 141           UNDISCH_TAC `k < x:num` THEN
 142           DISCH_THEN(X_CHOOSE_THEN `d:num` MP_TAC o MATCH_MP LESS_ADD_1) THEN
 143           REWRITE_TAC[GSYM ADD1; ADD_CLAUSES] THEN
 144           DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[SUC_SUB1] THEN
 145           RULE_ASSUM_TAC(REWRITE_RULE[LT_SUC]) THEN
 146           ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
 147           UNDISCH_TAC `(k + d) < k:num` THEN
 148           REWRITE_TAC[GSYM LE_SUC_LT] THEN CONV_TAC CONTRAPOS_CONV THEN
 149           REWRITE_TAC[GSYM NOT_LT; REWRITE_RULE[ADD_CLAUSES] LESS_ADD_SUC];
 150           SUBST_ALL_TAC(ASSUME `(p:num->num) x = n`) THEN
 151           UNDISCH_TAC `y < n:num` THEN ASM_REWRITE_TAC[LT_REFL]]];
 152       SUBGOAL_THEN `!z. q z :num = p(if z < k then z else SUC z)` MP_TAC THENL
 153        [GEN_TAC THEN EXPAND_TAC "q" THEN BETA_TAC THEN COND_CASES_TAC THEN
 154         REWRITE_TAC[];
 155         DISCH_THEN(fun th -> REWRITE_TAC[th])] THEN
 156       MAP_EVERY X_GEN_TAC [`x1:num`; `x2:num`] THEN STRIP_TAC THEN
 157       UNDISCH_TAC `!y. y < (SUC n) ==>
 158                           ?!x. x < (SUC n) /\ (p x = y)` THEN
 159       DISCH_THEN(MP_TAC o SPEC `y:num`) THEN
 160       REWRITE_TAC[MATCH_MP LESS_SUC (ASSUME `y < n:num`)] THEN
 161       CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) THEN
 162       DISCH_THEN(MP_TAC o SPECL [`if x1 < k then x1 else SUC x1`;
 163         `if x2 < k then x2 else SUC x2`] o CONJUNCT2) THEN
 164       ASM_REWRITE_TAC[] THEN
 165       W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
 166        [CONJ_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[LT_SUC] THEN
 167         MATCH_MP_TAC LESS_SUC THEN ASM_REWRITE_TAC[];
 168         DISCH_THEN(fun th -> DISCH_THEN(MP_TAC o C MATCH_MP th)) THEN
 169         REPEAT COND_CASES_TAC THEN REWRITE_TAC[SUC_INJ] THENL
 170          [DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC `~(x2 < k:num)` THEN
 171           CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
 172           REWRITE_TAC[] THEN MATCH_MP_TAC LT_TRANS THEN
 173           EXISTS_TAC `SUC x2` THEN ASM_REWRITE_TAC[LESS_SUC_REFL];
 174           DISCH_THEN(SUBST_ALL_TAC o SYM) THEN UNDISCH_TAC `~(x1  < k:num)` THEN
 175           CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
 176           REWRITE_TAC[] THEN MATCH_MP_TAC LT_TRANS THEN
 177           EXISTS_TAC `SUC x1` THEN ASM_REWRITE_TAC[LESS_SUC_REFL]]]];
 178     DISCH_THEN(fun th -> FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
 179     DISCH_THEN(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
 180       [GSYM th]) THEN BETA_TAC THEN
 181     UNDISCH_TAC `k < (SUC n)` THEN
 182     REWRITE_TAC[LE_SUC; LT_SUC_LE; LE_ADD2] THEN
 183     DISCH_THEN(X_CHOOSE_TAC `d:num` o MATCH_MP LESS_EQUAL_ADD) THEN
 184     GEN_REWRITE_TAC (RAND_CONV o RATOR_CONV o ONCE_DEPTH_CONV)
 185       [ASSUME `n = k + d:num`] THEN REWRITE_TAC[GSYM SUM_TWO] THEN
 186     GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV)
 187       [ASSUME `n = k + d:num`] THEN
 188     REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] (GSYM ADD_SUC)] THEN
 189     REWRITE_TAC[GSYM SUM_TWO; sum; ADD_CLAUSES] THEN BETA_TAC THEN
 190     REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN BINOP_TAC THENL
 191      [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN
 192       REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN
 193       BETA_TAC THEN EXPAND_TAC "q" THEN ASM_REWRITE_TAC[];
 194       GEN_REWRITE_TAC RAND_CONV [REAL_ADD_SYM] THEN
 195       REWRITE_TAC[ASSUME `(p:num->num) k = n`; REAL_EQ_LADD] THEN
 196       REWRITE_TAC[ADD1; SUM_REINDEX] THEN BETA_TAC THEN
 197       MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN BETA_TAC THEN
 198       REWRITE_TAC[GSYM NOT_LT] THEN DISCH_TAC THEN
 199       EXPAND_TAC "q" THEN BETA_TAC THEN ASM_REWRITE_TAC[ADD1]]]);;
 200
 201 let SUM_REVERSE_0 = prove
 202  (`!n f. sum(0,n) f = sum(0,n) (\k. f((n - 1) - k))`,
 203   REPEAT GEN_TAC THEN
 204   MP_TAC(SPECL [`n:num`; `\x. (n - 1) - x`] SUM_PERMUTE_0) THEN
 205   REWRITE_TAC[] THEN
 206   W(C SUBGOAL_THEN (fun th -> SIMP_TAC[th]) o funpow 2 lhand o snd) THEN
 207   X_GEN_TAC `m:num` THEN REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
 208   DISCH_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 209   EXISTS_TAC `n - 1 - m` THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
 210   POP_ASSUM MP_TAC THEN ARITH_TAC);;
 211
 212 let SUM_REVERSE = prove
 213  (`!n m f. sum(m,n) f = sum(m,n) (\k. f(((n + 2 * m) - 1) - k))`,
 214   REPEAT GEN_TAC THEN SUBST1_TAC(ARITH_RULE `m = 0 + m`) THEN
 215   REWRITE_TAC[SUM_REINDEX] THEN
 216   GEN_REWRITE_TAC LAND_CONV [SUM_REVERSE_0] THEN
 217   REWRITE_TAC[] THEN MATCH_MP_TAC SUM_EQ THEN
 218   GEN_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_0] THEN
 219   DISCH_THEN(fun th -> AP_TERM_TAC THEN MP_TAC th) THEN
 220   ARITH_TAC);;
 221
 222 (* ------------------------------------------------------------------------- *)
 223 (* Following is lifted from fsincos taylor series.                           *)
 224 (* ------------------------------------------------------------------------- *)
 225
 226 let MCLAURIN_SIN = prove
 227  (`!x n. abs(sin x -
 228              sum(0,n) (\m. (if EVEN m then &0
 229                             else -- &1 pow ((m - 1) DIV 2) / &(FACT m)) *
 230                             x pow m))
 231          <= inv(&(FACT n)) * abs(x) pow n`,
 232   REPEAT STRIP_TAC THEN
 233   MP_TAC(SPECL [`sin`; `\n x. if n MOD 4 = 0 then sin(x)
 234                               else if n MOD 4 = 1 then cos(x)
 235                               else if n MOD 4 = 2 then --sin(x)
 236                               else --cos(x)`] MCLAURIN_ALL_LE) THEN
 237   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
 238    [CONJ_TAC THENL
 239      [SIMP_TAC[MOD_0; ARITH_EQ; EQT_INTRO(SPEC_ALL ETA_AX)]; ALL_TAC] THEN
 240     X_GEN_TAC `m:num` THEN X_GEN_TAC `y:real` THEN REWRITE_TAC[] THEN
 241     MP_TAC(SPECL [`m:num`; `4`] DIVISION) THEN
 242     REWRITE_TAC[ARITH_EQ] THEN ABBREV_TAC `d = m MOD 4` THEN
 243     DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC MP_TAC) THEN
 244     REWRITE_TAC[ADD1; GSYM ADD_ASSOC; MOD_MULT_ADD] THEN
 245     SPEC_TAC(`d:num`,`d:num`) THEN CONV_TAC EXPAND_CASES_CONV THEN
 246     CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[] THEN
 247     REPEAT CONJ_TAC THEN
 248     W(MP_TAC o DIFF_CONV o lhand o rator o snd) THEN
 249     SIMP_TAC[REAL_MUL_RID; REAL_NEG_NEG]; ALL_TAC] THEN
 250   DISCH_THEN(MP_TAC o SPECL [`x:real`; `n:num`]) THEN
 251   DISCH_THEN(X_CHOOSE_THEN `t:real`
 252    (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
 253   MATCH_MP_TAC(REAL_ARITH
 254     `(x = y) /\ abs(u) <= v ==> abs((x + u) - y) <= v`) THEN
 255   CONJ_TAC THENL
 256    [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
 257     REWRITE_TAC[SIN_0; COS_0; REAL_NEG_0] THEN
 258     AP_THM_TAC THEN AP_TERM_TAC THEN
 259     MP_TAC(SPECL [`r:num`; `4`] DIVISION) THEN REWRITE_TAC[ARITH_EQ] THEN
 260     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 261     DISCH_THEN(fun th -> GEN_REWRITE_TAC
 262       (RAND_CONV o ONCE_DEPTH_CONV) [th] THEN
 263       MP_TAC(SYM th)) THEN
 264     REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH_EVEN] THEN
 265     UNDISCH_TAC `r MOD 4 < 4` THEN
 266     SPEC_TAC(`r MOD 4`,`d:num`) THEN CONV_TAC EXPAND_CASES_CONV THEN
 267     CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[] THEN
 268     REWRITE_TAC[real_div; REAL_MUL_LZERO] THEN
 269     SIMP_TAC[ARITH_RULE `(x + 1) - 1 = x`;
 270              ARITH_RULE `(x + 3) - 1 = x + 2`;
 271              ARITH_RULE `x * 4 + 2 = 2 * (2 * x + 1)`;
 272              ARITH_RULE `x * 4 = 2 * 2 * x`] THEN
 273     SIMP_TAC[DIV_MULT; ARITH_EQ] THEN
 274     REWRITE_TAC[REAL_POW_NEG; EVEN_ADD; EVEN_MULT; ARITH_EVEN; REAL_POW_ONE];
 275     ALL_TAC] THEN
 276   REWRITE_TAC[REAL_ABS_MUL; REAL_INV_MUL] THEN
 277   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL
 278    [REWRITE_TAC[real_div; REAL_ABS_MUL] THEN
 279     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 280     REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM] THEN
 281     MATCH_MP_TAC REAL_LE_RMUL THEN
 282     SIMP_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
 283     REPEAT COND_CASES_TAC THEN REWRITE_TAC[REAL_ABS_NEG; SIN_BOUND; COS_BOUND];
 284     ALL_TAC] THEN
 285   REWRITE_TAC[REAL_ABS_POW; REAL_LE_REFL]);;
 286
 287 (* ------------------------------------------------------------------------- *)
 288 (* The formulas marked with a star on p. 205 of Knopp's book.                *)
 289 (* ------------------------------------------------------------------------- *)
 290
 291 let COT_HALF_TAN = prove
 292  (`~(integer x)
 293    ==> (cot(pi * x) = &1 / &2 * (cot(pi * x / &2) - tan(pi * x / &2)))`,
 294   REPEAT STRIP_TAC THEN
 295   REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_ADD_LDISTRIB] THEN
 296   REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN
 297   REWRITE_TAC[cot; tan] THEN
 298   REWRITE_TAC[REAL_MUL_RID] THEN
 299   SUBGOAL_THEN `pi * x = &2 * pi * x / &2`
 300    (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 301   THENL
 302    [ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN
 303     SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 304     REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN
 305   ABBREV_TAC `y = pi * x / &2` THEN
 306   REWRITE_TAC[COS_DOUBLE; SIN_DOUBLE] THEN
 307   SUBGOAL_THEN `~(sin y = &0) /\ ~(cos y = &0)` STRIP_ASSUME_TAC THENL
 308    [EXPAND_TAC "y" THEN REWRITE_TAC[SIN_ZERO; COS_ZERO; real_div] THEN
 309     CONJ_TAC THEN
 310     ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c = d) <=> (b * a * c = d)`] THEN
 311     SIMP_TAC[GSYM REAL_MUL_LNEG; REAL_EQ_MUL_RCANCEL; REAL_ENTIRE;
 312              REAL_INV_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ; REAL_LT_IMP_NZ;
 313              PI_POS] THEN
 314     REWRITE_TAC[OR_EXISTS_THM] THEN
 315     REWRITE_TAC[TAUT `a /\ b \/ a /\ c <=> a /\ (b \/ c)`] THEN
 316     DISCH_THEN(CHOOSE_THEN(DISJ_CASES_THEN (MP_TAC o AP_TERM `abs`) o
 317       CONJUNCT2)) THEN
 318     UNDISCH_TAC `~(integer x)` THEN
 319     SIMP_TAC[integer; REAL_ABS_NEG; REAL_ABS_NUM; NOT_EXISTS_THM];
 320     ALL_TAC] THEN
 321   MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&2 * sin y * cos y` THEN
 322   ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 323   REWRITE_TAC[real_div] THEN
 324   ONCE_REWRITE_TAC[REAL_ARITH
 325     `(h * (c * s' - s * c')) * t * s * c =
 326      (t * h) * (c * c * s * s' - s * s * c * c')`] THEN
 327   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 328   REWRITE_TAC[REAL_MUL_RID; REAL_MUL_LID; REAL_POW_2]);;
 329
 330 let COT_HALF_POS = prove
 331  (`~(integer x)
 332    ==> (cot(pi * x) = &1 / &2 * (cot(pi * x / &2) + cot(pi * (x + &1) / &2)))`,
 333   REPEAT STRIP_TAC THEN
 334   REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_ADD_LDISTRIB] THEN
 335   REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN
 336   REWRITE_TAC[cot; COS_ADD; SIN_ADD; COS_PI2; SIN_PI2] THEN
 337   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; REAL_SUB_LZERO] THEN
 338   REWRITE_TAC[REAL_MUL_RID] THEN
 339   SUBGOAL_THEN `pi * x = &2 * pi * x / &2`
 340    (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 341   THENL
 342    [ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN
 343     SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 344     REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN
 345   ABBREV_TAC `y = pi * x / &2` THEN
 346   REWRITE_TAC[COS_DOUBLE; SIN_DOUBLE] THEN
 347   SUBGOAL_THEN `~(sin y = &0) /\ ~(cos y = &0)` STRIP_ASSUME_TAC THENL
 348    [EXPAND_TAC "y" THEN REWRITE_TAC[SIN_ZERO; COS_ZERO; real_div] THEN
 349     CONJ_TAC THEN
 350     ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c = d) <=> (b * a * c = d)`] THEN
 351     SIMP_TAC[GSYM REAL_MUL_LNEG; REAL_EQ_MUL_RCANCEL; REAL_ENTIRE;
 352              REAL_INV_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ; REAL_LT_IMP_NZ;
 353              PI_POS] THEN
 354     REWRITE_TAC[OR_EXISTS_THM] THEN
 355     REWRITE_TAC[TAUT `a /\ b \/ a /\ c <=> a /\ (b \/ c)`] THEN
 356     DISCH_THEN(CHOOSE_THEN(DISJ_CASES_THEN (MP_TAC o AP_TERM `abs`) o
 357       CONJUNCT2)) THEN
 358     UNDISCH_TAC `~(integer x)` THEN
 359     SIMP_TAC[integer; REAL_ABS_NEG; REAL_ABS_NUM; NOT_EXISTS_THM];
 360     ALL_TAC] THEN
 361   MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&2 * sin y * cos y` THEN
 362   ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 363   REWRITE_TAC[real_div] THEN
 364   ONCE_REWRITE_TAC[REAL_ARITH
 365     `(h * c * s' + h * --s * c') * t * s * c =
 366      (t * h) * (c * c * s * s' - s * s * c * c')`] THEN
 367   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 368   REWRITE_TAC[REAL_MUL_RID; REAL_MUL_LID; REAL_POW_2]);;
 369
 370 let COT_HALF_NEG = prove
 371  (`~(integer x)
 372    ==> (cot(pi * x) = &1 / &2 * (cot(pi * x / &2) + cot(pi * (x - &1) / &2)))`,
 373   STRIP_TAC THEN ASM_SIMP_TAC[COT_HALF_POS] THEN
 374   AP_TERM_TAC THEN AP_TERM_TAC THEN
 375   SUBST1_TAC(REAL_ARITH `x + &1 = (x - &1) + &2`) THEN
 376   ABBREV_TAC `y = x - &1` THEN
 377   REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_ADD_LDISTRIB] THEN
 378   SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 379   REWRITE_TAC[cot; SIN_ADD; COS_ADD; SIN_PI; COS_PI] THEN
 380   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID; REAL_SUB_RZERO] THEN
 381   REWRITE_TAC[real_div; REAL_MUL_RNEG; REAL_MUL_LNEG; REAL_INV_NEG] THEN
 382   REWRITE_TAC[REAL_NEG_NEG; REAL_MUL_RID]);;
 383
 384 (* ------------------------------------------------------------------------- *)
 385 (* By induction, the formula marked with the dagger.                         *)
 386 (* ------------------------------------------------------------------------- *)
 387
 388 let COT_HALF_MULTIPLE = prove
 389  (`~(integer x)
 390    ==> !n. cot(pi * x) =
 391            sum(0,2 EXP n)
 392              (\k. cot(pi * (x + &k) / &2 pow n) +
 393                   cot(pi * (x - &k) / &2 pow n)) / &2 pow (n + 1)`,
 394   DISCH_TAC THEN INDUCT_TAC THENL
 395    [REWRITE_TAC[EXP; real_pow; REAL_DIV_1; ADD_CLAUSES; REAL_POW_1] THEN
 396     CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
 397     REWRITE_TAC[real_div; REAL_ADD_RID; REAL_SUB_RZERO; GSYM REAL_MUL_2] THEN
 398     REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c = b * a * c`] THEN
 399     SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID; REAL_OF_NUM_EQ; ARITH_EQ];
 400     ALL_TAC] THEN
 401   FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
 402   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 403    `sum(0,2 EXP n)
 404        (\k. &1 / &2 * (cot (pi * (x + &k) / &2 pow n / &2) +
 405                        cot (pi * ((x + &k) / &2 pow n + &1) / &2)) +
 406             &1 / &2 * (cot (pi * (x - &k) / &2 pow n / &2) +
 407                        cot (pi * ((x - &k) / &2 pow n - &1) / &2))) /
 408     &2 pow (n + 1)` THEN
 409   CONJ_TAC THENL
 410    [AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SUM_EQ THEN
 411     X_GEN_TAC `k:num` THEN DISCH_THEN(K ALL_TAC) THEN
 412     REWRITE_TAC[] THEN BINOP_TAC THENL
 413      [MATCH_MP_TAC COT_HALF_POS THEN
 414       UNDISCH_TAC `~(integer x)` THEN
 415       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 416       SUBGOAL_THEN `x = &2 pow n * (x + &k) / &2 pow n - &k`
 417         (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 418       THENL
 419        [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN
 420         REAL_ARITH_TAC;
 421         SIMP_TAC[integer; REAL_INTEGER_CLOSURES]];
 422       MATCH_MP_TAC COT_HALF_NEG THEN
 423       UNDISCH_TAC `~(integer x)` THEN
 424       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 425       SUBGOAL_THEN `x = &2 pow n * (x - &k) / &2 pow n + &k`
 426         (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 427       THENL
 428        [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN
 429         REAL_ARITH_TAC;
 430         SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]]; ALL_TAC] THEN
 431   REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; SUM_CMUL] THEN
 432   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
 433   ONCE_REWRITE_TAC[real_div] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 434   BINOP_TAC THENL
 435    [ALL_TAC;
 436     REWRITE_TAC[real_pow; REAL_POW_ADD; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN
 437     CONV_TAC REAL_RAT_REDUCE_CONV] THEN
 438   SUBGOAL_THEN `!k. (x + &k) / &2 pow n + &1 = (x + &(2 EXP n + k)) / &2 pow n`
 439    (fun th -> ONCE_REWRITE_TAC[th])
 440   THENL
 441    [GEN_TAC THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
 442     EXISTS_TAC `&2 pow n` THEN
 443     ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES;
 444                  REAL_ADD_LDISTRIB] THEN
 445     REWRITE_TAC[REAL_MUL_RID; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN
 446     REWRITE_TAC[REAL_ADD_AC]; ALL_TAC] THEN
 447   SUBGOAL_THEN `!k. (x - &k) / &2 pow n - &1 = (x - &(2 EXP n + k)) / &2 pow n`
 448    (fun th -> ONCE_REWRITE_TAC[th])
 449   THENL
 450    [GEN_TAC THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
 451     EXISTS_TAC `&2 pow n` THEN
 452     ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES;
 453                  REAL_SUB_LDISTRIB] THEN
 454     REWRITE_TAC[REAL_MUL_RID; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN
 455     REAL_ARITH_TAC; ALL_TAC] THEN
 456   REWRITE_TAC[EXP; MULT_2;
 457               GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_OFFSET)] THEN
 458   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; GSYM REAL_INV_MUL] THEN
 459   REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] (GSYM(CONJUNCT2 real_pow))] THEN
 460   REWRITE_TAC[SUM_ADD] THEN
 461   CONV_TAC(ONCE_DEPTH_CONV (ALPHA_CONV `j:num`)) THEN
 462   REWRITE_TAC[REAL_ADD_AC; ADD_AC]);;
 463
 464 let COT_HALF_KNOPP = prove
 465  (`~(integer x)
 466    ==> !n. cot(pi * x) =
 467            cot(pi * x / &2 pow n) / &2 pow n +
 468            sum(1,2 EXP n - 1)
 469              (\k. cot(pi * (x + &k) / &2 pow (n + 1)) +
 470                   cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1)`,
 471   DISCH_TAC THEN GEN_TAC THEN
 472   FIRST_ASSUM(SUBST1_TAC o SPEC `n:num` o MATCH_MP COT_HALF_MULTIPLE) THEN
 473   SUBGOAL_THEN `!f. sum(0,2 EXP n) f = f 0 + sum(1,2 EXP n - 1) f`
 474    (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 475   THENL
 476    [GEN_TAC THEN SUBGOAL_THEN `2 EXP n = 1 + (2 EXP n - 1)`
 477      (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
 478     THENL
 479      [SIMP_TAC[ARITH_RULE `~(x = 0) ==> (1 + (x - 1) = x)`;
 480                EXP_EQ_0; ARITH_EQ]; ALL_TAC] THEN
 481     REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
 482     REWRITE_TAC[SUM_1; REAL_ADD_AC]; ALL_TAC] THEN
 483   REWRITE_TAC[REAL_ADD_RID; REAL_SUB_RZERO; GSYM REAL_MUL_2] THEN
 484   GEN_REWRITE_TAC LAND_CONV [real_div] THEN
 485   GEN_REWRITE_TAC LAND_CONV [REAL_ADD_RDISTRIB] THEN
 486   REWRITE_TAC[GSYM real_div] THEN
 487   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 488    `(&2 * cot (pi * x / &2 pow n)) / &2 pow (n + 1) +
 489     sum(1,2 EXP n - 1)
 490        (\k. &1 / &2 * (cot (pi * (x + &k) / &2 pow n / &2) +
 491                        cot (pi * ((x + &k) / &2 pow n - &1) / &2)) +
 492             &1 / &2 * (cot (pi * (x - &k) / &2 pow n / &2) +
 493                        cot (pi * ((x - &k) / &2 pow n + &1) / &2))) /
 494     &2 pow (n + 1)` THEN
 495   CONJ_TAC THENL
 496    [AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 497     MATCH_MP_TAC SUM_EQ THEN
 498     X_GEN_TAC `k:num` THEN DISCH_THEN(K ALL_TAC) THEN
 499     REWRITE_TAC[] THEN BINOP_TAC THENL
 500      [MATCH_MP_TAC COT_HALF_NEG THEN
 501       UNDISCH_TAC `~(integer x)` THEN
 502       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 503       SUBGOAL_THEN `x = &2 pow n * (x + &k) / &2 pow n - &k`
 504         (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 505       THENL
 506        [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN
 507         REAL_ARITH_TAC;
 508         SIMP_TAC[integer; REAL_INTEGER_CLOSURES]];
 509       MATCH_MP_TAC COT_HALF_POS THEN
 510       UNDISCH_TAC `~(integer x)` THEN
 511       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 512       SUBGOAL_THEN `x = &2 pow n * (x - &k) / &2 pow n + &k`
 513         (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 514       THENL
 515        [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN
 516         REAL_ARITH_TAC;
 517         SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]]; ALL_TAC] THEN
 518   REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; SUM_CMUL] THEN
 519   ONCE_REWRITE_TAC[AC REAL_ADD_AC
 520    `(a + b) + (c + d) = (a + c) + (b + d)`] THEN
 521   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SUM_ADD] THEN
 522   GEN_REWRITE_TAC (funpow 2 (LAND_CONV o RAND_CONV) o RAND_CONV)
 523     [SUM_REVERSE] THEN
 524   SUBGOAL_THEN `(2 EXP n - 1 + 2 * 1) - 1 = 2 EXP n` SUBST1_TAC THENL
 525    [SUBGOAL_THEN `~(2 EXP n = 0)` MP_TAC THENL
 526      [REWRITE_TAC[EXP_EQ_0; ARITH_EQ];
 527       SPEC_TAC(`2 EXP n`,`m:num`) THEN ARITH_TAC]; ALL_TAC] THEN
 528   REWRITE_TAC[GSYM SUM_ADD] THEN
 529   BINOP_TAC THENL
 530    [GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
 531     ONCE_REWRITE_TAC[ADD_SYM] THEN
 532     REWRITE_TAC[real_div; REAL_POW_ADD; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
 533     AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 534     CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN
 535   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM SUM_CMUL] THEN
 536   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `k:num` THEN
 537   REWRITE_TAC[LE_0; ADD_CLAUSES] THEN STRIP_TAC THEN
 538   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 539   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [real_div] THEN
 540   REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN
 541   SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 542   MATCH_MP_TAC(REAL_ARITH
 543    `(a = e) /\ (d = e) /\ (b = f) /\ (c = f)
 544     ==> ((a + b) + (c + d) = (e + f) * &2)`) THEN
 545   UNDISCH_TAC `k < 2 EXP n - 1 + 1` THEN
 546   SIMP_TAC[ARITH_RULE `~(p = 0) ==> (k < p - 1 + 1 <=> k < p)`;
 547            EXP_EQ_0; ARITH_EQ] THEN
 548   DISCH_TAC THEN
 549   SUBGOAL_THEN `!x. (x / &2 pow n + &1 = (x + &2 pow n) / &2 pow n) /\
 550                     (x / &2 pow n - &1 = (x - &2 pow n) / &2 pow n)`
 551    (fun th -> REWRITE_TAC[th])
 552   THENL
 553    [SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_POW2_CLAUSES; REAL_ADD_RDISTRIB;
 554              REAL_SUB_RDISTRIB; REAL_MUL_LID; REAL_DIV_RMUL;
 555              REAL_LT_IMP_NZ];
 556     ALL_TAC] THEN
 557   SUBGOAL_THEN `!x. x / &2 pow n / &2 = x / &2 pow (n + 1)`
 558    (fun th -> REWRITE_TAC[th])
 559   THENL
 560    [REWRITE_TAC[REAL_POW_ADD; real_div; REAL_POW_1; REAL_INV_MUL;
 561                 GSYM REAL_MUL_ASSOC]; ALL_TAC] THEN
 562   ASM_SIMP_TAC[LT_IMP_LE; GSYM REAL_OF_NUM_SUB; GSYM REAL_OF_NUM_POW] THEN
 563   CONJ_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 564   AP_THM_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC);;
 565
 566 (* ------------------------------------------------------------------------- *)
 567 (* Bounds on the terms in this series.                                       *)
 568 (* ------------------------------------------------------------------------- *)
 569
 570 let SIN_SUMDIFF_LEMMA = prove
 571  (`!x y. sin(x + y) * sin(x - y) = (sin x + sin y) * (sin x - sin y)`,
 572   REPEAT GEN_TAC THEN
 573   REWRITE_TAC[REAL_ARITH
 574    `(x + y) * (x - y) = x * x - y * y`] THEN
 575   REWRITE_TAC[SIN_ADD; real_sub; SIN_NEG; COS_NEG] THEN
 576   REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
 577   REWRITE_TAC[GSYM REAL_ADD_ASSOC; GSYM REAL_MUL_ASSOC;
 578               REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
 579   REWRITE_TAC[REAL_ARITH
 580    `(a = sx * sx + --(sy * sy)) <=> (a + sy * sy + --(sx * sx) = &0)`] THEN
 581   REWRITE_TAC[REAL_ARITH
 582    `a + --(sx * cy * cx * sy) + cx * sy * sx * cy + b = a + b`] THEN
 583   REWRITE_TAC[REAL_ARITH
 584    `(sx * cy * sx * cy + --(cx * sy * cx * sy)) + sy * sy + --(sx * sx) =
 585     (sy * sy + (sx * sx + cx * cx) * (cy * cy)) -
 586     (sx * sx + (sy * sy + cy * cy) * (cx * cx))`] THEN
 587   REWRITE_TAC[REWRITE_RULE[REAL_POW_2] SIN_CIRCLE; REAL_MUL_LID] THEN
 588   REWRITE_TAC[REAL_SUB_REFL]);;
 589
 590 let SIN_ZERO_LEMMA = prove
 591  (`!x. (sin(pi * x) = &0) <=> integer(x)`,
 592   REWRITE_TAC[integer; SIN_ZERO; EVEN_EXISTS] THEN
 593   ONCE_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
 594   SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
 595   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 596   REWRITE_TAC[real_div] THEN
 597   ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c * d = c * b * a * d`] THEN
 598   SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ; REAL_MUL_RID] THEN
 599   REWRITE_TAC[GSYM REAL_MUL_RNEG] THEN
 600   SIMP_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB;
 601            REAL_EQ_MUL_LCANCEL; PI_POS; REAL_LT_IMP_NZ] THEN
 602   REWRITE_TAC[NOT_IMP; NOT_FORALL_THM] THEN
 603   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 604   REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
 605   REWRITE_TAC[REAL_MUL_RNEG; OR_EXISTS_THM] THEN
 606   REWRITE_TAC[REAL_ARITH
 607      `(abs(x) = a) <=> &0 <= a /\ ((x = a) \/ (x = --a))`] THEN
 608   REWRITE_TAC[REAL_POS]);;
 609
 610 let NOT_INTEGER_LEMMA = prove
 611  (`~(x = &0) /\ abs(x) < &1 ==> ~(integer x)`,
 612   ONCE_REWRITE_TAC[GSYM REAL_ABS_ZERO] THEN
 613   CONV_TAC CONTRAPOS_CONV THEN SIMP_TAC[integer; LEFT_IMP_EXISTS_THM] THEN
 614   GEN_TAC THEN DISCH_TAC THEN
 615   REWRITE_TAC[REAL_OF_NUM_EQ; REAL_OF_NUM_LT] THEN
 616   ARITH_TAC);;
 617
 618 let NOT_INTEGER_DIV_POW2 = prove
 619  (`~(integer x) ==> ~(integer(x / &2 pow n))`,
 620   REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 621   SUBGOAL_THEN `x = &2 pow n * x / &2 pow n`
 622    (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 623   THENL
 624    [SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES];
 625     SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]);;
 626
 627 let SIN_ABS_LEMMA = prove
 628  (`!x. abs(x) < pi ==> (abs(sin x) = sin(abs x))`,
 629   GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
 630   ASM_REWRITE_TAC[SIN_0; REAL_ABS_NUM] THEN
 631   REWRITE_TAC[real_abs] THEN ASM_CASES_TAC `&0 <= x` THEN
 632   ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
 633    [SUBGOAL_THEN `&0 < sin x`
 634      (fun th -> ASM_SIMP_TAC[th; REAL_LT_IMP_LE]) THEN
 635     MATCH_MP_TAC SIN_POS_PI THEN ASM_REWRITE_TAC[real_abs] THEN
 636     ASM_REWRITE_TAC[REAL_LT_LE];
 637     SUBGOAL_THEN `&0 < --(sin x)`
 638      (fun th -> SIMP_TAC[th; SIN_NEG;
 639                          REAL_ARITH `&0 < --x ==> ~(&0 <= x)`]) THEN
 640     REWRITE_TAC[GSYM SIN_NEG] THEN MATCH_MP_TAC SIN_POS_PI THEN
 641     ASM_SIMP_TAC[REAL_ARITH `~(x = &0) /\ ~(&0 <= x) ==> &0 < --x`]]);;
 642
 643 let SIN_EQ_LEMMA = prove
 644  (`!x y. &0 <= x /\ x < pi / &2 /\ &0 <= y /\ y < pi / &2
 645          ==> ((sin x = sin y) <=> (x = y))`,
 646   SUBGOAL_THEN
 647    `!x y. &0 <= x /\ x < pi / &2 /\ &0 <= y /\ y < pi / &2 /\ x < y
 648           ==> sin x < sin y`
 649   ASSUME_TAC THENL
 650    [ALL_TAC;
 651     REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
 652     CONV_TAC CONTRAPOS_CONV THEN
 653     REWRITE_TAC[REAL_ARITH `~(x = y) <=> x < y \/ y < x`] THEN
 654     ASM_MESON_TAC[]] THEN
 655   REPEAT STRIP_TAC THEN
 656   MP_TAC(SPECL [`sin`; `cos`; `x:real`; `y:real`] MVT_ALT) THEN
 657   ASM_REWRITE_TAC[DIFF_SIN; REAL_EQ_SUB_RADD] THEN
 658   DISCH_THEN(X_CHOOSE_THEN `z:real` STRIP_ASSUME_TAC) THEN
 659   ASM_REWRITE_TAC[REAL_ARITH `x < a + x <=> &0 < a`] THEN
 660   MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
 661   MATCH_MP_TAC COS_POS_PI2 THEN
 662   ASM_MESON_TAC[REAL_LET_TRANS; REAL_LT_TRANS]);;
 663
 664 let KNOPP_TERM_EQUIVALENT = prove
 665  (`~(integer x) /\ k < 2 EXP n
 666    ==> ((cot(pi * (x + &k) / &2 pow (n + 1)) +
 667          cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1) =
 668         cot(pi * x / &2 pow (n + 1)) / &2 pow n /
 669         (&1 - sin(pi * &k / &2 pow (n + 1)) pow 2 /
 670               sin(pi * x / &2 pow (n + 1)) pow 2))`,
 671   let lemma = prove
 672    (`~(x = &0) /\ (x * a = b) ==> (a = b / x)`,
 673     REPEAT STRIP_TAC THEN
 674     MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `x:real` THEN
 675     ASM_SIMP_TAC[REAL_DIV_LMUL]) in
 676   REPEAT STRIP_TAC THEN SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_POW2_CLAUSES] THEN
 677   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_POW_ADD] THEN
 678   REWRITE_TAC[REAL_POW_1; real_div] THEN
 679   GEN_REWRITE_TAC RAND_CONV [AC REAL_MUL_AC
 680    `((a * b') * c) * b * &2 = (&2 * a) * c * b * b'`] THEN
 681   SIMP_TAC[REAL_MUL_RINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 682   REWRITE_TAC[real_div; REAL_ADD_LDISTRIB; REAL_SUB_LDISTRIB;
 683               REAL_ADD_RDISTRIB; REAL_SUB_RDISTRIB] THEN
 684   REWRITE_TAC[REAL_MUL_RID; GSYM real_div] THEN
 685   ABBREV_TAC `a = pi * x / &2 pow (n + 1)` THEN
 686   ABBREV_TAC `b = pi * &k / &2 pow (n + 1)` THEN
 687   SUBGOAL_THEN
 688    `~(sin(a + b) = &0) /\
 689     ~(sin a = &0) /\
 690     ~(sin(a - b) = &0) /\
 691     ~(&1 - sin(b) pow 2 / sin(a) pow 2 = &0)`
 692   STRIP_ASSUME_TAC THENL
 693    [MATCH_MP_TAC(TAUT
 694       `(a /\ b /\ c) /\ (b ==> d) ==> a /\ b /\ c /\ d`) THEN
 695     CONJ_TAC THENL
 696      [MAP_EVERY EXPAND_TAC ["a"; "b"] THEN
 697       REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB] THEN
 698       REWRITE_TAC[SIN_ZERO_LEMMA] THEN REWRITE_TAC[real_div] THEN
 699       REWRITE_TAC[GSYM REAL_ADD_RDISTRIB; GSYM REAL_SUB_RDISTRIB] THEN
 700       REWRITE_TAC[GSYM real_div] THEN REPEAT CONJ_TAC THEN
 701       MATCH_MP_TAC NOT_INTEGER_DIV_POW2 THEN
 702       ASM_REWRITE_TAC[] THENL
 703        [UNDISCH_TAC `~(integer x)` THEN
 704         REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 705         SUBGOAL_THEN `x = (x + &k) - &k`
 706          (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 707         THENL
 708          [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]];
 709         UNDISCH_TAC `~(integer x)` THEN
 710         REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 711         SUBGOAL_THEN `x = (x - &k) + &k`
 712          (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 713         THENL
 714          [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]];
 715       ALL_TAC] THEN
 716     DISCH_TAC THEN REWRITE_TAC[REAL_SUB_0] THEN
 717     DISCH_THEN(MP_TAC o AP_TERM `( * ) (sin(a) pow 2)`) THEN
 718     ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_POW_EQ_0; REAL_MUL_RID] THEN
 719     REWRITE_TAC[REAL_POW_2] THEN
 720     ONCE_REWRITE_TAC[REAL_ARITH
 721      `(a * a = b * b) <=> ((a + b) * (a - b) = &0)`] THEN
 722     REWRITE_TAC[GSYM SIN_SUMDIFF_LEMMA] THEN
 723     REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN
 724     MAP_EVERY EXPAND_TAC ["a"; "b"] THEN
 725     REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB] THEN
 726     REWRITE_TAC[SIN_ZERO_LEMMA] THEN
 727     REWRITE_TAC[real_div; GSYM REAL_ADD_RDISTRIB; GSYM REAL_SUB_RDISTRIB] THEN
 728     REWRITE_TAC[GSYM real_div] THEN CONJ_TAC THEN
 729     MATCH_MP_TAC NOT_INTEGER_DIV_POW2 THENL
 730      [UNDISCH_TAC `~(integer x)` THEN
 731       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 732       SUBGOAL_THEN `x = (x + &k) - &k`
 733        (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 734       THENL
 735        [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]];
 736       UNDISCH_TAC `~(integer x)` THEN
 737       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
 738       SUBGOAL_THEN `x = (x - &k) + &k`
 739        (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 740       THENL
 741        [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]];
 742     ALL_TAC] THEN
 743   REWRITE_TAC[cot; TAN_ADD; real_sub] THEN REWRITE_TAC[GSYM real_sub] THEN
 744   MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `sin(a + b)` THEN
 745   ASM_SIMP_TAC[REAL_ADD_LDISTRIB; REAL_DIV_LMUL] THEN
 746   MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `sin(a - b)` THEN
 747   ONCE_REWRITE_TAC[REAL_ARITH
 748    `a * (b + c * d) = a * b + c * a * d`] THEN
 749   ASM_SIMP_TAC[REAL_ADD_LDISTRIB; REAL_DIV_LMUL] THEN
 750   MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
 751   EXISTS_TAC `&1 - sin(b) pow 2 / sin(a) pow 2` THEN
 752   ONCE_REWRITE_TAC[REAL_ARITH
 753    `a * b * c * da = b * c * a * da`] THEN
 754   ASM_SIMP_TAC[REAL_DIV_LMUL] THEN
 755   MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `sin(a) pow 2` THEN
 756   ASM_REWRITE_TAC[REAL_POW_2; REAL_ENTIRE] THEN
 757   REWRITE_TAC[real_div; REAL_INV_MUL] THEN
 758   ONCE_REWRITE_TAC[REAL_ARITH
 759    `((sa * sa) * (&1 - sb2 * sa' * sa') * others =
 760      (sa * sa) * v * w * x * y * sa') =
 761     (others * (sa * sa - sb2 * (sa * sa') * (sa * sa')) =
 762      sa * v * w * x * y * sa * sa')`] THEN
 763   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; REAL_MUL_RID] THEN
 764   SUBGOAL_THEN `sin(a - b) * cos(a + b) + sin(a + b) * cos(a - b) =
 765                 sin(&2 * a)`
 766   SUBST1_TAC THENL
 767    [GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
 768     REWRITE_TAC[GSYM SIN_ADD] THEN AP_TERM_TAC THEN REAL_ARITH_TAC;
 769     ALL_TAC] THEN
 770   REWRITE_TAC[SIN_DOUBLE] THEN
 771   GEN_REWRITE_TAC RAND_CONV [REAL_ARITH
 772    `sa * samb * sapb * &2 * ca = (&2 * sa * ca) * samb * sapb`] THEN
 773   AP_TERM_TAC THEN
 774   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 775   REWRITE_TAC[SIN_SUMDIFF_LEMMA] THEN REAL_ARITH_TAC);;
 776
 777 let SIN_LINEAR_ABOVE = prove
 778  (`!x. abs(x) < &1 ==> abs(sin x) <= &2 * abs(x)`,
 779   REPEAT STRIP_TAC THEN
 780   MP_TAC(SPECL [`x:real`; `2`] MCLAURIN_SIN) THEN
 781   CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
 782   REWRITE_TAC[real_pow; REAL_POW_1] THEN
 783   CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 784   REWRITE_TAC[REAL_DIV_1; REAL_MUL_LID; REAL_POW_1; REAL_ADD_LID] THEN
 785   MATCH_MP_TAC(REAL_ARITH
 786    `abs(a) <= abs(x) ==> abs(s - x) <= a ==> abs(s) <= &2 * abs(x)`) THEN
 787   REWRITE_TAC[REAL_POW_2; REAL_MUL_ASSOC; REAL_ABS_MUL] THEN
 788   REWRITE_TAC[REAL_ABS_ABS] THEN
 789   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 790   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 791   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 792   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 / &2 * &1` THEN
 793   CONJ_TAC THENL [ALL_TAC; CONV_TAC REAL_RAT_REDUCE_CONV] THEN
 794   MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
 795   CONV_TAC REAL_RAT_REDUCE_CONV);;
 796
 797 let SIN_LINEAR_BELOW = prove
 798  (`!x. abs(x) < &2 ==> abs(sin x) >= abs(x) / &3`,
 799   REPEAT STRIP_TAC THEN
 800   MP_TAC(SPECL [`x:real`; `3`] MCLAURIN_SIN) THEN
 801   CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
 802   REWRITE_TAC[real_pow; REAL_POW_1] THEN
 803   CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 804   REWRITE_TAC[REAL_DIV_1; REAL_MUL_LID; REAL_POW_1; REAL_ADD_LID] THEN
 805   REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN
 806   SIMP_TAC[real_ge; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 807   MATCH_MP_TAC(REAL_ARITH
 808    `&3 * abs(a) <= &2 * abs(x)
 809     ==> abs(s - x) <= a ==> abs(x) <= abs(s) * &3`) THEN
 810   REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_ABS; REAL_MUL_ASSOC] THEN
 811   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 812   CONV_TAC(LAND_CONV(RAND_CONV(RAND_CONV num_CONV))) THEN
 813   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 814   REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN
 815   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 816   REWRITE_TAC[real_div; REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN
 817   SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 818   REWRITE_TAC[GSYM REAL_POW_2] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
 819   ASM_SIMP_TAC[REAL_ABS_POS; REAL_LT_IMP_LE]);;
 820
 821 let KNOPP_TERM_BOUND_LEMMA = prove
 822  (`~(integer x) /\ k < 2 EXP n /\ &6 * abs(x) < &k
 823    ==> abs(a / (&1 - sin(pi * &k / &2 pow (n + 1)) pow 2 /
 824                      sin(pi * x / &2 pow (n + 1)) pow 2))
 825        <= abs(a) / ((&k / (&6 * x)) pow 2 - &1)`,
 826   REPEAT STRIP_TAC THEN
 827   SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
 828    [UNDISCH_TAC `~(integer x)` THEN
 829     REWRITE_TAC[TAUT `(~b ==> ~a) <=> (a ==> b)`] THEN
 830     SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL];
 831     ALL_TAC] THEN
 832   REWRITE_TAC[REAL_ABS_DIV] THEN
 833   ONCE_REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
 834   REWRITE_TAC[REAL_ABS_POS] THEN
 835   MATCH_MP_TAC REAL_LE_INV2 THEN CONJ_TAC THENL
 836    [REWRITE_TAC[REAL_SUB_LT] THEN
 837     ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
 838     REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_MUL; REAL_ABS_NUM] THEN
 839     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
 840     REWRITE_TAC[GSYM REAL_POW_2] THEN
 841     MATCH_MP_TAC REAL_POW_LT2 THEN
 842     REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
 843     UNDISCH_TAC `&6 * abs(x) < &k` THEN
 844     GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_MUL_LID] THEN
 845     MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
 846     MATCH_MP_TAC REAL_LT_RDIV_EQ THEN
 847     ASM_SIMP_TAC[REAL_LT_MUL; REAL_OF_NUM_LT; ARITH; GSYM REAL_ABS_NZ];
 848     ALL_TAC] THEN
 849   MATCH_MP_TAC(REAL_ARITH
 850    `&0 <= x /\ x <= y ==> x - &1 <= abs(&1 - y)`) THEN
 851   CONJ_TAC THENL [REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]; ALL_TAC] THEN
 852   REWRITE_TAC[GSYM REAL_POW_DIV] THEN
 853   ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
 854   MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
 855   MATCH_MP_TAC REAL_LE_TRANS THEN
 856   EXISTS_TAC `(abs(pi * &k / &2 pow (n + 1)) / &3) *
 857               inv(&2 * abs(pi * x / &2 pow (n + 1)))` THEN
 858   CONJ_TAC THENL
 859    [REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN
 860     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_INV_MUL] THEN
 861     ONCE_REWRITE_TAC[AC REAL_MUL_AC
 862      `p * k * q' * k1 * k2 * p' * x' * q =
 863       k * (k1 * k2) * x' * (p * p') * (q * q')`] THEN
 864     SIMP_TAC[REAL_INV_INV; REAL_MUL_RINV; REAL_ABS_ZERO;
 865              REAL_LT_IMP_NZ; REAL_POW2_CLAUSES; PI_POS] THEN
 866     CONV_TAC REAL_RAT_REDUCE_CONV THEN
 867   REWRITE_TAC[REAL_MUL_RID; REAL_LE_REFL]; ALL_TAC] THEN
 868   GEN_REWRITE_TAC RAND_CONV [REAL_ABS_DIV] THEN
 869   GEN_REWRITE_TAC RAND_CONV [real_div] THEN
 870   MATCH_MP_TAC REAL_LE_MUL2 THEN
 871   SIMP_TAC[REAL_LE_INV_EQ; REAL_LE_DIV; REAL_LE_MUL;
 872            REAL_ABS_POS; REAL_POS] THEN
 873   CONJ_TAC THENL
 874    [REWRITE_TAC[GSYM real_ge] THEN MATCH_MP_TAC SIN_LINEAR_BELOW THEN
 875     REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN
 876     SIMP_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM;
 877              REAL_LT_LDIV_EQ; REAL_POW2_CLAUSES] THEN
 878     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
 879     SIMP_TAC[real_abs; REAL_LT_IMP_LE; PI_POS] THEN
 880     MATCH_MP_TAC REAL_LTE_TRANS THEN
 881     EXISTS_TAC `pi * &2 pow n` THEN CONJ_TAC THENL
 882      [ASM_SIMP_TAC[REAL_LT_LMUL_EQ; PI_POS; REAL_OF_NUM_POW; REAL_OF_NUM_LT];
 883       ALL_TAC] THEN
 884     ONCE_REWRITE_TAC[ADD_SYM] THEN
 885     REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC] THEN
 886     SIMP_TAC[REAL_LE_RMUL_EQ; REAL_POW2_CLAUSES] THEN
 887     MATCH_MP_TAC(C MATCH_MP PI_APPROX_25_BITS (REAL_ARITH
 888      `abs(p - y) <= e ==> y + e <= a ==> p <= a`)) THEN
 889     CONV_TAC REAL_RAT_REDUCE_CONV;
 890     MATCH_MP_TAC REAL_LE_INV2 THEN
 891     REWRITE_TAC[GSYM REAL_ABS_NZ; SIN_ZERO_LEMMA] THEN
 892     ASM_SIMP_TAC[NOT_INTEGER_DIV_POW2] THEN
 893     MATCH_MP_TAC SIN_LINEAR_ABOVE THEN
 894     REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN
 895     SIMP_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM;
 896              REAL_LT_LDIV_EQ; REAL_POW2_CLAUSES] THEN
 897     REWRITE_TAC[REAL_MUL_LID] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 898     MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(&6)` THEN
 899     CONV_TAC (LAND_CONV REAL_RAT_REDUCE_CONV) THEN
 900     REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_MUL_ASSOC] THEN
 901     MATCH_MP_TAC REAL_LTE_TRANS THEN
 902     EXISTS_TAC `abs(&k * pi)` THEN CONJ_TAC THENL
 903      [ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
 904       MATCH_MP_TAC REAL_LT_RMUL THEN
 905       ASM_REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
 906       SIMP_TAC[PI_POS; REAL_ARITH `&0 < x ==> &0 < abs x`];
 907       ALL_TAC] THEN
 908     MATCH_MP_TAC REAL_LE_TRANS THEN
 909     EXISTS_TAC `abs(&2 pow n * pi)` THEN CONJ_TAC THENL
 910      [ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
 911       MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 912       REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_POW; REAL_OF_NUM_LE] THEN
 913       ASM_SIMP_TAC[LT_IMP_LE]; ALL_TAC] THEN
 914     GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
 915     REWRITE_TAC[REAL_POW_ADD; REAL_ABS_POW; REAL_ABS_NUM;
 916                 REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN
 917     SIMP_TAC[REAL_LE_LMUL_EQ; REAL_POW2_CLAUSES] THEN
 918     MATCH_MP_TAC(C MATCH_MP PI_APPROX_25_BITS (REAL_ARITH
 919      `abs(p - y) <= e ==> abs y + e <= a ==> abs p <= a`)) THEN
 920     CONV_TAC REAL_RAT_REDUCE_CONV]);;
 921
 922 let KNOPP_TERM_BOUND = prove
 923  (`~(integer x) /\ k < 2 EXP n /\ &6 * abs(x) < &k
 924    ==> abs((cot(pi * (x + &k) / &2 pow (n + 1)) +
 925             cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1))
 926        <= abs(cot(pi * x / &2 pow (n + 1)) / &2 pow n) *
 927           (&36 * x pow 2) / (&k pow 2 - &36 * x pow 2)`,
 928   REPEAT STRIP_TAC THEN
 929   ASM_SIMP_TAC[KNOPP_TERM_EQUIVALENT] THEN
 930   MATCH_MP_TAC REAL_LE_TRANS THEN
 931   EXISTS_TAC `abs(cot(pi * x / &2 pow (n + 1)) / &2 pow n) /
 932               ((&k / (&6 * x)) pow 2 - &1)` THEN
 933   ASM_SIMP_TAC[KNOPP_TERM_BOUND_LEMMA] THEN
 934   GEN_REWRITE_TAC LAND_CONV [real_div] THEN
 935   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 936   MATCH_MP_TAC REAL_EQ_IMP_LE THEN
 937   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_DIV] THEN AP_TERM_TAC THEN
 938   SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&6 pow 2`)) THEN
 939   REWRITE_TAC[GSYM REAL_POW_MUL] THEN REWRITE_TAC[REAL_POW_DIV] THEN
 940   SUBGOAL_THEN `&0 < (&6 * x) pow 2`
 941    (fun th -> SIMP_TAC[th; REAL_EQ_RDIV_EQ; REAL_SUB_RDISTRIB;
 942                        REAL_MUL_LID; REAL_DIV_RMUL; REAL_LT_IMP_NZ]) THEN
 943   ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN MATCH_MP_TAC REAL_POW_LT THEN
 944   REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN
 945   UNDISCH_TAC `~(integer x)` THEN
 946   REWRITE_TAC[TAUT `(~b ==> ~a) <=> (a ==> b)`] THEN
 947   SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);;
 948
 949 (* ------------------------------------------------------------------------- *)
 950 (* Show that the series we're looking at do in fact converge...              *)
 951 (* ------------------------------------------------------------------------- *)
 952
 953 let SUMMABLE_INVERSE_SQUARES_LEMMA = prove
 954  (`(\n. inv(&(n + 1) * &(n + 2))) sums &1`,
 955   REWRITE_TAC[sums] THEN
 956   SUBGOAL_THEN
 957    `!n. sum(0,n) (\m. inv(&(m + 1) * &(m + 2))) = &1 - inv(&(n + 1))`
 958    (fun th -> REWRITE_TAC[th])
 959   THENL
 960    [INDUCT_TAC THEN REWRITE_TAC[sum] THEN
 961     CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 962     ASM_REWRITE_TAC[ADD_CLAUSES] THEN
 963     REWRITE_TAC[REAL_ARITH `(&1 - a + b = &1 - c) <=> (b + c = a)`] THEN
 964     CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN
 965     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 966     REWRITE_TAC[REAL_INV_MUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
 967     SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_RULE `~(n + 1 = 0)`] THEN
 968     REWRITE_TAC[REAL_MUL_LID; ARITH_RULE `SUC(n + 1) = n + 2`] THEN
 969     MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&(n + 2)` THEN
 970     SIMP_TAC[REAL_ADD_RDISTRIB; real_div; GSYM REAL_MUL_ASSOC; REAL_OF_NUM_EQ;
 971              REAL_MUL_LINV; ARITH_RULE `~(n + 2 = 0)`; REAL_MUL_LID;
 972              REAL_MUL_RID] THEN
 973     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN ARITH_TAC;
 974     ALL_TAC] THEN
 975   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_SUB_RZERO] THEN
 976   MATCH_MP_TAC SEQ_SUB THEN REWRITE_TAC[SEQ_CONST] THEN
 977   MATCH_MP_TAC SEQ_INV0 THEN X_GEN_TAC `x:real` THEN
 978   X_CHOOSE_TAC `N:num` (SPEC `x:real` REAL_ARCH_SIMPLE) THEN
 979   EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN
 980   REWRITE_TAC[real_gt; GE] THEN DISCH_TAC THEN
 981   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[] THEN
 982   ASM_SIMP_TAC[REAL_OF_NUM_LT; ARITH_RULE `a < b + 1 <=> a <= b`]);;
 983
 984 let SUMMABLE_INVERSE_SQUARES = prove
 985  (`summable (\n. inv(&n pow 2))`,
 986   MATCH_MP_TAC SUM_SUMMABLE THEN
 987   EXISTS_TAC `sum(0,2) (\n. inv(&n pow 2)) +
 988               suminf (\n. inv(&(n + 2) pow 2))` THEN
 989   MATCH_MP_TAC SER_OFFSET_REV THEN
 990   MATCH_MP_TAC SER_ACONV THEN MATCH_MP_TAC SER_COMPARA THEN
 991   EXISTS_TAC `\n. inv(&(n + 1) * &(n + 2))` THEN CONJ_TAC THENL
 992    [ALL_TAC;
 993     MATCH_MP_TAC SUM_SUMMABLE THEN EXISTS_TAC `&1` THEN
 994     REWRITE_TAC[SUMMABLE_INVERSE_SQUARES_LEMMA]] THEN
 995   EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
 996   REWRITE_TAC[REAL_POW_2; REAL_INV_MUL; REAL_ABS_INV; REAL_ABS_NUM;
 997               REAL_ABS_MUL] THEN
 998   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
 999   MATCH_MP_TAC REAL_LE_INV2 THEN
1000   REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC);;
1001
1002 let SUMMABLE_INVERSE_POWERS = prove
1003  (`!m. 2 <= m ==> summable (\n. inv(&(n + 1) pow m))`,
1004   REPEAT STRIP_TAC THEN MATCH_MP_TAC SER_COMPAR THEN
1005   EXISTS_TAC `\m. inv (&(m + 1) pow 2)` THEN CONJ_TAC THENL
1006    [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
1007     REWRITE_TAC[REAL_ABS_INV; REAL_ABS_POW; REAL_ABS_NUM] THEN
1008     MATCH_MP_TAC REAL_LE_INV2 THEN
1009     SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH_RULE `0 < n + 1`] THEN
1010     MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
1011     ARITH_TAC;
1012     REWRITE_TAC[summable] THEN
1013     EXISTS_TAC
1014      `suminf (\m. inv (&m pow 2)) - sum(0,1) (\m. inv (&m pow 2))` THEN
1015     MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM] SER_OFFSET) THEN
1016     REWRITE_TAC[SUMMABLE_INVERSE_SQUARES]]);;
1017
1018 let COT_TYPE_SERIES_CONVERGES = prove
1019  (`!x. ~(integer x) ==> summable (\n. inv(&n pow 2 - x))`,
1020   REPEAT STRIP_TAC THEN
1021   MATCH_MP_TAC SER_ACONV THEN MATCH_MP_TAC SER_COMPARA THEN
1022   EXISTS_TAC `\n. &2 / &n pow 2` THEN CONJ_TAC THENL
1023    [ALL_TAC;
1024     MATCH_MP_TAC SUM_SUMMABLE THEN
1025     EXISTS_TAC `&2 * suminf (\n. inv(&n pow 2))` THEN
1026     REWRITE_TAC[real_div] THEN MATCH_MP_TAC SER_CMUL THEN
1027     MATCH_MP_TAC SUMMABLE_SUM THEN
1028     REWRITE_TAC[SUMMABLE_INVERSE_SQUARES]] THEN
1029   MP_TAC(SPEC `&2 * abs x + &1` REAL_ARCH_SIMPLE) THEN
1030   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
1031   EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN
1032   REWRITE_TAC[GE] THEN DISCH_TAC THEN
1033   SUBGOAL_THEN `&0 < &n pow 2`
1034    (fun th -> SIMP_TAC[th; REAL_LE_RDIV_EQ])
1035   THENL
1036    [MATCH_MP_TAC REAL_POW_LT THEN
1037     MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN
1038     ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
1039     UNDISCH_TAC `&2 * abs x + &1 <= &N` THEN REAL_ARITH_TAC;
1040     ALL_TAC] THEN
1041   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_ABS_INV] THEN
1042   REWRITE_TAC[GSYM real_div] THEN
1043   SUBGOAL_THEN `&0 < abs(&n pow 2 - x)`
1044    (fun th -> SIMP_TAC[REAL_LE_LDIV_EQ; th])
1045   THENL
1046    [REWRITE_TAC[GSYM REAL_ABS_NZ] THEN
1047     UNDISCH_TAC `~(integer x)` THEN
1048     REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
1049     DISCH_TAC THEN
1050     SUBST1_TAC(REAL_ARITH `x = &n pow 2 - (&n pow 2 - x)`) THEN
1051     ASM_REWRITE_TAC[REAL_SUB_RZERO] THEN
1052     SIMP_TAC[integer; REAL_INTEGER_CLOSURES]; ALL_TAC] THEN
1053   MATCH_MP_TAC(REAL_ARITH
1054    `&2 * abs(x) + &1 <= a ==> a <= &2 * abs(a - x)`) THEN
1055   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[] THEN
1056   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N pow 2` THEN CONJ_TAC THENL
1057    [REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; EXP_2; LE_SQUARE_REFL];
1058     ASM_SIMP_TAC[REAL_POW_LE2; REAL_OF_NUM_LE; LE_0]]);;
1059
1060 (* ------------------------------------------------------------------------- *)
1061 (* Now the rather tricky limiting argument gives the result.                 *)
1062 (* ------------------------------------------------------------------------- *)
1063
1064 let SIN_X_RANGE = prove
1065  (`!x. abs(sin(x) - x) <= abs(x) pow 2 / &2`,
1066   GEN_TAC THEN
1067   MP_TAC(SPECL [`x:real`; `2`] MCLAURIN_SIN) THEN
1068   CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1069   REWRITE_TAC[ARITH; REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID] THEN
1070   CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1071   REWRITE_TAC[REAL_DIV_1; REAL_POW_1; REAL_MUL_LID] THEN
1072   REWRITE_TAC[real_div; REAL_MUL_LID] THEN REWRITE_TAC[REAL_MUL_AC]);;
1073
1074 let SIN_X_X_RANGE = prove
1075  (`!x. ~(x = &0) ==> abs(sin(x) / x - &1) <= abs(x) / &2`,
1076   REPEAT STRIP_TAC THEN
1077   MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN
1078   ASM_REWRITE_TAC[GSYM REAL_ABS_MUL; GSYM REAL_ABS_NZ] THEN
1079   ASM_SIMP_TAC[REAL_SUB_LDISTRIB; REAL_DIV_LMUL] THEN
1080   REWRITE_TAC[real_div; REAL_MUL_ASSOC; REAL_MUL_RID] THEN
1081   REWRITE_TAC[GSYM REAL_POW_2; SIN_X_RANGE; GSYM real_div]);;
1082
1083 let SIN_X_LIMIT = prove
1084  (`((\x. sin(x) / x) tends_real_real &1)(&0)`,
1085   REWRITE_TAC[LIM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1086   REWRITE_TAC[REAL_SUB_RZERO] THEN EXISTS_TAC `e:real` THEN
1087   ASM_REWRITE_TAC[] THEN
1088   X_GEN_TAC `x:real` THEN STRIP_TAC THEN
1089   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(x) / &2` THEN
1090   ASM_SIMP_TAC[SIN_X_X_RANGE; REAL_ABS_NZ] THEN
1091   ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1092   UNDISCH_TAC `abs(x) < e` THEN REAL_ARITH_TAC);;
1093
1094 let COT_X_LIMIT = prove
1095  (`((\x. x * cot(x)) tends_real_real &1)(&0)`,
1096   SUBGOAL_THEN `(cos tends_real_real &1)(&0)` MP_TAC THENL
1097    [MP_TAC(SPEC `&0` DIFF_COS) THEN
1098     DISCH_THEN(MP_TAC o MATCH_MP DIFF_CONT) THEN
1099     REWRITE_TAC[contl; REAL_ADD_LID; COS_0] THEN
1100     CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]; ALL_TAC] THEN
1101   DISCH_THEN(MP_TAC o C CONJ SIN_X_LIMIT) THEN
1102   DISCH_THEN(MP_TAC o C CONJ (REAL_ARITH `~(&1 = &0)`)) THEN
1103   REWRITE_TAC[GSYM CONJ_ASSOC] THEN
1104   DISCH_THEN(MP_TAC o MATCH_MP LIM_DIV) THEN
1105   REWRITE_TAC[REAL_DIV_1; cot] THEN
1106   REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_AC; REAL_INV_INV]);;
1107
1108 let COT_LIMIT_LEMMA = prove
1109  (`!x. ~(x = &0)
1110        ==> (\n. (x / &2 pow n) * cot(x / &2 pow n)) tends_num_real &1`,
1111   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SEQ] THEN
1112   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1113   MP_TAC COT_X_LIMIT THEN REWRITE_TAC[LIM] THEN
1114   DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1115   DISCH_THEN(X_CHOOSE_THEN `d:real` MP_TAC) THEN
1116   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1117   REWRITE_TAC[REAL_SUB_RZERO] THEN DISCH_TAC THEN
1118   X_CHOOSE_TAC `N:num` (SPEC `abs(x) / d` REAL_ARCH_POW2) THEN
1119   EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[GE] THEN
1120   DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1121   REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM] THEN
1122   ASM_SIMP_TAC[REAL_POW2_CLAUSES; REAL_LT_DIV; GSYM REAL_ABS_NZ] THEN
1123   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_POW2_CLAUSES] THEN
1124   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1125   ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ] THEN
1126   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 pow N` THEN
1127   ASM_REWRITE_TAC[REAL_POW2_THM]);;
1128
1129 let COT_LIMIT_LEMMA1 = prove
1130  (`~(x = &0)
1131    ==> (\n. (pi / &2 pow (n + 1)) * cot(pi * x / &2 pow (n + 1)))
1132        tends_num_real (inv(x))`,
1133   DISCH_TAC THEN
1134   MP_TAC(SPEC `pi * x * inv(&2)` COT_LIMIT_LEMMA) THEN
1135   ASM_SIMP_TAC[REAL_ENTIRE; REAL_LT_IMP_NZ; PI_POS] THEN
1136   CONV_TAC REAL_RAT_REDUCE_CONV THEN
1137   REWRITE_TAC[real_div; REAL_MUL_LID; GSYM REAL_MUL_ASSOC] THEN
1138   ONCE_REWRITE_TAC[AC REAL_MUL_AC
1139    `p * x * a * b * c = x * (p * (a * b)) * c`] THEN
1140   REWRITE_TAC[GSYM REAL_INV_MUL] THEN
1141   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
1142   REWRITE_TAC[ADD1; GSYM real_div] THEN DISCH_TAC THEN
1143   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [GSYM REAL_MUL_LID] THEN
1144   FIRST_ASSUM(SUBST1_TAC o GSYM o MATCH_MP REAL_MUL_LINV) THEN
1145   REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1146   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1147   MATCH_MP_TAC SEQ_MUL THEN REWRITE_TAC[SEQ_CONST] THEN
1148   ONCE_REWRITE_TAC[AC REAL_MUL_AC `x * p * q * c = x * (p * q) * c`] THEN
1149   ASM_REWRITE_TAC[GSYM real_div]);;
1150
1151 let COT_X_BOUND_LEMMA_POS = prove
1152  (`?M. !x. &0 < x /\ abs(x) <= &1 ==> abs(x * cot(x)) <= M`,
1153   MP_TAC COT_X_LIMIT THEN REWRITE_TAC[LIM] THEN
1154   DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN
1155   REWRITE_TAC[REAL_SUB_RZERO] THEN
1156   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1157   MP_TAC(SPECL [`\x. x * cot(x)`; `d:real`; `&1`] CONT_BOUNDED_ABS) THEN
1158   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
1159    [X_GEN_TAC `x:real` THEN STRIP_TAC THEN
1160     MATCH_MP_TAC CONT_MUL THEN CONJ_TAC THENL
1161      [MATCH_MP_TAC DIFF_CONT THEN
1162       EXISTS_TAC `&1` THEN REWRITE_TAC[DIFF_X]; ALL_TAC] THEN
1163     GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
1164     REWRITE_TAC[cot] THEN MATCH_MP_TAC CONT_DIV THEN REPEAT CONJ_TAC THENL
1165      [MATCH_MP_TAC DIFF_CONT THEN
1166       EXISTS_TAC `--(sin x)` THEN REWRITE_TAC[DIFF_COS];
1167       MATCH_MP_TAC DIFF_CONT THEN
1168       EXISTS_TAC `cos x` THEN REWRITE_TAC[DIFF_SIN];
1169       MATCH_MP_TAC REAL_LT_IMP_NZ THEN MATCH_MP_TAC SIN_POS_PI THEN
1170       SUBGOAL_THEN `&1 < pi`
1171        (fun th -> ASM_MESON_TAC[th; REAL_LET_TRANS; REAL_LTE_TRANS]) THEN
1172       MP_TAC PI_APPROX_25_BITS THEN
1173       MATCH_MP_TAC(REAL_ARITH
1174        `&1 + e < a ==> abs(p - a) <= e ==> &1 < p`) THEN
1175       CONV_TAC REAL_RAT_REDUCE_CONV]; ALL_TAC] THEN
1176   DISCH_THEN(X_CHOOSE_TAC `M:real`) THEN EXISTS_TAC `abs M + &2` THEN
1177   X_GEN_TAC `x:real` THEN STRIP_TAC THEN
1178   DISJ_CASES_TAC(SPECL [`abs x`; `d:real`] REAL_LTE_TOTAL) THENL
1179    [MATCH_MP_TAC(REAL_ARITH `abs(x - &1) < &1 ==> abs(x) <= abs(m) + &2`) THEN
1180     FIRST_ASSUM MATCH_MP_TAC THEN
1181     ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`];
1182     MATCH_MP_TAC(REAL_ARITH `x <= m ==> x <= abs(m) + &2`) THEN
1183     FIRST_ASSUM MATCH_MP_TAC THEN
1184     MAP_EVERY UNDISCH_TAC [`&0 < x`; `abs(x) <= &1`; `d <= abs(x)`] THEN
1185     REAL_ARITH_TAC]);;
1186
1187 let COT_X_BOUND_LEMMA = prove
1188  (`?M. !x. ~(x = &0) /\ abs(x) <= &1 ==> abs(x * cot(x)) <= M`,
1189   X_CHOOSE_TAC `M:real` COT_X_BOUND_LEMMA_POS THEN
1190   EXISTS_TAC `M:real` THEN X_GEN_TAC `x:real` THEN
1191   REPEAT STRIP_TAC THEN
1192   FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
1193    `~(x = &0) ==> &0 < x \/ &0 < --x`)) THEN
1194   ASM_SIMP_TAC[] THEN
1195   SUBGOAL_THEN `x * cot(x) = --x * cot(--x)` SUBST1_TAC THENL
1196    [ALL_TAC; ASM_SIMP_TAC[REAL_ABS_NEG]] THEN
1197   REWRITE_TAC[cot; SIN_NEG; COS_NEG; real_div; REAL_INV_NEG;
1198               REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
1199
1200 let COT_PARTIAL_FRACTIONS = prove
1201  (`~(integer x)
1202    ==> (\n. (&2 * x pow 2) / (x pow 2 - &n pow 2)) sums
1203        ((pi * x) * cot(pi * x) + &1)`,
1204   REPEAT STRIP_TAC THEN
1205   SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
1206    [UNDISCH_TAC `~(integer x)` THEN
1207     REWRITE_TAC[TAUT `(~b ==> ~a) <=> (a ==> b)`] THEN
1208     SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL];
1209     ALL_TAC] THEN
1210   ABBREV_TAC
1211    `A = \n k. (pi * x / &2 pow n) * cot(pi * x / &2 pow n) +
1212               (pi * x / &2 pow (n + 1)) *
1213               sum(1,k) (\m. cot (pi * (x + &m) / &2 pow (n + 1)) +
1214                             cot (pi * (x - &m) / &2 pow (n + 1)))` THEN
1215   ABBREV_TAC
1216    `B = \n k. (pi * x / &2 pow (n + 1)) *
1217               sum(k + 1,2 EXP n - 1 - k)
1218                  (\m. cot(pi * (x + &m) / &2 pow (n + 1)) +
1219                       cot(pi * (x - &m) / &2 pow (n + 1)))` THEN
1220   SUBGOAL_THEN `!n. ~(x - &n = &0)` ASSUME_TAC THENL
1221    [X_GEN_TAC `n:num` THEN UNDISCH_TAC `~(integer x)` THEN
1222     REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN DISCH_TAC THEN
1223     SUBGOAL_THEN `x = (x - &n) + &n` SUBST1_TAC THENL
1224      [REAL_ARITH_TAC; ASM_SIMP_TAC[integer; REAL_INTEGER_CLOSURES]];
1225     ALL_TAC] THEN
1226   SUBGOAL_THEN `!n. ~(x + &n = &0)` ASSUME_TAC THENL
1227    [X_GEN_TAC `n:num` THEN UNDISCH_TAC `~(integer x)` THEN
1228     REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN DISCH_TAC THEN
1229     SUBGOAL_THEN `x = (x + &n) - &n` SUBST1_TAC THENL
1230      [REAL_ARITH_TAC; ASM_SIMP_TAC[integer; REAL_INTEGER_CLOSURES]];
1231     ALL_TAC] THEN
1232   SUBGOAL_THEN `!n. ~(x pow 2 - &n pow 2 = &0)` ASSUME_TAC THENL
1233    [GEN_TAC THEN REWRITE_TAC[REAL_POW_2] THEN
1234     ONCE_REWRITE_TAC[REAL_ARITH `a * a - b * b = (a + b) * (a - b)`] THEN
1235     ASM_REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM]; ALL_TAC] THEN
1236   SUBGOAL_THEN
1237    `!n. (&2 * x) / (x pow 2 - &n pow 2) = inv(x + &n) + inv(x - &n)`
1238   ASSUME_TAC THENL
1239    [X_GEN_TAC `n:num` THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN
1240     EXISTS_TAC `x pow 2 - &n pow 2` THEN ASM_SIMP_TAC[REAL_DIV_LMUL] THEN
1241     REWRITE_TAC[REAL_POW_2; REAL_ADD_LDISTRIB] THEN
1242     ONCE_REWRITE_TAC[REAL_ARITH `a * a - b * b = (a + b) * (a - b)`] THEN
1243     ONCE_REWRITE_TAC[REAL_ARITH
1244      `(p * m) * p' + (p * m) * m' = m * p * p' + p * m * m'`] THEN
1245     ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN REAL_ARITH_TAC;
1246     ALL_TAC] THEN
1247   SUBGOAL_THEN `!k. (\n. A n k) tends_num_real
1248                     (&1 + sum(1,k) (\n. (&2 * x pow 2) / (x pow 2 - &n pow 2)))`
1249   ASSUME_TAC THENL
1250    [X_GEN_TAC `k:num` THEN EXPAND_TAC "A" THEN REWRITE_TAC[] THEN
1251     MATCH_MP_TAC SEQ_ADD THEN CONJ_TAC THENL
1252      [REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
1253       REWRITE_TAC[GSYM real_div] THEN
1254       MATCH_MP_TAC COT_LIMIT_LEMMA THEN
1255       ASM_SIMP_TAC[REAL_ENTIRE; PI_POS; REAL_LT_IMP_NZ];
1256       ALL_TAC] THEN
1257     REWRITE_TAC[GSYM SUM_CMUL] THEN MATCH_MP_TAC SEQ_SUM THEN
1258     X_GEN_TAC `r:num` THEN STRIP_TAC THEN
1259     REWRITE_TAC[REAL_POW_2; real_div] THEN
1260     ONCE_REWRITE_TAC[REAL_ARITH `(&2 * x * x) * d = x * (&2 * x) * d`] THEN
1261     REWRITE_TAC[GSYM REAL_POW_2; GSYM real_div] THEN
1262     ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
1263     MATCH_MP_TAC SEQ_ADD THEN
1264     REWRITE_TAC[real_div] THEN
1265     ONCE_REWRITE_TAC[REAL_ARITH `(p * x * d) * cc = x * (p * d) * cc`] THEN
1266     CONJ_TAC THEN MATCH_MP_TAC SEQ_MUL THEN REWRITE_TAC[SEQ_CONST] THEN
1267     REWRITE_TAC[GSYM real_div] THEN
1268     ASM_SIMP_TAC[COT_LIMIT_LEMMA1]; ALL_TAC] THEN
1269   SUBGOAL_THEN
1270    `!k n. &6 * abs(x) < &k
1271           ==> abs(B n k)
1272               <= abs((pi * x / &2 pow (n + 1)) *
1273                      cot(pi * x / &2 pow (n + 1))) *
1274                  sum(k + 1,2 EXP n - 1 - k)
1275                     (\m. (&72 * x pow 2) / (&m pow 2 - &36 * x pow 2))`
1276   ASSUME_TAC THENL
1277    [REPEAT STRIP_TAC THEN
1278     EXPAND_TAC "B" THEN REWRITE_TAC[GSYM SUM_CMUL] THEN
1279     W(fun (asl,w) -> MP_TAC(PART_MATCH lhand SUM_ABS_LE (lhand w))) THEN
1280     MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1281     MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN
1282     REWRITE_TAC[ARITH_RULE
1283      `k + 1 <= r /\ r < (p - 1 - k) + k + 1 <=> k < r /\ r < p`] THEN
1284     STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
1285     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1286     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
1287     MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN
1288     EXISTS_TAC `abs(inv(&2 pow (n + 1)))` THEN
1289     REWRITE_TAC[GSYM REAL_ABS_MUL] THEN REWRITE_TAC[GSYM real_div] THEN
1290     SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`; REAL_LT_INV_EQ;
1291              REAL_POW2_CLAUSES] THEN
1292     MATCH_MP_TAC REAL_LE_TRANS THEN
1293     EXISTS_TAC
1294      `abs(cot (pi * x / &2 pow (n + 1)) / &2 pow n) *
1295       (&36 * x pow 2) / (&r pow 2 - &36 * x pow 2)` THEN
1296     CONJ_TAC THENL
1297      [MATCH_MP_TAC KNOPP_TERM_BOUND THEN ASM_REWRITE_TAC[] THEN
1298       MATCH_MP_TAC REAL_LT_TRANS THEN
1299       EXISTS_TAC `&k` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LT]; ALL_TAC] THEN
1300     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_POW_ADD;
1301                 REAL_ABS_MUL; REAL_INV_MUL] THEN
1302     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
1303     GEN_REWRITE_TAC RAND_CONV
1304      [AC REAL_MUL_AC `a * b * c * d * e = b * c * d * a * e`] THEN
1305     CONV_TAC REAL_RAT_REDUCE_CONV THEN
1306     REWRITE_TAC[REAL_MUL_AC; REAL_LE_REFL]; ALL_TAC] THEN
1307   SUBGOAL_THEN
1308    `!e. &0 < e
1309         ==> ?N. !n k:num. N <= k /\ pi * abs(x) <= &2 pow (n + 1)
1310                           ==> abs(B n k) < e`
1311   ASSUME_TAC THENL
1312    [X_CHOOSE_TAC `Bd:real` COT_X_BOUND_LEMMA THEN
1313     SUBGOAL_THEN
1314      `!k n. &9 * abs x < &k
1315             ==> abs(sum(k + 1,2 EXP n - 1 - k)
1316                        (\m. (&72 * x pow 2) / (&m pow 2 - &36 * x pow 2)))
1317                 <= &144 * x pow 2 / &k`
1318     ASSUME_TAC THENL
1319      [REPEAT STRIP_TAC THEN REWRITE_TAC[real_div; SUM_CMUL] THEN
1320       REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM; REAL_ABS_POW; REAL_POW2_ABS] THEN
1321       REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1322       ONCE_REWRITE_TAC[REAL_ARITH `&144 * x * y = &72 * x * &2 * y`] THEN
1323       MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
1324       MATCH_MP_TAC REAL_LE_LMUL THEN
1325       REWRITE_TAC[REAL_LE_SQUARE; REAL_POW_2] THEN
1326       MATCH_MP_TAC REAL_LE_TRANS THEN
1327       EXISTS_TAC `&2 * sum(k + 1,2 EXP n - 1 - k) (\m. inv(&m * &m))` THEN
1328       CONJ_TAC THENL
1329        [REWRITE_TAC[GSYM SUM_CMUL] THEN
1330         W(fun (asl,w) -> MP_TAC(PART_MATCH lhand SUM_ABS_LE (lhand w))) THEN
1331         MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1332         MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
1333         REWRITE_TAC[] THEN
1334         SUBGOAL_THEN `&0 < &r * &r - &36 * x * x` ASSUME_TAC THENL
1335          [REWRITE_TAC[GSYM REAL_POW_2] THEN
1336           ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
1337           REWRITE_TAC[REAL_POW_2] THEN
1338           REWRITE_TAC[REAL_ARITH
1339            `&0 < r * r - &36 * x * x <=> (&6 * x) * (&6 * x) < r * r`] THEN
1340           MATCH_MP_TAC REAL_LT_MUL2 THEN
1341           SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ABS_POS] THEN
1342           MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&k` THEN
1343           ASM_REWRITE_TAC[REAL_ABS_NUM] THEN
1344           REWRITE_TAC[REAL_OF_NUM_LE] THEN
1345           ASM_SIMP_TAC[REAL_ARITH `&9 * abs(x) < a ==> &6 * abs(x) < a`] THEN
1346           UNDISCH_TAC `k + 1 <= r` THEN ARITH_TAC; ALL_TAC] THEN
1347         ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_LE_INV_EQ] THEN
1348         GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
1349         ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ] THEN
1350         REWRITE_TAC[real_div] THEN
1351         ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c = (a * c) * b`] THEN
1352         REWRITE_TAC[GSYM real_div] THEN
1353         SUBGOAL_THEN `&0 < &r` ASSUME_TAC THENL
1354          [UNDISCH_TAC `k + 1 <= r` THEN REWRITE_TAC[REAL_OF_NUM_LT] THEN
1355           ARITH_TAC; ALL_TAC] THEN
1356         ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_MUL] THEN
1357         REWRITE_TAC[REAL_ARITH `&1 * x <= &2 * (x - y) <=> &2 * y <= x`] THEN
1358         MATCH_MP_TAC(REAL_ARITH
1359          `&0 <= x /\ &81 * x <= y ==> &2 * &36 * x <= y`) THEN
1360         REWRITE_TAC[REAL_LE_SQUARE] THEN
1361         REWRITE_TAC[REAL_ARITH `&81 * x * x = (&9 * x) * (&9 * x)`] THEN
1362         REWRITE_TAC[GSYM REAL_POW_2] THEN
1363         ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
1364         MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
1365         REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
1366         MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&k` THEN
1367         ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
1368         UNDISCH_TAC `k + 1 <= r` THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
1369         ARITH_TAC;
1370         ALL_TAC] THEN
1371       MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
1372       REWRITE_TAC[SUM_REINDEX] THEN
1373       SUBGOAL_THEN `?d. k = 1 + d` (CHOOSE_THEN SUBST1_TAC) THENL
1374        [REWRITE_TAC[GSYM LE_EXISTS] THEN
1375         MATCH_MP_TAC(ARITH_RULE `0 < k ==> 1 <= k`) THEN
1376         REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN
1377         UNDISCH_TAC `&9 * abs(x) < &k` THEN REAL_ARITH_TAC; ALL_TAC] THEN
1378       SPEC_TAC(`2 EXP n - 1 - (1 + d)`,`n:num`) THEN
1379       POP_ASSUM_LIST(K ALL_TAC) THEN GEN_TAC THEN
1380       GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o LAND_CONV) [ADD_SYM] THEN
1381       REWRITE_TAC[SUM_REINDEX] THEN
1382       REWRITE_TAC[ARITH_RULE `(r + 1) + 1 = r + 2`] THEN
1383       MATCH_MP_TAC REAL_LE_TRANS THEN
1384       EXISTS_TAC `sum(d,n) (\r. inv(&(r + 1) * &(r + 2)))` THEN
1385       CONJ_TAC THENL
1386        [MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC THEN
1387         SIMP_TAC[REAL_LE_RMUL_EQ; REAL_LT_INV_EQ; REAL_OF_NUM_LT;
1388                  REAL_INV_MUL; ARITH_RULE `0 < n + 2`] THEN
1389         MATCH_MP_TAC REAL_LE_INV2 THEN
1390         REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC;
1391         ALL_TAC] THEN
1392       SUBGOAL_THEN
1393        `!n. sum(d,n) (\r. inv (&(r + 1) * &(r + 2))) =
1394             inv(&(d + 1)) - inv(&(d + n + 1))`
1395        (fun th -> REWRITE_TAC[th])
1396       THENL
1397        [INDUCT_TAC THEN REWRITE_TAC[sum; ADD_CLAUSES; REAL_SUB_REFL] THEN
1398         ASM_REWRITE_TAC[REAL_ARITH
1399          `((a - x) + y = a - z) <=> (y + z = x)`] THEN
1400         REWRITE_TAC[GSYM ADD_ASSOC; REAL_INV_MUL;
1401           ARITH_RULE `SUC(d + n + 1) = d + n + 2`] THEN
1402         MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
1403         EXISTS_TAC `&(d + n + 1) * &(d + n + 2)` THEN
1404         REWRITE_TAC[REAL_ARITH
1405          `(dn1' * dn2' + dn2') * (dn1 * dn2) =
1406           (dn1 * dn1' + dn1) * (dn2 * dn2')`] THEN
1407         SIMP_TAC[REAL_ENTIRE; REAL_MUL_RINV; REAL_OF_NUM_EQ;
1408                  ARITH_RULE `~(d + n + 1 = 0) /\ ~(d + n + 2 = 0)`] THEN
1409         SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV;
1410                  REAL_OF_NUM_EQ; ARITH_RULE `~(d + n + 1 = 0)`] THEN
1411         REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
1412         ARITH_TAC; ALL_TAC] THEN
1413       REWRITE_TAC[ADD_AC] THEN
1414       MATCH_MP_TAC(REAL_ARITH `&0 <= y ==> x - y <= x`) THEN
1415       REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS]; ALL_TAC] THEN
1416     X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1417     SUBGOAL_THEN
1418      `?N. &9 * abs(x) + &1 <= &N /\
1419           (Bd * &144 * x pow 2) / e + &1 <= &N`
1420      (X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC)
1421     THENL
1422      [X_CHOOSE_TAC `N1:num` (SPEC `&9 * abs(x) + &1` REAL_ARCH_SIMPLE) THEN
1423       X_CHOOSE_TAC `N2:num`
1424        (SPEC `(Bd * &144 * x pow 2) / e + &1` REAL_ARCH_SIMPLE) THEN
1425       EXISTS_TAC `N1 + N2:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
1426       ASM_MESON_TAC[REAL_POS;
1427                     REAL_ARITH `a <= m /\ b <= n /\ &0 <= m /\ &0 <= n
1428                                 ==> a <= m + n /\ b <= m + n`];
1429       ALL_TAC] THEN
1430     EXISTS_TAC `N:num` THEN
1431     MAP_EVERY X_GEN_TAC [`n:num`; `k:num`] THEN
1432     STRIP_TAC THEN
1433     MATCH_MP_TAC REAL_LET_TRANS THEN
1434     EXISTS_TAC
1435      `abs((pi * x / &2 pow (n + 1)) * cot (pi * x / &2 pow (n + 1))) *
1436           sum(k + 1,2 EXP n - 1 - k)
1437               (\m. (&72 * x pow 2) / (&m pow 2 - &36 * x pow 2))` THEN
1438     CONJ_TAC THENL
1439      [FIRST_ASSUM MATCH_MP_TAC THEN
1440       MATCH_MP_TAC REAL_LTE_TRANS THEN
1441       EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
1442       UNDISCH_TAC `&9 * abs x + &1 <= &N` THEN REAL_ARITH_TAC;
1443       ALL_TAC] THEN
1444     MATCH_MP_TAC REAL_LET_TRANS THEN
1445     EXISTS_TAC `Bd * &144 * x pow 2 / &k` THEN CONJ_TAC THENL
1446      [ALL_TAC;
1447       REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
1448       REWRITE_TAC[GSYM real_div] THEN
1449       SUBGOAL_THEN `&0 < &k` (fun th -> SIMP_TAC[REAL_LT_LDIV_EQ; th]) THENL
1450        [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN
1451         ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
1452         UNDISCH_TAC `&9 * abs x + &1 <= &N` THEN REAL_ARITH_TAC; ALL_TAC] THEN
1453       GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
1454       ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ] THEN
1455       REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
1456       REWRITE_TAC[GSYM real_div] THEN
1457       MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN
1458       ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_OF_NUM_LE] THEN
1459       ASM_SIMP_TAC[REAL_ARITH `x + &1 <= y ==> x < y`]] THEN
1460     MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> x <= a`) THEN
1461     ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
1462     MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
1463     CONJ_TAC THENL
1464      [REWRITE_TAC[REAL_ABS_ABS] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1465       ASM_SIMP_TAC[real_div; REAL_ENTIRE; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES;
1466                    REAL_MUL_ASSOC; REAL_LT_INV_EQ; PI_POS] THEN
1467       SIMP_TAC[GSYM real_div; REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM] THEN
1468       SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW2_CLAUSES; REAL_MUL_LID] THEN
1469       REWRITE_TAC[REAL_ABS_MUL] THEN
1470       SIMP_TAC[real_abs; REAL_LT_IMP_LE; PI_POS] THEN
1471       ASM_REWRITE_TAC[GSYM real_abs]; ALL_TAC] THEN
1472     FIRST_ASSUM MATCH_MP_TAC THEN
1473     MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N:real` THEN
1474     ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
1475     UNDISCH_TAC `&9 * abs x + &1 <= &N` THEN
1476     REAL_ARITH_TAC; ALL_TAC] THEN
1477   SUBGOAL_THEN
1478    `!n k. k < 2 EXP n
1479           ==> ((pi * x) *
1480                (cot (pi * x / &2 pow n) / &2 pow n +
1481                 sum (1,2 EXP n - 1)
1482                     (\k. cot(pi * (x + &k) / &2 pow (n + 1)) +
1483                          cot(pi * (x - &k) / &2 pow (n + 1))) /
1484                 &2 pow (n + 1)) = A n k + B n k)`
1485   MP_TAC THENL
1486    [REPEAT GEN_TAC THEN DISCH_TAC THEN
1487     MAP_EVERY EXPAND_TAC ["A"; "B"] THEN
1488     REWRITE_TAC[GSYM REAL_ADD_ASSOC; GSYM REAL_ADD_LDISTRIB] THEN
1489     GEN_REWRITE_TAC (funpow 3 RAND_CONV o funpow 3 LAND_CONV)
1490       [ARITH_RULE `x = 0 + x`] THEN
1491     REWRITE_TAC[SUM_REINDEX] THEN
1492     ONCE_REWRITE_TAC
1493      [REWRITE_RULE[REAL_ARITH `(a = b - c) <=> (c + a = b)`] SUM_DIFF] THEN
1494     ASM_SIMP_TAC[ARITH_RULE `n < p ==> (n + p - 1 - n = p - 1)`] THEN
1495     GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV o funpow 3 LAND_CONV)
1496      [ARITH_RULE `x = 0 + x`] THEN
1497     REWRITE_TAC[SUM_REINDEX] THEN
1498     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; GSYM REAL_ADD_LDISTRIB] THEN
1499     REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN
1500   FIRST_ASSUM(MP_TAC o MATCH_MP COT_HALF_KNOPP) THEN
1501   DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN DISCH_TAC THEN
1502   REWRITE_TAC[sums; SEQ] THEN
1503   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1504   UNDISCH_TAC
1505    `!e. &0 < e
1506         ==> ?N. !n k:num. N <= k /\ pi * abs(x) <= &2 pow (n + 1)
1507                           ==> abs (B n k) < e` THEN
1508   DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
1509   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1510   DISCH_THEN(X_CHOOSE_THEN `N1:num` STRIP_ASSUME_TAC) THEN
1511   EXISTS_TAC `N1 + 1` THEN X_GEN_TAC `n:num` THEN
1512   REWRITE_TAC[GE] THEN DISCH_TAC THEN
1513   UNDISCH_TAC
1514    `!k. (\n. A n k) tends_num_real
1515            &1 + sum (1,k) (\n. (&2 * x pow 2) / (x pow 2 - &n pow 2))` THEN
1516   DISCH_THEN(MP_TAC o SPEC `n - 1`) THEN REWRITE_TAC[SEQ] THEN
1517   DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
1518   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN REWRITE_TAC[GE] THEN
1519   DISCH_THEN(X_CHOOSE_THEN `N2:num` ASSUME_TAC) THEN
1520   SUBGOAL_THEN
1521    `?m. n - 1 < 2 EXP m /\ N2 <= m /\ pi * abs(x) <= &2 pow (m + 1)`
1522   MP_TAC THENL
1523    [SUBGOAL_THEN `?m. &(n - 1) + &1 <= &m /\ &N2 <= &m /\ pi * abs(x) <= &m`
1524     MP_TAC THENL
1525      [X_CHOOSE_TAC `m1:num` (SPEC `&(n - 1) + &1` REAL_ARCH_SIMPLE) THEN
1526       X_CHOOSE_TAC `m2:num` (SPEC `&N2` REAL_ARCH_SIMPLE) THEN
1527       X_CHOOSE_TAC `m3:num` (SPEC `pi * abs(x)` REAL_ARCH_SIMPLE) THEN
1528       EXISTS_TAC `m1 + m2 + m3:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
1529       MATCH_MP_TAC(REAL_ARITH
1530        `x <= a /\ y <= b /\ z <= c /\ &0 <= a /\ &0 <= b /\ &0 <= c
1531         ==> x <= a + b + c /\ y <= a + b + c /\ z <= a + b + c`) THEN
1532       ASM_REWRITE_TAC[REAL_POS]; ALL_TAC] THEN
1533     REWRITE_TAC[GSYM REAL_OF_NUM_LT; GSYM REAL_OF_NUM_LE] THEN
1534     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN
1535     REWRITE_TAC[GSYM REAL_OF_NUM_POW] THEN
1536     MATCH_MP_TAC(REAL_ARITH
1537      `m <= m2 /\ m2 <= m22
1538       ==> x1 + &1 <= m /\ x2 <= m /\ x3 <= m
1539           ==> x1 < m2 /\ x2 <= m /\ x3 <= m22`) THEN
1540     REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN
1541     REWRITE_TAC[REAL_ARITH `x <= x * &2 <=> &0 <= x`] THEN
1542     REWRITE_TAC[REAL_POW2_CLAUSES] THEN
1543     MATCH_MP_TAC REAL_LT_IMP_LE THEN
1544     REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_POW] THEN
1545     POP_ASSUM_LIST(K ALL_TAC) THEN
1546     SPEC_TAC(`m:num`,`n:num`) THEN
1547     INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH] THEN
1548     MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `SUC(2 EXP n)` THEN
1549     ASM_REWRITE_TAC[LT_SUC] THEN REWRITE_TAC[MULT_2; ADD1; LE_ADD_LCANCEL] THEN
1550     REWRITE_TAC[num_CONV `1`; LE_SUC_LT; EXP_LT_0; ARITH_EQ]; ALL_TAC] THEN
1551   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
1552   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `e / &2 + e / &2` THEN
1553   CONJ_TAC THENL
1554    [ALL_TAC;
1555     SIMP_TAC[REAL_LE_REFL; GSYM REAL_MUL_2; REAL_DIV_LMUL;
1556              REAL_OF_NUM_EQ; ARITH_EQ]] THEN
1557   UNDISCH_TAC
1558    `!n k. k < 2 EXP n ==> ((pi * x) * cot (pi * x) = A n k + B n k)` THEN
1559   DISCH_THEN(MP_TAC o SPECL [`m:num`; `n - 1`]) THEN
1560   ASM_SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN
1561   MATCH_MP_TAC(REAL_ARITH
1562    `abs(b) < e /\ abs((s - &1) - a) < e
1563     ==> abs(s - ((a + b) + &1)) < e + e`) THEN
1564   CONJ_TAC THENL
1565    [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1566     UNDISCH_TAC `N1 + 1 <= n` THEN ARITH_TAC; ALL_TAC] THEN
1567   SUBGOAL_THEN
1568    `sum (0,n) (\r. (&2 * x pow 2) / (x pow 2 - &r pow 2)) - &1 =
1569     &1 + sum(1,n-1) (\r. (&2 * x pow 2) / (x pow 2 - &r pow 2))`
1570   SUBST1_TAC THENL
1571    [SUBGOAL_THEN `n = 1 + (n - 1)`
1572      (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
1573     THENL
1574      [UNDISCH_TAC `N1 + 1 <= n` THEN ARITH_TAC; ALL_TAC] THEN
1575     REWRITE_TAC[GSYM(REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
1576     MATCH_MP_TAC(REAL_ARITH `(a = &2) ==> ((x + a) - &1 = &1 + x)`) THEN
1577     CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1578     REWRITE_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_SUB_RZERO] THEN
1579     REWRITE_TAC[GSYM REAL_POW_2] THEN REWRITE_TAC[real_div] THEN
1580     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1581     ASM_SIMP_TAC[GSYM real_div; REAL_DIV_REFL; REAL_POW_EQ_0] THEN
1582     REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN
1583   ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN
1584   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
1585
1586 (* ------------------------------------------------------------------------- *)
1587 (* Expansion of each term as a power series.                                 *)
1588 (* ------------------------------------------------------------------------- *)
1589
1590 let COT_PARTIAL_FRACTIONS_SUBTERM = prove
1591  (`abs(x) < &n
1592    ==> (\k. --(&2) * (x pow 2 / &n pow 2) pow (k + 1))
1593        sums ((&2 * x pow 2) / (x pow 2 - &n pow 2))`,
1594   REPEAT STRIP_TAC THEN
1595   SUBGOAL_THEN `&0 < &n` ASSUME_TAC THENL
1596    [UNDISCH_TAC `abs(x) < &n` THEN REAL_ARITH_TAC; ALL_TAC] THEN
1597   SUBGOAL_THEN
1598    `(\k. (x pow 2 / &n pow 2) pow k) sums
1599     inv(&1 - (x pow 2 / &n pow 2))`
1600   MP_TAC THENL
1601    [MATCH_MP_TAC GP THEN
1602     REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM] THEN
1603     ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_POW_LT; REAL_MUL_LID] THEN
1604     ASM_SIMP_TAC[REAL_POW_LT2; REAL_ABS_POS; ARITH_EQ]; ALL_TAC] THEN
1605   DISCH_THEN(MP_TAC o
1606     SPEC `--(&2) * (x pow 2 / &n pow 2)` o MATCH_MP SER_CMUL) THEN
1607   REWRITE_TAC[] THEN
1608   MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
1609    [REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM(CONJUNCT2 real_pow)] THEN
1610     REWRITE_TAC[ADD1]; ALL_TAC] THEN
1611   REWRITE_TAC[real_div; GSYM REAL_INV_MUL;
1612               GSYM REAL_MUL_ASSOC; REAL_MUL_LNEG] THEN
1613   REWRITE_TAC[GSYM REAL_MUL_RNEG; GSYM REAL_INV_NEG] THEN
1614   AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
1615   REWRITE_TAC[REAL_NEG_SUB; REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN
1616   ASM_SIMP_TAC[GSYM real_div; REAL_DIV_LMUL; REAL_POW_LT; REAL_LT_IMP_NZ]);;
1617
1618 (* ------------------------------------------------------------------------- *)
1619 (* General theorem about swapping a double series of positive terms.         *)
1620 (* ------------------------------------------------------------------------- *)
1621
1622 let SEQ_LE_CONST = prove
1623  (`!a x l N. (!n. n >= N ==> x(n) <= a) /\ x tends_num_real l ==> l <= a`,
1624   REPEAT STRIP_TAC THEN MATCH_MP_TAC SEQ_LE THEN
1625   MAP_EVERY EXISTS_TAC [`x:num->real`; `\n:num. a:real`] THEN
1626   ASM_REWRITE_TAC[SEQ_CONST] THEN ASM_MESON_TAC[]);;
1627
1628 let SEQ_GE_CONST = prove
1629  (`!a x l N. (!n. n >= N ==> a <= x(n)) /\ x tends_num_real l ==> a <= l`,
1630   REPEAT STRIP_TAC THEN MATCH_MP_TAC SEQ_LE THEN
1631   MAP_EVERY EXISTS_TAC [`\n:num. a:real`; `x:num->real`] THEN
1632   ASM_REWRITE_TAC[SEQ_CONST] THEN ASM_MESON_TAC[]);;
1633
1634 let SUM_SWAP_0 = prove
1635  (`!m n. sum(0,m) (\i. sum(0,n) (\j. a i j)) =
1636          sum(0,n) (\j. sum(0,m) (\i. a i j))`,
1637   INDUCT_TAC THEN
1638   ASM_SIMP_TAC[sum; SUM_CONST; REAL_MUL_RZERO; SUM_ADD]);;
1639
1640 let SUM_SWAP = prove
1641  (`!m1 m2 n1 n2.
1642         sum(m1,m2) (\i. sum(n1,n2) (\j. a i j)) =
1643         sum(n1,n2) (\j. sum(m1,m2) (\i. a i j))`,
1644   REPEAT GEN_TAC THEN
1645   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o LAND_CONV)
1646     [ARITH_RULE `m = 0 + m`] THEN
1647   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o LAND_CONV)
1648     [ARITH_RULE `m = 0 + m`] THEN
1649   REPEAT GEN_TAC THEN
1650   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o BINDER_CONV o LAND_CONV o LAND_CONV)
1651     [ARITH_RULE `m = 0 + m`] THEN
1652   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o BINDER_CONV o LAND_CONV o LAND_CONV)
1653     [ARITH_RULE `m = 0 + m`] THEN
1654   REWRITE_TAC[SUM_REINDEX; SUM_SWAP_0]);;
1655
1656 let SER_SWAPDOUBLE_POS = prove
1657  (`!z a l. (!m n. &0 <= a m n) /\ (!m. (a m) sums (z m)) /\ z sums l
1658            ==> ?s. (!n. (\m. a m n) sums (s n)) /\ s sums l`,
1659   REPEAT STRIP_TAC THEN
1660   SUBGOAL_THEN `!m:num n. sum(0,n) (a m) <= z m` ASSUME_TAC THENL
1661    [REPEAT GEN_TAC THEN MATCH_MP_TAC SEQ_GE_CONST THEN
1662     EXISTS_TAC `\n. sum(0,n) (a(m:num))` THEN
1663     ASM_REWRITE_TAC[GSYM sums] THEN
1664     EXISTS_TAC `n:num` THEN X_GEN_TAC `p:num` THEN
1665     SIMP_TAC[GE; LEFT_IMP_EXISTS_THM; LE_EXISTS] THEN
1666     ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN
1667     ASM_SIMP_TAC[GSYM SUM_DIFF; SUM_POS]; ALL_TAC] THEN
1668   SUBGOAL_THEN `!m:num. &0 <= z m` ASSUME_TAC THENL
1669    [GEN_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1670     EXISTS_TAC `sum(0,n) (a(m:num))` THEN
1671     ASM_SIMP_TAC[SUM_POS]; ALL_TAC] THEN
1672   SUBGOAL_THEN `!n. sum(0,n) z <= l` ASSUME_TAC THENL
1673    [GEN_TAC THEN MATCH_MP_TAC SEQ_GE_CONST THEN
1674     EXISTS_TAC `\n. sum(0,n) z` THEN
1675     ASM_REWRITE_TAC[GSYM sums] THEN
1676     EXISTS_TAC `n:num` THEN X_GEN_TAC `p:num` THEN
1677     SIMP_TAC[GE; LEFT_IMP_EXISTS_THM; LE_EXISTS] THEN
1678     ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN
1679     ASM_SIMP_TAC[GSYM SUM_DIFF; SUM_POS]; ALL_TAC] THEN
1680   SUBGOAL_THEN `&0 <= l` ASSUME_TAC THENL
1681    [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum(0,n) z` THEN
1682     ASM_SIMP_TAC[SUM_POS]; ALL_TAC] THEN
1683   SUBGOAL_THEN
1684    `!e. &0 < e
1685         ==> ?M N. !m n. M <= m /\ N <= n ==>
1686                         l - e <= sum(0,m) (\i. sum(0,n) (\j. a i j)) /\
1687                         sum(0,m) (\i. sum(0,n) (\j. a i j)) <= l`
1688   ASSUME_TAC THENL
1689    [X_GEN_TAC `e:real` THEN DISCH_TAC THEN UNDISCH_TAC `z sums l` THEN
1690     REWRITE_TAC[sums; SEQ] THEN
1691     DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
1692     ASM_SIMP_TAC[REAL_LT_DIV; GE; REAL_OF_NUM_LT; ARITH] THEN
1693     DISCH_THEN(X_CHOOSE_TAC `M:num`) THEN
1694     SUBGOAL_THEN
1695      `?N. !m n. m < M /\ n >= N
1696                 ==> abs(sum (0,n) (a m) - z m) < e / (&2 * &(M + 1))`
1697     MP_TAC THENL
1698      [SUBGOAL_THEN `&0 < e / (&2 * &(M + 1))` MP_TAC THENL
1699        [ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; REAL_LT_MUL; ARITH;
1700                      ARITH_RULE `0 < n + 1`]; ALL_TAC] THEN
1701       SPEC_TAC(`e / (&2 * &(M + 1))`,`d:real`) THEN
1702       SPEC_TAC(`M:num`,`n:num`) THEN
1703       GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN
1704       REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1705       GEN_TAC THEN DISCH_TAC THEN
1706       INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN
1707       UNDISCH_TAC `!m:num. (a m) sums (z m)` THEN
1708       DISCH_THEN(MP_TAC o SPEC `n:num`) THEN
1709       REWRITE_TAC[sums; SEQ] THEN
1710       DISCH_THEN(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[] THEN
1711       DISCH_THEN(X_CHOOSE_TAC `N0:num`) THEN
1712       FIRST_X_ASSUM(X_CHOOSE_TAC `N1:num`) THEN
1713       EXISTS_TAC `N0 + N1:num` THEN
1714       X_GEN_TAC `m:num` THEN X_GEN_TAC `p:num` THEN
1715       REWRITE_TAC[LT] THEN
1716       ASM_MESON_TAC[ARITH_RULE `a >= m + n ==> a >= m /\ a >= n:num`];
1717       ALL_TAC] THEN
1718     REWRITE_TAC[GE] THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
1719     MAP_EVERY EXISTS_TAC [`M:num`; `N:num`] THEN
1720     MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
1721     MATCH_MP_TAC(REAL_ARITH
1722      `!s0. s0 <= s /\ s <= l /\ abs(s0 - l) < e
1723            ==> l - e <= s /\ s <= l`) THEN
1724     EXISTS_TAC `sum(0,M) (\i. sum (0,n) (\j. a i j))` THEN
1725     CONJ_TAC THENL
1726      [UNDISCH_TAC `M <= m:num` THEN
1727       SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1728       ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN
1729       REWRITE_TAC[GSYM SUM_DIFF] THEN ASM_SIMP_TAC[SUM_POS]; ALL_TAC] THEN
1730     CONJ_TAC THENL
1731      [MATCH_MP_TAC REAL_LE_TRANS THEN
1732       EXISTS_TAC `sum (0,m) z` THEN ASM_REWRITE_TAC[] THEN
1733       MATCH_MP_TAC SUM_LE THEN
1734       CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
1735     MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `e / &2 + e / &2` THEN
1736     CONJ_TAC THENL
1737      [ALL_TAC;
1738       SIMP_TAC[REAL_LE_REFL; GSYM REAL_MUL_2; REAL_DIV_LMUL;
1739                REAL_OF_NUM_EQ; ARITH_EQ]] THEN
1740     MATCH_MP_TAC(REAL_ARITH
1741      `!z. abs(x - z) <= e /\ abs(z - y) < e ==> abs(x - y) < e + e`) THEN
1742     EXISTS_TAC `sum(0,M) z` THEN ASM_SIMP_TAC[LE_REFL] THEN
1743     REWRITE_TAC[GSYM SUM_SUB] THEN
1744     MATCH_MP_TAC REAL_LE_TRANS THEN
1745     EXISTS_TAC `&M * e / (&2 * &(M + 1))` THEN CONJ_TAC THENL
1746      [ALL_TAC;
1747       REWRITE_TAC[real_div; REAL_INV_MUL] THEN
1748       ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d = (b * c) * a * d`] THEN
1749       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1750       MATCH_MP_TAC REAL_LE_LMUL THEN
1751       ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_LE_INV_EQ; REAL_POS] THEN
1752       SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT;
1753                ARITH_RULE `0 < n + 1`] THEN
1754       REWRITE_TAC[REAL_MUL_LID; REAL_OF_NUM_LE; LE_ADD]] THEN
1755     W(fun (asl,w) -> MP_TAC(PART_MATCH lhand SUM_ABS_LE (lhand w))) THEN
1756     MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
1757     MATCH_MP_TAC REAL_LE_TRANS THEN
1758     EXISTS_TAC `sum(0,M) (\n. e / (&2 * &(M + 1)))` THEN CONJ_TAC THENL
1759      [MATCH_MP_TAC SUM_LE THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
1760       ASM_SIMP_TAC[ADD_CLAUSES; REAL_LT_IMP_LE];
1761       REWRITE_TAC[SUM_CONST; REAL_LE_REFL]]; ALL_TAC] THEN
1762   SUBGOAL_THEN `!m n. sum(0,m) (\i. (a:num->num->real) i n) <= l`
1763   ASSUME_TAC THENL
1764    [REPEAT GEN_TAC THEN
1765     FIRST_X_ASSUM(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN
1766     DISCH_THEN(X_CHOOSE_THEN `M:num` MP_TAC) THEN
1767     DISCH_THEN(X_CHOOSE_THEN `N:num` ASSUME_TAC) THEN
1768     MATCH_MP_TAC REAL_LE_TRANS THEN
1769     EXISTS_TAC `sum(0,M+m) (\i. sum(0,N+n+1) (\j. a i j))` THEN
1770     ASM_SIMP_TAC[LE_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
1771     ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
1772     MATCH_MP_TAC(REAL_ARITH `x <= y /\ &0 <= z ==> x <= z + y`) THEN
1773     ASM_SIMP_TAC[SUM_POS] THEN MATCH_MP_TAC SUM_LE THEN
1774     X_GEN_TAC `r:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[] THEN
1775     REWRITE_TAC[GSYM ADD_ASSOC] THEN
1776     ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
1777     MATCH_MP_TAC(REAL_ARITH `x <= y /\ &0 <= z ==> x <= y + z`) THEN
1778     ASM_SIMP_TAC[SUM_POS] THEN
1779     MATCH_MP_TAC REAL_LE_TRANS THEN
1780     EXISTS_TAC `sum(n,1) (\j. a (r:num) j)` THEN CONJ_TAC THENL
1781      [REWRITE_TAC[SUM_1; REAL_LE_REFL]; ALL_TAC] THEN
1782     SUBST1_TAC(ARITH_RULE `n = 0 + n`) THEN REWRITE_TAC[SUM_REINDEX] THEN
1783     ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
1784     ASM_SIMP_TAC[SUM_POS; REAL_LE_ADDL]; ALL_TAC] THEN
1785   SUBGOAL_THEN `!n:num. ?s. (\m. a m n) sums s` MP_TAC THENL
1786    [GEN_TAC THEN REWRITE_TAC[sums; GSYM convergent] THEN
1787     MATCH_MP_TAC SEQ_BCONV THEN CONJ_TAC THENL
1788      [MATCH_MP_TAC SEQ_BOUNDED_2 THEN
1789       MAP_EVERY EXISTS_TAC [`&0`; `l:real`] THEN ASM_SIMP_TAC[SUM_POS];
1790       REWRITE_TAC[mono] THEN DISJ1_TAC THEN
1791       SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1792       REPEAT STRIP_TAC THEN
1793       ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
1794       ASM_SIMP_TAC[SUM_POS; REAL_LE_ADDL]];
1795     ALL_TAC] THEN
1796   REWRITE_TAC[SKOLEM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
1797   X_GEN_TAC `s:num->real` THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1798   SUBGOAL_THEN
1799    `!e. &0 < e
1800         ==> ?N. !n. N <= n
1801                     ==> l - e <= sum (0,n) s /\ sum(0,n) s <= l`
1802   ASSUME_TAC THENL
1803    [X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1804     FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1805     DISCH_THEN(X_CHOOSE_THEN `M:num` MP_TAC) THEN
1806     DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC) THEN
1807     ONCE_REWRITE_TAC[SUM_SWAP_0] THEN DISCH_TAC THEN
1808     EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN
1809     DISCH_TAC THEN CONJ_TAC THENL
1810      [MATCH_MP_TAC(REAL_ARITH
1811        `!s0. l - e <= s0 /\ s0 <= s ==> l - e <= s`) THEN
1812       EXISTS_TAC `sum (0,n) (\j. sum (0,M) (\i. a i j))` THEN
1813       ASM_SIMP_TAC[LE_REFL] THEN MATCH_MP_TAC SUM_LE THEN
1814       X_GEN_TAC `r:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[] THEN
1815       MATCH_MP_TAC SEQ_GE_CONST THEN
1816       EXISTS_TAC `\m. sum(0,m) (\m. a m (r:num))` THEN
1817       EXISTS_TAC `M:num` THEN ASM_REWRITE_TAC[GSYM sums] THEN
1818       SIMP_TAC[GE; LEFT_IMP_EXISTS_THM; LE_EXISTS] THEN
1819       ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN
1820       ASM_SIMP_TAC[SUM_POS; REAL_LE_ADDL]; ALL_TAC] THEN
1821     MATCH_MP_TAC SEQ_LE_CONST THEN
1822     EXISTS_TAC `\m. sum (0,n) (\j. sum (0,m) (\i. a i j))` THEN
1823     REWRITE_TAC[] THEN EXISTS_TAC `0` THEN CONJ_TAC THENL
1824      [X_GEN_TAC `m:num` THEN DISCH_THEN(K ALL_TAC) THEN
1825       ONCE_REWRITE_TAC[SUM_SWAP_0] THEN
1826       MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum(0,m) z` THEN
1827       ASM_REWRITE_TAC[] THEN
1828       MATCH_MP_TAC SUM_LE THEN ASM_REWRITE_TAC[] THEN
1829       CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
1830     MATCH_MP_TAC SEQ_SUM THEN X_GEN_TAC `m:num` THEN
1831     ASM_REWRITE_TAC[GSYM sums]; ALL_TAC] THEN
1832   REWRITE_TAC[sums; SEQ] THEN
1833   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1834   UNDISCH_TAC
1835    `!e. &0 < e
1836         ==> (?N. !n. N <= n ==> l - e <= sum (0,n) s /\ sum (0,n) s <= l)` THEN
1837   DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
1838   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1839   REWRITE_TAC[GE] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
1840   MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
1841   MATCH_MP_TAC(TAUT `(a ==> b ==> c) ==> (a ==> b) ==> (a ==> c)`) THEN
1842   DISCH_TAC THEN
1843   MATCH_MP_TAC(REAL_ARITH
1844    `d < e ==> l - d <= x /\ x <= l ==> abs(x - l) < e`) THEN
1845   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
1846   UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC);;
1847
1848 (* ------------------------------------------------------------------------- *)
1849 (* Hence we get a power series for cot with nice convergence property.       *)
1850 (* ------------------------------------------------------------------------- *)
1851
1852 let COT_PARTIAL_FRACTIONS_FROM1 = prove
1853  (`~integer x
1854     ==> (\n. (&2 * x pow 2) / (x pow 2 - &(n + 1) pow 2)) sums
1855         (pi * x) * cot (pi * x) - &1`,
1856   DISCH_TAC THEN
1857   SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
1858    [UNDISCH_TAC `~(integer x)` THEN
1859     REWRITE_TAC[TAUT `(~b ==> ~a) <=> (a ==> b)`] THEN
1860     SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL];
1861     ALL_TAC] THEN
1862   FIRST_ASSUM(MP_TAC o MATCH_MP COT_PARTIAL_FRACTIONS) THEN
1863   DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
1864   DISCH_THEN(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN
1865   DISCH_THEN(MP_TAC o SPEC `1` o MATCH_MP SER_OFFSET) THEN
1866   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
1867   MATCH_MP_TAC EQ_IMP THEN
1868   REWRITE_TAC[] THEN AP_TERM_TAC THEN REWRITE_TAC[SUM_1] THEN
1869   REWRITE_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_SUB_RZERO] THEN
1870   REWRITE_TAC[real_div] THEN
1871   ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b * b) * c = a * (b * b) * c`] THEN
1872   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_ENTIRE; REAL_MUL_RID] THEN
1873   REAL_ARITH_TAC);;
1874
1875 let COT_ALT_POWSER = prove
1876  (`!x. &0 < abs(x) /\ abs(x) < &1
1877        ==> ?s. (!n. (\m. &2 * (x pow 2 / &(m + 1) pow 2) pow (n + 1))
1878                     sums s n) /\
1879                s sums --((pi * x) * cot(pi * x) - &1)`,
1880   REPEAT STRIP_TAC THEN MATCH_MP_TAC SER_SWAPDOUBLE_POS THEN
1881   EXISTS_TAC `\n. (--(&2) * x pow 2) / (x pow 2 - &(n + 1) pow 2)` THEN
1882   REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
1883    [SIMP_TAC[REAL_POS; REAL_POW_LE; REAL_LE_MUL;
1884              REAL_POW_2; REAL_LE_DIV; REAL_LE_SQUARE];
1885     X_GEN_TAC `m:num` THEN
1886     GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o LAND_CONV)
1887      [GSYM REAL_NEG_NEG] THEN
1888     REWRITE_TAC[real_div; REAL_MUL_LNEG] THEN
1889     MATCH_MP_TAC SER_NEG THEN
1890     REWRITE_TAC[GSYM REAL_MUL_LNEG] THEN
1891     REWRITE_TAC[GSYM real_div] THEN
1892     MATCH_MP_TAC COT_PARTIAL_FRACTIONS_SUBTERM THEN
1893     MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1` THEN
1894     ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC;
1895     REWRITE_TAC[real_div; REAL_MUL_LNEG] THEN
1896     MATCH_MP_TAC SER_NEG THEN
1897     REWRITE_TAC[GSYM REAL_MUL_LNEG] THEN
1898     REWRITE_TAC[GSYM real_div] THEN
1899     MATCH_MP_TAC COT_PARTIAL_FRACTIONS_FROM1 THEN
1900     UNDISCH_TAC `&0 < abs x` THEN UNDISCH_TAC `abs x < &1` THEN
1901     ONCE_REWRITE_TAC[TAUT `a ==> b ==> ~c <=> c ==> ~(a /\ b)`] THEN
1902     SIMP_TAC[integer; LEFT_IMP_EXISTS_THM] THEN
1903     GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[REAL_OF_NUM_LT] THEN
1904     ARITH_TAC]);;
1905
1906 (* ------------------------------------------------------------------------- *)
1907 (* General unpairing result.                                                 *)
1908 (* ------------------------------------------------------------------------- *)
1909
1910 let SER_INSERTZEROS = prove
1911  (`(\n. c(2 * n)) sums l
1912    ==> (\n. if ODD n then &0 else c(n)) sums l`,
1913   REWRITE_TAC[sums; SEQ; GE] THEN
1914   DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1915   FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN
1916   ASM_REWRITE_TAC[] THEN
1917   DISCH_THEN(X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC) THEN
1918   EXISTS_TAC `2 * N` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
1919   DISJ_CASES_THEN MP_TAC (SPEC `n:num` EVEN_OR_ODD) THENL
1920    [REWRITE_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1921     X_GEN_TAC `m:num` THEN DISCH_THEN SUBST_ALL_TAC THEN
1922     REWRITE_TAC[ONCE_REWRITE_RULE[MULT_SYM] (GSYM SUM_GROUP)] THEN
1923     REWRITE_TAC[SUM_2; ODD_ADD; ODD_MULT; ARITH_ODD; REAL_ADD_RID] THEN
1924     FIRST_ASSUM MATCH_MP_TAC THEN
1925     UNDISCH_TAC `2 * N <= 2 * m` THEN ARITH_TAC;
1926     REWRITE_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
1927     X_GEN_TAC `m:num` THEN DISCH_THEN SUBST_ALL_TAC THEN
1928     REWRITE_TAC[GSYM ODD_EXISTS] THEN REWRITE_TAC[sum] THEN
1929     REWRITE_TAC[ONCE_REWRITE_RULE[MULT_SYM] (GSYM SUM_GROUP)] THEN
1930     REWRITE_TAC[SUM_2; ODD_ADD; ODD_MULT; ARITH_ODD; REAL_ADD_RID] THEN
1931     ONCE_REWRITE_TAC[ARITH_RULE `0 + 2 * m = 2 * (0 + m)`] THEN
1932     REWRITE_TAC[GSYM(CONJUNCT2 sum)] THEN
1933     FIRST_ASSUM MATCH_MP_TAC THEN
1934     UNDISCH_TAC `2 * N <= SUC(2 * m)` THEN ARITH_TAC]);;
1935
1936 (* ------------------------------------------------------------------------- *)
1937 (* Mangle this into a standard power series.                                 *)
1938 (* ------------------------------------------------------------------------- *)
1939
1940 let COT_POWSER_SQUARED_FORM = prove
1941  (`!x. &0 < abs(x) /\ abs(x) < pi
1942        ==> (\n. &2 * (x / pi) pow (2 * (n + 1)) *
1943                 suminf (\m. inv (&(m + 1) pow (2 * (n + 1)))))
1944            sums --(x * cot x - &1)`,
1945   REPEAT STRIP_TAC THEN
1946   MP_TAC(SPEC `x / pi` COT_ALT_POWSER) THEN
1947   REWRITE_TAC[REAL_ABS_DIV] THEN
1948   SIMP_TAC[real_abs; REAL_LT_IMP_LE; PI_POS] THEN
1949   REWRITE_TAC[GSYM real_abs] THEN
1950   SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_LDIV_EQ; PI_POS] THEN
1951   ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_LID] THEN
1952   SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; PI_POS] THEN
1953   DISCH_THEN(X_CHOOSE_THEN `s:num->real` STRIP_ASSUME_TAC) THEN
1954   UNDISCH_TAC `s sums --(x * cot(x) - &1)` THEN
1955   MATCH_MP_TAC EQ_IMP THEN
1956   AP_THM_TAC THEN AP_TERM_TAC THEN
1957   REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `n:num` THEN
1958   FIRST_ASSUM(MP_TAC o MATCH_MP SER_CMUL o SPEC `n:num`) THEN
1959   DISCH_THEN(MP_TAC o SPEC `inv(&2 * (x / pi) pow (2 * (n + 1)))`) THEN
1960   REWRITE_TAC[] THEN
1961   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ABS_CONV o
1962                    RAND_CONV o ONCE_DEPTH_CONV)
1963       [REAL_POW_DIV] THEN
1964   REWRITE_TAC[REAL_POW_POW] THEN
1965   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ABS_CONV o
1966                    RAND_CONV o ONCE_DEPTH_CONV)
1967       [real_div] THEN
1968   ONCE_REWRITE_TAC[REAL_ARITH
1969    `a * &2 * b * c = c * ((&2 * b) * a)`] THEN
1970   SUBGOAL_THEN
1971    `~(&2 * (x / pi) pow (2 * (n + 1)) = &0)`
1972   ASSUME_TAC THENL
1973    [REWRITE_TAC[REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ; REAL_POW_EQ_0] THEN
1974     REWRITE_TAC[DE_MORGAN_THM] THEN DISJ1_TAC THEN
1975     REWRITE_TAC[real_div; REAL_ENTIRE; REAL_INV_EQ_0] THEN
1976     ASM_SIMP_TAC[PI_POS; REAL_LT_IMP_NZ;
1977                  snd(EQ_IMP_RULE(SPEC_ALL REAL_ABS_NZ))];
1978     ALL_TAC] THEN
1979   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
1980   DISCH_THEN(MP_TAC o MATCH_MP SUM_UNIQ) THEN
1981   DISCH_THEN(MP_TAC o AP_TERM `( * ) (&2 * (x / pi) pow (2 * (n + 1)))`) THEN
1982   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV)
1983    [AC REAL_MUL_AC `a * b * c = (a * b) * c`] THEN
1984   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID] THEN
1985   REWRITE_TAC[GSYM REAL_MUL_ASSOC]);;
1986
1987 let COT_POWSER_SQUAREDAGAIN = prove
1988  (`!x. &0 < abs(x) /\ abs(x) < pi
1989        ==> (\n. (if n = 0 then &1
1990                  else --(&2) *
1991                       suminf (\m. inv (&(m + 1) pow (2 * n))) /
1992                       pi pow (2 * n)) *
1993                 x pow (2 * n))
1994            sums (x * cot(x))`,
1995   GEN_TAC THEN DISCH_TAC THEN
1996   FIRST_ASSUM(MP_TAC o MATCH_MP COT_POWSER_SQUARED_FORM) THEN
1997   DISCH_THEN(MP_TAC o MATCH_MP SER_NEG) THEN
1998   REWRITE_TAC[REAL_NEG_NEG] THEN DISCH_TAC THEN
1999   SUBGOAL_THEN
2000    `(\n. if n = 0 then &1 else
2001          --(&2 * (x / pi) pow (2 * n) *
2002                  suminf (\m. inv (&(m + 1) pow (2 * n)))))
2003     sums (sum(0,1) (\n. if n = 0 then &1 else
2004                         --(&2 * (x / pi) pow (2 * n) *
2005                            suminf (\m. inv (&(m + 1) pow (2 * n))))) +
2006           suminf (\n. if n + 1 = 0 then &1 else
2007                         --(&2 * (x / pi) pow (2 * (n + 1)) *
2008                            suminf (\m. inv (&(m + 1) pow (2 * (n + 1)))))))`
2009   MP_TAC THENL
2010    [MATCH_MP_TAC SER_OFFSET_REV THEN
2011     REWRITE_TAC[ARITH_RULE `~(n + 1 = 0)`] THEN
2012     REWRITE_TAC[summable] THEN
2013     EXISTS_TAC `x * cot(x) - &1` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
2014   REWRITE_TAC[SUM_1; ARITH_RULE `~(n + 1 = 0)`] THEN
2015   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
2016   REWRITE_TAC[REAL_ARITH `&1 + x - &1 = x`] THEN
2017   MATCH_MP_TAC EQ_IMP THEN
2018   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
2019   X_GEN_TAC `n:num` THEN REWRITE_TAC[] THEN
2020   COND_CASES_TAC THEN
2021   ASM_REWRITE_TAC[MULT_CLAUSES; real_pow; REAL_MUL_LID] THEN
2022   REWRITE_TAC[REAL_POW_DIV; REAL_MUL_LNEG] THEN AP_TERM_TAC THEN
2023   REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV] THEN
2024   REWRITE_TAC[REAL_MUL_AC]);;
2025
2026 let COT_X_POWSER = prove
2027  (`!x. &0 < abs(x) /\ abs(x) < pi
2028        ==> (\n. (if n = 0 then &1 else if ODD n then &0 else
2029                  --(&2) * suminf (\m. inv (&(m + 1) pow n)) / pi pow n) *
2030                 x pow n)
2031            sums (x * cot(x))`,
2032   GEN_TAC THEN DISCH_TAC THEN
2033   FIRST_ASSUM(MP_TAC o MATCH_MP COT_POWSER_SQUAREDAGAIN) THEN
2034   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
2035    [ARITH_RULE `(n = 0) <=> (2 * n = 0)`] THEN
2036   DISCH_THEN(MP_TAC o MATCH_MP SER_INSERTZEROS) THEN
2037   MATCH_MP_TAC EQ_IMP THEN
2038   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
2039   X_GEN_TAC `n:num` THEN REWRITE_TAC[] THEN
2040   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN
2041   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LZERO]);;
2042
2043 (* ------------------------------------------------------------------------- *)
2044 (* Hence use the double-angle formula to get a series for tangent.           *)
2045 (* ------------------------------------------------------------------------- *)
2046
2047 let TAN_COT_DOUBLE = prove
2048  (`!x. &0 < abs(x) /\ abs(x) < pi / &2
2049         ==> (tan(x) = cot(x) - &2 * cot(&2 * x))`,
2050   REPEAT STRIP_TAC THEN
2051   SUBGOAL_THEN `~(sin x = &0)` ASSUME_TAC THENL
2052    [REWRITE_TAC[SIN_ZERO] THEN
2053     POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
2054     CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2055     REWRITE_TAC[OR_EXISTS_THM] THEN
2056     REWRITE_TAC[TAUT `a /\ b \/ a /\ c <=> a /\ (b \/ c)`] THEN
2057     DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
2058     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2059     DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2060      `(x = a) \/ (x = --a) ==> &0 <= a ==> (abs(x) = a)`)) THEN
2061     SIMP_TAC[REAL_LE_MUL; REAL_LE_DIV; REAL_LT_IMP_LE; PI_POS; REAL_POS] THEN
2062     DISCH_THEN(K ALL_TAC) THEN
2063     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
2064     DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
2065     ASM_CASES_TAC `m = 0` THEN
2066     ASM_REWRITE_TAC[MULT_CLAUSES; REAL_MUL_LZERO; REAL_LT_REFL] THEN
2067     DISJ1_TAC THEN
2068     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_ARITH `x = &1 * x`] THEN
2069     SIMP_TAC[REAL_LT_RMUL_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; PI_POS] THEN
2070     UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC; ALL_TAC] THEN
2071   SUBGOAL_THEN `~(cos x = &0)` ASSUME_TAC THENL
2072    [REWRITE_TAC[COS_ZERO] THEN
2073     MAP_EVERY UNDISCH_TAC [`abs x < pi / &2`; `&0 < abs x`] THEN
2074     REWRITE_TAC[IMP_IMP] THEN
2075     CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2076     REWRITE_TAC[OR_EXISTS_THM; NOT_EVEN] THEN
2077     REWRITE_TAC[TAUT `a /\ b \/ a /\ c <=> a /\ (b \/ c)`] THEN
2078     DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
2079     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2080     DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2081      `(x = a) \/ (x = --a) ==> &0 <= a ==> (abs(x) = a)`)) THEN
2082     SIMP_TAC[REAL_LE_MUL; REAL_LE_DIV; REAL_LT_IMP_LE; PI_POS; REAL_POS] THEN
2083     DISCH_THEN(K ALL_TAC) THEN
2084     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ODD_EXISTS]) THEN
2085     DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
2086     DISJ2_TAC THEN
2087     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_ARITH `x = &1 * x`] THEN
2088     SIMP_TAC[REAL_LT_RMUL_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; PI_POS] THEN
2089     ARITH_TAC; ALL_TAC] THEN
2090   SUBGOAL_THEN `~(sin(&2 * x) = &0)` ASSUME_TAC THENL
2091    [REWRITE_TAC[SIN_ZERO] THEN
2092     MAP_EVERY UNDISCH_TAC [`abs x < pi / &2`; `&0 < abs x`] THEN
2093     REWRITE_TAC[IMP_IMP] THEN
2094     CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2095     REWRITE_TAC[OR_EXISTS_THM] THEN
2096     REWRITE_TAC[TAUT `a /\ b \/ a /\ c <=> a /\ (b \/ c)`] THEN
2097     DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
2098     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2099     DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2100      `(x = a) \/ (x = --a) ==> &0 <= a ==> (abs(x) = a)`)) THEN
2101     SIMP_TAC[REAL_LE_MUL; REAL_LE_DIV; REAL_LT_IMP_LE; PI_POS; REAL_POS] THEN
2102     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
2103     GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
2104     SIMP_TAC[GSYM REAL_EQ_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2105     DISCH_THEN(K ALL_TAC) THEN
2106     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
2107     DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
2108     ASM_CASES_TAC `m = 0` THEN
2109     ASM_REWRITE_TAC[MULT_CLAUSES; REAL_MUL_LZERO; REAL_LT_REFL] THEN
2110     CONV_TAC REAL_RAT_REDUCE_CONV THEN
2111     DISJ2_TAC THEN
2112     REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
2113     ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c = b * a * c`] THEN
2114     SIMP_TAC[REAL_LT_DIV2_EQ; REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH;
2115              REAL_OF_NUM_LT] THEN
2116     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_ARITH `x = &1 * x`] THEN
2117     SIMP_TAC[REAL_LT_RMUL_EQ; PI_POS; REAL_OF_NUM_LT] THEN
2118     UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC; ALL_TAC] THEN
2119   REWRITE_TAC[tan; cot] THEN
2120   MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
2121   EXISTS_TAC `sin(&2 * x)` THEN ASM_REWRITE_TAC[real_div] THEN
2122   ONCE_REWRITE_TAC[REAL_ARITH
2123    `(d * e - &2 * f * g) * h = h * d * e - &2 * f * (h * g)`] THEN
2124   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
2125   MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `sin(x)` THEN
2126   ASM_SIMP_TAC[REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC;
2127                REAL_MUL_LINV; REAL_MUL_RID] THEN
2128   GEN_REWRITE_TAC LAND_CONV
2129    [AC REAL_MUL_AC `a * b * c * d = a * c * d * b`] THEN
2130   MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `cos(x)` THEN
2131   ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID] THEN
2132   REWRITE_TAC[SIN_DOUBLE; COS_DOUBLE; REAL_POW_2] THEN
2133   REWRITE_TAC[REAL_ARITH
2134    `((&2 * s * c) * c - &2 * (c * c - s * s) * s) * c =
2135     &2 * c * s * s * s`] THEN
2136   REWRITE_TAC[REAL_MUL_AC]);;
2137
2138 let TAN_POWSER_WEAK = prove
2139  (`!x. &0 < abs(x) /\ abs(x) < pi / &2
2140        ==> (\n. (if EVEN n then &0 else
2141                  &2 * (&2 pow (n + 1) - &1) *
2142                  suminf (\m. inv (&(m + 1) pow (n + 1))) / pi pow (n + 1)) *
2143                 x pow n)
2144            sums (tan x)`,
2145   REPEAT STRIP_TAC THEN
2146   MP_TAC(SPEC `x:real` COT_X_POWSER) THEN
2147   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
2148    [ASM_REWRITE_TAC[] THEN
2149     MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `pi / &2` THEN
2150     ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2151     MP_TAC PI_POS THEN REAL_ARITH_TAC; ALL_TAC] THEN
2152   DISCH_THEN(MP_TAC o SPEC `inv(x)` o MATCH_MP SER_CMUL) THEN
2153   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_ASSOC] THEN
2154   ASM_SIMP_TAC[REAL_MUL_LINV; REAL_ABS_NZ; REAL_MUL_LID] THEN
2155   MP_TAC(SPEC `&2 * x` COT_X_POWSER) THEN
2156   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
2157    [ASM_SIMP_TAC[REAL_ABS_MUL; REAL_ABS_NUM;
2158                  REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
2159     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2160     ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH]; ALL_TAC] THEN
2161   DISCH_THEN(MP_TAC o SPEC `inv(x)` o MATCH_MP SER_CMUL) THEN
2162   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
2163    [AC REAL_MUL_AC `a * (b * c) * d = (a * c) * b * d`] THEN
2164   ASM_SIMP_TAC[REAL_MUL_LINV; REAL_ABS_NZ; REAL_MUL_LID] THEN
2165   ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
2166   DISCH_THEN(MP_TAC o MATCH_MP SER_SUB) THEN
2167   ASM_SIMP_TAC[GSYM TAN_COT_DOUBLE] THEN
2168   DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN
2169   DISCH_THEN(ASSUME_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
2170   DISCH_THEN(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN
2171   DISCH_THEN(MP_TAC o SPEC `1` o MATCH_MP SER_OFFSET) THEN
2172   ASM_REWRITE_TAC[SUM_1] THEN
2173   REWRITE_TAC[real_pow; REAL_MUL_RID; REAL_SUB_REFL; REAL_SUB_RZERO] THEN
2174   REWRITE_TAC[ODD_ADD; ARITH_ODD; ADD_EQ_0; ARITH_EQ] THEN
2175   MATCH_MP_TAC EQ_IMP THEN
2176   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
2177   X_GEN_TAC `n:num` THEN REWRITE_TAC[NOT_ODD] THEN
2178   COND_CASES_TAC THEN
2179   ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_SUB_REFL] THEN
2180   REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; REAL_POW_MUL; GSYM REAL_MUL_ASSOC] THEN
2181   ONCE_REWRITE_TAC[REAL_ARITH
2182    `x' * m2 * s * xp * x - x' * m2 * s * pn * t * xp * x =
2183     (x' * x) * --m2 * (t * pn - &1) * s * xp`] THEN
2184   ASM_SIMP_TAC[REAL_NEG_NEG; REAL_MUL_LINV; REAL_ABS_NZ; REAL_MUL_LID] THEN
2185   REWRITE_TAC[REAL_MUL_AC]);;
2186
2187 let TAN_POWSER = prove
2188  (`!x. abs(x) < pi / &2
2189        ==> (\n. (if EVEN n then &0 else
2190                  &2 * (&2 pow (n + 1) - &1) *
2191                  suminf (\m. inv (&(m + 1) pow (n + 1))) / pi pow (n + 1)) *
2192                 x pow n)
2193            sums (tan x)`,
2194   REPEAT GEN_TAC THEN
2195   ASM_CASES_TAC `&0 < abs(x)` THEN ASM_SIMP_TAC[TAN_POWSER_WEAK] THEN
2196   DISCH_THEN(K ALL_TAC) THEN
2197   POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM REAL_ABS_NZ] THEN
2198   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[TAN_0] THEN
2199   W(fun (asl,w) -> MP_TAC(SPECL [lhand w; `0`] SER_0)) THEN
2200   REWRITE_TAC[sum] THEN DISCH_THEN MATCH_MP_TAC THEN
2201   X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN
2202   ASM_CASES_TAC `EVEN n` THEN ASM_REWRITE_TAC[REAL_MUL_LZERO] THEN
2203   UNDISCH_TAC `~(EVEN n)` THEN
2204   REWRITE_TAC[NOT_EVEN; ODD_EXISTS; real_pow; LEFT_IMP_EXISTS_THM] THEN
2205   SIMP_TAC[real_pow; REAL_MUL_LZERO; REAL_MUL_RZERO]);;
2206
2207 (* ------------------------------------------------------------------------- *)
2208 (* Add polynomials to differentiator's known functions, for next proofs.     *)
2209 (* ------------------------------------------------------------------------- *)
2210
2211 let th = prove
2212  (`(f diffl l)(x) ==>
2213     ((\x. poly p (f x)) diffl (l * poly (poly_diff p) (f x)))(x)`,
2214   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2215   MP_TAC(SPECL [`\x. poly p x`; `f:real->real`;
2216                 `poly (poly_diff p) (f(x:real))`;
2217                 `l:real`; `x:real`] DIFF_CHAIN) THEN
2218   ASM_REWRITE_TAC[POLY_DIFF]) in
2219 add_to_diff_net th;;
2220
2221 (* ------------------------------------------------------------------------- *)
2222 (* Main recurrence relation.                                                 *)
2223 (* ------------------------------------------------------------------------- *)
2224
2225 let DIFF_CHAIN_TAN = prove
2226  (`~(cos x = &0)
2227    ==> ((\x. poly p (tan x)) diffl
2228         (poly ([&1; &0; &1] ** poly_diff p) (tan x))) (x)`,
2229   REPEAT STRIP_TAC THEN REWRITE_TAC[tan] THEN
2230   W(MP_TAC o SPEC `x:real` o DIFF_CONV o lhand o rator o snd) THEN
2231   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN
2232   AP_THM_TAC THEN AP_TERM_TAC THEN
2233   REWRITE_TAC[POLY_MUL] THEN
2234   AP_THM_TAC THEN AP_TERM_TAC THEN
2235   REWRITE_TAC[poly; REAL_MUL_RID; REAL_MUL_RZERO; REAL_ADD_RID;
2236               REAL_ADD_LID] THEN
2237   REWRITE_TAC[REAL_ARITH `a - --s * s = (s * s + a)`] THEN
2238   REWRITE_TAC[GSYM REAL_POW_2; SIN_CIRCLE] THEN
2239   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_POW2_ABS] THEN
2240   ASM_SIMP_TAC[REAL_POW_LT; GSYM REAL_ABS_NZ; REAL_EQ_LDIV_EQ] THEN
2241   REWRITE_TAC[REAL_POW2_ABS] THEN
2242   REWRITE_TAC[REAL_ADD_RDISTRIB; GSYM REAL_POW_MUL] THEN
2243   ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_MUL_LID] THEN
2244   ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[SIN_CIRCLE]);;
2245
2246 (* ------------------------------------------------------------------------- *)
2247 (* Define tangent polynomials and tangent numbers on this pattern.           *)
2248 (* ------------------------------------------------------------------------- *)
2249
2250 let tanpoly = new_recursive_definition num_RECURSION
2251   `(tanpoly 0 = [&0; &1]) /\
2252    (!n. tanpoly (SUC n) = [&1; &0; &1] ** poly_diff(tanpoly n))`;;
2253
2254 let TANPOLYS_RULE =
2255   let pth1,pth2 = CONJ_PAIR tanpoly in
2256   let base = [pth1]
2257   and rule = GEN_REWRITE_RULE LAND_CONV [GSYM pth2] in
2258   let poly_diff_tm = `poly_diff`
2259   and poly_mul_tm = `( ** ) [&1; &0; &1]` in
2260   let rec tanpolys n =
2261     if n < 0 then []
2262     else if n = 0 then base else
2263     let thl = tanpolys (n - 1) in
2264     let th1 = AP_TERM poly_diff_tm (hd thl) in
2265     let th2 = TRANS th1 (POLY_DIFF_CONV (rand(concl th1))) in
2266     let th3 = AP_TERM poly_mul_tm th2 in
2267     let th4 = TRANS th3 (POLY_MUL_CONV (rand(concl th3))) in
2268     let th5 = rule th4 in
2269     let th6 = CONV_RULE (LAND_CONV(RAND_CONV NUM_SUC_CONV)) th5 in
2270     th6::thl in
2271   rev o tanpolys;;
2272
2273 let TANPOLY_CONV =
2274   let tanpoly_tm = `tanpoly` in
2275   fun tm ->
2276     let l,r = dest_comb tm in
2277     if l <> tanpoly_tm then failwith "TANPOLY_CONV"
2278     else last(TANPOLYS_RULE(dest_small_numeral r));;
2279
2280 let tannumber = new_definition
2281   `tannumber n = poly (tanpoly n) (&0)`;;
2282
2283 let TANNUMBERS_RULE,TANNUMBER_CONV =
2284   let POLY_0_THM = prove
2285    (`(poly [] (&0) = &0) /\
2286      (poly (CONS h t) (&0) = h)`,
2287     REWRITE_TAC[poly; REAL_MUL_LZERO; REAL_ADD_RID]) in
2288   let poly_tm = `poly`
2289   and zero_tm = `&0`
2290   and tannumber_tm = `tannumber`
2291   and depoly_conv = GEN_REWRITE_CONV I [POLY_0_THM]
2292   and tannumber_rule = GEN_REWRITE_RULE LAND_CONV [GSYM tannumber] in
2293   let process th =
2294     let th1 = AP_THM (AP_TERM poly_tm th) zero_tm in
2295     let th2 = TRANS th1 (depoly_conv (rand(concl th1))) in
2296     let th3 = tannumber_rule th2 in
2297     th3 in
2298   let TANNUMBERS_RULE = map process o TANPOLYS_RULE
2299   and TANNUMBER_CONV tm =
2300     let l,r = dest_comb tm in
2301     if l <> tannumber_tm then failwith "TANNUMBER_CONV" else
2302     process(last(TANPOLYS_RULE(dest_small_numeral r))) in
2303   TANNUMBERS_RULE,TANNUMBER_CONV;;
2304
2305 (* ------------------------------------------------------------------------- *)
2306 (* Chaining rules using the tangent polynomials.                             *)
2307 (* ------------------------------------------------------------------------- *)
2308
2309 let DIFF_CHAIN_TAN_TANPOLYS = prove
2310  (`~(cos x = &0)
2311    ==> ((\x. poly (tanpoly n) (tan x)) diffl
2312         (poly (tanpoly(SUC n)) (tan x))) (x)`,
2313   REWRITE_TAC[tanpoly; DIFF_CHAIN_TAN]);;
2314
2315 let th = prove
2316  (`(f diffl l)(x) /\ ~(cos(f x) = &0)
2317    ==> ((\x. poly (tanpoly n) (tan(f x))) diffl
2318         (l * poly (tanpoly(SUC n)) (tan(f x))))(x)`,
2319   REPEAT STRIP_TAC THEN
2320   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2321   MP_TAC(SPECL [`\x. poly (tanpoly n) (tan x)`; `f:real->real`;
2322                 `poly (tanpoly(SUC n)) (tan(f(x:real)))`;
2323                 `l:real`; `x:real`] DIFF_CHAIN) THEN
2324   ASM_SIMP_TAC[DIFF_CHAIN_TAN_TANPOLYS]) in
2325 add_to_diff_net th;;
2326
2327 (* ------------------------------------------------------------------------- *)
2328 (* Hence rewrite coefficients of tan and cot series in terms of tannumbers.  *)
2329 (* ------------------------------------------------------------------------- *)
2330
2331 let TERMDIFF_ALT = prove
2332  (`!f f' c k.
2333         (!x. abs(x) < k ==> (\n. c(n) * x pow n) sums f(x))
2334         ==> (!x. abs(x) < k ==> (f diffl f'(x))(x))
2335             ==> (!x. abs(x) < k ==> (\n. (diffs c)(n) * x pow n) sums f'(x))`,
2336   REPEAT STRIP_TAC THEN
2337   SUBGOAL_THEN
2338    `summable (\n. diffs c n * x pow n) /\
2339     (f'(x) = suminf (\n. diffs c n * x pow n))`
2340   MP_TAC THENL
2341    [ALL_TAC; SIMP_TAC[SUMMABLE_SUM]] THEN
2342   CONJ_TAC THENL
2343    [UNDISCH_TAC `abs(x) < k` THEN SPEC_TAC(`x:real`,`x:real`) THEN
2344     MATCH_MP_TAC TERMDIFF_CONVERGES THEN
2345     REPEAT STRIP_TAC THEN REWRITE_TAC[summable] THEN
2346     EXISTS_TAC `(f:real->real) x` THEN ASM_SIMP_TAC[]; ALL_TAC] THEN
2347   ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
2348   MATCH_MP_TAC DIFF_LCONST THEN
2349   EXISTS_TAC `\x. f x - suminf (\n. c(n) * x pow n)` THEN
2350   EXISTS_TAC `x:real` THEN CONJ_TAC THENL
2351    [MATCH_MP_TAC DIFF_SUB THEN ASM_SIMP_TAC[] THEN
2352     MATCH_MP_TAC TERMDIFF_STRONG THEN
2353     EXISTS_TAC `(abs(x) + k) / &2` THEN CONJ_TAC THENL
2354      [REWRITE_TAC[summable] THEN
2355       EXISTS_TAC `(f:real->real)((abs(x) + k) / &2)` THEN
2356       FIRST_ASSUM MATCH_MP_TAC; ALL_TAC] THEN
2357     SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NUM; REAL_LT_LDIV_EQ;
2358              REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2359     UNDISCH_TAC `abs(x) < k` THEN REAL_ARITH_TAC; ALL_TAC] THEN
2360   EXISTS_TAC `k - abs(x)` THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
2361   X_GEN_TAC `y:real` THEN DISCH_TAC THEN
2362   MATCH_MP_TAC(REAL_ARITH `(a = b) /\ (c = d) ==> (a - b = c - d)`) THEN
2363   CONJ_TAC THEN MATCH_MP_TAC SUM_UNIQ THEN
2364   FIRST_ASSUM MATCH_MP_TAC THEN
2365   UNDISCH_TAC `abs(x - y) < k - abs(x)` THEN REAL_ARITH_TAC);;
2366
2367 let TAN_DERIV_POWSER = prove
2368  (`!n x. abs(x) < pi / &2
2369          ==> (\m. ITER n diffs
2370                    (\i. if EVEN i
2371                         then &0
2372                         else &2 *
2373                              (&2 pow (i + 1) - &1) *
2374                              suminf (\m. inv (&(m + 1) pow (i + 1))) /
2375                              pi pow (i + 1)) m *
2376                   x pow m)
2377              sums (poly (tanpoly n) (tan x))`,
2378   INDUCT_TAC THENL
2379    [REPEAT STRIP_TAC THEN REWRITE_TAC[ITER; tanpoly; poly] THEN
2380     REWRITE_TAC[REAL_ADD_LID; REAL_ADD_RID; REAL_MUL_RZERO; REAL_MUL_RID] THEN
2381     ASM_SIMP_TAC[TAN_POWSER]; ALL_TAC] THEN
2382   FIRST_ASSUM(MP_TAC o MATCH_MP TERMDIFF_ALT) THEN
2383   REWRITE_TAC[ITER] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
2384   DISCH_THEN MATCH_MP_TAC THEN
2385   X_GEN_TAC `x:real` THEN DISCH_TAC THEN
2386   MATCH_MP_TAC DIFF_CHAIN_TAN_TANPOLYS THEN
2387   REWRITE_TAC[COS_ZERO] THEN
2388   UNDISCH_TAC `abs x < pi / &2` THEN
2389   CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN
2390   REWRITE_TAC[OR_EXISTS_THM; NOT_EVEN] THEN
2391   REWRITE_TAC[TAUT `a /\ b \/ a /\ c <=> a /\ (b \/ c)`] THEN
2392   DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
2393   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2394   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2395    `(x = a) \/ (x = --a) ==> &0 <= a ==> (abs(x) = a)`)) THEN
2396   SIMP_TAC[REAL_LE_MUL; REAL_LE_DIV; REAL_LT_IMP_LE; PI_POS; REAL_POS] THEN
2397   DISCH_THEN(K ALL_TAC) THEN
2398   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ODD_EXISTS]) THEN
2399   DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
2400   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_ARITH `x = &1 * x`] THEN
2401   SIMP_TAC[REAL_LT_RMUL_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; PI_POS] THEN
2402   ARITH_TAC);;
2403
2404 let ITER_DIFFS_LEMMA = prove
2405  (`!n c. ITER n diffs c 0 = &(FACT n) * c(n)`,
2406   INDUCT_TAC THEN ASM_REWRITE_TAC[ITER_ALT; diffs; FACT; REAL_MUL_LID] THEN
2407   REWRITE_TAC[GSYM REAL_OF_NUM_MUL; REAL_MUL_AC]);;
2408
2409 let TANNUMBER_HARMONICSUMS = prove
2410  (`!n. ODD n
2411        ==> (&2 * (&2 pow (n + 1) - &1) * &(FACT n) *
2412             suminf (\m. inv (&(m + 1) pow (n + 1))) / pi pow (n + 1) =
2413             tannumber n)`,
2414   REPEAT STRIP_TAC THEN
2415   MP_TAC(SPECL [`n:num`; `&0`] TAN_DERIV_POWSER) THEN
2416   SIMP_TAC[REAL_ABS_NUM; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; PI_POS] THEN
2417   REWRITE_TAC[TAN_0; GSYM tannumber] THEN
2418   MP_TAC(SPECL
2419    [`\m. ITER n diffs
2420       (\i. if EVEN i
2421            then &0
2422            else &2 *
2423                 (&2 pow (i + 1) - &1) *
2424                 suminf (\m. inv (&(m + 1) pow (i + 1))) / pi pow (i + 1))
2425       m *
2426       &0 pow m`;
2427     `1`] SER_0) THEN
2428   REWRITE_TAC[SUM_1] THEN
2429   SIMP_TAC[snd(EQ_IMP_RULE(SPEC_ALL REAL_POW_EQ_0));
2430            ARITH_RULE `1 <= n ==> ~(n = 0)`] THEN
2431   REWRITE_TAC[REAL_MUL_RZERO; real_pow] THEN
2432   ONCE_REWRITE_TAC[IMP_IMP] THEN
2433   DISCH_THEN(MP_TAC o MATCH_MP SER_UNIQ) THEN
2434   DISCH_THEN(SUBST1_TAC o SYM) THEN
2435   REWRITE_TAC[ITER_DIFFS_LEMMA; REAL_MUL_RID] THEN
2436   ASM_REWRITE_TAC[GSYM NOT_ODD] THEN REWRITE_TAC[REAL_MUL_AC]);;
2437
2438 let HARMONICSUMS_TANNUMBER = prove
2439  (`!n. EVEN n /\ ~(n = 0)
2440        ==> (suminf (\m. inv (&(m + 1) pow n)) / pi pow n =
2441             tannumber(n - 1) / (&2 * &(FACT(n - 1)) * (&2 pow n - &1)))`,
2442   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; EVEN; NOT_EVEN] THEN
2443   REWRITE_TAC[SUC_SUB1] THEN SIMP_TAC[GSYM TANNUMBER_HARMONICSUMS] THEN
2444   REWRITE_TAC[ADD1] THEN
2445   ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d = (a * c * b) * d`] THEN
2446   REWRITE_TAC[real_div] THEN DISCH_TAC THEN
2447   ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b * c) * d = a * (b * c) * d`] THEN
2448   REWRITE_TAC[GSYM real_div] THEN CONV_TAC SYM_CONV THEN
2449   MATCH_MP_TAC REAL_DIV_LMUL THEN MATCH_MP_TAC REAL_LT_IMP_NZ THEN
2450   MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
2451   MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_OF_NUM_LT; FACT_LT] THEN
2452   REWRITE_TAC[REAL_SUB_LT] THEN
2453   REWRITE_TAC[REAL_POW2_CLAUSES; ADD_EQ_0; ARITH_EQ]);;
2454
2455 (* ------------------------------------------------------------------------- *)
2456 (* For uniformity, show that even tannumbers are zero.                       *)
2457 (* ------------------------------------------------------------------------- *)
2458
2459 let ODD_POLY_DIFF = prove
2460  (`(!x. poly p (--x) = poly p x)
2461    ==> (!x. poly (poly_diff p) (--x) = --(poly(poly_diff p) x))`,
2462   REPEAT STRIP_TAC THEN MATCH_MP_TAC DIFF_UNIQ THEN
2463   EXISTS_TAC `\x. poly p (--x)` THEN EXISTS_TAC `--x` THEN CONJ_TAC THENL
2464    [FIRST_ASSUM(SUBST1_TAC o SYM o HALF_MK_ABS o GSYM) THEN
2465     REWRITE_TAC[CONV_RULE(ONCE_DEPTH_CONV ETA_CONV) POLY_DIFF];
2466     MP_TAC(SPECL [`\x. poly p x`; `\x. --x`; `poly (poly_diff p) x`;
2467                   `--(&1)`; `--x`]
2468            DIFF_CHAIN) THEN
2469     REWRITE_TAC[POLY_DIFF; REAL_MUL_RNEG; REAL_MUL_RID; REAL_NEG_NEG] THEN
2470     DISCH_THEN MATCH_MP_TAC THEN
2471     W(MP_TAC o SPEC `--x` o DIFF_CONV o lhand o rator o snd) THEN
2472     REWRITE_TAC[]]);;
2473
2474 let EVEN_POLY_DIFF = prove
2475  (`(!x. poly p (--x) = --(poly p x))
2476    ==> (!x. poly (poly_diff p) (--x) = poly(poly_diff p) x)`,
2477   REPEAT STRIP_TAC THEN MATCH_MP_TAC DIFF_UNIQ THEN
2478   EXISTS_TAC `\x. poly p x` THEN EXISTS_TAC `--x` THEN
2479   REWRITE_TAC[POLY_DIFF] THEN
2480   FIRST_ASSUM(MP_TAC o
2481     ONCE_REWRITE_RULE[REAL_ARITH `(a = --b) <=> (--a = b)`]) THEN
2482   DISCH_THEN(SUBST1_TAC o HALF_MK_ABS o GSYM) THEN
2483   REWRITE_TAC[] THEN
2484   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_NEG_NEG] THEN
2485   MATCH_MP_TAC DIFF_NEG THEN
2486   MP_TAC(SPECL [`\x. poly p x`; `\x. --x`; `poly (poly_diff p) x`;
2487                   `--(&1)`; `--x`]
2488            DIFF_CHAIN) THEN
2489   REWRITE_TAC[POLY_DIFF; REAL_MUL_RNEG; REAL_MUL_RID; REAL_NEG_NEG] THEN
2490   DISCH_THEN MATCH_MP_TAC THEN
2491   W(MP_TAC o SPEC `--x` o DIFF_CONV o lhand o rator o snd) THEN
2492   REWRITE_TAC[]);;
2493
2494 let TANPOLY_ODD_EVEN = prove
2495  (`!n x. (poly (tanpoly n) (--x) =
2496           if EVEN n then --(poly (tanpoly n) x) else poly (tanpoly n) x)`,
2497   INDUCT_TAC THENL
2498    [REWRITE_TAC[EVEN; tanpoly] THEN
2499     CONV_TAC(ONCE_DEPTH_CONV POLY_DIFF_CONV) THEN
2500     REWRITE_TAC[poly] THEN REAL_ARITH_TAC; ALL_TAC] THEN
2501   POP_ASSUM MP_TAC THEN REWRITE_TAC[EVEN] THEN
2502   ASM_CASES_TAC `EVEN n` THEN ASM_REWRITE_TAC[] THEN
2503   REPEAT STRIP_TAC THEN
2504   ASM_SIMP_TAC[tanpoly; POLY_MUL; ODD_POLY_DIFF; EVEN_POLY_DIFF] THEN
2505   REWRITE_TAC[REAL_MUL_RNEG] THEN TRY AP_TERM_TAC THEN
2506   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[poly] THEN REAL_ARITH_TAC);;
2507
2508 let TANNUMBER_EVEN = prove
2509  (`!n. EVEN n ==> (tannumber n = &0)`,
2510   REPEAT STRIP_TAC THEN REWRITE_TAC[tannumber] THEN
2511   MATCH_MP_TAC(REAL_ARITH `(x = --x) ==> (x = &0)`) THEN
2512   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_NEG_0] THEN
2513   ASM_SIMP_TAC[TANPOLY_ODD_EVEN]);;
2514
2515 (* ------------------------------------------------------------------------- *)
2516 (* Hence get tidy series.                                                    *)
2517 (* ------------------------------------------------------------------------- *)
2518
2519 let TAYLOR_TAN_CONVERGES = prove
2520  (`!x. abs(x) < pi / &2
2521        ==> (\n. tannumber n / &(FACT n) * x pow n) sums (tan x)`,
2522   GEN_TAC THEN
2523   DISCH_THEN(MP_TAC o MATCH_MP TAN_POWSER) THEN
2524   MATCH_MP_TAC EQ_IMP THEN
2525   AP_THM_TAC THEN AP_TERM_TAC THEN
2526   REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `n:num` THEN
2527   COND_CASES_TAC THENL
2528    [ASM_SIMP_TAC[real_div; TANNUMBER_EVEN; REAL_MUL_LZERO; REAL_MUL_RZERO];
2529     ALL_TAC] THEN
2530   ASM_SIMP_TAC[HARMONICSUMS_TANNUMBER; EVEN_ADD; ARITH; ADD_EQ_0] THEN
2531   REWRITE_TAC[ADD_SUB; real_div; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN
2532   ONCE_REWRITE_TAC[AC REAL_MUL_AC
2533    `a * b * c * a' * d * b' * e = (c * d * e) * ((a * a') * (b * b'))`] THEN
2534   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN AP_TERM_TAC THEN
2535   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_LID] THEN
2536   MATCH_MP_TAC REAL_MUL_RINV THEN
2537   SIMP_TAC[REAL_ARITH `&1 < x ==> ~(x - &1 = &0)`;
2538            REAL_POW2_CLAUSES; ADD_EQ_0; ARITH_EQ]);;
2539
2540 let TAYLOR_X_COT_CONVERGES = prove
2541  (`!x. &0 < abs(x) /\ abs(x) < pi
2542        ==> (\n. (if n = 0 then &1 else
2543                  tannumber (n - 1) / ((&1 - &2 pow n) * &(FACT(n - 1)))) *
2544                 x pow n)
2545            sums (x * cot(x))`,
2546   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP COT_X_POWSER) THEN
2547   MATCH_MP_TAC EQ_IMP THEN
2548   AP_THM_TAC THEN AP_TERM_TAC THEN
2549   REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `n:num` THEN
2550   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
2551   ASM_CASES_TAC `ODD n` THEN ASM_REWRITE_TAC[] THENL
2552    [SUBGOAL_THEN `tannumber(n - 1) = &0`
2553      (fun th -> SIMP_TAC[th; real_div; REAL_MUL_LZERO; REAL_MUL_RZERO]) THEN
2554     MATCH_MP_TAC TANNUMBER_EVEN THEN
2555     UNDISCH_TAC `ODD n` THEN
2556     SUBGOAL_THEN `n = SUC(n - 1)` MP_TAC THENL
2557      [UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
2558     DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
2559     REWRITE_TAC[ODD; NOT_ODD]; ALL_TAC] THEN
2560   AP_THM_TAC THEN AP_TERM_TAC THEN
2561   ASM_SIMP_TAC[HARMONICSUMS_TANNUMBER; GSYM NOT_ODD] THEN
2562   REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN
2563   ONCE_REWRITE_TAC[REAL_ARITH
2564    `--(&2) * x * y * z * a = (&2 * y) * x * --a * z`] THEN
2565   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2566   REWRITE_TAC[GSYM REAL_INV_NEG; REAL_NEG_SUB; REAL_MUL_LID]);;
2567
2568 (* ------------------------------------------------------------------------- *)
2569 (* Get a simple bound on the tannumbers.                                     *)
2570 (* ------------------------------------------------------------------------- *)
2571
2572 let TANNUMBER_BOUND = prove
2573  (`!n. abs(tannumber n) <= &4 * &(FACT n) * (&2 / pi) pow (n + 1)`,
2574   GEN_TAC THEN DISJ_CASES_TAC(SPEC `n:num` EVEN_OR_ODD) THEN
2575   ASM_SIMP_TAC[TANNUMBER_EVEN; GSYM TANNUMBER_HARMONICSUMS] THEN
2576   (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 5)
2577     [REAL_ABS_NUM; REAL_LE_MUL; REAL_POW_LE; REAL_POS; REAL_LE_DIV;
2578      PI_POS; REAL_LT_IMP_LE] THEN
2579   REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2580   ONCE_REWRITE_TAC[AC REAL_MUL_AC
2581    `a * b * c * d * e = (a * d) * c * b * e`] THEN
2582   ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
2583   REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL
2584    [REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
2585     REWRITE_TAC[REAL_ARITH `&2 * x <= &4 <=> x <= &2`] THEN
2586     MP_TAC(SPEC `\m. inv (&(m + 1) pow (n + 1))` SER_ABS) THEN
2587     REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM; REAL_ABS_POW] THEN
2588     W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
2589      [MATCH_MP_TAC SUMMABLE_INVERSE_POWERS THEN
2590       UNDISCH_TAC `ODD n` THEN
2591       SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
2592       REPEAT STRIP_TAC THEN ARITH_TAC; ALL_TAC] THEN
2593     MATCH_MP_TAC(REAL_ARITH `b <= c ==> a <= b ==> a <= c`) THEN
2594     MATCH_MP_TAC REAL_LE_TRANS THEN
2595     EXISTS_TAC `suminf (\m. inv(&(m + 1) pow 2))` THEN CONJ_TAC THENL
2596      [MATCH_MP_TAC SER_LE THEN REPEAT CONJ_TAC THENL
2597        [GEN_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
2598         SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH_RULE `0 < n + 1`] THEN
2599         MATCH_MP_TAC REAL_POW_MONO THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN
2600         UNDISCH_TAC `ODD n` THEN
2601         SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
2602         REPEAT STRIP_TAC THEN ARITH_TAC;
2603         MATCH_MP_TAC SUMMABLE_INVERSE_POWERS THEN
2604         UNDISCH_TAC `ODD n` THEN
2605         SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
2606         REPEAT STRIP_TAC THEN ARITH_TAC;
2607         MATCH_MP_TAC SUMMABLE_INVERSE_POWERS THEN REWRITE_TAC[LE_REFL]];
2608       ALL_TAC] THEN
2609     MATCH_MP_TAC REAL_LE_TRANS THEN
2610     EXISTS_TAC `sum(0,1) (\n. inv(&(n + 1) pow 2)) +
2611                 suminf (\n. inv(&((n + 1) + 1) pow 2))` THEN
2612     CONJ_TAC THENL
2613      [MATCH_MP_TAC(REAL_ARITH `(y = x) ==> x <= y`) THEN
2614       MATCH_MP_TAC SUM_UNIQ THEN
2615       MATCH_MP_TAC SER_OFFSET_REV THEN
2616       REWRITE_TAC[summable] THEN
2617       EXISTS_TAC
2618        `suminf (\n. inv(&(n + 1) pow 2)) -
2619        sum(0,1) (\n. inv(&(n + 1) pow 2))` THEN
2620       MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM] SER_OFFSET) THEN
2621       MATCH_MP_TAC SUMMABLE_INVERSE_POWERS THEN REWRITE_TAC[LE_REFL];
2622       ALL_TAC] THEN
2623     REWRITE_TAC[SUM_1; ADD_CLAUSES] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2624     REWRITE_TAC[REAL_ARITH `&1 + x <= &2 <=> x <= &1`] THEN
2625     SUBST1_TAC(MATCH_MP SUM_UNIQ SUMMABLE_INVERSE_SQUARES_LEMMA) THEN
2626     MATCH_MP_TAC SER_LE THEN REPEAT CONJ_TAC THENL
2627      [X_GEN_TAC `m:num` THEN REWRITE_TAC[REAL_POW_2] THEN
2628       REWRITE_TAC[ARITH_RULE `(n + 1) + 1 = n + 2`] THEN
2629       REWRITE_TAC[REAL_POW_2; REAL_INV_MUL; REAL_ABS_INV; REAL_ABS_NUM;
2630                   REAL_ABS_MUL] THEN
2631       MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN
2632       MATCH_MP_TAC REAL_LE_INV2 THEN
2633       REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC;
2634       REWRITE_TAC[summable] THEN
2635       EXISTS_TAC
2636        `suminf (\n. inv(&(n + 1) pow 2)) -
2637        sum(0,1) (\n. inv(&(n + 1) pow 2))` THEN
2638       MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM] SER_OFFSET) THEN
2639       MATCH_MP_TAC SUMMABLE_INVERSE_POWERS THEN REWRITE_TAC[LE_REFL];
2640       REWRITE_TAC[summable] THEN
2641       EXISTS_TAC `&1` THEN REWRITE_TAC[SUMMABLE_INVERSE_SQUARES_LEMMA]];
2642     ALL_TAC] THEN
2643   ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN REWRITE_TAC[REAL_ABS_NUM] THEN
2644   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
2645   REWRITE_TAC[REAL_POW_MUL; REAL_POW_INV] THEN
2646   ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
2647   REWRITE_TAC[REAL_ABS_INV; REAL_ABS_POW] THEN
2648   SIMP_TAC[real_abs; PI_POS; REAL_LT_IMP_LE] THEN
2649   REWRITE_TAC[GSYM real_abs] THEN
2650   MATCH_MP_TAC REAL_LE_RMUL THEN
2651   SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LT; REAL_LT_IMP_LE; PI_POS] THEN
2652   MATCH_MP_TAC(REAL_ARITH
2653    `&1 <= x ==> abs(x - &1) <= x`) THEN
2654   REWRITE_TAC[REAL_POW2_CLAUSES]);;
2655
2656 (* ------------------------------------------------------------------------- *)
2657 (* Also get some harmonic sums.                                              *)
2658 (* ------------------------------------------------------------------------- *)
2659
2660 let HARMONIC_SUMS = prove
2661  (`!n. (\m. inv (&(m + 1) pow (2 * (n + 1))))
2662        sums (pi pow (2 * (n + 1)) *
2663              tannumber(2 * n + 1) /
2664              (&2 * (&2 pow (2 * (n + 1)) - &1) * &(FACT(2 * n + 1))))`,
2665   GEN_TAC THEN
2666   SUBGOAL_THEN `summable (\m. inv (&(m + 1) pow (2 * (n + 1))))` MP_TAC THENL
2667    [MATCH_MP_TAC SUMMABLE_INVERSE_POWERS THEN ARITH_TAC; ALL_TAC] THEN
2668   DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
2669   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
2670   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
2671   SIMP_TAC[GSYM REAL_EQ_LDIV_EQ; REAL_POW_LT; PI_POS] THEN
2672   REWRITE_TAC[ARITH_RULE `2 * n + 1 = 2 * (n + 1) - 1`] THEN
2673   ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = a * c * b`] THEN
2674   MATCH_MP_TAC HARMONICSUMS_TANNUMBER THEN
2675   REWRITE_TAC[MULT_EQ_0; ADD_EQ_0; ARITH; EVEN_MULT]);;
2676
2677 let mk_harmonic =
2678   let pth = prove
2679    (`x * &1 / n = x / n`,
2680     REWRITE_TAC[real_div; REAL_MUL_LID]) in
2681   let final_RULE = CONV_RULE(TRY_CONV(GEN_REWRITE_CONV RAND_CONV [pth])) in
2682   fun n ->
2683     let th1 = SPEC(mk_small_numeral((n-1)/2)) HARMONIC_SUMS in
2684     let th2 = CONV_RULE NUM_REDUCE_CONV th1 in
2685     let th3 = CONV_RULE(ONCE_DEPTH_CONV TANNUMBER_CONV) th2 in
2686     let th4 = CONV_RULE REAL_RAT_REDUCE_CONV th3 in
2687     final_RULE th4;;
2688
2689 (* ------------------------------------------------------------------------- *)
2690 (* A little test.                                                            *)
2691 (* ------------------------------------------------------------------------- *)
2692
2693 map (fun n -> time mk_harmonic (2 * n)) (0--8);;
2694
2695 (* ------------------------------------------------------------------------- *)
2696 (* Isolate the most famous special case.                                     *)
2697 (* ------------------------------------------------------------------------- *)
2698
2699 let EULER_HARMONIC_SUM = mk_harmonic 2;;
2700
2701 (* ------------------------------------------------------------------------- *)
2702 (* Canonical Taylor series for tan and cot with truncation bounds.           *)
2703 (* ------------------------------------------------------------------------- *)
2704
2705 let TAYLOR_TAN_BOUND_GENERAL = prove
2706  (`!x n. abs(x) <= &1
2707          ==> abs(tan x - sum (0,n) (\m. tannumber m / &(FACT m) * x pow m))
2708              <= &12 * (&2 / &3) pow (n + 1) * abs(x) pow n`,
2709   REPEAT STRIP_TAC THEN
2710   SUBGOAL_THEN `abs(x) < pi / &2` MP_TAC THENL
2711    [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&1` THEN
2712     ASM_REWRITE_TAC[] THEN
2713     SIMP_TAC[REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2714     MP_TAC PI_APPROX_25_BITS THEN
2715     MATCH_MP_TAC(REAL_ARITH
2716      `b + e < a ==> abs(p - a) <= e ==> b < p`) THEN
2717     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
2718   DISCH_THEN(MP_TAC o MATCH_MP TAYLOR_TAN_CONVERGES) THEN
2719   DISCH_THEN(fun th ->
2720     ASSUME_TAC th THEN MP_TAC(MATCH_MP SUM_SUMMABLE th)) THEN
2721   DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP SER_OFFSET) THEN
2722   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
2723   REWRITE_TAC[sums] THEN DISCH_THEN(MP_TAC o MATCH_MP SEQ_ABS_IMP) THEN
2724   REWRITE_TAC[] THEN DISCH_TAC THEN
2725   MATCH_MP_TAC SEQ_LE_CONST THEN
2726   EXISTS_TAC `\r. abs(sum(0,r) (\m. (tannumber(m + n) / &(FACT(m + n))) *
2727                                     x pow (m + n)))` THEN
2728   EXISTS_TAC `0` THEN ASM_REWRITE_TAC[] THEN
2729   X_GEN_TAC `m:num` THEN DISCH_THEN(K ALL_TAC) THEN
2730   W(MP_TAC o PART_MATCH lhand SUM_ABS_LE o lhand o snd) THEN
2731   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
2732   MATCH_MP_TAC REAL_LE_TRANS THEN
2733   EXISTS_TAC
2734    `sum(0,m) (\r. &4 * (&2 / pi) pow (r + n + 1) * abs(x pow (r + n)))` THEN
2735   REWRITE_TAC[] THEN CONJ_TAC THENL
2736    [MATCH_MP_TAC SUM_LE THEN
2737     X_GEN_TAC `r:num` THEN REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN
2738     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_DIV; REAL_ABS_NUM] THEN
2739     REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
2740     REWRITE_TAC[REAL_ABS_POS] THEN
2741     SIMP_TAC[REAL_ABS_DIV; REAL_ABS_NUM;
2742              REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; FACT_LT] THEN
2743     MP_TAC(SPEC `r + n:num` TANNUMBER_BOUND) THEN
2744     REWRITE_TAC[REAL_MUL_AC; GSYM ADD_ASSOC]; ALL_TAC] THEN
2745   REWRITE_TAC[GSYM ADD1; ADD_CLAUSES] THEN
2746   REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN
2747   REWRITE_TAC[REAL_ABS_POW; GSYM REAL_POW_MUL] THEN
2748   ONCE_REWRITE_TAC[ADD_SYM] THEN
2749   REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC] THEN
2750   REWRITE_TAC[SUM_CMUL] THEN
2751   SUBGOAL_THEN `&2 / pi * abs(x) < &2 / &3` ASSUME_TAC THENL
2752    [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&2 / pi * &1` THEN
2753     CONJ_TAC THENL
2754      [ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LE_DIV; REAL_POS; REAL_LT_IMP_LE;
2755                    PI_POS];
2756       ALL_TAC] THEN
2757     REWRITE_TAC[REAL_MUL_RID] THEN
2758     SIMP_TAC[REAL_LT_LDIV_EQ; PI_POS] THEN
2759     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
2760     SIMP_TAC[GSYM REAL_LT_LDIV_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
2761     MP_TAC PI_APPROX_25_BITS THEN
2762     MATCH_MP_TAC(REAL_ARITH
2763      `b + e < a ==> abs(p - a) <= e ==> b < p`) THEN
2764     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
2765   SUBGOAL_THEN `~(&2 / pi * abs(x) = &1)` ASSUME_TAC THENL
2766    [UNDISCH_TAC `&2 / pi * abs x < &2 / &3` THEN
2767     ONCE_REWRITE_TAC[TAUT `a ==> ~b <=> b ==> ~a`] THEN
2768     SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
2769   GEN_REWRITE_TAC LAND_CONV [AC REAL_MUL_AC `(a * b) * c = (a * c) * b`] THEN
2770   MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> x <= a`) THEN
2771   ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
2772   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL
2773    [ALL_TAC;
2774     REWRITE_TAC[REAL_POW_MUL; GSYM REAL_ABS_POW;
2775                 REAL_ABS_MUL; REAL_ABS_ABS] THEN
2776     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
2777     REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
2778     REWRITE_TAC[REAL_ABS_POS] THEN
2779     REWRITE_TAC[REAL_ABS_MUL; real_div; REAL_ABS_NUM] THEN
2780     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
2781     REWRITE_TAC[REAL_ABS_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
2782     REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
2783     MP_TAC PI_APPROX_25_BITS THEN
2784     MATCH_MP_TAC(REAL_ARITH
2785      `b + e <= a ==> abs(p - a) <= e ==> b <= abs p`) THEN
2786     CONV_TAC REAL_RAT_REDUCE_CONV] THEN
2787   REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM; GSYM REAL_MUL_ASSOC] THEN
2788   REWRITE_TAC[REAL_ARITH
2789    `&4 * x * y <= &12 * z <=> x * y <= z * &3`] THEN
2790   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL
2791    [REWRITE_TAC[REAL_ABS_MUL; real_div; REAL_ABS_NUM] THEN
2792     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
2793     REWRITE_TAC[REAL_ABS_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
2794     REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
2795     MP_TAC PI_APPROX_25_BITS THEN
2796     MATCH_MP_TAC(REAL_ARITH
2797      `b + e <= a ==> abs(p - a) <= e ==> b <= abs p`) THEN
2798     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
2799   ASM_SIMP_TAC[GP_FINITE] THEN
2800   REWRITE_TAC[REAL_ABS_DIV] THEN ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN
2801   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
2802   REWRITE_TAC[real_div; GSYM REAL_ABS_INV] THEN
2803   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
2804   REWRITE_TAC[GSYM real_div] THEN CONJ_TAC THENL
2805    [MATCH_MP_TAC(REAL_ARITH
2806      `&0 <= x /\ x <= &1 ==> abs(&1 - x) <= &1`) THEN
2807     (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 4)
2808        [REAL_POW_LE; REAL_LE_DIV; REAL_LE_MUL; REAL_POS;
2809         REAL_ABS_POS; PI_POS; REAL_LT_IMP_LE] THEN
2810     MATCH_MP_TAC REAL_POW_1_LE THEN
2811     (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 4)
2812        [REAL_POW_LE; REAL_LE_DIV; REAL_LE_MUL; REAL_POS;
2813         REAL_ABS_POS; PI_POS; REAL_LT_IMP_LE] THEN
2814     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 / pi * &1` THEN
2815     ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LE_DIV; REAL_POS;
2816                  REAL_LT_IMP_LE; PI_POS] THEN
2817     SIMP_TAC[REAL_MUL_RID; REAL_LE_LDIV_EQ; PI_POS] THEN
2818     MP_TAC PI_APPROX_25_BITS THEN
2819     MATCH_MP_TAC(REAL_ARITH
2820      `b + e <= a ==> abs(p - a) <= e ==> b <= &1 * p`) THEN
2821     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
2822   REWRITE_TAC[REAL_ABS_INV] THEN
2823   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_INV] THEN
2824   MATCH_MP_TAC REAL_LE_INV2 THEN
2825   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2826   MATCH_MP_TAC(REAL_ARITH
2827    `x <= (&1 - a) * &1 ==> a <= abs(&1 - x)`) THEN
2828   MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_ABS_POS] THEN
2829   SIMP_TAC[REAL_LE_DIV; REAL_POS; REAL_LT_IMP_LE; PI_POS] THEN
2830   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2831   REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
2832   REWRITE_TAC[REAL_POS] THEN
2833   MATCH_MP_TAC REAL_LE_INV2 THEN
2834   REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
2835   MP_TAC PI_APPROX_25_BITS THEN
2836   MATCH_MP_TAC(REAL_ARITH
2837    `b + e <= a ==> abs(p - a) <= e ==> b <= p`) THEN
2838   CONV_TAC REAL_RAT_REDUCE_CONV);;
2839
2840 let TAYLOR_TAN_BOUND = prove
2841  (`!x n k. abs(x) <= inv(&2 pow k)
2842            ==> abs(tan x -
2843                    sum (0,n) (\m. tannumber(m) / &(FACT(m)) * x pow m))
2844                <= &12 * (&2 / &3) pow (n + 1) * inv(&2 pow (k * n))`,
2845   REPEAT STRIP_TAC THEN
2846   MATCH_MP_TAC REAL_LE_TRANS THEN
2847   EXISTS_TAC `&12 * (&2 / &3) pow (n + 1) * abs(x) pow n` THEN
2848   CONJ_TAC THENL
2849    [MATCH_MP_TAC TAYLOR_TAN_BOUND_GENERAL THEN
2850     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
2851     ASM_REWRITE_TAC[] THEN
2852     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2 pow 0)`)) THEN
2853     REWRITE_TAC[REAL_POW2_THM; LE_0];
2854     REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
2855     SIMP_TAC[REAL_LE_MUL; REAL_POW_LE; REAL_LE_DIV; REAL_POS] THEN
2856     REWRITE_TAC[GSYM REAL_POW_POW] THEN
2857     ONCE_REWRITE_TAC[GSYM REAL_POW_INV] THEN
2858     MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]]);;
2859
2860 let TAYLOR_TANX_BOUND = prove
2861  (`!x n k. abs(x) <= inv(&2 pow k) /\ ~(x = &0)
2862            ==> abs(tan x / x -
2863                    sum (0,n) (\m. tannumber(m+1) / &(FACT(m+1)) * x pow m))
2864                <= &12 * (&2 / &3) pow (n + 2) * inv(&2 pow (k * n))`,
2865   REPEAT STRIP_TAC THEN
2866   MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN
2867   ASM_SIMP_TAC[GSYM REAL_ABS_NZ] THEN
2868   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_RDISTRIB] THEN
2869   ASM_SIMP_TAC[REAL_DIV_RMUL] THEN
2870   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
2871   REWRITE_TAC[GSYM SUM_CMUL] THEN
2872   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
2873    [AC REAL_MUL_AC `a * b * c = b * (a * c)`] THEN
2874   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
2875   REWRITE_TAC[ADD1; SPECL [`f:num->real`; `n:num`; `1`] SUM_OFFSET] THEN
2876   REWRITE_TAC[SUM_1] THEN
2877   CONV_TAC(ONCE_DEPTH_CONV TANNUMBER_CONV) THEN
2878   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[real_pow] THEN
2879   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
2880   MATCH_MP_TAC REAL_LE_TRANS THEN
2881   EXISTS_TAC `&12 * (&2 / &3) pow ((n + 1) + 1) * abs(x) pow (n + 1)` THEN
2882   CONJ_TAC THENL
2883    [MATCH_MP_TAC TAYLOR_TAN_BOUND_GENERAL THEN
2884     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
2885     ASM_REWRITE_TAC[] THEN
2886     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2 pow 0)`)) THEN
2887     REWRITE_TAC[REAL_POW2_THM; LE_0]; ALL_TAC] THEN
2888   REWRITE_TAC[ARITH_RULE `(n + 1) + 1 = n + 2`] THEN
2889   REWRITE_TAC[GSYM ADD1; real_pow] THEN
2890   GEN_REWRITE_TAC RAND_CONV [AC REAL_MUL_AC
2891    `(a * b * c) * d = (a * b * d) * c`] THEN
2892   REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
2893   (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 4)
2894     [REAL_LE_MUL; REAL_POW_LE; REAL_ABS_POS; REAL_LE_DIV; REAL_POS] THEN
2895   REWRITE_TAC[GSYM REAL_POW_POW] THEN
2896   ONCE_REWRITE_TAC[GSYM REAL_POW_INV] THEN
2897   MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]);;
2898
2899 let TAYLOR_TANX_SQRT_BOUND = prove
2900  (`!x n k. abs(x) <= inv(&2 pow k) /\ &0 < x
2901            ==> abs(tan (sqrt x) / sqrt(x) -
2902                    sum(0,n) (\m. tannumber(2 * m + 1) / &(FACT(2 * m + 1)) *
2903                                  x pow m))
2904                <= &12 * (&2 / &3) pow (2 * n + 2) *
2905                   inv(&2 pow (k DIV 2 * 2 * n))`,
2906   REPEAT STRIP_TAC THEN
2907   MP_TAC(SPECL [`sqrt x`; `2 * n`; `k DIV 2`] TAYLOR_TANX_BOUND) THEN
2908   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
2909    [ASM_SIMP_TAC[SQRT_POS_LT; REAL_LT_IMP_NZ; DIV_EQ_0; ARITH_EQ; NOT_LT] THEN
2910     SUBGOAL_THEN `&2 pow (k DIV 2) = sqrt(&2 pow (2 * (k DIV 2)))`
2911     SUBST1_TAC THENL
2912      [SIMP_TAC[SQRT_EVEN_POW2; EVEN_MULT; ARITH_EVEN; DIV_MULT; ARITH_EQ];
2913       ALL_TAC] THEN
2914     ASM_SIMP_TAC[GSYM SQRT_INV; REAL_LT_IMP_LE; REAL_POW2_CLAUSES] THEN
2915     ASM_SIMP_TAC[real_abs; SQRT_POS_LT; REAL_LT_IMP_LE] THEN
2916     MATCH_MP_TAC SQRT_MONO_LE THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2917     MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> x <= a`) THEN
2918     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
2919     ASM_REWRITE_TAC[] THEN
2920     MATCH_MP_TAC REAL_LE_INV2 THEN SIMP_TAC[REAL_POW2_CLAUSES] THEN
2921     MATCH_MP_TAC REAL_POW_MONO THEN
2922     REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
2923     MESON_TAC[LE_ADD; DIVISION; NUM_EQ_CONV `2 = 0`; MULT_SYM]; ALL_TAC] THEN
2924   MATCH_MP_TAC EQ_IMP THEN
2925   REWRITE_TAC[GSYM MULT_ASSOC] THEN
2926   AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
2927   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[GSYM SUM_GROUP] THEN
2928   SIMP_TAC[SUM_2; TANNUMBER_EVEN; ARITH_EVEN; EVEN_ADD; EVEN_MULT] THEN
2929   REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_ADD_RID] THEN
2930   ONCE_REWRITE_TAC[MULT_SYM] THEN
2931   ASM_SIMP_TAC[GSYM REAL_POW_POW; SQRT_POW_2; REAL_LT_IMP_LE]);;
2932
2933 let TAYLOR_COT_BOUND_GENERAL = prove
2934  (`!x n. abs(x) <= &1 /\ ~(x = &0)
2935          ==> abs((&1 / x - cot x) -
2936                  sum (0,n) (\m. (tannumber m /
2937                                  ((&2 pow (m+1) - &1) * &(FACT(m)))) *
2938                                 x pow m))
2939              <= &4 * (abs(x) / &3) pow n`,
2940   REPEAT STRIP_TAC THEN
2941   MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN
2942   ASM_SIMP_TAC[GSYM REAL_ABS_NZ] THEN
2943   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_LDISTRIB] THEN
2944   ASM_SIMP_TAC[REAL_DIV_LMUL] THEN REWRITE_TAC[GSYM SUM_CMUL] THEN
2945   REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN
2946   ONCE_REWRITE_TAC[AC REAL_MUL_AC `x * a * y = a * x * y`] THEN
2947   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN REWRITE_TAC[ADD1] THEN
2948   REWRITE_TAC[SUM_1; REAL_MUL_LZERO; REAL_SUB_RZERO; real_pow] THEN
2949   CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2950   REWRITE_TAC[REAL_SUB_RZERO] THEN
2951   SUBGOAL_THEN `abs(x) < pi` MP_TAC THENL
2952    [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&1` THEN
2953     ASM_REWRITE_TAC[] THEN
2954     MP_TAC PI_APPROX_25_BITS THEN
2955     MATCH_MP_TAC(REAL_ARITH
2956      `b + e < a ==> abs(p - a) <= e ==> b < p`) THEN
2957     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
2958   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_ABS_NZ]) THEN
2959   REWRITE_TAC[IMP_IMP] THEN
2960   DISCH_THEN(MP_TAC o MATCH_MP TAYLOR_X_COT_CONVERGES) THEN
2961   DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN
2962   DISCH_THEN(ASSUME_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
2963   DISCH_THEN(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN
2964   DISCH_THEN(MP_TAC o SPEC `1` o MATCH_MP SER_OFFSET) THEN
2965   ASM_REWRITE_TAC[SUM_1; ADD_EQ_0; ARITH_EQ] THEN
2966   REWRITE_TAC[real_pow; REAL_MUL_LID] THEN
2967   DISCH_THEN(MP_TAC o MATCH_MP SER_NEG) THEN
2968   REWRITE_TAC[REAL_NEG_SUB] THEN
2969   ONCE_REWRITE_TAC[GSYM REAL_MUL_LNEG] THEN
2970   REWRITE_TAC[real_div] THEN
2971   ONCE_REWRITE_TAC[GSYM REAL_MUL_RNEG] THEN
2972   REWRITE_TAC[GSYM REAL_INV_NEG] THEN
2973   REWRITE_TAC[GSYM real_div] THEN
2974   ONCE_REWRITE_TAC[GSYM REAL_MUL_LNEG] THEN
2975   REWRITE_TAC[REAL_NEG_SUB] THEN REWRITE_TAC[ADD_SUB] THEN
2976   DISCH_THEN(fun th ->
2977     ASSUME_TAC th THEN MP_TAC(MATCH_MP SUM_SUMMABLE th)) THEN
2978   DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP SER_OFFSET) THEN
2979   FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
2980   REWRITE_TAC[sums] THEN DISCH_THEN(MP_TAC o MATCH_MP SEQ_ABS_IMP) THEN
2981   REWRITE_TAC[] THEN DISCH_TAC THEN
2982   MATCH_MP_TAC SEQ_LE_CONST THEN
2983   FIRST_ASSUM(fun th ->
2984    EXISTS_TAC(lhand(concl th)) THEN EXISTS_TAC `0` THEN
2985    CONJ_TAC THENL [ALL_TAC; ACCEPT_TAC th]) THEN
2986   X_GEN_TAC `m:num` THEN DISCH_THEN(K ALL_TAC) THEN
2987   REWRITE_TAC[] THEN
2988   W(MP_TAC o PART_MATCH lhand SUM_ABS_LE o lhand o snd) THEN
2989   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
2990   REWRITE_TAC[GSYM ADD_ASSOC] THEN
2991   MATCH_MP_TAC REAL_LE_TRANS THEN
2992   EXISTS_TAC
2993    `sum(0,m) (\r. &4 *
2994                   (&2 / pi) pow (r + n + 1) / (&2 pow (r + n + 1) - &1) *
2995                   abs(x pow (r + n + 1)))` THEN
2996   REWRITE_TAC[] THEN CONJ_TAC THENL
2997    [MATCH_MP_TAC SUM_LE THEN
2998     X_GEN_TAC `r:num` THEN REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN
2999     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_DIV; REAL_ABS_NUM] THEN
3000     REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
3001     REWRITE_TAC[REAL_ABS_POS] THEN
3002     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_ABS_MUL] THEN
3003     REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN
3004     GEN_REWRITE_TAC RAND_CONV [AC REAL_MUL_AC `a * b * c = (c * a) * b`] THEN
3005     REWRITE_TAC[REAL_MUL_ASSOC; real_abs; REAL_SUB_LE] THEN
3006     REWRITE_TAC[REAL_POW2_CLAUSES] THEN REWRITE_TAC[GSYM real_abs] THEN
3007     MATCH_MP_TAC REAL_LE_RMUL THEN
3008     REWRITE_TAC[REAL_LE_INV_EQ; REAL_SUB_LE; REAL_POW2_CLAUSES] THEN
3009     SIMP_TAC[GSYM real_div; REAL_ABS_DIV; REAL_ABS_NUM;
3010              REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; FACT_LT] THEN
3011     MP_TAC(SPEC `r + n:num` TANNUMBER_BOUND) THEN
3012     REWRITE_TAC[REAL_MUL_AC; GSYM ADD_ASSOC]; ALL_TAC] THEN
3013   REWRITE_TAC[real_div] THEN
3014   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
3015    [AC REAL_MUL_AC `a * (b * c) * d = a * c * (b * d)`] THEN
3016   REWRITE_TAC[REAL_ABS_POW; GSYM REAL_POW_MUL] THEN
3017   MATCH_MP_TAC REAL_LE_TRANS THEN
3018   EXISTS_TAC
3019    `sum(0,m) (\r. &8 * inv(&2 pow (r + n + 1)) *
3020                        ((&2 * inv pi) * abs x) pow (r + n + 1))` THEN
3021   CONJ_TAC THENL
3022    [MATCH_MP_TAC SUM_LE THEN
3023     X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
3024     REWRITE_TAC[REAL_ARITH `&4 * x <= &8 * y <=> x <= &2 * y`] THEN
3025     REWRITE_TAC[REAL_MUL_ASSOC] THEN
3026     MATCH_MP_TAC REAL_LE_RMUL THEN
3027     (CONV_TAC o GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV (basic_ss []) 4)
3028       [REAL_POW_LE; REAL_LE_MUL; REAL_ABS_POS; REAL_POS;
3029        REAL_LT_IMP_LE; PI_POS; REAL_LE_INV_EQ] THEN
3030     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_INV_INV] THEN
3031     REWRITE_TAC[GSYM REAL_INV_MUL] THEN
3032     MATCH_MP_TAC REAL_LE_INV2 THEN
3033     SIMP_TAC[REAL_LT_MUL; REAL_LT_INV_EQ; REAL_OF_NUM_LT;
3034              ARITH; REAL_POW_LT] THEN
3035     REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; real_pow] THEN
3036     REWRITE_TAC[REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
3037     REWRITE_TAC[REAL_ARITH `&1 * x <= &2 * x - &1 <=> &1 <= x`] THEN
3038     REWRITE_TAC[REAL_POW2_CLAUSES]; ALL_TAC] THEN
3039   REWRITE_TAC[GSYM REAL_POW_INV; GSYM REAL_POW_MUL] THEN
3040   REWRITE_TAC[REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
3041   REWRITE_TAC[REAL_ARITH `(&1 * x) * y = y * x`] THEN
3042   REWRITE_TAC[GSYM real_div] THEN
3043   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_POW_ADD] THEN
3044   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
3045    [AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN
3046   REWRITE_TAC[SUM_CMUL] THEN
3047   SUBGOAL_THEN
3048    `(&4 * abs x) * (abs x * &1 / &3) pow n =
3049     &12 * (abs x / &3) pow (n + 1)`
3050   SUBST1_TAC THENL
3051    [REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN
3052     REWRITE_TAC[real_div; REAL_MUL_LID] THEN
3053     REWRITE_TAC[REAL_POW_MUL; GSYM REAL_MUL_ASSOC] THEN
3054     GEN_REWRITE_TAC RAND_CONV
3055      [AC REAL_MUL_AC `a * b * c * d * e = (a * e) * d * b * c`] THEN
3056     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
3057   SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&8 * &3 / &2`)) THEN
3058   GEN_REWRITE_TAC RAND_CONV [AC REAL_MUL_AC
3059    `(a * b) * c = (a * c) * b`] THEN
3060   MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> x <= a`) THEN
3061   ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
3062   REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL
3063    [REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN
3064     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
3065     REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
3066     REWRITE_TAC[REAL_ABS_POS] THEN
3067     REWRITE_TAC[real_div; REAL_ABS_MUL; REAL_ABS_ABS] THEN
3068     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
3069     REWRITE_TAC[REAL_ABS_INV] THEN
3070     MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
3071     MP_TAC PI_APPROX_25_BITS THEN
3072     MATCH_MP_TAC(REAL_ARITH
3073      `b + e <= a ==> abs(p - a) <= e ==> b <= abs p`) THEN
3074     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
3075   SUBGOAL_THEN `abs(x) / pi < &1 / &3` ASSUME_TAC THENL
3076    [MATCH_MP_TAC REAL_LET_TRANS THEN
3077     EXISTS_TAC `&1 / pi` THEN
3078     ASM_SIMP_TAC[REAL_LE_DIV2_EQ; PI_POS] THEN
3079     REWRITE_TAC[real_div; REAL_MUL_LID] THEN
3080     MATCH_MP_TAC REAL_LT_INV2 THEN
3081     CONV_TAC REAL_RAT_REDUCE_CONV THEN
3082     MP_TAC PI_APPROX_25_BITS THEN
3083     MATCH_MP_TAC(REAL_ARITH
3084      `b + e < a ==> abs(p - a) <= e ==> b < p`) THEN
3085     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
3086   SUBGOAL_THEN `~(abs(x) / pi = &1)` ASSUME_TAC THENL
3087    [UNDISCH_TAC `abs x / pi < &1 / &3` THEN
3088     ONCE_REWRITE_TAC[TAUT `a ==> ~b <=> b ==> ~a`] THEN
3089     SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
3090   ASM_SIMP_TAC[GP_FINITE] THEN
3091   ONCE_REWRITE_TAC[REAL_ARITH `x - &1 = --(&1 - x)`] THEN
3092   REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
3093   REWRITE_TAC[REAL_NEG_NEG] THEN REWRITE_TAC[REAL_ABS_MUL] THEN
3094   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
3095   MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL
3096    [MATCH_MP_TAC(REAL_ARITH
3097      `&0 <= x /\ x <= &1 ==> abs(&1 - x) <= &1`) THEN
3098     SIMP_TAC[REAL_POW_LE; REAL_LE_MUL; REAL_LE_INV_EQ; REAL_ABS_POS;
3099              REAL_LT_IMP_LE; PI_POS] THEN
3100     MATCH_MP_TAC REAL_POW_1_LE THEN
3101     SIMP_TAC[REAL_LE_MUL; REAL_ABS_POS; REAL_LE_INV_EQ;
3102              REAL_LT_IMP_LE; PI_POS] THEN
3103     SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ; PI_POS] THEN
3104     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN
3105     ASM_REWRITE_TAC[] THEN
3106     MP_TAC PI_APPROX_25_BITS THEN
3107     MATCH_MP_TAC(REAL_ARITH
3108      `b + e <= a ==> abs(p - a) <= e ==> b <= &1 * p`) THEN
3109     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
3110   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_INV] THEN
3111   REWRITE_TAC[REAL_ABS_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
3112   CONV_TAC REAL_RAT_REDUCE_CONV THEN
3113   REWRITE_TAC[GSYM real_div] THEN
3114   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
3115      `x < a ==> b <= &1 - a ==> b <= abs(&1 - x)`)) THEN
3116   CONV_TAC REAL_RAT_REDUCE_CONV);;
3117
3118 let TAYLOR_COT_BOUND = prove
3119  (`!x n k. abs(x) <= inv(&2 pow k) /\ ~(x = &0)
3120            ==> abs((&1 / x - cot x) -
3121                    sum (0,n) (\m. (tannumber m /
3122                                    ((&2 pow (m+1) - &1) * &(FACT(m)))) *
3123                                   x pow m))
3124                <= &4 / &3 pow n * inv(&2 pow (k * n))`,
3125   REPEAT STRIP_TAC THEN
3126   SUBGOAL_THEN `abs(x) <= &1 /\ ~(x = &0)` MP_TAC THENL
3127    [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
3128     EXISTS_TAC `inv(&2 pow k)` THEN ASM_REWRITE_TAC[] THEN
3129     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2 pow 0)`)) THEN
3130     REWRITE_TAC[REAL_POW2_THM; LE_0]; ALL_TAC] THEN
3131   DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP TAYLOR_COT_BOUND_GENERAL) THEN
3132   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
3133   REWRITE_TAC[real_div; REAL_POW_MUL; GSYM REAL_MUL_ASSOC] THEN
3134   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
3135   REWRITE_TAC[GSYM REAL_POW_INV; GSYM REAL_POW_POW] THEN
3136   REWRITE_TAC[GSYM REAL_POW_MUL] THEN
3137   MATCH_MP_TAC REAL_POW_LE2 THEN
3138   SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_POS; REAL_ABS_POS] THEN
3139   GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
3140   MATCH_MP_TAC REAL_LE_LMUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
3141   ASM_REWRITE_TAC[real_div; REAL_MUL_LID; REAL_POW_INV]);;
3142
3143 let TAYLOR_COTX_BOUND = prove
3144  (`!x n k. abs(x) <= inv(&2 pow k) /\ ~(x = &0)
3145            ==> abs((&1 / x - cot x) / x -
3146                    sum (0,n) (\m. (tannumber(m+1) /
3147                                    ((&2 pow (m+2) - &1) * &(FACT(m+1)))) *
3148                                   x pow m))
3149                <= (&4 / &3) / &3 pow n * inv(&2 pow (k * n))`,
3150   REPEAT STRIP_TAC THEN
3151   MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN
3152   ASM_SIMP_TAC[GSYM REAL_ABS_NZ] THEN
3153   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_RDISTRIB] THEN
3154   ASM_SIMP_TAC[REAL_DIV_RMUL] THEN
3155   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
3156   REWRITE_TAC[GSYM SUM_CMUL] THEN
3157   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
3158    [AC REAL_MUL_AC `a * b * c = b * (a * c)`] THEN
3159   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
3160   REWRITE_TAC[ARITH_RULE `n + 2 = (n + 1) + 1`] THEN
3161   REWRITE_TAC[ADD1; SPECL [`f:num->real`; `n:num`; `1`] SUM_OFFSET] THEN
3162   REWRITE_TAC[SUM_1] THEN
3163   CONV_TAC(ONCE_DEPTH_CONV TANNUMBER_CONV) THEN
3164   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[real_pow] THEN
3165   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
3166   REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
3167   SUBGOAL_THEN `abs(x) <= &1 /\ ~(x = &0)` MP_TAC THENL
3168    [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
3169     EXISTS_TAC `inv(&2 pow k)` THEN ASM_REWRITE_TAC[] THEN
3170     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2 pow 0)`)) THEN
3171     REWRITE_TAC[REAL_POW2_THM; LE_0]; ALL_TAC] THEN
3172   DISCH_THEN(MP_TAC o SPEC `n + 1` o MATCH_MP TAYLOR_COT_BOUND_GENERAL) THEN
3173   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
3174   REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN
3175   REWRITE_TAC[real_div] THEN
3176   ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d = ((a * d) * b) * c`] THEN
3177   MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
3178   REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_POW_MUL; GSYM REAL_INV_MUL] THEN
3179   REWRITE_TAC[GSYM REAL_POW_POW; GSYM REAL_POW_MUL] THEN
3180   REWRITE_TAC[REAL_INV_MUL; REAL_MUL_ASSOC] THEN
3181   CONV_TAC REAL_RAT_REDUCE_CONV THEN
3182   MATCH_MP_TAC REAL_LE_LMUL THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
3183   REWRITE_TAC[GSYM REAL_POW_INV] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
3184   SIMP_TAC[REAL_LE_MUL; REAL_ABS_POS; REAL_LE_DIV; REAL_POS] THEN
3185   REWRITE_TAC[REAL_INV_MUL] THEN
3186   GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
3187   CONV_TAC REAL_RAT_REDUCE_CONV THEN
3188   MATCH_MP_TAC REAL_LE_RMUL THEN ASM_REWRITE_TAC[] THEN
3189   CONV_TAC REAL_RAT_REDUCE_CONV);;
3190
3191 let TAYLOR_COTXX_BOUND = prove
3192  (`!x n k. abs(x) <= inv(&2 pow k) /\ ~(x = &0)
3193            ==> abs((&1 - x * cot(x)) -
3194                    sum(0,n) (\m. (tannumber (m-1) /
3195                                   ((&2 pow m - &1) * &(FACT(m-1)))) *
3196                                  x pow m))
3197                <= &12 / &3 pow n * inv(&2 pow (k * n))`,
3198   REPEAT STRIP_TAC THEN
3199   MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `abs(inv x)` THEN
3200   ASM_SIMP_TAC[GSYM REAL_ABS_NZ; REAL_INV_EQ_0] THEN
3201   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_RDISTRIB] THEN
3202   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV o RAND_CONV)
3203    [AC REAL_MUL_AC `(a * b) * c = b * a * c`] THEN
3204   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN
3205   REWRITE_TAC[GSYM real_div] THEN
3206   REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
3207   SUBGOAL_THEN `abs(x) <= &1 /\ ~(x = &0)` MP_TAC THENL
3208    [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
3209     EXISTS_TAC `inv(&2 pow k)` THEN ASM_REWRITE_TAC[] THEN
3210     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2 pow 0)`)) THEN
3211     REWRITE_TAC[REAL_POW2_THM; LE_0]; ALL_TAC] THEN
3212   DISCH_THEN(MP_TAC o SPEC `n - 1` o MATCH_MP TAYLOR_COT_BOUND_GENERAL) THEN
3213   ASM_CASES_TAC `n = 0` THENL
3214    [ASM_REWRITE_TAC[] THEN CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[sum] THEN
3215     REWRITE_TAC[real_pow; real_div; REAL_MUL_LZERO; REAL_SUB_RZERO] THEN
3216     REWRITE_TAC[GSYM real_div] THEN
3217     MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN
3218     REWRITE_TAC[real_div; REAL_MUL_ASSOC; MULT_CLAUSES; REAL_INV_MUL] THEN
3219     CONV_TAC REAL_RAT_REDUCE_CONV THEN
3220     ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
3221     SIMP_TAC[GSYM REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
3222     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_DIV] THEN
3223     REWRITE_TAC[REAL_ABS_INV] THEN
3224     MATCH_MP_TAC REAL_LE_INV2 THEN
3225     ASM_REWRITE_TAC[GSYM REAL_ABS_NZ] THEN
3226     MATCH_MP_TAC REAL_LE_TRANS THEN
3227     EXISTS_TAC `inv(&2 pow k)` THEN ASM_REWRITE_TAC[] THEN
3228     MATCH_MP_TAC REAL_LE_TRANS THEN
3229     EXISTS_TAC `inv(&2 pow 0)` THEN
3230     REWRITE_TAC[REAL_POW2_THM; LE_0] THEN
3231     CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
3232   SUBGOAL_THEN `n = (n - 1) + 1` MP_TAC THENL
3233    [UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
3234   DISCH_THEN(fun th -> GEN_REWRITE_TAC
3235    (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
3236   REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_OFFSET)] THEN
3237   REWRITE_TAC[SUB_0; ADD_SUB; SUM_1] THEN
3238   SIMP_TAC[TANNUMBER_EVEN; EVEN] THEN
3239   REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_ADD_RID] THEN
3240   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o RAND_CONV)
3241         [REAL_MUL_SYM] THEN
3242   REWRITE_TAC[GSYM SUM_CMUL] THEN
3243   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)
3244         [REAL_MUL_SYM] THEN
3245   REWRITE_TAC[GSYM real_div] THEN
3246   MATCH_MP_TAC(REAL_ARITH
3247    `(s1 = s2) /\ a <= b ==> s1 <= a ==> s2 <= b`) THEN
3248   CONJ_TAC THENL
3249    [AP_TERM_TAC THEN
3250     REWRITE_TAC[real_div; REAL_MUL_LID; REAL_MUL_RID] THEN AP_TERM_TAC THEN
3251     AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN
3252     REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; GSYM REAL_MUL_ASSOC] THEN
3253     REPEAT AP_TERM_TAC THEN
3254     ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID]; ALL_TAC] THEN
3255   ONCE_REWRITE_TAC[ADD_SYM] THEN
3256   REWRITE_TAC[REAL_POW_ADD; REAL_INV_MUL; REAL_MUL_ASSOC; real_div] THEN
3257   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
3258   MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
3259   REWRITE_TAC[real_div; REAL_MUL_LID] THEN
3260   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
3261   REWRITE_TAC[REAL_POW_MUL; REAL_POW_INV] THEN
3262   MATCH_MP_TAC REAL_LE_LMUL THEN
3263   SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
3264   REWRITE_TAC[REAL_ABS_INV; GSYM real_div] THEN
3265   ASM_SIMP_TAC[REAL_LE_RDIV_EQ; GSYM REAL_ABS_NZ] THEN
3266   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
3267   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
3268   REWRITE_TAC[GSYM REAL_POW_POW] THEN
3269   REWRITE_TAC[GSYM REAL_POW_INV] THEN
3270   REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD1] THEN
3271   MATCH_MP_TAC REAL_POW_LE2 THEN
3272   ASM_REWRITE_TAC[REAL_ABS_POS; REAL_POW_INV]);;
3273
3274 let TAYLOR_COTXX_SQRT_BOUND = prove
3275  (`!x n k. abs(x) <= inv(&2 pow k) /\ &0 < x
3276            ==> abs((&1 - sqrt(x) * cot(sqrt(x))) -
3277                    sum(0,n) (\m. (tannumber (2*m-1) /
3278                                   ((&2 pow (2*m) - &1) * &(FACT(2*m-1)))) *
3279                                  x pow m))
3280                <= &12 / &3 pow (2 * n) * inv(&2 pow (k DIV 2 * 2 * n))`,
3281   REPEAT STRIP_TAC THEN
3282   MP_TAC(SPECL [`sqrt x`; `2 * n`; `k DIV 2`] TAYLOR_COTXX_BOUND) THEN
3283   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
3284    [ASM_SIMP_TAC[SQRT_POS_LT; REAL_LT_IMP_NZ; DIV_EQ_0; ARITH_EQ; NOT_LT] THEN
3285     SUBGOAL_THEN `&2 pow (k DIV 2) = sqrt(&2 pow (2 * (k DIV 2)))`
3286     SUBST1_TAC THENL
3287      [SIMP_TAC[SQRT_EVEN_POW2; EVEN_MULT; ARITH_EVEN; DIV_MULT; ARITH_EQ];
3288       ALL_TAC] THEN
3289     ASM_SIMP_TAC[GSYM SQRT_INV; REAL_LT_IMP_LE; REAL_POW2_CLAUSES] THEN
3290     ASM_SIMP_TAC[real_abs; SQRT_POS_LT; REAL_LT_IMP_LE] THEN
3291     MATCH_MP_TAC SQRT_MONO_LE THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
3292     MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> x <= a`) THEN
3293     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
3294     ASM_REWRITE_TAC[] THEN
3295     MATCH_MP_TAC REAL_LE_INV2 THEN SIMP_TAC[REAL_POW2_CLAUSES] THEN
3296     MATCH_MP_TAC REAL_POW_MONO THEN
3297     REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
3298     MESON_TAC[LE_ADD; DIVISION; NUM_EQ_CONV `2 = 0`; MULT_SYM]; ALL_TAC] THEN
3299   MATCH_MP_TAC EQ_IMP THEN
3300   REWRITE_TAC[GSYM MULT_ASSOC] THEN
3301   AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
3302   ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[GSYM SUM_GROUP] THEN
3303   SUBGOAL_THEN `!n. EVEN(((n * 2) + 1) - 1)` ASSUME_TAC THENL
3304    [INDUCT_TAC THEN
3305     REWRITE_TAC[ADD_CLAUSES; SUC_SUB1; SUB_0;
3306                 MULT_CLAUSES; SUB_REFL; ADD_SUB] THEN
3307     REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH]; ALL_TAC] THEN
3308   ASM_SIMP_TAC[SUM_2; TANNUMBER_EVEN; ARITH_EVEN; EVEN_ADD; EVEN_MULT] THEN
3309   REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_ADD_RID] THEN
3310   ONCE_REWRITE_TAC[MULT_SYM] THEN
3311   ASM_SIMP_TAC[GSYM REAL_POW_POW; SQRT_POW_2; REAL_LT_IMP_LE]);;