(* ========================================================================= *)
(* Derivation of Machin's formula and other similar ones.                    *)
(* ========================================================================= *)

needs "Library/transc.ml";;

let REAL_LE_1_POW2 = prove
 (`!n. &1 <= &2 pow n`,
  REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> 0 < n`;
              EXP_LT_0; ARITH]);;

let REAL_LT_1_POW2 = prove
 (`!n. &1 < &2 pow n <=> ~(n = 0)`,
  GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN
  SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&2 pow 0`)) THEN
  MATCH_MP_TAC REAL_POW_MONO_LT THEN
  REWRITE_TAC[REAL_OF_NUM_LT] THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;

let REAL_POW2_CLAUSES = prove
 (`(!n. &0 <= &2 pow n) /\
   (!n. &0 < &2 pow n) /\
   (!n. &0 <= inv(&2 pow n)) /\
   (!n. &0 < inv(&2 pow n)) /\
   (!n. inv(&2 pow n) <= &1) /\
   (!n. &1 - inv(&2 pow n) <= &1) /\
   (!n. &1 <= &2 pow n) /\
   (!n. &1 < &2 pow n <=> ~(n = 0)) /\
   (!n. &0 <= &1 - inv(&2 pow n)) /\
   (!n. &0 <= &2 pow n - &1) /\
   (!n. &0 < &1 - inv(&2 pow n) <=> ~(n = 0))`,
  SIMP_TAC[REAL_LE_1_POW2; REAL_LT_1_POW2; REAL_SUB_LE; REAL_SUB_LT;
           REAL_INV_LE_1] THEN
  SIMP_TAC[REAL_LE_INV_EQ; REAL_LT_INV_EQ; REAL_POW_LT; REAL_POW_LE;
           REAL_OF_NUM_LE; REAL_OF_NUM_LT; ARITH;
           REAL_ARITH `&1 - x <= &1 <=> &0 <= x`] THEN
  GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN
  MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv(&2 pow 1)` THEN
  ASM_SIMP_TAC[REAL_LE_INV2; REAL_POW_MONO; REAL_POW_LT; REAL_OF_NUM_LT; ARITH;
               REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV);;

let REAL_POW2_THM = prove
 (`&0 < &2 pow n /\
   &1 <= &2 pow n /\
   (&1 < &2 pow n <=> ~(n = 0)) /\
   (&2 pow m <= &2 pow n <=> m <= n) /\
   (&2 pow m < &2 pow n <=> m < n) /\
   (inv(&2 pow m) <= inv(&2 pow n) <=> n <= m) /\
   (inv(&2 pow m) < inv(&2 pow n) <=> n < m)`,
  REWRITE_TAC[REAL_POW2_CLAUSES] THEN
  SUBGOAL_THEN `!m n. &2 pow m <= &2 pow n <=> m <= n` ASSUME_TAC THENL
   [REPEAT GEN_TAC THEN EQ_TAC THEN
    SIMP_TAC[REAL_POW_MONO; REAL_OF_NUM_LE; ARITH] THEN
    CONV_TAC CONTRAPOS_CONV THEN
    SIMP_TAC[REAL_NOT_LE; REAL_NOT_LT; REAL_POW_MONO_LT; REAL_OF_NUM_LT;
             NOT_LE; ARITH]; ALL_TAC] THEN
  ASM_REWRITE_TAC[GSYM REAL_NOT_LE] THEN REWRITE_TAC[GSYM NOT_LE] THEN
  SUBGOAL_THEN `!m n. inv(&2 pow m) <= inv(&2 pow n) <=> &2 pow n <= &2 pow m`
   (fun th -> ASM_REWRITE_TAC[th]) THEN
  REPEAT GEN_TAC THEN EQ_TAC THEN
  SIMP_TAC[REAL_LE_INV2; REAL_POW2_CLAUSES] THEN
  CONV_TAC CONTRAPOS_CONV THEN
  SIMP_TAC[REAL_NOT_LE; REAL_LT_INV2; REAL_POW2_CLAUSES]);;

(* ------------------------------------------------------------------------- *)
(* Compound errors given bounds in assumptions.                              *)
(* ------------------------------------------------------------------------- *)

let BOUND_SUMPROD_RULE =
  let pth_add = REAL_ARITH
    `abs(x1) <= b1 /\ abs(x2) <= b2 ==> abs(x1 + x2) <= b1 + b2`
  and pth_sub = REAL_ARITH
    `abs(x1) <= b1 /\ abs(x2) <= b2 ==> abs(x1 - x2) <= b1 + b2`
  and pth_mul = prove
   (`abs(x1) <= b1 /\ abs(x2) <= b2 ==> abs(x1 * x2) <= b1 * b2`,
    REWRITE_TAC[REAL_ABS_MUL] THEN
    SIMP_TAC[REAL_LE_MUL2; REAL_ABS_POS])
  and pth_neg = REAL_ARITH
    `abs(x1) <= b1 ==> abs(--x1) <= b1`
  and pth_pow = prove
   (`abs(x) <= b1 ==> abs(x pow n) <= b1 pow n`,
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ABS_POW] THEN
    MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[REAL_ABS_POS])
  and pth_abs = REAL_ARITH `abs(x) <= b ==> abs(abs(x)) <= b`
  and pth_triv = REAL_ARITH `abs(x) <= abs(x)`
  and n_tm = `n:num` in
  let rec BOUND_SUMPROD_RULE (asl,w) =
    let tm = rator w in
    try tryfind (fun (_,th) -> if rator(concl th) = tm then th
                               else fail()) asl
    with Failure _ -> try
        let pth,th = tryfind
          (fun pth -> pth,PART_MATCH (rator o rand) pth tm)
          [pth_neg; pth_abs] in
        let th1 = BOUND_SUMPROD_RULE (asl,lhand(concl th)) in
        MATCH_MP pth th1
    with Failure _ -> try
        let pth = INST [funpow 3 rand tm,n_tm] pth_pow in
        let th = PART_MATCH (rator o rand) pth tm in
        let th1 = BOUND_SUMPROD_RULE (asl,lhand(concl th)) in
        MATCH_MP (INST [funpow 3 rand tm,n_tm] pth_pow) th1
    with Failure _ -> try
        let pth,th = tryfind
          (fun pth -> pth,PART_MATCH (rator o rand) pth tm)
          [pth_add; pth_sub; pth_mul] in
        let trm = lhand(concl th) in
        let th1 = BOUND_SUMPROD_RULE (asl,lhand trm)
        and th2 = BOUND_SUMPROD_RULE (asl,rand trm) in
        MATCH_MP pth (CONJ th1 th2)
    with Failure _ ->
        PART_MATCH rator pth_triv tm in
  BOUND_SUMPROD_RULE;;

let BOUND_SUMPROD_TAC =
  let tac =
    let pth =
      REAL_ARITH `x <= a ==> (!b. a <= b ==> x <= b) /\
                             (!b. a < b ==> x < b)` in
    fun th ->
      let th1,th2 = CONJ_PAIR(MATCH_MP pth th) in
      MATCH_MP_TAC th1 ORELSE MATCH_MP_TAC th2
  and le_tm = `(<=):real->real->bool` in
  fun (asl,w as gl) ->
    let l,r = dest_comb w in
    let gv = genvar(type_of r) in
    let tm = mk_comb(mk_comb(le_tm,rand l),gv) in
    let th = BOUND_SUMPROD_RULE(asl,tm) in
    tac th gl;;

(* ------------------------------------------------------------------------- *)
(* Power series for atn.                                                     *)
(* ------------------------------------------------------------------------- *)

let REAL_ATN_POWSER_SUMMABLE = prove
 (`!x. abs(x) < &1
       ==> summable (\n. (if EVEN n then &0
                          else --(&1) pow ((n - 1) DIV 2) / &n) * x pow n)`,
  REPEAT STRIP_TAC THEN MATCH_MP_TAC SER_COMPAR THEN
  EXISTS_TAC `\n. abs(x) pow n` THEN CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
    COND_CASES_TAC THEN
    SIMP_TAC[REAL_POW_LE; REAL_MUL_LZERO; REAL_ABS_POS; REAL_ABS_NUM] THEN
    REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_DIV; REAL_ABS_NEG; REAL_ABS_POW] THEN
    REWRITE_TAC[REAL_ABS_NUM; REAL_POW_ONE; REAL_MUL_LID] THEN
    REWRITE_TAC[real_div; REAL_MUL_LID] THEN
    ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
    MATCH_MP_TAC REAL_LE_LDIV THEN
    CONJ_TAC THENL [ASM_MESON_TAC[REAL_OF_NUM_LT; EVEN; LT_NZ]; ALL_TAC] THEN
    GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
    MATCH_MP_TAC REAL_LE_LMUL THEN
    SIMP_TAC[REAL_POW_LE; REAL_ABS_POS] THEN
    ASM_MESON_TAC[REAL_OF_NUM_LE; EVEN; ARITH_RULE `1 <= n <=> ~(n = 0)`];
    ALL_TAC] THEN
  REWRITE_TAC[summable] THEN EXISTS_TAC `inv(&1 - abs x)` THEN
  MATCH_MP_TAC GP THEN ASM_REWRITE_TAC[REAL_ABS_ABS]);;

let REAL_ATN_POWSER_DIFFS_SUMMABLE = prove
 (`!x. abs(x) < &1
       ==> summable (\n. diffs (\n. (if EVEN n then &0
                                     else --(&1) pow ((n - 1) DIV 2) / &n)) n *
                         x pow n)`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[diffs] THEN
  MATCH_MP_TAC SER_COMPAR THEN
  EXISTS_TAC `\n. abs(x) pow n` THEN CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN REWRITE_TAC[] THEN
    COND_CASES_TAC THEN
    SIMP_TAC[REAL_POW_LE; REAL_MUL_LZERO; REAL_MUL_RZERO;
             REAL_ABS_POS; REAL_ABS_NUM] THEN
    SIMP_TAC[REAL_MUL_ASSOC; REAL_DIV_LMUL; REAL_OF_NUM_EQ; NOT_SUC] THEN
    REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_DIV; REAL_ABS_NEG; REAL_ABS_POW] THEN
    REWRITE_TAC[REAL_ABS_NUM; REAL_POW_ONE; REAL_MUL_LID; REAL_LE_REFL];
    ALL_TAC] THEN
  REWRITE_TAC[summable] THEN EXISTS_TAC `inv(&1 - abs x)` THEN
  MATCH_MP_TAC GP THEN ASM_REWRITE_TAC[REAL_ABS_ABS]);;

let REAL_ATN_POWSER_DIFFS_SUM = prove
 (`!x. abs(x) < &1
       ==> (\n. diffs (\n. (if EVEN n then &0
                            else --(&1) pow ((n - 1) DIV 2) / &n)) n * x pow n)
           sums (inv(&1 + x pow 2))`,
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP REAL_ATN_POWSER_DIFFS_SUMMABLE) THEN
  DISCH_THEN(fun th -> MP_TAC(MATCH_MP SUMMABLE_SUM th) THEN
                       MP_TAC(MATCH_MP SER_PAIR th)) THEN
  SUBGOAL_THEN
   `(\n. sum (2 * n,2) (\n. diffs
      (\n. (if EVEN n then &0
            else --(&1) pow ((n - 1) DIV 2) / &n)) n * x pow n)) =
    (\n. --(x pow 2) pow n)`
  SUBST1_TAC THENL
   [ABS_TAC THEN
    CONV_TAC(LAND_CONV(LAND_CONV(RAND_CONV(TOP_DEPTH_CONV num_CONV)))) THEN
    REWRITE_TAC[sum; diffs; ADD_CLAUSES; EVEN_MULT; ARITH_EVEN; EVEN] THEN
    REWRITE_TAC[REAL_ADD_LID; REAL_ADD_RID; REAL_MUL_LZERO;
                REAL_MUL_RZERO] THEN
    SIMP_TAC[ARITH_RULE `SUC n - 1 = n`; DIV_MULT; ARITH_EQ] THEN
    SIMP_TAC[REAL_MUL_ASSOC; REAL_DIV_LMUL; REAL_OF_NUM_EQ; NOT_SUC] THEN
    ONCE_REWRITE_TAC[GSYM REAL_POW_POW] THEN
    REWRITE_TAC[GSYM REAL_POW_MUL] THEN
    REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_LID]; ALL_TAC] THEN
  SUBGOAL_THEN `(\n. --(x pow 2) pow n) sums inv (&1 + x pow 2)` MP_TAC THENL
   [ONCE_REWRITE_TAC[REAL_ARITH `&1 + x = &1 - (--x)`] THEN
    MATCH_MP_TAC GP THEN
    REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW] THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
    ASM_SIMP_TAC[REAL_POW_2; REAL_LT_MUL2; REAL_ABS_POS]; ALL_TAC] THEN
  MESON_TAC[SUM_UNIQ]);;

let REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE = prove
 (`!x. abs(x) < &1
       ==> summable
             (\n. diffs (diffs
                 (\n. (if EVEN n then &0
                       else --(&1) pow ((n - 1) DIV 2) / &n))) n * x pow n)`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[diffs] THEN
  MATCH_MP_TAC SER_COMPAR THEN
  EXISTS_TAC `\n. &(SUC n) * abs(x) pow n` THEN CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN
    REWRITE_TAC[REAL_ABS_NUM; REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN
    MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
    COND_CASES_TAC THEN
    SIMP_TAC[REAL_POW_LE; REAL_MUL_LZERO; REAL_MUL_RZERO;
             REAL_ABS_POS; REAL_ABS_NUM] THEN
    REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_NUM; REAL_MUL_ASSOC] THEN
    SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; NOT_SUC] THEN
    REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NEG; REAL_POW_ONE; REAL_MUL_LID;
                REAL_ABS_NUM; REAL_LE_REFL]; ALL_TAC] THEN
  MATCH_MP_TAC SER_RATIO THEN
  SUBGOAL_THEN `?c. abs(x) < c /\ c < &1` STRIP_ASSUME_TAC THENL
   [EXISTS_TAC `(&1 + abs(x)) / &2` THEN
    SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
    UNDISCH_TAC `abs(x) < &1` THEN REAL_ARITH_TAC; ALL_TAC] THEN
  EXISTS_TAC `c:real` THEN ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN `?N. !n. n >= N ==> &(SUC(SUC n)) * abs(x) <= &(SUC n) * c`
  STRIP_ASSUME_TAC THENL
   [ALL_TAC;
    EXISTS_TAC `N:num` THEN REPEAT STRIP_TAC THEN
    REWRITE_TAC[real_pow; REAL_ABS_MUL; REAL_MUL_ASSOC] THEN
    MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
    REWRITE_TAC[REAL_ABS_NUM; REAL_ABS_ABS] THEN
    GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN ASM_SIMP_TAC[]] THEN
  ASM_CASES_TAC `x = &0` THENL
   [ASM_REWRITE_TAC[REAL_ABS_NUM; REAL_MUL_RZERO] THEN
    EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN
    REWRITE_TAC[REAL_POS] THEN UNDISCH_TAC `abs(x) < c` THEN REAL_ARITH_TAC;
    ALL_TAC] THEN
  ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ; GSYM REAL_ABS_NZ] THEN
  REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
  REWRITE_TAC[GSYM real_div] THEN
  REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
  ONCE_REWRITE_TAC[REAL_ARITH `x + &1 <= y <=> &1 <= y - x * &1`] THEN
  REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN
  SUBGOAL_THEN `?N. &1 <= &N * (c / abs x - &1)` STRIP_ASSUME_TAC THENL
   [ALL_TAC;
    EXISTS_TAC `N:num` THEN REWRITE_TAC[GE] THEN REPEAT STRIP_TAC THEN
    FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `&1 <= x ==> x <= y ==> &1 <= y`)) THEN
    MATCH_MP_TAC REAL_LE_RMUL THEN
    ASM_SIMP_TAC[REAL_ARITH `a <= b ==> a <= b + &1`;
                 REAL_OF_NUM_LE; REAL_LE_RADD] THEN
    REWRITE_TAC[REAL_LE_SUB_LADD; REAL_ADD_LID] THEN
    ASM_SIMP_TAC[REAL_LE_RDIV_EQ; GSYM REAL_ABS_NZ; REAL_MUL_LID;
                 REAL_LT_IMP_LE]] THEN
  ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ; REAL_LT_SUB_LADD; REAL_ADD_LID;
               REAL_LT_RDIV_EQ; GSYM REAL_ABS_NZ; REAL_MUL_LID;
               REAL_ARCH_SIMPLE]);;

let REAL_ATN_POWSER_DIFFL = prove
 (`!x. abs(x) < &1
       ==> ((\x. suminf (\n. (if EVEN n then &0
                              else --(&1) pow ((n - 1) DIV 2) / &n) * x pow n))
            diffl (inv(&1 + x pow 2))) x`,
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP REAL_ATN_POWSER_DIFFS_SUM) THEN
  DISCH_THEN(SUBST1_TAC o MATCH_MP SUM_UNIQ) THEN
  MATCH_MP_TAC TERMDIFF THEN
  SUBGOAL_THEN `?K. abs(x) < abs(K) /\ abs(K) < &1` STRIP_ASSUME_TAC THENL
   [EXISTS_TAC `(&1 + abs(x)) / &2` THEN
    SIMP_TAC[REAL_LT_LDIV_EQ; REAL_ABS_DIV; REAL_ABS_NUM;
             REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
    UNDISCH_TAC `abs(x) < &1` THEN REAL_ARITH_TAC; ALL_TAC] THEN
  EXISTS_TAC `K:real` THEN ASM_REWRITE_TAC[] THEN
  ASM_SIMP_TAC[REAL_ATN_POWSER_SUMMABLE; REAL_ATN_POWSER_DIFFS_SUMMABLE;
               REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE]);;

let REAL_ATN_POWSER = prove
 (`!x. abs(x) < &1
       ==> (\n. (if EVEN n then &0
                 else --(&1) pow ((n - 1) DIV 2) / &n) * x pow n)
           sums (atn x)`,
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP REAL_ATN_POWSER_SUMMABLE) THEN
  DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
  SUBGOAL_THEN
   `suminf (\n. (if EVEN n then &0
                 else --(&1) pow ((n - 1) DIV 2) / &n) * x pow n) = atn(x)`
   (fun th -> REWRITE_TAC[th]) THEN
  ONCE_REWRITE_TAC[REAL_ARITH `(a = b) <=> (a - b = &0)`] THEN
  SUBGOAL_THEN
   `suminf (\n. (if EVEN n then &0
                 else --(&1) pow ((n - 1) DIV 2) / &n) * &0 pow n) -
    atn(&0) = &0`
  MP_TAC THENL
   [MATCH_MP_TAC(REAL_ARITH `(a = &0) /\ (b = &0) ==> (a - b = &0)`) THEN
    CONJ_TAC THENL
     [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_UNIQ THEN
      MP_TAC(SPEC `&0` GP) THEN
      REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_LT; ARITH] THEN
      DISCH_THEN(MP_TAC o SPEC `&0` o MATCH_MP SER_CMUL) THEN
      REWRITE_TAC[REAL_MUL_LZERO] THEN
      MATCH_MP_TAC(TAUT `(a = b) ==> a ==> b`) THEN
      AP_THM_TAC THEN AP_TERM_TAC THEN ABS_TAC THEN
      COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LZERO] THEN
      CONV_TAC SYM_CONV THEN
      REWRITE_TAC[REAL_ENTIRE; REAL_POW_EQ_0] THEN ASM_MESON_TAC[EVEN];
      GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM TAN_0] THEN
      MATCH_MP_TAC TAN_ATN THEN
      SIMP_TAC[PI2_BOUNDS; REAL_ARITH `&0 < x ==> --x < &0`]];
    ALL_TAC] THEN
  ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
  MP_TAC(SPEC `\x. suminf (\n. (if EVEN n then &0

                       else --(&1) pow ((n - 1) DIV 2) / &n) * x pow n) -
          atn x` DIFF_ISCONST_END_SIMPLE) THEN
  FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
    `~(x = &0) ==> &0 < x \/ x < &0`))
  THENL
   [DISCH_THEN(MP_TAC o SPECL [`&0`; `x:real`]);
    CONV_TAC(RAND_CONV SYM_CONV) THEN
    DISCH_THEN(MP_TAC o SPECL [`x:real`; `&0`])] THEN
  (REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
   ASM_REWRITE_TAC[] THEN
   X_GEN_TAC `u:real` THEN REPEAT STRIP_TAC THEN
   SUBGOAL_THEN `abs(u) < &1` (MP_TAC o MATCH_MP REAL_ATN_POWSER_DIFFL) THENL
    [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC;
     ALL_TAC] THEN
   DISCH_THEN(MP_TAC o C CONJ (SPEC `u:real` DIFF_ATN)) THEN
   DISCH_THEN(MP_TAC o MATCH_MP DIFF_SUB) THEN
   REWRITE_TAC[REAL_SUB_REFL]));;

(* ------------------------------------------------------------------------- *)
(* A more Taylor-like version with a simply bounded remainder term.          *)
(* ------------------------------------------------------------------------- *)

let MCLAURIN_ATN_SIMPLE = prove
 (`!x n k. abs(x) <= inv(&2 pow k) /\ ~(k = 0)
           ==> abs(atn x -
                   sum(0,n) (\m. (if EVEN m then &0
                                  else --(&1) pow ((m - 1) DIV 2) / &m) *
                                  x pow m))
               <= &2 * abs(x) pow n`,
  REPEAT STRIP_TAC THEN SUBGOAL_THEN `abs(x) < &1` ASSUME_TAC THENL
   [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
    ASM_REWRITE_TAC[REAL_ARITH `a < &1 <=> &0 < &1 - a`; REAL_POW2_CLAUSES];
    ALL_TAC] THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP REAL_ATN_POWSER) THEN
  DISCH_THEN(fun th -> ASSUME_TAC(SYM(MATCH_MP SUM_UNIQ th)) THEN
                       MP_TAC(MATCH_MP SUM_SUMMABLE th)) THEN
  DISCH_THEN(MP_TAC o MATCH_MP SER_OFFSET) THEN
  DISCH_THEN(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(MP_TAC o MATCH_MP SUM_UNIQ) THEN
  MATCH_MP_TAC(REAL_ARITH
   `abs(r) <= e ==> (f - s = r) ==> abs(f - s) <= e`) THEN
  SUBGOAL_THEN
   `(\m. abs(x) pow (m + n)) sums (abs(x) pow n) * inv(&1 - abs(x))`
  ASSUME_TAC THENL
   [FIRST_ASSUM(MP_TAC o MATCH_MP GP o MATCH_MP (REAL_ARITH
      `abs(x) < &1 ==> abs(abs x) < &1`)) THEN
    DISCH_THEN(MP_TAC o SPEC `abs(x) pow n` o MATCH_MP SER_CMUL) THEN
    ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM REAL_POW_ADD];
    ALL_TAC] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `suminf (\m. abs(x) pow (m + n))` THEN CONJ_TAC THENL
   [ALL_TAC;
    FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP SUM_UNIQ) THEN
    GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
    MATCH_MP_TAC REAL_LE_LMUL THEN SIMP_TAC[REAL_ABS_POS; REAL_POW_LE] THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_INV] THEN
    MATCH_MP_TAC REAL_LE_INV2 THEN
    ONCE_REWRITE_TAC[REAL_ARITH `a <= &1 - b <=> b <= &1 - a`] THEN
    CONV_TAC REAL_RAT_REDUCE_CONV THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
    ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN
    MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
    GEN_REWRITE_TAC LAND_CONV [GSYM REAL_POW_1] THEN
    ASM_SIMP_TAC[REAL_POW_MONO; REAL_OF_NUM_LE; ARITH;
                 ARITH_RULE `~(k = 0) ==> 1 <= k`]] THEN
  SUBGOAL_THEN
   `!m. abs((if EVEN (m + n) then &0
             else --(&1) pow (((m + n) - 1) DIV 2) / &(m + n)) *
             x pow (m + n))
        <= abs(x) pow (m + n)`
  ASSUME_TAC THENL
   [GEN_TAC THEN COND_CASES_TAC THEN
    SIMP_TAC[REAL_MUL_LZERO; REAL_ABS_NUM; REAL_POW_LE; REAL_ABS_POS] THEN
    REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NEG] THEN
    REWRITE_TAC[REAL_ABS_NUM; REAL_POW_ONE; REAL_MUL_LID] THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
    MATCH_MP_TAC REAL_LE_RMUL THEN SIMP_TAC[REAL_POW_LE; REAL_ABS_POS] THEN
    REWRITE_TAC[real_div; REAL_MUL_LID] THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_1] THEN
    MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[REAL_OF_NUM_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
    ASM_MESON_TAC[EVEN]; ALL_TAC] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC
   `suminf (\m. abs((if EVEN (m + n) then &0
                     else --(&1) pow (((m + n) - 1) DIV 2) / &(m + n)) *
                    x pow (m + n)))` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC SER_ABS THEN MATCH_MP_TAC SER_COMPARA THEN
    EXISTS_TAC `\m. abs(x) pow (m + n)` THEN
    ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[SUM_SUMMABLE]; ALL_TAC] THEN
  MATCH_MP_TAC SER_LE THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
   [MATCH_MP_TAC SER_COMPARA THEN
    EXISTS_TAC `\m. abs(x) pow (m + n)` THEN
    ASM_REWRITE_TAC[]; ALL_TAC] THEN
  ASM_MESON_TAC[SUM_SUMMABLE]);;

let MCLAURIN_ATN_APPROX = prove
 (`!x n k. abs(x) <= inv(&2 pow k) /\ ~(k = 0)
           ==> abs(atn x -
                   sum(0,n) (\m. (if EVEN m then &0
                                  else --(&1) pow ((m - 1) DIV 2) / &m) *
                                  x pow m))
               <= inv(&2 pow (n * k - 1))`,
  REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THENL
   [ASM_REWRITE_TAC[sum; REAL_SUB_RZERO; MULT_CLAUSES; SUB_0] THEN
    MP_TAC(SPECL [`x:real`; `2`; `k:num`] MCLAURIN_ATN_SIMPLE) THEN
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC(REAL_ARITH
     `abs(y) + d <= e ==> abs(x - y) <= d ==> abs(x) <= e`) THEN
    CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
    REWRITE_TAC[real_pow; REAL_POW_1] THEN CONV_TAC NUM_REDUCE_CONV THEN
    CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[real_div; REAL_MUL_LID; REAL_INV_1; REAL_ADD_LID] THEN
    SUBGOAL_THEN `abs(x) <= inv(&2)` ASSUME_TAC THENL
     [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN
      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
      CONV_TAC REAL_RAT_REDUCE_CONV THEN
      CONV_TAC REAL_RAT_REDUCE_CONV THEN
      GEN_REWRITE_TAC LAND_CONV [GSYM REAL_POW_1] THEN
      ASM_SIMP_TAC[REAL_POW_MONO; REAL_OF_NUM_LE; ARITH;
                   ARITH_RULE `~(k = 0) ==> 1 <= k`];
      ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `inv(&2) + &2 * inv(&2) pow 2` THEN
    CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[REAL_POW_1] THEN
    MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
    ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_OF_NUM_LT; ARITH;
                 REAL_POW_LE2; REAL_OF_NUM_LE; REAL_ABS_POS];
    ALL_TAC] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * abs(x) pow n` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC MCLAURIN_ATN_SIMPLE THEN ASM_MESON_TAC[]; ALL_TAC] THEN
  ASM_SIMP_TAC[REAL_POW_SUB; REAL_OF_NUM_EQ; ARITH_EQ;
               ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0] THEN
  REWRITE_TAC[REAL_INV_DIV; REAL_POW_1] THEN REWRITE_TAC[real_div] THEN
  SIMP_TAC[REAL_LE_LMUL_EQ; REAL_OF_NUM_LT; ARITH] THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[GSYM REAL_POW_POW] THEN
  ONCE_REWRITE_TAC[GSYM REAL_POW_INV] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
  ASM_REWRITE_TAC[REAL_ABS_POS]);;

