formal_ineqs/jordan/taylor_atn.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: Taylor Series for atn function                                      *)
   5 (* Chapter: Nonlinear Inequalities                                            *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-14                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 (*
  12 This file gives the half-angle identity for atan
  13     atn (2 x) = 2 atn (...)
  14
  15 It gives a general formula for the nth derivative of catn
  16
  17 It gives the complex Taylor polynomial of catn at Cx(&0).
  18
  19 It gives the real Taylor polynomial of atn at (&0)
  20 *)
  21
  22 module Taylor_atn =
  23  (*  sig
  24     val halfatn:thm
  25     val halfatn_bounds_abs:thm
  26     val halfatn_bounds:thm
  27     val halfatn_half :thm
  28     val abs_pass_through:thm
  29     val atn_abs:thm
  30     val atn_half_range:thm
  31   end = *)
  32 struct
  33
  34
  35 let FORCE_EQ = REPEAT (CHANGED_TAC (AP_TERM_TAC ORELSE AP_THM_TAC ORELSE BINOP_TAC)) ;;
  36
  37 let FORCE_MATCH = (MATCH_MP_TAC (TAUT `(a = b) ==> (a ==> b)`)) THEN FORCE_EQ ;;
  38
  39 let FORCE_MATCH_MP_TAC th =
  40   MP_TAC th THEN ANTS_TAC THENL[ALL_TAC;FORCE_MATCH
  41       ];;
  42
  43 (* first we develop the half-angle identity for the atn function *)
  44
  45 let halfatn = new_definition `halfatn x = x / (sqrt(&1 + x pow 2) + &1)`;;
  46
  47 let pos1 = prove(
  48   `!x. &0 < &1 + x pow 2 `,
  49   MESON_TAC[REAL_LE_POW_2;REAL_ARITH `&0 <= t ==> &0 < &1 + t`];
  50 );;
  51
  52 let ssqrt = new_definition `!x. ssqrt x = (if x < &0 then &0 else sqrt x)`;;
  53
  54 let halfsqrt_ssqrt = prove_by_refinement(
  55   `!x.  sqrt(&1+ x pow 2) = ssqrt(&1 + x pow 2)`,
  56   (* {{{ proof *)
  57   [
  58   REWRITE_TAC[ssqrt;];
  59   MESON_TAC[pos1;REAL_ARITH `&0 < x ==> ~(x < &0)`];
  60   ]);;
  61   (* }}} *)
  62
  63 let pos2 = prove (
  64   `!x. &0 < sqrt(&1 + x pow 2) + &1`,
  65 (* {{{ proof *)
  66    MESON_TAC[pos1;REAL_ARITH `(&0 <= t ==> &0 < t + &1) /\ (&0 < t ==> &0 <= t)`;SQRT_POS_LE;]
  67 (* }}} *));;
  68
  69 let halfatn_bounds_abs = prove_by_refinement(
  70  `!x.  abs(halfatn x) < &1 `,
  71 (* {{{ proof *)
  72 [
  73 REWRITE_TAC[halfatn;REAL_ABS_DIV];
  74 GEN_TAC;
  75 ASSUME_TAC (ISPEC `x:real` pos2);
  76 ASM_SIMP_TAC[REAL_ARITH `(&0 < x ==> abs(x) = x)/\ (&1 * t = t)`;REAL_LT_LDIV_EQ];
  77 (* *)
  78 REWRITE_TAC[GSYM POW_2_SQRT_ABS];
  79 MATCH_MP_TAC REAL_LET_TRANS;
  80 EXISTS_TAC `sqrt(&1 + x pow 2)`;
  81 CONJ_TAC;
  82 MATCH_MP_TAC SQRT_MONO_LE;
  83 REWRITE_TAC[REAL_LE_POW_2];
  84 ARITH_TAC;
  85 ARITH_TAC;
  86 ]
  87 (* }}} *));;
  88
  89 let halfatn_bounds = prove(
  90  `!x. -- &1 < halfatn x /\ halfatn x < &1 `,
  91  REWRITE_TAC[REAL_BOUNDS_LT;halfatn_bounds_abs]);;
  92
  93 let halfatn_half = prove_by_refinement(
  94  `!x t. (abs (x) < t ==> abs(halfatn x) < t / &2) `,
  95 (* {{{ proof *)
  96 [
  97 REWRITE_TAC[halfatn;REAL_ABS_DIV];
  98 REPEAT STRIP_TAC;
  99 ASSUME_TAC (ISPEC `x:real` pos2);
 100 ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`;REAL_LT_LDIV_EQ];
 101 MATCH_MP_TAC REAL_LTE_TRANS;
 102 EXISTS_TAC `t:real`;
 103 ASM_REWRITE_TAC[REAL_ARITH `(t / &2 * x = t * (x / &2)) /\ (t <= t * x/ &2 <=> t * &2 <= t * x)`];
 104 MATCH_MP_TAC REAL_LE_LMUL;
 105 CONJ_TAC;
 106 UNDISCH_TAC `abs x < t`;
 107 REAL_ARITH_TAC;
 108 ASM_SIMP_TAC [REAL_ARITH `&0 < x ==> (abs(x) = x)`];
 109 REWRITE_TAC[REAL_ARITH `(&2 <= x + &1) = (&1 <= x)`];
 110 MATCH_MP_TAC REAL_LE_TRANS;
 111 EXISTS_TAC `sqrt(&1)`;
 112 CONJ_TAC;
 113 REWRITE_TAC[SQRT_1;REAL_ARITH `&1 <= &1`];
 114 MATCH_MP_TAC SQRT_MONO_LE;
 115 CONJ_TAC;
 116 ARITH_TAC;
 117 MATCH_MP_TAC (REAL_ARITH `&0 <= x ==> &1 <= &1 + x`);
 118 REWRITE_TAC[REAL_LE_POW_2];
 119 ]
 120 (* }}} *));;
 121
 122 let abs_pass_through = prove_by_refinement (
 123  `(!x f.  (f (-- x) = -- f x) /\ (!y. &0 <= y ==> &0 <= f y)
 124      ==> (abs (f x) = f (abs x)))`,
 125 (* {{{ proof *)
 126  [
 127  REPEAT STRIP_TAC;
 128  DISJ_CASES_TAC (REAL_ARITH `&0 <= x \/ &0 <= --x`);
 129    POP_ASSUM MP_TAC;
 130    POP_ASSUM MP_TAC;
 131   MESON_TAC[REAL_ARITH `&0 <= x ==> abs(x ) = x`];
 132  REPEAT (POP_ASSUM MP_TAC);
 133   MESON_TAC[REAL_ARITH `&0 <= --x ==> abs(x) = -- x`; REAL_ARITH `abs( -- x ) = abs(x)`];
 134  ]
 135 (* }}} *));;
 136
 137 let atn_abs = prove_by_refinement(
 138  `!x. abs(atn x) = atn (abs x) `,
 139 (* {{{ proof *)
 140 [
 141 GEN_TAC;
 142 MATCH_MP_TAC abs_pass_through;
 143 REWRITE_TAC[ATN_NEG;ATN_POS_LE];
 144 ]
 145 (* }}} *));;
 146
 147 let atn_half_range = prove_by_refinement (
 148  `!x. abs(atn (halfatn x)) < pi / &4 `,
 149 (* {{{ proof *)
 150 [
 151 REWRITE_TAC[GSYM ATN_1;atn_abs;ATN_MONO_LT_EQ];
 152 GEN_TAC;
 153 REWRITE_TAC [halfatn_bounds;GSYM REAL_BOUNDS_LT];
 154 ]
 155 (* }}} *));;
 156
 157 let tan_one_one = prove_by_refinement(
 158  `!x y. (abs(x) < pi/ &2 /\ (abs y < pi / &2 ) /\ (tan x = tan y) ==> (x = y))`,
 159 (* {{{ proof *)
 160 [
 161 REPEAT STRIP_TAC;
 162 DISJ_CASES_TAC (REAL_ARITH `x < y \/ y < x \/ x = (y:real)`);
 163 REPEAT (POP_ASSUM MP_TAC);
 164 REWRITE_TAC[GSYM REAL_BOUNDS_LT];
 165 MESON_TAC[TAN_MONO_LT_EQ;REAL_ARITH `(x:real<y ) ==> ~(x = y)`];
 166 POP_ASSUM DISJ_CASES_TAC;
 167 REPEAT (POP_ASSUM MP_TAC);
 168 REWRITE_TAC[GSYM REAL_BOUNDS_LT];
 169 MESON_TAC[TAN_MONO_LT_EQ;REAL_ARITH `(x:real<y ) ==> ~(x = y)`];
 170 ASM_REWRITE_TAC[];
 171 ]
 172 (* }}} *));;
 173
 174 let abs_lemma = prove(
 175  `!f x. (?n. x = f n) \/ (?n. x = -- f n) <=> (?n. abs(x) = abs(f n))`,
 176   ASM_MESON_TAC[REAL_ARITH `!x y. abs(x) = abs(y) <=> (x = y)\/ (x = -- y)`]);;
 177
 178 let cos_nz = prove_by_refinement (
 179   `!x. (abs(x) < pi / &2) ==> ~(cos x = &0) `,
 180 (* {{{ proof *)
 181
 182 [
 183 GEN_TAC;
 184 REWRITE_TAC[COS_ZERO_PI;abs_lemma];
 185 ONCE_REWRITE_TAC[TAUT `(a ==> ~b) <=> (b ==> ~a)`];
 186 ONCE_REWRITE_TAC[REAL_ARITH `~(x < y) <=> (y <= x)`];
 187 REPEAT STRIP_TAC;
 188 ASM_REWRITE_TAC[];
 189 MATCH_MP_TAC REAL_LE_TRANS;
 190 EXISTS_TAC`(&n +  &1/ &2) * pi `;
 191 REWRITE_TAC[REAL_ARITH `x <= abs(x)`];
 192 MP_TAC PI_POS;
 193 MP_TAC (REAL_ARITH `&1/ &2 <= (&n + &1/ &2)`);
 194 REWRITE_TAC[REAL_ARITH `pi / &2 = (&1 / &2) * pi`];
 195 ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 <= x`;Real_ext.REAL_LE_RMUL_IMP];
 196 ]
 197
 198 (* }}} *));;
 199
 200 let cos_2nz =  prove_by_refinement(
 201    `!x. (abs(x) < pi / &4) ==> ~(cos (&2 * x) = &0) `,
 202 (* {{{ proof *)
 203  [
 204  STRIP_TAC THEN STRIP_TAC;
 205  MATCH_MP_TAC cos_nz;
 206  REWRITE_TAC[REAL_ABS_MUL;REAL_ARITH `abs(&2)= &2 /\ (&2 * x < pi/ &2 <=> x < pi/ &4)`];
 207  ASM_REWRITE_TAC[];
 208  ]
 209 (* }}} *));;
 210
 211 let halfatn_double  =prove_by_refinement(
 212  `!x. ~(cos (atn (halfatn x)) = &0) /\ ~(cos(&2 * atn (halfatn x)) = &0) `,
 213 (* {{{ proof *)
 214 [
 215 REPLICATE_TAC 2 (STRIP_TAC);
 216 MATCH_MP_TAC cos_nz;
 217 MATCH_MP_TAC REAL_LTE_TRANS;
 218 EXISTS_TAC `pi/ &4`;
 219 REWRITE_TAC[atn_half_range];
 220 MP_TAC PI_POS;
 221 REAL_ARITH_TAC;
 222 MATCH_MP_TAC cos_2nz;
 223 REWRITE_TAC[atn_half_range];
 224 ]
 225 (* }}} *));;
 226
 227 let REAL_DIV_MUL2z =  REAL_FIELD
 228  `!x y z. (&0 < x)  ==> (y /z = (x pow 2 * y) / (x pow 2* z)) `;;
 229
 230 let atn_half = prove_by_refinement (
 231  `!x. atn x = &2 * atn (halfatn x) `,
 232 (* {{{ proof *)
 233 [
 234 GEN_TAC;
 235 MATCH_MP_TAC tan_one_one;
 236 MATCH_MP_TAC (TAUT `a /\ b /\ (a /\ b ==> c) ==> a /\ b /\ c`);
 237 REPEAT CONJ_TAC;
 238 REWRITE_TAC[GSYM REAL_BOUNDS_LT;ATN_BOUNDS];
 239 (* *)
 240 REWRITE_TAC[REAL_ABS_MUL;REAL_ARITH `abs (&2) = &2`;REAL_ARITH `&2 * x < y / &2 <=> x < y / &4`;atn_half_range];
 241 (* *)
 242 REPEAT STRIP_TAC;
 243 ASSUME_TAC (ISPEC `x:real` halfatn_double);
 244 ASM_SIMP_TAC[TAN_DOUBLE;ATN_TAN];
 245 REWRITE_TAC[halfatn];
 246 ASSUME_TAC (ISPEC `x:real` pos2);
 247 ABBREV_TAC `t = sqrt(&1 + x pow 2) + &1`;
 248 MP_TAC (ISPECL [`t:real`;`&2 * x / t`;`&1 - (x / t) pow 2`] REAL_DIV_MUL2z);
 249 ASM_REWRITE_TAC[];
 250 DISCH_THEN (fun t-> REWRITE_TAC[t]);
 251 ASM_SIMP_TAC[REAL_FIELD `&0 < t ==> t pow 2 * &2 * x / t = t * &2 * x`];
 252 ASM_SIMP_TAC[REAL_FIELD `&0 < t ==> t pow 2 * (&1 - (x / t) pow 2) = t pow 2 - x pow 2`];
 253 EXPAND_TAC "t";
 254 REWRITE_TAC[REAL_FIELD `(a + &1) pow 2 = a pow 2 + &2 * a  + &1`];
 255 ASM_SIMP_TAC[pos1;REAL_ARITH `!x. &0 < x ==> &0 <= x`;SQRT_POW_2];
 256 ASM_REWRITE_TAC[REAL_ARITH `((&1 + v) + &2 * u + &1) - v = (u + &1) * &2`];
 257 UNDISCH_TAC `&0 < t`;
 258 CONV_TAC REAL_FIELD;
 259 ]
 260 (* }}} *));;
 261
 262 (* complex taylor for atn *)
 263
 264 prioritize_complex();;
 265
 266 let id1 = COMPLEX_RING `inv (Cx (&1) + z pow 2)   = (inv (Cx (&2))) * ( ( inv (Cx (&1) + z pow 2) * (Cx (&1) - ii *z)) +  (inv (Cx (&1) + z pow 2)) * ( (Cx (&1) + ii * z)))`;;
 267
 268 let id2 = SIMPLE_COMPLEX_ARITH  ` (Cx (&1) + ii * z) * (Cx (&1) - ii * z) = (Cx (&1) - ii * ii * z * z)`;;
 269
 270 let id3 = prove_by_refinement (`!u a. a - ii * ii * u = a + u`,
 271 (* {{{ proof *)
 272 [
 273 REWRITE_TAC[ii];
 274 SIMPLE_COMPLEX_ARITH_TAC;
 275 ]
 276 (* }}} *));;
 277
 278 let id4 = prove_by_refinement (`!z. (Cx (&1) + z pow 2) = (Cx (&1) + ii*z) * (Cx (&1) - ii*z)`,
 279 (* {{{ proof *)
 280 [
 281 REWRITE_TAC[id2;id3;COMPLEX_POW_2];
 282 ]
 283 (* }}} *));;
 284
 285
 286 let tactic_list = [SUBGOAL_THEN `(Re (z) = &0) /\ (abs(Im (z)) = &1)` ASSUME_TAC ;
 287 POP_ASSUM MP_TAC ;
 288 ASM_REWRITE_TAC[] ;
 289 REWRITE_TAC[REAL_ARITH `abs(x) = &1 <=> (x = &1 \/ x = -- &1)`;ii] ;
 290 SIMPLE_COMPLEX_ARITH_TAC ;
 291 ASM_MESON_TAC[]];;
 292
 293 let idz = prove_by_refinement(
 294   `!z a.  (Re z = &0 ==> abs(Im z) < &1) /\ ((a = ii \/ a = --ii))  ==>
 295      ~(Cx (&1) + a * z = Cx (&0))`,
 296   (* {{{ proof *)
 297   [
 298 ASSUME_TAC (REAL_ARITH `~(&1 < &1)`);
 299 REPEAT STRIP_TAC;
 300 ] @ (tactic_list @ tactic_list));;
 301   (* }}} *)
 302
 303
 304 let id4a = prove_by_refinement (`!z. (Re z = &0 ==> abs(Im z) < &1)
 305   ==>( inv(Cx (&1) + ii* z) * (Cx (&1)  + ii*z) = Cx (&1))`,
 306 (* {{{ proof *)
 307 [
 308 REPEAT STRIP_TAC;
 309 MATCH_MP_TAC COMPLEX_MUL_LINV;
 310 MATCH_MP_TAC idz;
 311 ASM_REWRITE_TAC[];
 312 ]
 313 (* }}} *));;
 314
 315 let id4b = prove_by_refinement (`!z. (Re z = &0 ==> abs(Im z) < &1)
 316   ==>( inv(Cx (&1) -  ii* z) * (Cx (&1)  - ii*z) = Cx (&1))`,
 317 (* {{{ proof *)
 318 [
 319 REPEAT STRIP_TAC;
 320 MATCH_MP_TAC COMPLEX_MUL_LINV;
 321 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a - ii * z = a + (-- ii) * z`];
 322 MATCH_MP_TAC idz;
 323 ASM_REWRITE_TAC[];
 324 ]
 325 (* }}} *));;
 326
 327 let id5 = prove_by_refinement (`!z. (Re z = &0 ==> abs(Im z) < &1) ==> ( inv (Cx (&1) + z pow 2) = (inv (Cx (&2))) * ( inv (Cx (&1) + ii * z) + inv (Cx (&1) - ii * z)))`,
 328 (* {{{ proof *)
 329 [
 330 REPEAT STRIP_TAC;
 331 ONCE_REWRITE_TAC[id1];
 332 REWRITE_TAC[id4;COMPLEX_INV_MUL];
 333 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `((a*b)*c + (e*f)*g = (a:complex)*(b*c) + f * (e *g))`];
 334 ASM_SIMP_TAC[id4a;id4b];
 335 REWRITE_TAC[COMPLEX_MUL_RID];
 336 ]
 337 (* }}} *));;
 338
 339 let taylor_coeff_catn = new_definition `taylor_coeff_catn n (z:complex) =
 340   if (n=0) then catn z else Cx (& (FACT (n-1))) *
 341    (inv(Cx (&2))) * ( ( (-- ii) pow (n - 1) * ((inv (Cx (&1) + ii * z)) pow n)) +
 342       ( ii pow (n - 1) * ((inv (Cx (&1) - ii * z)) pow n)))`;;
 343
 344 let taylor_coeff_catn0 = prove_by_refinement (
 345   `taylor_coeff_catn 0 = catn `,
 346 (* {{{ proof *)
 347  [
 348  ONCE_REWRITE_TAC[FUN_EQ_THM];
 349  REWRITE_TAC[taylor_coeff_catn];
 350  ]
 351 (* }}} *));;
 352
 353 let taylor_coeff_catn1 = prove_by_refinement (
 354    `!z.  (Re z = &0 ==> abs(Im z) < &1) ==>
 355        (catn has_complex_derivative (taylor_coeff_catn 1 z)) (at z)`,
 356 (* {{{ proof *)
 357   [
 358   REPEAT STRIP_TAC;
 359     SUBGOAL_THEN `taylor_coeff_catn 1 z = inv (Cx (&1) + z pow 2)` ASSUME_TAC;
 360   REWRITE_TAC[taylor_coeff_catn;ARITH_RULE `~(1=0) /\ (1-1 = 0) /\ (FACT 0 =1)`;COMPLEX_POW_1;complex_pow;COMPLEX_MUL_LID];
 361   ASM_SIMP_TAC[id5];
 362   (* *)
 363   ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_CATN;];
 364   ]
 365 (* }}} *));;
 366
 367 let taylor_coeff_catn_pos = prove_by_refinement(
 368   `!n. (n > 0) ==> (taylor_coeff_catn n  = (\z.
 369                 Cx (& (FACT (n-1))) *
 370    (inv(Cx (&2))) * ( ( (-- ii) pow (n - 1) * ((inv (Cx (&1) + ii * z)) pow n)) +
 371       ( ii pow (n - 1) * ((inv (Cx (&1) - ii * z)) pow n)))                       ))`,
 372 (* {{{ proof *)
 373   [
 374   REPEAT STRIP_TAC;
 375   ONCE_REWRITE_TAC[FUN_EQ_THM];
 376   REWRITE_TAC[taylor_coeff_catn];
 377   ASM_SIMP_TAC[ARITH_RULE `n > 0 ==> ~(n=0)`];
 378   ]
 379 (* }}} *));;
 380
 381 let taylor_series_inv_pow = prove_by_refinement(
 382   `!n a z. ~(Cx (&1) + a * z = Cx(&0)) ==>
 383    (((\z. (inv (Cx (&1) + a * z)) pow n) has_complex_derivative
 384       (-- Cx(&n) * a * (inv (Cx(&1) + a * z)) pow (n+1))) (at z))`,
 385   (* {{{ proof *)
 386
 387   [
 388   REPEAT STRIP_TAC;
 389   DISJ_CASES_TAC (ARITH_RULE `(n=0) \/ (n > 0)`);
 390   ASM_REWRITE_TAC[ARITH_RULE `0+1=1`;complex_pow;COMPLEX_POW_1;SIMPLE_COMPLEX_ARITH `-- Cx (&0) * u = Cx(&0)`;HAS_COMPLEX_DERIVATIVE_CONST];
 391   ASM_SIMP_TAC[ARITH_RULE `(n>0) ==> (n+1 = 2 + (n-1))`;];
 392   REWRITE_TAC[COMPLEX_POW_ADD];
 393   ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `-- r * s * t * u = r * u * ( -- s * t)`];
 394   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_POW_AT;
 395   REWRITE_TAC[COMPLEX_POW_INV;GSYM complex_div];
 396   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_INV_AT;
 397   ASM_REWRITE_TAC[];
 398   CONV_TAC (PATH_CONV "lr" (ONCE_REWRITE_CONV[SIMPLE_COMPLEX_ARITH `a = Cx(&0) + a * Cx (&1)` ]));
 399  MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_ADD;
 400   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_CONST];
 401   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT;
 402   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_ID];
 403   ]);;
 404
 405   (* }}} *)
 406
 407 let factorial_lemma = prove_by_refinement(
 408   `!n. (n>0) ==> (FACT n = n * FACT (n-1))`,
 409   (* {{{ proof *)
 410   [
 411 REPEAT STRIP_TAC;
 412 DISJ_CASES_TAC (ISPEC `n:num` num_CASES);
 413 ASM_MESON_TAC[ARITH_RULE `(n>0) ==> ~(n=0)`];
 414 ASM_MESON_TAC[FACT;ARITH_RULE `SUC n - 1 = n`];
 415   ]);;
 416   (* }}} *)
 417
 418 let taylor_coeff_catn_deriv = prove_by_refinement(
 419   `!z n. (Re z = &0 ==> abs(Im z) < &1) ==>
 420        ((taylor_coeff_catn n) has_complex_derivative
 421               (taylor_coeff_catn (n+1) z)) (at z)`,
 422 (* {{{ proof *)
 423 [
 424 REPEAT STRIP_TAC;
 425 DISJ_CASES_TAC (ARITH_RULE `(n = 0) \/ (n >0)`);
 426 ASM_SIMP_TAC[ taylor_coeff_catn0;taylor_coeff_catn1;ARITH_RULE `0+1=1`];
 427 REWRITE_TAC[taylor_coeff_catn;ARITH_RULE `(n+1)-1 = n`];
 428 ASM_SIMP_TAC[ARITH_RULE `(n>0) ==> ~(n+1=0)`];
 429 ASM_SIMP_TAC[taylor_coeff_catn_pos;factorial_lemma];
 430 (* fact finding *)
 431 SUBGOAL_THEN `!u. Cx (&(n * FACT (n-1))) * u = Cx (&n) * (Cx (&(FACT (n-1))) * u)` MP_TAC;
 432 REWRITE_TAC[CX_MUL;GSYM REAL_OF_NUM_MUL];
 433 SIMPLE_COMPLEX_ARITH_TAC;
 434 DISCH_THEN (fun t-> REWRITE_TAC[t]);
 435 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(a:complex) * b * c * d = b * c * a * d`];
 436 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(a:complex) * b * u = (a*b)*u`];
 437 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT;
 438 REWRITE_TAC[COMPLEX_ADD_LDISTRIB];
 439 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_ADD;
 440 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a - ii * z = a + (-- ii) * z`];
 441 SUBGOAL_THEN `!a b r. a * b pow n * r = b pow (n-1) * ( -- a * ( -- b) * r)` MP_TAC;
 442 REPEAT STRIP_TAC;
 443 MP_TAC(ARITH_RULE `n>0 ==> n = (n-1) + 1`);
 444 ASM_REWRITE_TAC[];
 445 DISCH_THEN   (fun t -> CONV_TAC (PATH_CONV "lr" (ONCE_REWRITE_CONV[t])));
 446 REWRITE_TAC[COMPLEX_POW_ADD;COMPLEX_POW_1];
 447 SIMPLE_COMPLEX_ARITH_TAC;
 448 DISCH_THEN (fun t->REWRITE_TAC[t]);
 449 CONJ_TAC THEN (MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT) ;
 450 (* highly parallel branches *)
 451 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `-- --ii = ii`];
 452 MATCH_MP_TAC  taylor_series_inv_pow;
 453 STRIP_TAC;
 454 ASM_MESON_TAC[idz];
 455 (* *)
 456 MATCH_MP_TAC  taylor_series_inv_pow;
 457 STRIP_TAC;
 458 ASM_MESON_TAC[idz];
 459 ]
 460 (* }}} *));;
 461
 462 let ipows2 = prove_by_refinement(
 463   `!n. (--ii ) pow (n + 2) = -- ((-- ii) pow n)`,
 464   (* {{{ proof *)
 465   [
 466   GEN_TAC;
 467   REWRITE_TAC[COMPLEX_POW_ADD;COMPLEX_POW_2;];
 468   MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `(a * a = -- Cx(&1) ) ==> r * a * a = -- r`);
 469   REWRITE_TAC[ii];
 470   SIMPLE_COMPLEX_ARITH_TAC;
 471   ]);;
 472   (* }}} *)
 473
 474 let ipowsc2 = prove_by_refinement(
 475   `!n. (ii ) pow (n + 2) = -- ((ii) pow n)`,
 476   (* {{{ proof *)
 477   [
 478   GEN_TAC;
 479   REWRITE_TAC[COMPLEX_POW_ADD;COMPLEX_POW_2;];
 480   MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `(a * a = -- Cx(&1) ) ==> r * a * a = -- r`);
 481   REWRITE_TAC[ii];
 482   SIMPLE_COMPLEX_ARITH_TAC;
 483   ]);;
 484   (* }}} *)
 485
 486
 487 let taylor_coeff0 = prove_by_refinement(
 488   `!n. (taylor_coeff_catn n (Cx (&0)) = if (EVEN n) then (Cx (&0)) else
 489     Cx (&(FACT (n-1))  * (-- &1) pow ((n - 1) DIV 2)))`,
 490   (* {{{ proof *)
 491   [
 492   GEN_TAC;
 493   DISJ_CASES_TAC (ISPEC `n:num` EVEN_OR_ODD);
 494    DISJ_CASES_TAC (ARITH_RULE `(n=0) \/ (n >0)`);
 495   ASM_REWRITE_TAC[taylor_coeff_catn;GSYM CX_ATN;ATN_0];
 496   (* *)
 497   ASM_SIMP_TAC[taylor_coeff_catn_pos];
 498   REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a + b * Cx(&0) = a /\ a - b * Cx(&0)  =a`];
 499   REWRITE_TAC[SIMPLE_COMPLEX_ARITH `inv(Cx (&1)) = Cx (&1) /\ a * Cx(&1) = a`;COMPLEX_POW_ONE];
 500   MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `c = Cx(&0) ==> a*b*c = Cx(&0)`);
 501   SUBGOAL_THEN (  `EVEN n  ==> (?k. (n - 1) = 2 * k + 1)`) MP_TAC;
 502   REWRITE_TAC[EVEN_EXISTS];
 503    REPEAT STRIP_TAC;
 504   EXISTS_TAC `m-1`;
 505   REPEAT (POP_ASSUM MP_TAC);
 506   ARITH_TAC;
 507   ASM_REWRITE_TAC[];
 508   REPEAT STRIP_TAC;
 509   ASM_REWRITE_TAC[];
 510   SPEC_TAC (`k:num`,`k:num`);
 511   INDUCT_TAC;
 512   REWRITE_TAC[ARITH_RULE `2* 0 + 1 = 1`;COMPLEX_POW_1];
 513   SIMPLE_COMPLEX_ARITH_TAC;
 514   ASM_REWRITE_TAC[ipows2;ipowsc2;ARITH_RULE `2* SUC k' + 1 = (2 * k' + 1) + 2`;SIMPLE_COMPLEX_ARITH `--a  + --b = --(a+b) /\ -- Cx(&0) = Cx(&0) `];
 515   (* ODD *)
 516   ASM_REWRITE_TAC[GSYM NOT_ODD];
 517   SUBGOAL_THEN (`ODD n ==> (?k. n = 2 * k + 1)`) MP_TAC;
 518   REWRITE_TAC[ODD_EXISTS];
 519   REPEAT STRIP_TAC;
 520   EXISTS_TAC `m:num`;
 521   ASM_REWRITE_TAC[];
 522   ARITH_TAC;
 523   ASM_REWRITE_TAC[];
 524    REPEAT STRIP_TAC;
 525    SUBGOAL_THEN `n > 0` ASSUME_TAC;
 526   POP_ASSUM MP_TAC;
 527   ARITH_TAC;
 528   ASM_SIMP_TAC[taylor_coeff_catn_pos];
 529   REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a + b * Cx (&0) = a /\ a - b * Cx (&0) = a /\ inv (Cx (&1)) = Cx (&1) /\ a * Cx (&1) = a`;COMPLEX_POW_ONE;ARITH_RULE `(2 * k + 1 ) - 1 = 2 * k`;CX_MUL];
 530   MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `(b = c) ==> (a*b = a*c)`);
 531   SPEC_TAC (`k:num`,`k:num`);
 532   INDUCT_TAC;
 533   REWRITE_TAC[ARITH_RULE `2 * 0 =0 /\ 0 DIV 2 = 0`;complex_pow;real_pow];
 534   SIMPLE_COMPLEX_ARITH_TAC;
 535   REWRITE_TAC[ARITH_RULE `2 * SUC k' = 2 * k' + 2 /\ (2 * SUC k) DIV 2 = ((2 * k) DIV 2) + 1`;SIMPLE_COMPLEX_ARITH `a * (-- b + -- c) = -- (a * (b+c))`;ipows2;ipowsc2;COMPLEX_POW_ADD;REAL_POW_ADD;CX_MUL;REAL_POW_1];
 536   ASM_REWRITE_TAC[];
 537   SIMPLE_COMPLEX_ARITH_TAC;
 538   ]);;
 539   (* }}} *)
 540
 541 let term_bound = prove_by_refinement(
 542   `!a n z.  Im (z) = &0 ==>
 543          norm((Cx(a)* ii) pow n * ((inv (Cx (&1) - Cx(a)* ii * z)) pow (n+1)))
 544   <= (abs a) pow n `,
 545   (* {{{ proof *)
 546   [
 547   REPEAT STRIP_TAC;
 548   REWRITE_TAC[COMPLEX_NORM_MUL;COMPLEX_NORM_II;COMPLEX_NORM_CX;COMPLEX_NORM_POW;COMPLEX_NORM_INV;REAL_ARITH `a * &1 = a`];
 549   MATCH_MP_TAC (MESON[REAL_LE_LMUL;REAL_ARITH `x = x* &1`]  ( `!x y. &0 <= x /\ y <= &1 ==> x *y <= x`)) ;
 550   CONJ_TAC;
 551   MATCH_MP_TAC REAL_POW_LE;
 552   REWRITE_TAC[REAL_ABS_POS];
 553   MATCH_MP_TAC (MESON[REAL_POW_LE2;REAL_POW_ONE] `!x. &0 <= x /\ x <= &1 ==> x pow n <= &1`);
 554   REWRITE_TAC[REAL_LE_INV_EQ;NORM_POS_LE];
 555   MATCH_MP_TAC (MESON[REAL_LE_INV2;REAL_INV_1;REAL_ARITH `&0 < &1`] `&1 <= x ==> inv (x) <= &1`);
 556   SUBGOAL_THEN `Im z = &0 ==> Cx(&1) - Cx a * ii * z = complex(&1, -- a * Re(z))` MP_TAC;
 557   REWRITE_TAC[ii];
 558   SIMPLE_COMPLEX_ARITH_TAC;
 559   ASM_REWRITE_TAC[];
 560   DISCH_THEN (fun t -> REWRITE_TAC[t]);
 561   (* *)
 562   MATCH_MP_TAC (MESON[REAL_ABS_REFL;REAL_LE_SQUARE_ABS;REAL_ARITH `&0 <= &1 /\ &1 pow 2 = &1`;NORM_POS_LE] `&1 <= norm x pow 2 ==> &1 <= norm x`);
 563   REWRITE_TAC[COMPLEX_SQNORM;RE;IM];
 564   MESON_TAC[REAL_LE_POW_2;REAL_ARITH `&1 pow 2 = &1 /\ (&0 <= t ==> &1 <= &1 + t)`];
 565   ]);;
 566   (* }}} *)
 567
 568 let taylor_error_bound = prove_by_refinement(
 569   `!n z. Im(z) = &0 ==> norm(taylor_coeff_catn (n+1) z) <= &(FACT n)`,
 570   (* {{{ proof *)
 571
 572   [
 573   REPEAT STRIP_TAC;
 574   SIMP_TAC[taylor_coeff_catn_pos;ARITH_RULE `(n+1)>0 /\ ((n+1)-1 = n)`];
 575   REWRITE_TAC[COMPLEX_NORM_MUL;COMPLEX_NORM_NUM;COMPLEX_NORM_INV];
 576   REWRITE_TAC[COMPLEX_NORM_NUM];
 577  MATCH_MP_TAC (MESON[REAL_LE_LMUL;REAL_ARITH `x = x* &1`]  ( `!x y. &0 <= x /\ y <= &1 ==> x *y <= x`)) ;
 578   CONJ_TAC;
 579   REWRITE_TAC[REAL_OF_NUM_LE];
 580   ARITH_TAC;
 581 MATCH_MP_TAC (REAL_ARITH `x <= &1 + &1 ==> inv (&2)* x <= &1`);
 582 MATCH_MP_TAC REAL_LE_TRANS;
 583 EXISTS_TAC `norm (--ii pow n * inv (Cx (&1) + ii * z) pow (n + 1)) + norm ( ii pow n * inv (Cx (&1) - ii * z) pow (n + 1))`;
 584 REWRITE_TAC[NORM_TRIANGLE];
 585 MATCH_MP_TAC REAL_LE_ADD2;
 586 (*  *)
 587 CONJ_TAC;
 588 (* FORCE_MATCH_MP_TAC *)
 589 FORCE_MATCH_MP_TAC (ISPECL [`-- &1`;`n:num`;`z:complex`] term_bound);
 590 ASM_REWRITE_TAC[];
 591 ONCE_REWRITE_TAC[FUN_EQ_THM];
 592 SIMPLE_COMPLEX_ARITH_TAC;
 593 SIMPLE_COMPLEX_ARITH_TAC;
 594 REWRITE_TAC[REAL_ABS_NEG;REAL_ABS_NUM;REAL_POW_ONE];
 595 (* second *)
 596 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `ii * z = Cx(&1) * ii * z`];
 597 FORCE_MATCH_MP_TAC (ISPECL [` &1`;`n:num`;`z:complex`] term_bound);
 598 ASM_REWRITE_TAC[];
 599 SIMPLE_COMPLEX_ARITH_TAC;
 600 REWRITE_TAC[REAL_ABS_NEG;REAL_ABS_NUM;REAL_POW_ONE];
 601   ]);;
 602
 603   (* }}} *)
 604
 605 let complex_taylor_catn = prove_by_refinement(
 606    ` !n s. (s = {z | Im (z) = &0 }) ==> (!z.
 607                   (Cx(&0)) IN s /\ z IN s
 608                   ==> norm
 609                       (catn z -
 610                        vsum (0..n)
 611                        (\i. taylor_coeff_catn i (Cx(&0)) * (z) pow i / Cx (&(FACT i)))) <=
 612                        norm (z) pow (n + 1) )`,
 613   (* {{{ proof *)
 614
 615   [
 616   GEN_TAC THEN GEN_TAC;
 617   DISCH_TAC;
 618   MP_TAC (SPECL[`taylor_coeff_catn`;`n:num`;`s:complex->bool`;`&(FACT n)`] COMPLEX_TAYLOR);
 619   ASM_REWRITE_TAC[IN_ELIM_THM];
 620   ANTS_TAC;
 621   REPEAT (CONJ_TAC THEN (REPEAT STRIP_TAC));
 622   REWRITE_TAC[convex;IN_ELIM_THM;IM_ADD;IM_CMUL];
 623   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
 624   REAL_ARITH_TAC;
 625   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_AT_WITHIN;
 626   MATCH_MP_TAC taylor_coeff_catn_deriv;
 627   ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
 628   (*  *)
 629   MATCH_MP_TAC taylor_error_bound;
 630   ASM_REWRITE_TAC[];
 631   DISCH_THEN (MP_TAC o (ISPEC `Cx (&0)`));
 632   REWRITE_TAC[taylor_coeff_catn0;SIMPLE_COMPLEX_ARITH `z - Cx (&0) = z /\ Im (Cx (&0)) = &0`];
 633   DISCH_THEN (fun t-> REPEAT STRIP_TAC THEN MP_TAC t) ;
 634   DISCH_THEN (MP_TAC o (ISPEC `z:complex`));
 635   DISCH_THEN FORCE_MATCH_MP_TAC;
 636   ASM_REWRITE_TAC[];
 637   MATCH_MP_TAC REAL_DIV_LMUL;
 638   REWRITE_TAC[REAL_OF_NUM_EQ];
 639   MESON_TAC[ FACT_LT;ARITH_RULE `0 < x ==> ~(x =0)`];
 640   ]);;
 641
 642   (* }}} *)
 643
 644 let real_axis = prove_by_refinement( (* not needed *)
 645   `!z.  (Im z = &0 <=> (?x. z = Cx(x)))`,
 646   (* {{{ proof *)
 647   [
 648   GEN_TAC;
 649   EQ_TAC;
 650   DISCH_TAC;
 651   EXISTS_TAC `(Re z)`;
 652   POP_ASSUM MP_TAC;
 653   SIMPLE_COMPLEX_ARITH_TAC;
 654   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[IM_CX];
 655   ]);;
 656   (* }}} *)
 657
 658 let THREAD_IF = prove_by_refinement(
 659   `!x y z f. (f:A->B) (if x then y else z) = if x then f y else f z`,
 660   (* {{{ proof *)
 661   [
 662   REPEAT GEN_TAC;
 663   BOOL_CASES_TAC `x:bool` THEN REWRITE_TAC[];
 664   ]);;
 665   (* }}} *)
 666
 667
 668 let real_taylor_atn_ver1 = prove_by_refinement(
 669   `!n x.  abs(atn x - sum (0..n) (\i. if EVEN i then &0 else ( -- &1 pow ((i-1) DIV 2)  *      x pow i / &i ))) <= abs(x) pow (n+1)`,
 670   (* {{{ proof *)
 671   [
 672   REPEAT GEN_TAC;
 673   MP_TAC (ISPECL [`n:num`;`{ z | Im(z) = &0 }`] complex_taylor_catn);
 674   REWRITE_TAC[];
 675   DISCH_THEN (fun t -> MP_TAC (ISPEC `Cx (x)` t));
 676   REWRITE_TAC[VSUM_CX_NUMSEG;COMPLEX_NORM_CX;GSYM CX_SUB;GSYM CX_POW;IN_ELIM_THM;GSYM CX_MUL;GSYM CX_DIV;GSYM CX_ATN;IM_CX;taylor_coeff0;GSYM THREAD_IF];
 677   FORCE_MATCH;
 678  ONCE_REWRITE_TAC[FUN_EQ_THM];
 679   X_GEN_TAC `i:num`;
 680   BETA_TAC;
 681   DISJ_CASES_TAC (TAUT `EVEN i \/ ~(EVEN i)`) THEN ASM_REWRITE_TAC[];
 682   REAL_ARITH_TAC;
 683   POP_ASSUM MP_TAC;
 684   REWRITE_TAC[NOT_EVEN;ODD_EXISTS];
 685   REPEAT STRIP_TAC;
 686   ASM_REWRITE_TAC[ARITH_RULE `SUC x - 1 = x`;FACT;GSYM REAL_OF_NUM_MUL ];
 687   ONCE_REWRITE_TAC[REAL_FIELD `((a:real) * b) * c/(d*a) = (b * c/d) * (a/a)`];
 688   MATCH_MP_TAC (REAL_FIELD `x = &1 ==> (y * x = y)`);
 689   MATCH_MP_TAC REAL_DIV_REFL;
 690   REWRITE_TAC[REAL_OF_NUM_EQ];
 691   MESON_TAC[FACT_LT;ARITH_RULE `0 < x ==> ~(x = 0)`];
 692   ]);;
 693   (* }}} *)
 694
 695 let sum_odd  = prove_by_refinement(
 696   `!(g:num->real) n. sum { i | ODD i /\ i IN 0.. 2 * n + 2 } g =   sum (0.. n) (\i. g (2 * i +1))`,
 697   (* {{{ proof *)
 698   [
 699   REPEAT STRIP_TAC;
 700   FORCE_MATCH_MP_TAC (ISPECL [`\i. (2 * i + 1)`; `g:num->real`;`(0..n)`] SUM_IMAGE);
 701   BETA_TAC;
 702   ARITH_TAC;
 703   REWRITE_TAC[IMAGE;numseg;IN_ELIM_THM;ODD_EXISTS];
 704   ONCE_REWRITE_TAC[FUN_EQ_THM];
 705   REWRITE_TAC[IN_ELIM_THM];
 706   GEN_TAC;
 707   EQ_TAC;
 708   REPEAT STRIP_TAC;
 709   EXISTS_TAC `x':num`;
 710   POP_ASSUM MP_TAC;
 711   ARITH_TAC;
 712   REPEAT (POP_ASSUM MP_TAC);
 713   ARITH_TAC;
 714   REPEAT (POP_ASSUM MP_TAC);
 715   ARITH_TAC;
 716   REPEAT STRIP_TAC;
 717   EXISTS_TAC `m:num`;
 718   REPEAT (POP_ASSUM MP_TAC);
 719   ARITH_TAC;
 720   ONCE_REWRITE_TAC[FUN_EQ_THM;];
 721   REWRITE_TAC[o_THM]]
 722   (* }}} *)
 723 );;
 724
 725 let sum_even = prove_by_refinement(
 726   `!g n. sum {i | ODD i /\ i IN 0..n } (\i. if EVEN i then &0 else g i) = sum (0..n) (\i. if EVEN i then &0 else g i)`,
 727   (* {{{ proof *)
 728   [
 729   REPEAT GEN_TAC;
 730   ONCE_REWRITE_TAC [MESON[] `x = y <=> y = x`];
 731   FORCE_MATCH_MP_TAC (ISPECL [`(\i. if EVEN i then &0 else (g i))`;`{i | ODD i /\ i IN 0..n}`;`(0..n)`] SUM_SUPERSET);
 732   REPEAT STRIP_TAC;
 733   SET_TAC[];
 734   REPEAT (POP_ASSUM MP_TAC);
 735   REWRITE_TAC[IN_ELIM_THM;numseg];
 736   MESON_TAC[NOT_ODD];
 737   REWRITE_TAC[];
 738   ]);;
 739   (* }}} *)
 740
 741 let real_taylor_atn = prove_by_refinement(
 742   `!n x. abs(atn x - sum (0..n) (\j. (-- &1 pow j) * x pow (2 * j + 1)/ &(2 * j+ 1))) <= abs(x) pow (2 * n + 3)`,
 743   (* {{{ proof *)
 744   [
 745   REPEAT STRIP_TAC;
 746   MP_TAC (ISPECL [`2*n + 2`;`x:real`] real_taylor_atn_ver1);
 747   REWRITE_TAC[ARITH_RULE `(2*n + 2) +1 = 2 *n + 3`];
 748   REWRITE_TAC[GSYM sum_even];
 749   REWRITE_TAC[sum_odd];
 750   SUBGOAL_THEN `!i. ~(EVEN (2 *i + 1))` MP_TAC;
 751   MP_TAC NOT_EVEN;
 752   REWRITE_TAC[EVEN_EXISTS;ODD_EXISTS;ARITH_RULE `!m. SUC (m) = m+1`];
 753    MESON_TAC[];
 754   DISCH_TAC;
 755   ASM_REWRITE_TAC[];
 756   REWRITE_TAC[ARITH_RULE `((2 * i + 1) - 1) DIV 2 = i`];
 757   ]);;
 758   (* }}} *)
 759
 760 let halfatn4 = new_definition `halfatn4 = halfatn o halfatn o halfatn o halfatn`;;
 761
 762 let real_taylor_atn_halfatn4 = prove_by_refinement(
 763   `!n x. abs (atn(halfatn4 x) - sum (0..n) (\j. (-- &1 pow j) * halfatn4 x pow (2 * j + 1)/ &(2 * j+ 1))) <= inv (&8 pow (2 * n + 3))`,
 764   (* {{{ proof *)
 765   [
 766   REPEAT STRIP_TAC;
 767   MATCH_MP_TAC REAL_LE_TRANS;
 768   EXISTS_TAC `abs(halfatn4 x) pow (2 * n + 3)`;
 769   REWRITE_TAC[real_taylor_atn;REAL_INV_POW];
 770   MATCH_MP_TAC Real_ext.REAL_PROP_LE_POW;
 771   REWRITE_TAC[REAL_ABS_POS;halfatn4;o_THM];
 772   MATCH_MP_TAC (REAL_ARITH `x < y ==> x <= y`);
 773   MP_TAC (ISPEC `x:real` halfatn_bounds_abs);
 774   REPLICATE_TAC 3(  DISCH_THEN (fun t-> MP_TAC (MATCH_MP halfatn_half t)));
 775   FORCE_MATCH;
 776   CONV_TAC REAL_FIELD;
 777   ]);;
 778   (* }}} *)
 779
 780 let atn_halfatn4 = prove_by_refinement(
 781   `!x. atn x = &16 * atn(halfatn4 x)`,
 782   (* {{{ proof *)
 783   [
 784   ONCE_REWRITE_TAC[REAL_ARITH `&16 * x = &2 * &2 * &2 * &2 * x`];
 785   REWRITE_TAC[halfatn4;o_THM;GSYM atn_half];
 786   ]);;
 787   (* }}} *)
 788
 789 let real_taylor_atn_halfatn4_a = prove_by_refinement(
 790   `!n x. abs (atn x - &16 * sum (0..n) (\j. (-- &1 pow j) * halfatn4 x pow (2 * j + 1)/ &(2 * j+ 1))) <= inv (&2 pow (6 * n + 5 ))`,
 791   (* {{{ proof *)
 792   [
 793   REPEAT GEN_TAC;
 794   ONCE_REWRITE_TAC [atn_halfatn4];
 795   REWRITE_TAC[REAL_ARITH `abs (&16 * x - &16 * y) <=  z <=> abs(x - y) <= z *inv (&2 pow 4)`];
 796   MP_TAC (ISPECL [`n:num`;`x:real`]  real_taylor_atn_halfatn4);
 797   FORCE_MATCH;
 798   REWRITE_TAC[GSYM REAL_INV_MUL;GSYM REAL_POW_ADD;REAL_ARITH `&8 = &2 pow 3`;REAL_POW_POW];
 799   REPEAT AP_TERM_TAC;
 800   ARITH_TAC;
 801   ]);;
 802   (* }}} *)
 803
 804 let halfatn4_co = new_definition `halfatn4_co x j =  (-- &1 pow j) * halfatn4 x pow (2 * j + 1)/ &(2 * j+ 1)`;;
 805
 806 let atn_bounds_anti = prove_by_refinement(
 807   `!x y. x <= y  ==> abs(atn x - atn y) <= abs(x - y)`,
 808   (* {{{ proof *)
 809   [
 810   REPEAT STRIP_TAC;
 811   MP_TAC (ISPECL [`atn`;`(\t. inv(&1 + t pow 2))`;`x:real`;`y:real`] REAL_MVT_VERY_SIMPLE);
 812   REWRITE_TAC[real_interval;IN_ELIM_THM];
 813   ANTS_TAC;
 814   ASM_REWRITE_TAC[];
 815   REPEAT STRIP_TAC;
 816   MATCH_MP_TAC HAS_REAL_DERIVATIVE_ATREAL_WITHIN;
 817   REWRITE_TAC[HAS_REAL_DERIVATIVE_ATN];
 818   REPEAT STRIP_TAC;
 819   ONCE_REWRITE_TAC[REAL_ARITH `abs(y - x) = abs(x-y)`];
 820   ASM_REWRITE_TAC[];
 821   REWRITE_TAC[REAL_ABS_MUL];
 822   FORCE_MATCH_MP_TAC (ISPECL [`abs(inv (&1 + x' pow 2))`;`&1`;`abs(y-x)`] REAL_LE_RMUL);
 823   REWRITE_TAC[REAL_ABS_POS;REAL_ABS_INV];
 824  FORCE_MATCH_MP_TAC (ISPECL [`&1`;`abs(&1 + x' pow 2)`] REAL_LE_INV2);
 825   CONJ_TAC THEN TRY(REAL_ARITH_TAC);
 826   MP_TAC (ISPEC `x':real` pos1);
 827   SIMP_TAC [REAL_ARITH `(&0 < x ==> (abs x = x)) /\  (&1 <= &1 + u <=> &0 <= u)`;REAL_LE_POW_2];
 828  REAL_ARITH_TAC;
 829  REAL_ARITH_TAC;
 830   ]);;
 831   (* }}} *)
 832
 833 prioritize_real();;
 834
 835 let atn_bounds = prove_by_refinement(
 836   `!x y. abs(atn x - atn y) <= abs(x-y)`,
 837   (* {{{ proof *)
 838   [
 839   REPEAT STRIP_TAC;
 840   DISJ_CASES_TAC (REAL_ARITH `x<= y \/ y <= x`);
 841   ASM_SIMP_TAC[atn_bounds_anti];
 842   ONCE_REWRITE_TAC[REAL_ARITH `abs(x -y) = abs(y-x)`];
 843   ASM_SIMP_TAC[atn_bounds_anti];
 844   ]);;
 845   (* }}} *)
 846
 847
 848 (*
 849 let real_taylor_atn_approx = prove_by_refinement(
 850   `!n x u v eps1 eps2 eps3 eps.
 851      abs(x - u ) <= eps1 /\
 852     inv (&2 pow (6 * n + 5)) <= eps2 /\
 853     abs(&16 *sum (0..n) (halfatn4_co u) - v )<= eps3 /\
 854    (eps1 + eps2 + eps3 <= eps) ==>
 855    abs(atn(x) - v) <= eps`,
 856   (* {{{ proof *)
 857   [
 858   REPEAT STRIP_TAC;
 859     MATCH_MP_TAC REAL_LE_TRANS;
 860   EXISTS_TAC `(eps1:real) + eps2 + eps3`;
 861   ASM_REWRITE_TAC[];
 862   MATCH_MP_TAC REAL_LE_TRANS;
 863   ABBREV_TAC `r = &16 * sum(0..n) (halfatn4_co u)`;
 864   EXISTS_TAC`  abs(atn x - atn u) +abs(atn u - r) + abs(r - v)`;
 865   CONJ_TAC;
 866   CONV_TAC (PATH_CONV "l" (ONCE_REWRITE_CONV[REAL_ARITH `atn x - v = (atn x - atn u) + (atn u - r) +  (r - v)`]));
 867   MATCH_MP_TAC REAL_LE_TRANS;
 868   EXISTS_TAC `abs(atn x - atn u) + abs(atn u - r + r - v)`;
 869   REWRITE_TAC[REAL_ABS_TRIANGLE;REAL_ARITH `(x:real) + y <= x + z <=> y <= z`];
 870   MATCH_MP_TAC (REAL_ARITH `a1 <= b1 /\ a2 <= b2 /\ a3 <= b3 ==> a1 + a2 + a3 <= b1 + b2 + b3`);
 871   ASM_REWRITE_TAC[];
 872   CONJ_TAC;
 873   MATCH_MP_TAC REAL_LE_TRANS;
 874   EXISTS_TAC `abs(x - u)`;
 875   ASM_REWRITE_TAC[atn_bounds];
 876   MATCH_MP_TAC REAL_LE_TRANS;
 877   EXISTS_TAC `inv(&2 pow (6 * n + 5))`;
 878   ASM_REWRITE_TAC[];
 879   EXPAND_TAC "r";
 880   MP_TAC (ISPECL [`n:num`;`u:real`] real_taylor_atn_halfatn4_a);
 881   FORCE_MATCH;
 882   REWRITE_TAC[FUN_EQ_THM;halfatn4_co];
 883   ]);;
 884   (* }}} *)
 885 *)
 886
 887 let real_taylor_atn_approx = prove_by_refinement(
 888   `!n x  v eps1 eps2 eps.
 889     inv (&2 pow (6 * n + 5)) <= eps1 /\
 890     abs(&16 *sum (0..n) (halfatn4_co x) - v )<= eps2 /\
 891    (eps1 + eps2 <= eps) ==>
 892    abs(atn(x) - v) <= eps`,
 893   (* {{{ proof *)
 894   [
 895   REPEAT STRIP_TAC;
 896     MATCH_MP_TAC REAL_LE_TRANS;
 897   EXISTS_TAC `( eps1:real) + eps2`;
 898   ASM_REWRITE_TAC[];
 899   MATCH_MP_TAC REAL_LE_TRANS;
 900   ABBREV_TAC `r = &16 * sum(0..n) (halfatn4_co x)`;
 901   EXISTS_TAC`abs(atn x - r) + abs(r - v)`;
 902   CONJ_TAC;
 903   MESON_TAC[REAL_ABS_TRIANGLE;REAL_ARITH `atn x - v = (atn x - r) + r - v`];
 904  MATCH_MP_TAC (REAL_ARITH `a1 <= b1 /\ a2 <= b2  ==> a1 + a2  <= b1 + b2`);
 905  ASM_REWRITE_TAC[];
 906   MATCH_MP_TAC REAL_LE_TRANS;
 907   EXISTS_TAC `inv(&2 pow (6 * n + 5))`;
 908   ASM_REWRITE_TAC[];
 909   EXPAND_TAC "r";
 910   MP_TAC (ISPECL [`n:num`;`x:real`] real_taylor_atn_halfatn4_a);
 911   FORCE_MATCH;
 912   REWRITE_TAC[FUN_EQ_THM;halfatn4_co];
 913   ]);;
 914   (* }}} *)
 915
 916
 917 end;;