text_formalization/jordan/taylor_atn.hl

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