(* ------------------------------------------------------------------------- *)
(* Rules to return approximations to atn(x) good to 2^-p given |x| <= 2^-k.  *)
(* ------------------------------------------------------------------------- *)

let mclaurin_atn_rule,MCLAURIN_ATN_RULE =
  let x_tm = `x:real`
  and n_tm = `n:num`
  and k_tm = `k:num`
  and inv_tm = `inv`
  and le_tm = `(<=):real->real->bool`
  and pow2_tm = `(pow) (&2)` in
  let pth = SPECL [x_tm; n_tm; k_tm] MCLAURIN_ATN_APPROX
  and CLEAN_RULE = REWRITE_RULE[real_pow]
  and MATCH_REAL_LE_TRANS = MATCH_MP REAL_LE_TRANS
  and num_0 = Int 0
  and num_1 = Int 1 in
  let mclaurin_atn_rule k0 p0 =
    if k0 = 0 then failwith "mclaurin_atn_rule: must have |x| <= 1/2" else
    let k = Int k0
    and p = Int p0 in
    let n = Num.int_of_num(ceiling_num ((p +/ k) // k)) in
    let ns = if n mod 2 = 0 then 0--(n - 1) else 0--(n - 2) in
    map (fun m -> if m mod 2 = 0 then num_0 else
                  (if (m - 1) mod 4 = 0 then I else minus_num)
                  (num_1 // Int m)) ns
  and MCLAURIN_ATN_RULE k0 p0 =
    if k0 = 0 then failwith "MCLAURIN_ATN_RULE: must have |x| <= 1/2" else
    let k = Int k0
    and p = Int p0 in
    let n = ceiling_num ((p +/ k) // k) in
    let th1 = INST [mk_numeral k,k_tm; mk_numeral n,n_tm] pth in
    let th2 = ASSUME (lhand(lhand(concl th1)))
    and th3 = EQF_ELIM(NUM_REDUCE_CONV(rand(rand(lhand(concl th1))))) in
    let th4 = MP th1 (CONJ th2 th3) in
    let th5 = CONV_RULE(ONCE_DEPTH_CONV REAL_HORNER_SUM_CONV) th4 in
    let th6 = CLEAN_RULE th5 in
    let th7 = CONV_RULE (NUM_REDUCE_CONV THENC LAND_CONV REAL_RAT_REDUCE_CONV)
                        (BETA_RULE th6) in
    let tm1 = mk_comb(inv_tm,mk_comb(pow2_tm,mk_numeral p)) in
    let tm2 = mk_comb(mk_comb(le_tm,rand(concl th7)),tm1) in
    let th8 = EQT_ELIM((NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV) tm2) in
    let th9 = MATCH_REAL_LE_TRANS (CONJ th7 th8) in
    GEN x_tm (DISCH_ALL th9) in
  mclaurin_atn_rule,MCLAURIN_ATN_RULE;;

(* ------------------------------------------------------------------------- *)
(* Lemmas for Machin-type formulas.                                          *)
(* ------------------------------------------------------------------------- *)

let TAN_ADD_ATN_SIDECOND = prove
 (`!x y. ~(x * y = &1) ==> ~(cos(atn x + atn y) = &0)`,
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  REWRITE_TAC[COS_ADD; REAL_ARITH `(a - b = &0) <=> (a = b)`] THEN
  DISCH_THEN(MP_TAC o AP_TERM `(*) (inv(cos(atn x)))`) THEN
  SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV; COS_ATN_NZ; REAL_MUL_LID] THEN
  DISCH_THEN(MP_TAC o AP_TERM `(*) (inv(cos(atn y)))`) THEN
  SIMP_TAC[REAL_MUL_LINV; COS_ATN_NZ; REAL_MUL_LID; GSYM REAL_MUL_ASSOC] THEN
  ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d = (c * b) * (d * a)`] THEN
  ASM_REWRITE_TAC[GSYM tan; GSYM real_div; ATN_TAN]);;

let ATN_ADD = prove
 (`!x y. ~(x * y = &1) /\
         abs(atn x + atn y) < pi / &2
         ==> (atn(x) + atn(y) = atn((x + y) / (&1 - x * y)))`,
  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `tan(atn(x) + atn(y)) = (x + y) / (&1 - x * y)` MP_TAC THENL
   [ASM_SIMP_TAC[ATN_TAN; TAN_ADD; COS_ATN_NZ; TAN_ADD_ATN_SIDECOND];
    DISCH_THEN(SUBST1_TAC o SYM) THEN CONV_TAC SYM_CONV THEN
    ASM_SIMP_TAC[TAN_ATN; REAL_ARITH `abs(x) < e ==> --e < x /\ x < e`]]);;

let ATN_ADD_SMALL_LEMMA_POS = prove
 (`!x y. &0 < y /\ x * y < &1
         ==> atn(x) + atn(y) < pi / &2`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_LT_SUB_LADD] THEN
  SUBGOAL_THEN `pi / &2 - atn y = atn(tan(pi / &2 - atn y))` SUBST1_TAC THENL
   [CONV_TAC SYM_CONV THEN MATCH_MP_TAC TAN_ATN THEN
    MATCH_MP_TAC(REAL_ARITH
     `&0 < x /\ x < a ==> --a < a - x /\ a - x < a`) THEN
    REWRITE_TAC[ATN_BOUNDS] THEN
    GEN_REWRITE_TAC LAND_CONV [GSYM ATN_0] THEN
    ASM_SIMP_TAC[ATN_MONO_LT];
    MATCH_MP_TAC ATN_MONO_LT THEN REWRITE_TAC[TAN_COT; ATN_TAN] THEN
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
    ASM_SIMP_TAC[GSYM real_div; REAL_LT_RDIV_EQ; REAL_LT_IMP_NZ]]);;

let ATN_ADD_SMALL_LEMMA = prove
 (`!x y. abs(x * y) < &1 ==> abs(atn(x) + atn(y)) < pi / &2`,
  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(REAL_ARITH
   `--a < x /\ x < a /\ --a < y /\ y < a /\
    (&0 < y ==> x + y < a) /\
    (&0 < --y ==> --x + --y < a)
    ==> abs(x + y) < a`) THEN
  REWRITE_TAC[ATN_BOUNDS] THEN CONJ_TAC THEN
  REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM ATN_NEG] THEN
  MATCH_MP_TAC ATN_ADD_SMALL_LEMMA_POS THEN
  ASM_SIMP_TAC[REAL_ARITH `abs(x) < &1 ==> x < &1`;
               REAL_ARITH `--x * -- y = x * y`] THEN
  FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
   `&0 < y ==> (z <= &0 ==> y <= &0) ==> &0 < z`)) THEN
  MATCH_MP_TAC(REAL_ARITH
   `(y < &0 ==> z < &0) /\ ((y = &0) ==> (z = &0))
    ==> y <= &0 ==> z <= &0`) THEN
  SIMP_TAC[ATN_0; GSYM ATN_NEG] THEN
  GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM ATN_0] THEN
  SIMP_TAC[ATN_MONO_LT]);;

let ATN_ADD_SMALL = prove
 (`!x y. abs(x * y) < &1
         ==> (atn(x) + atn(y) = atn((x + y) / (&1 - x * y)))`,
  REPEAT STRIP_TAC THEN MATCH_MP_TAC ATN_ADD THEN
  ASM_SIMP_TAC[ATN_ADD_SMALL_LEMMA] THEN
  POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;

let ATN_ADD_CONV =
  let match_fn = PART_MATCH (lhand o rand) ATN_ADD_SMALL in
  let overall_fn =
    C MP TRUTH o
    CONV_RULE
       (COMB2_CONV REAL_RAT_REDUCE_CONV
         (RAND_CONV REAL_RAT_REDUCE_CONV)) o
    match_fn in
  fun tm -> if is_ratconst(rand(rand tm)) &
               is_ratconst(rand(lhand tm))
            then overall_fn tm
            else failwith "ATN_ADD_CONV: Atn of nonconstant";;

let ATN_CMUL_CONV =
  let pth_base = prove
   (`(&0 * atn(x) = &0) /\
     (&1 * atn(x) = atn(x))`,
    REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_LID])
  and pth_0,pth_1 = (CONJ_PAIR o prove)
   (`(&(NUMERAL(BIT0 n)) * atn(x) =
      &(NUMERAL n) * atn(x) + &(NUMERAL n) * atn(x)) /\
     (&(NUMERAL(BIT1 n)) * atn(x) =
      atn(x) + &(NUMERAL n) * atn(x) + &(NUMERAL n) * atn(x))`,
    REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_LID] THEN
    REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_SUC] THEN
    REAL_ARITH_TAC) in
  let rewr_base = GEN_REWRITE_CONV I [pth_base]
  and rewr_0 = GEN_REWRITE_CONV I [pth_0]
  and rewr_1 = GEN_REWRITE_CONV I [pth_1] in
  let rec ATN_CMUL_CONV tm =
    if not (is_ratconst(rand(rand tm))) then failwith "ATN_CMUL_CONV" else
    try rewr_base tm with Failure _ ->
    try let th1 = rewr_0 tm in
        let tm1 = rand(concl th1) in
        let th2 = ATN_CMUL_CONV(rand tm1) in
        let th3 = MK_COMB(AP_TERM (rator(rator tm1)) th2,th2) in
        let th4 = TRANS th3 (ATN_ADD_CONV(rand(concl th3))) in
        TRANS th1 th4
    with Failure _ ->
        let th1 = rewr_1 tm in
        let tm1 = rand(rand(concl th1)) in
        let th2 = ATN_CMUL_CONV(rand tm1) in
        let th3 = MK_COMB(AP_TERM (rator(rator tm1)) th2,th2) in
        let th4 = TRANS th3 (ATN_ADD_CONV(rand(concl th3))) in
        let th5 = AP_TERM (rator(rand(concl th1))) th4 in
        let th6 = TRANS th5 (ATN_ADD_CONV(rand(concl th5))) in
        TRANS th1 th6 in
  ATN_CMUL_CONV;;

let ATN_SUB_CONV =
  let pth = prove
   (`(atn(x) - atn(y) = atn(x) + atn(--y))`,
    REWRITE_TAC[real_sub; ATN_NEG]) in
  GEN_REWRITE_CONV I [pth] THENC
  RAND_CONV(RAND_CONV REAL_RAT_NEG_CONV) THENC
  ATN_ADD_CONV;;

let MACHIN_CONV =
  DEPTH_CONV(ATN_ADD_CONV ORELSEC ATN_SUB_CONV ORELSEC ATN_CMUL_CONV);;

let MACHIN_RULE tm = SYM(TRANS (MACHIN_CONV tm) ATN_1);;

let MACHIN_1 = time MACHIN_RULE `&4 * atn(&1 / &5) - atn(&1 / &239)`;;
let MACHIN_2 = time MACHIN_RULE `atn(&1 / &2) + atn(&1 / &3)`;;
let MACHIN_3 = time MACHIN_RULE `&2 * atn(&1 / &2) - atn(&1 / &7)`;;
let MACHIN_4 = time MACHIN_RULE `&2 * atn(&1 / &3) + atn(&1 / &7)`;;

let EULER = time MACHIN_RULE `&5 * atn(&1 / &7) + &2 * atn (&3 / &79)`;;

let GAUSS_MACHIN = time MACHIN_RULE
  `&12 * atn(&1 / &18) + &8 * atn (&1 / &57) - &5 * atn(&1 / &239)`;;

let STRASSNITZKY_MACHIN = time MACHIN_RULE
  `atn(&1 / &2) + atn (&1 / &5) + atn(&1 / &8)`;;

let MACHINLIKE_1 = time MACHIN_RULE
  `&6 * atn(&1 / &8) + &2 * atn(&1 / &57) + atn(&1 / &239)`;;
let MACHINLIKE_2 = time MACHIN_RULE
  `&4 * atn(&1 / &5) - &1 * atn(&1 / &70) + atn(&1 / &99)`;;
let MACHINLIKE_3 = time MACHIN_RULE
  `&1 * atn(&1 / &2) + &1 * atn(&1 / &5) + atn(&1 / &8)`;;
let MACHINLIKE_4 = time MACHIN_RULE
  `&8 * atn(&1 / &10) - &1 * atn(&1 / &239) - &4 * atn(&1 / &515)`;;
let MACHINLIKE_5 = time MACHIN_RULE
  `&5 * atn(&1 / &7) + &4 * atn(&1 / &53) + &2 * atn(&1 / &4443)`;;

(***** Hopefully this one would work, but it takes a long time

let HWANG_MACHIN = time MACHIN_RULE
  `&183 * atn(&1 / &239) + &32 * atn(&1 / &1023) -
   &68 * atn(&1 / &5832) + &12 * atn(&1 / &110443) -
   &12 * atn(&1 / &4841182) - &100 * atn(&1 / &6826318)`;;

 *****)

(* ------------------------------------------------------------------------- *)
(* Approximate the arctan of a rational number.                              *)
(* ------------------------------------------------------------------------- *)

let rec POLY l x =
  if l = [] then num_0
  else hd l +/ (x */ POLY (tl l) x);;

let atn_approx_conv,ATN_APPROX_CONV =
  let atn_tm = `atn`
  and num_0 = Int 0
  and num_1 = Int 1
  and num_2 = Int 2 in
  let rec log_2 x = if x <=/ num_1 then log_2 (num_2 */ x) -/ num_1
       else if x >/ num_2 then log_2 (x // num_2) +/ num_1
                      else num_1 in
  let pth = prove
   (`!p. abs(atn(&0) - &0) <= inv(&2 pow p)`,
    SIMP_TAC[ATN_0; REAL_SUB_REFL; REAL_ABS_NUM; REAL_LE_INV_EQ;
             REAL_POW_LE; REAL_POS]) in
  let atn_approx_conv p r =
    if r =/ num_0 then num_0 else
    let k = Num.int_of_num(minus_num(log_2(abs_num r))) in
    if k < 1 then failwith "atn_approx_conv: argument too big" else
    let rats = mclaurin_atn_rule k p in
    POLY rats r
  and ATN_APPROX_CONV p tm =
    let atm,rtm = dest_comb tm in
    if atm <> atn_tm then failwith "ATN_APPROX_CONV" else
    let r = rat_of_term rtm in
    if r =/ num_0 then SPEC (mk_small_numeral p) pth else
    let k = Num.int_of_num(minus_num(log_2(abs_num r))) in
    if k < 1 then failwith "ATN_APPROX_CONV: argument too big" else
    let th1 = MCLAURIN_ATN_RULE k p in
    let th2 = SPEC rtm th1 in
    let th3 = MP th2 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th2)))) in
    CONV_RULE(LAND_CONV(RAND_CONV(RAND_CONV REAL_RAT_REDUCE_CONV))) th3 in
  atn_approx_conv,ATN_APPROX_CONV;;

(* ------------------------------------------------------------------------- *)
(* Approximate pi using this and a Machin-type formula.                      *)
(* ------------------------------------------------------------------------- *)

let pi_approx_rule,PI_APPROX_RULE =
  let const_1_8 = Int 1 // Int 8
  and const_1_57 = Int 1 // Int 57
  and const_1_239 = Int 1 // Int 239
  and const_24 = Int 24
  and const_8 = Int 8
  and const_4 = Int 4
  and tm_1_8 = `atn(&1 / &8)`
  and tm_1_57 = `atn(&1 / &57)`
  and tm_1_239 = `atn(&1 / &239)`
  and q1_tm = `q1:num`
  and q2_tm = `q2:num`
  and p_tm = `p:num` in
  let pth = prove
   (`(q1 = p + 5) /\
     (q2 = p + 6) /\
     abs(atn(&1 / &8) - a1) <= inv(&2 pow q1) /\
     abs(atn(&1 / &57) - a2) <= inv(&2 pow q2) /\
     abs(atn(&1 / &239) - a3) <= inv(&2 pow q2)
     ==> abs(pi - (&24 * a1 + &8 * a2 + &4 * a3)) <= inv(&2 pow p)`,
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
    ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(K ALL_TAC) THEN STRIP_TAC THEN
    MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(inv(&2 pow 2))` THEN
    SIMP_TAC[REAL_POW2_CLAUSES; REAL_ARITH `&0 < x ==> &0 < abs(x)`] THEN
    REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
    REWRITE_TAC[REAL_ABS_INV; REAL_ABS_POW; REAL_ABS_NUM] THEN
    REWRITE_TAC[GSYM REAL_INV_MUL; GSYM REAL_POW_ADD] THEN
    CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_ADD_LDISTRIB; REAL_MUL_ASSOC] THEN
    CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[real_div; REAL_MUL_LID] THEN
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
    REWRITE_TAC[GSYM real_div; MACHINLIKE_1] THEN
    REWRITE_TAC[REAL_ARITH `(x1 + x2 + x3) - (y1 + y2 + y3) =
                            (x1 - y1) + (x2 - y2) + (x3 - y3)`] THEN
    REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN BOUND_SUMPROD_TAC THEN
    GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN
    REWRITE_TAC[REAL_POW_ADD; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
    SIMP_TAC[GSYM REAL_ADD_RDISTRIB; REAL_LE_RMUL_EQ; REAL_POW2_CLAUSES] THEN
    CONV_TAC REAL_RAT_REDUCE_CONV) in
  let pi_approx_rule p =
    let q1 = p + 5
    and q2 = p + 6 in
    let a1 = atn_approx_conv q1 const_1_8
    and a2 = atn_approx_conv q2 const_1_57
    and a3 = atn_approx_conv q2 const_1_239 in
    const_24 */ a1 +/ const_8 */ a2 +/ const_4 */ a3
  and PI_APPROX_RULE p =
    let q1 = p + 5
    and q2 = p + 6 in
    let th1 = ATN_APPROX_CONV q1 tm_1_8
    and th2 = ATN_APPROX_CONV q2 tm_1_57
    and th3 = ATN_APPROX_CONV q2 tm_1_239 in
    let th4 = INST [mk_small_numeral p,p_tm;
                    mk_small_numeral q1,q1_tm;
                    mk_small_numeral q2,q2_tm] pth in
    let th5 = EQT_ELIM(NUM_REDUCE_CONV(lhand(lhand(concl th4))))
    and th6 = EQT_ELIM(NUM_REDUCE_CONV(lhand(rand(lhand(concl th4))))) in
    let th7 = MATCH_MP th4 (end_itlist CONJ [th5; th6; th1; th2; th3]) in
    CONV_RULE(LAND_CONV(RAND_CONV(RAND_CONV REAL_RAT_REDUCE_CONV))) th7 in
  pi_approx_rule,PI_APPROX_RULE;;

(* ------------------------------------------------------------------------- *)
(* A version that yields a fraction with power of two denominator.           *)
(* ------------------------------------------------------------------------- *)

let pi_approx_binary_rule,PI_APPROX_BINARY_RULE =
  let pth = prove
   (`abs(x - r) <= inv(&2 pow (SUC p))
     ==> !a. abs(&2 pow p * r - a) <= inv(&2)
             ==> abs(x - a / &2 pow p) <= inv(&2 pow p)`,
    REPEAT STRIP_TAC THEN
    FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
      `abs(x - r) <= q ==> abs(r - r') <= p - q ==> abs(x - r') <= p`)) THEN
    MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(&2 pow p)` THEN
    SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`; REAL_POW2_THM] THEN
    REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_LDISTRIB] THEN
    SIMP_TAC[REAL_ABS_POW; REAL_ABS_NUM; GSYM real_div;
             REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES;
             REAL_DIV_POW2; REAL_OF_NUM_EQ; ARITH_EQ;
             LE_REFL; ARITH_RULE `~(SUC p <= p)`;
             ARITH_RULE `SUC p - p = 1`; SUB_REFL] THEN
    UNDISCH_TAC `abs (&2 pow p * r - a) <= inv (&2)` THEN
    CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV)
  and num_2 = Int 2 in
  let pi_approx_binary_rule p =
    let ppow = power_num num_2 (Int p) in
    let r = pi_approx_rule (p + 1) in
    let a = round_num (ppow */ r) in
    a // ppow
  and PI_APPROX_BINARY_RULE p =
    let ppow = power_num num_2 (Int p) in
    let th1 = PI_APPROX_RULE (p + 1) in
    let th2 = CONV_RULE(funpow 3 RAND_CONV num_CONV) th1 in
    let r = rat_of_term(rand(rand(lhand(concl th2)))) in
    let th3 = SPEC (mk_realintconst(round_num(ppow */ r))) (MATCH_MP pth th2) in
    let th4 = MP th3 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th3)))) in
    CONV_RULE(LAND_CONV(RAND_CONV(RAND_CONV REAL_RAT_REDUCE_CONV))) th4 in
  pi_approx_binary_rule,PI_APPROX_BINARY_RULE;;

(* ------------------------------------------------------------------------- *)
(* Rule to expand atn(r) for rational r into more easily calculable bits.    *)
(* ------------------------------------------------------------------------- *)

let ATN_EXPAND_CONV =
  let num_0 = Int 0
  and num_1 = Int 1
  and num_2 = Int 2
  and eighth = Int 1 // Int 8
  and atn_tm = `atn`
  and eighth_tm = `&1 / &8`
  and mk_mul = mk_binop `(*)`
  and mk_add = mk_binop `(+)`
  and amp_tm = `&` in
  let home_in =
    let rec homein n x =
      let x' = (x -/ eighth) // (num_1 +/ x */ eighth) in
      if x' </ num_0 then
        if abs_num(x') </ abs_num(x) then (x',n+1) else (x,n)
      else homein (n + 1) x' in
    homein 0 in
  fun tm ->
    let ltm,rtm = dest_comb tm in
    if ltm <> atn_tm then failwith "ATN_EXPAND_CONV" else
    let r = rat_of_term rtm in
    let (x,n) = home_in r in
    let xtm = mk_add (mk_mul (mk_comb(amp_tm,mk_small_numeral n))
                             (mk_comb(atn_tm,eighth_tm)))
                     (mk_comb(atn_tm,term_of_rat x)) in
    SYM(MACHIN_CONV xtm);;