text_formalization/trigonometry/euler_multivariate.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*          COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA                       *)
   4 (*                                                                           *)
   5 (*                  LEMMA ABOUT DERIVATIVES                                  *)
   6 (*                                                                           *)
   7 (*      Authour : VU KHAC KY                                                 *)
   8 (*                                                                           *)
   9 (* ========================================================================= *)
  10
  11 flyspeck_needs "trigonometry/euler_complement.hl";;
  12
  13 module Euler_multivariate = struct
  14
  15 open Sphere;;
  16 open Trigonometry1;;
  17 open Trigonometry2;;
  18 open Prove_by_refinement;;
  19 open Delta_x;;
  20 open Euler_complement;;
  21
  22 (* ========================================================================= *)
  23 (*                                                                           *)
  24 (*                    SOME NECESSARY LEMMAS                                  *)
  25 (*                                                                           *)
  26 (* ========================================================================= *)
  27
  28 (* ========================================================================= *)
  29 (*         LEMMA 1                                                           *)
  30 (* ========================================================================= *)
  31
  32 let REDUCE_WITH_DIV_Euler_lemma = prove_by_refinement
  33  (`!x y z . ~ (y = &0) /\ ~ (z = &0) ==> x * y / (z * y) = x / z`,
  34 [ (REPEAT STRIP_TAC);
  35  (MATCH_MP_TAC REAL_EQ_LCANCEL_IMP);
  36  (EXISTS_TAC `z:real`);
  37  (ASM_REWRITE_TAC[]);
  38  (REWRITE_TAC[REAL_ARITH `a * b * c = (a * c) * b`]);
  39
  40   (SUBGOAL_THEN `z * x / z = x` ASSUME_TAC);
  41   (MATCH_MP_TAC REAL_DIV_LMUL);
  42   (ASM_REWRITE_TAC[]);
  43
  44  (PURE_ONCE_ASM_REWRITE_TAC[]);
  45  (MATCH_MP_TAC (MESON[REAL_MUL_LID] `a = &1 ==> a * b = b`));
  46  (REWRITE_TAC[REAL_ARITH `a * b / c = (a * b) / c`]);
  47  (MATCH_MP_TAC REAL_DIV_REFL);
  48  (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
  49  (ASM_REWRITE_TAC[])]);;
  50
  51
  52 (* ========================================================================= *)
  53 (*         LEMMAS MODIFIED FROM j.HARRISON FILES                             *)
  54 (* ========================================================================= *)
  55
  56 let HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 = prove (
  57
  58 `!f a b c s.
  59          is_realinterval s /\ (a IN s) /\
  60          (!x. x IN s ==> (f has_real_derivative &0) (atreal x within s))  /\
  61          (f a = c )
  62          ==> (!x. x IN s ==> f x = c)`,
  63   MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT THEN
  64   MESON_TAC[]);;
  65
  66 (* ------------------------------------------------------------------------- *)
  67
  68 let HAS_REAL_DERIVATIVE_CHAIN2 = prove
  69   (`!P f g x s.
  70       (!x. P x ==> (g has_real_derivative g' x) (atreal x))
  71       ==> ((f has_real_derivative f') (atreal x within s) /\ P (f x))
  72                ==> ((\x. g (f x)) has_real_derivative f' * g' (f x))
  73                    (atreal x within s) `,
  74    REPEAT GEN_TAC THEN
  75    MP_TAC HAS_REAL_DERIVATIVE_CHAIN THEN
  76    MESON_TAC[]);;
  77
  78 (* ========================================================================= *)
  79 (*         LEMMAS ABOUT INTERVALS                                            *)
  80 (* ========================================================================= *)
  81
  82
  83 let INTERVAL_DIVIDE_Euler_lemma = prove_by_refinement
  84  (`!c. &0 < (&4 - c) * c ==> &0 < c /\ c < &4`,
  85 [(REPEAT STRIP_TAC);
  86
  87   (MATCH_MP_TAC (REAL_ARITH `~(&0 <= -- x) ==> &0 < x`));
  88   STRIP_TAC;
  89     (SUBGOAL_THEN `(&4 - c) * (-- c) < &0` ASSUME_TAC);
  90     ASM_REAL_ARITH_TAC;
  91     (SUBGOAL_THEN `&0 <= (&4 - c) * (-- c)` ASSUME_TAC);
  92     (MATCH_MP_TAC REAL_LE_MUL);
  93     (ASM_REWRITE_TAC[]);
  94     ASM_REAL_ARITH_TAC;
  95   ASM_REAL_ARITH_TAC;
  96
  97   (MATCH_MP_TAC (REAL_ARITH `~(&0 <= x - &4) ==> x < &4`));
  98   STRIP_TAC;
  99     (SUBGOAL_THEN `(c - &4) * c < &0` ASSUME_TAC);
 100     ASM_REAL_ARITH_TAC;
 101     (SUBGOAL_THEN `&0 <= (c - &4) * c` ASSUME_TAC);
 102     (MATCH_MP_TAC REAL_LE_MUL);
 103     (ASM_REWRITE_TAC[]);
 104     ASM_REAL_ARITH_TAC;
 105   ASM_REAL_ARITH_TAC]);;
 106
 107 (* ---------------------------------------------------------------------------*)
 108
 109 let SQRT_RULE_Euler_lemma = prove
 110  (`!x y. x pow 2 = y /\ &0 <= x ==> x = sqrt y`,
 111  REPEAT STRIP_TAC THEN
 112  REWRITE_TAC[GSYM (ASSUME `x pow 2 = y`);REAL_POW_2] THEN
 113  ASM_SIMP_TAC[SQRT_MUL] THEN
 114  ASM_MESON_TAC[GSYM REAL_POW_2;SQRT_POW_2]);;
 115
 116
 117 let REAL_INTERVAL_Euler_lemma = prove
 118 ( `!a b.  let P1 = {x| x < a} in
 119           let P2 = {x| a < x} in
 120           let P3 = {x| a < x /\ x < b} in
 121         is_realinterval P1 /\ is_realinterval P2 /\ is_realinterval P3`,
 122  REPEAT GEN_TAC THEN
 123  REPEAT LET_TAC THEN
 124  EXPAND_TAC "P1" THEN EXPAND_TAC "P2" THEN EXPAND_TAC "P3" THEN
 125  REWRITE_TAC[is_realinterval] THEN
 126  REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 127
 128 (* ========================================================================= *)
 129 (*         FIRST LEMMA ABOUT DERIVATIVE                                      *)
 130 (* ========================================================================= *)
 131
 132
 133 let DERIVATIVE_WRT_C1_Euler_lemma = prove_by_refinement (
 134
 135  `!P. is_realinterval P /\ (&2) IN P /\
 136    (!x. x IN P ==> ~ (x = &0) /\ ~ (&4 - x = &0)) ==>
 137    (!c. c IN P ==> --pi / &2 - &2 * atn (&1 - c / &2) +
 138                   &2 * atn ((&4 - c) / c) = &0) `,
 139
 140 [ (GEN_TAC THEN STRIP_TAC);
 141  (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 THEN EXISTS_TAC `&2`);
 142  (ASM_REWRITE_TAC[]);
 143  (REWRITE_TAC[REAL_ARITH `&1 - &2 / &2 = &0`;ATN_0]);
 144  (REWRITE_TAC[REAL_ARITH
 145    `(--a / &2 - &2 * &0 + &2 * s = &0) <=> s = a / &4`]);
 146  (REWRITE_TAC[REAL_ARITH `(&4 - &2) / &2 = &1`;ATN_1]);
 147  (GEN_TAC THEN STRIP_TAC);
 148
 149    (SUBGOAL_THEN `~(c = &0) /\ ~(&4 - c = &0)` ASSUME_TAC);
 150     (* Subgoal 1 *)
 151    (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
 152    (UP_ASM_TAC THEN STRIP_TAC);
 153
 154  (ABBREV_TAC
 155   `f = (\c. --pi / &2 - &2 * atn (&1 - c / &2) + &2 * atn ((&4 - c) / c))`);
 156  (ABBREV_TAC `F1 = (\c. atn (&1 - c / &2))`);
 157  (ABBREV_TAC `F2 = (\c. atn ((&4 - c) / c))`);
 158
 159    (SUBGOAL_THEN
 160     `f = (\c:real. --pi / &2 - &2 * F1 c + &2 * F2 c)` ASSUME_TAC);
 161     (* Subgoal 2 *)
 162    (EXPAND_TAC "f" THEN EXPAND_TAC "F1" THEN EXPAND_TAC "F2");
 163    (MESON_TAC[]);
 164
 165  (ASM_REWRITE_TAC[] THEN DEL_TAC);
 166  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
 167
 168    (SUBGOAL_THEN
 169     `!c. (:real) c ==> (atn has_real_derivative (g':real->real) c) (atreal c)`
 170      ASSUME_TAC);
 171     (* Subgoal 3 *)
 172    (EXPAND_TAC "g'");
 173    (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (*    Compute the derivative of F1                                           *)
 177 (* ------------------------------------------------------------------------- *)
 178
 179  (ABBREV_TAC `f1 = (\c. &1 - c / &2)`);
 180
 181    (SUBGOAL_THEN `F1 = (\c:real.  atn (f1 c))` ASSUME_TAC);
 182     (* Subgoal 4 *)
 183    (EXPAND_TAC "F1" THEN EXPAND_TAC "f1" THEN MESON_TAC[]);
 184
 185    (SUBGOAL_THEN
 186     `(F1 has_real_derivative (-- &1 / &2) * g' ((f1:real -> real) c))
 187      (atreal c within P)` ASSUME_TAC);
 188     (* Subgoal 5 *)
 189    (ONCE_ASM_REWRITE_TAC[]);
 190
 191      (SUBGOAL_THEN
 192       `(f1 has_real_derivative -- &1 / &2) (atreal c within P) /\
 193        (:real) (f1 c)` ASSUME_TAC);
 194       (* Subgoal 5.1 *)
 195      CONJ_TAC;  (* break into 2 subgoal 5.1.1 & 5.1.2 *)
 196        (EXPAND_TAC "f1" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC); (*End 5.1.1*)
 197        (MESON_TAC[EQ_UNIV;IN_UNIV; IN]); (* End 5.1.2 *)
 198        (* End subgoal 5.1 *)
 199
 200    (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC);
 201    (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
 202    (MESON_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 203     (* End subgoal 5 *)
 204
 205    (SUBGOAL_THEN
 206     `-- &1 / &2 / (&2 - c + c * c / &4) = -- &1 / &2 * g' ((f1:real -> real) c)`
 207      ASSUME_TAC);
 208     (* Subgoal 6 *)
 209    (EXPAND_TAC "g'" THEN EXPAND_TAC "f1");
 210    (REWRITE_TAC[REAL_ARITH
 211     `&1 + (&1 - c / &2) pow 2 = &2 - c + c * c / &4`]);
 212    (ABBREV_TAC `m = -- &1 / &2`);
 213    (ABBREV_TAC `n = (&2 - c + c * c / &4)`);
 214
 215      (SUBGOAL_THEN `m = (m * inv n) * n  ==> (m / n = m * inv n)` ASSUME_TAC);
 216      (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (b ==> a)`));
 217      (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 218      (EXPAND_TAC "n");
 219      (REWRITE_TAC[REAL_ARITH
 220      `&2 - c + c * c / &4 = &1 + (&1 - c / &2) pow 2 `]);
 221      (MATCH_MP_TAC (REAL_ARITH `&0 <= a ==> &0 < &1 + a`));
 222      (REWRITE_TAC[REAL_LE_POW_2]);
 223
 224    (FIRST_X_ASSUM MATCH_MP_TAC);
 225    (REWRITE_TAC[GSYM REAL_MUL_ASSOC]);
 226    (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> a = a * x`));
 227    (MATCH_MP_TAC REAL_MUL_LINV);
 228    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
 229    (EXPAND_TAC "n");
 230    (REWRITE_TAC[REAL_ARITH
 231     `&2 - c + c * c / &4 = &1 + (&1 - c / &2) pow 2 `]);
 232    (MATCH_MP_TAC (REAL_ARITH `&0 <= a ==> &0 < &1 + a`));
 233    (REWRITE_TAC[REAL_LE_POW_2]);
 234
 235    (SUBGOAL_THEN
 236     `(F1 has_real_derivative -- &1 / &2 / (&2 - c + c * c / &4))
 237      (atreal c within P)` ASSUME_TAC);
 238     (* Subgoal 7 *)
 239    (ASM_MESON_TAC[]);
 240
 241  (UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC THEN REPEAT DISCH_TAC);
 242  SWITCH_TAC;
 243
 244 (* ------------------------------------------------------------------------- *)
 245 (*    Compute the derivative of F2                                           *)
 246 (* ------------------------------------------------------------------------- *)
 247
 248  (ABBREV_TAC `f2 = (\c. (&4 - c) / c)`);
 249
 250    (SUBGOAL_THEN `F2 = (\c:real.  atn (f2 c))` ASSUME_TAC);
 251     (* Subgoal 8 *)
 252    (EXPAND_TAC "F2" THEN EXPAND_TAC "f2" THEN MESON_TAC[]);
 253
 254    (SUBGOAL_THEN
 255     `(F2 has_real_derivative (-- &4 / (c * c)) * g' ((f2:real -> real) c))
 256      (atreal c within P)` ASSUME_TAC);
 257     (* Subgoal 9 *)
 258    (ONCE_ASM_REWRITE_TAC[]);
 259
 260      (SUBGOAL_THEN
 261       `(f2 has_real_derivative (-- &4 / (c * c))) (atreal c within P) /\
 262        (:real) (f2 c)` ASSUME_TAC);
 263       (* Subgoal 9.1 *)
 264      CONJ_TAC;  (* Break into 2 subgoals *)
 265
 266        (EXPAND_TAC "f2" THEN REAL_DIFF_TAC);
 267        (ASM_REWRITE_TAC[]);
 268        (REWRITE_TAC[REAL_POW_2]);
 269        (AP_THM_TAC THEN AP_TERM_TAC);
 270        REAL_ARITH_TAC;
 271        (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
 272
 273    (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC);
 274    (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
 275    (MESON_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 276
 277    (SUBGOAL_THEN
 278     `-- &1 / &2 / (&2 - c + c * c / &4) =
 279      -- &4 / (c * c) * g' ((f2:real -> real) c)` ASSUME_TAC);
 280     (* Subgoal 10 *)
 281    (EXPAND_TAC "g'" THEN EXPAND_TAC "f2");
 282    (REWRITE_TAC[REAL_POW_DIV]);
 283
 284      (SUBGOAL_THEN
 285       `&1 + (&4 - c) pow 2 / c pow 2 = (&16 - &8 * c + &2 * c * c) / (c * c)`
 286       ASSUME_TAC);
 287      (REWRITE_TAC[REAL_ARITH
 288       `(&16 - &8 * c + &2 * c * c) = c * c + (&4 - c) pow 2`]);
 289      (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
 290      (REWRITE_TAC[REAL_POW_2]);
 291      (AP_THM_TAC THEN AP_TERM_TAC);
 292      (REWRITE_TAC[EQ_SYM_EQ]);
 293      (MATCH_MP_TAC (REAL_DIV_REFL));
 294      (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(x \/ y) <=> ~ x /\ ~ y`]);
 295      (ASM_REWRITE_TAC[]);
 296
 297    (ASM_REWRITE_TAC[]);
 298    (REWRITE_TAC[REAL_INV_DIV]);
 299    (REWRITE_TAC[REAL_ARITH `t / x * y / z = (y / x) * (t / z)`]);
 300
 301      (SUBGOAL_THEN `(c * c) / (c * c) = &1` ASSUME_TAC);
 302      (MATCH_MP_TAC (REAL_DIV_REFL));
 303      (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(x \/ y) <=> ~ x /\ ~ y`]);
 304      (ASM_REWRITE_TAC[]);
 305
 306    (ASM_REWRITE_TAC[REAL_MUL_LID]);
 307    (REWRITE_TAC[REAL_ARITH
 308     `&16 - &8 * c + &2 * c * c = (&2 - c + c * c / &4) * &8`]);
 309    (REWRITE_TAC[REAL_ARITH `-- &4 = (-- &1 / &2) * &8`]);
 310    (REWRITE_TAC[EQ_SYM_EQ]);
 311
 312    (ABBREV_TAC `m = -- &1 / &2`);
 313    (ABBREV_TAC `n = (&2 - c + c * c / &4)`);
 314    (REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]);
 315    (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
 316    (REWRITE_TAC[REAL_ARITH `~ (&8 = &0)`]);
 317    (EXPAND_TAC "n");
 318    (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
 319    (REWRITE_TAC[REAL_ARITH
 320      `&2 - c + c * c / &4 = &1 + (&1 - c / &2) pow 2 `]);
 321    (MATCH_MP_TAC (REAL_ARITH `&0 <= a ==> &0 < &1 + a`));
 322    (REWRITE_TAC[REAL_LE_POW_2]);
 323
 324    (SUBGOAL_THEN
 325     `(F2 has_real_derivative
 326      -- &1 / &2 / (&2 - c + c * c / &4))(atreal c within P)` ASSUME_TAC);
 327     (* Subgoal 11 *)
 328    (ASM_MESON_TAC[]);
 329
 330  (UP_ASM_TAC THEN REPLICATE_TAC 5 DEL_TAC THEN DISCH_TAC);
 331
 332 (* ------------------------------------------------------------------------- *)
 333 (*    Compute the derivative of f                                            *)
 334 (* ------------------------------------------------------------------------- *)
 335
 336  (ABBREV_TAC `f' = -- &1 / &2 / (&2 - c + c * c / &4)`);
 337  (ABBREV_TAC `F3 = (\c:real. F1 c - F2 c)`);
 338
 339    (SUBGOAL_THEN
 340     `(F3 has_real_derivative &0) (atreal c within P)` ASSUME_TAC);
 341    (EXPAND_TAC "F3");
 342    (ASM_MESON_TAC[HAS_REAL_DERIVATIVE_SUB; REAL_ARITH `a - a = &0`]);
 343
 344  (ABBREV_TAC `2F3 = (\c:real. &2 * F3 c)`);
 345
 346    (SUBGOAL_THEN
 347     `(2F3 has_real_derivative (&2) * (&0)) (atreal c within P)` ASSUME_TAC);
 348    (EXPAND_TAC "2F3");
 349    (DEL_TAC THEN UP_ASM_TAC);
 350    (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN);
 351    (MESON_TAC[]);
 352
 353    (SUBGOAL_THEN
 354    `(\c:real. --pi / &2 - &2 * F1 c + &2 * F2 c) = (\c:real. --pi / &2 - 2F3 c)`
 355     ASSUME_TAC);
 356    (EXPAND_TAC "2F3");
 357    (EXPAND_TAC "F3");
 358    (REWRITE_TAC[REAL_ARITH `a - &2 * (x - y) = a - &2 * x + &2 * y`]);
 359
 360  (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
 361
 362    (SUBGOAL_THEN `((\c. --pi / &2) has_real_derivative &0)
 363                    (atreal c within P)` ASSUME_TAC);
 364    (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 365
 366  (UP_ASM_TAC THEN UP_ASM_TAC);
 367  (MP_TAC HAS_REAL_DERIVATIVE_SUB);
 368  (MESON_TAC [REAL_ARITH `&2 * &0 = &0 /\ &0 - &0 = &0`;
 369    HAS_REAL_DERIVATIVE_SUB])]);;
 370
 371
 372
 373
 374
 375 let DERIVATIVE_WRT_A_Euler_lemma = prove_by_refinement (
 376  `! a b c.
 377   let d = ups_x a b c - a * b * c in
 378  ((&0 < d) /\ (&0 < a /\ &0 < b /\ &0 < c) /\
 379               (a < &4 /\ b < &4 /\ c < &4) ==>
 380  pi / &2 - atn ((-- &2 * a + &2 * b + &2 * c - b * c) / (&2 * sqrt d)) +
 381  pi / &2 - atn ((-- &2 * b + &2 * c + &2 * a - c * a) / (&2 * sqrt d)) +
 382  pi / &2 - atn ((-- &2 * c + &2 * a + &2 * b - a * b) / (&2 * sqrt d)) - pi =
 383  pi - &2 * atn ((&8 - a - b - c) / sqrt d))`,
 384
 385 [ (REPEAT GEN_TAC THEN LET_TAC THEN STRIP_TAC);
 386  (REWRITE_TAC[REAL_ARITH ` pi / &2 - x + pi / &2 - y + pi / &2 - z - pi =
 387    pi - t <=> -- pi / &2 - x - y - z + t = &0`]);
 388
 389  (ABBREV_TAC `s = {(x:real) | &0 < ups_x x b c - x * b * c }`);
 390
 391
 392 (* ========================================================================= *)
 393 (*                             The main subgoal.                             *)
 394 (* ========================================================================= *)
 395
 396  (SUBGOAL_THEN `!a. (a IN s) ==> --pi / &2 -
 397  atn
 398   ((-- &2 * a + &2 * b + &2 * c - b * c) /
 399   (&2 * sqrt (ups_x a b c - a * b * c))) -
 400  atn
 401  ((-- &2 * b + &2 * c + &2 * a - c * a) /
 402   (&2 * sqrt (ups_x a b c - a * b * c))) -
 403  atn
 404  ((-- &2 * c + &2 * a + &2 * b - a * b) /
 405   (&2 * sqrt (ups_x a b c - a * b * c))) +
 406  &2 * atn ((&8 - a - b - c) / sqrt (ups_x a b c - a * b * c)) =
 407  &0` ASSUME_TAC);
 408
 409  (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 THEN EXISTS_TAC
 410   `b + c - (b * c) / & 2`);
 411  (REPEAT CONJ_TAC);   (* Break into 3 Subgoals *)
 412
 413   (EXPAND_TAC "s");
 414   (ASM_MESON_TAC[EULER_TRIANGLE_REAL_INTERVAL]);  (* End subgoal 1 *)
 415
 416 (* ------------------------------------------------------------------------- *)
 417 (*                b + c - (b * c) / &2 IN s                                  *)
 418 (* ------------------------------------------------------------------------- *)
 419
 420   (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM]);
 421   (ABBREV_TAC `a' = b + c - (b * c) / &2`);
 422   (MATCH_MP_TAC (REAL_ARITH `&0 < d /\ d <= x ==> &0 < x`));
 423   (ASM_REWRITE_TAC[]);
 424   (EXPAND_TAC "d" THEN REWRITE_TAC[ups_x]);
 425   (ONCE_REWRITE_TAC [REAL_ARITH `a <= b <=> &0 <= b - a `]);
 426
 427     (SUBGOAL_THEN
 428       `(--a' * a' - b * b - c * c + &2 * a' * c + &2 * a' * b + &2 * b * c) -
 429        a' * b * c -
 430        ((--a * a - b * b - c * c + &2 * a * c + &2 * a * b + &2 * b * c) -
 431        a * b * c) =
 432        (a - a') pow 2`
 433       ASSUME_TAC);
 434     (EXPAND_TAC "a'" THEN REAL_ARITH_TAC);
 435
 436   (ASM_REWRITE_TAC[]);
 437   (ASM_MESON_TAC[REAL_LE_POW_2]);
 438
 439 (* ========================================================================= *)
 440 (*                                                                           *)
 441 (*                 BEGIN COMPUTE DERIVATIVES                                 *)
 442 (*                                                                           *)
 443 (* ========================================================================= *)
 444  (GEN_TAC THEN DISCH_TAC);
 445  (ABBREV_TAC `Da = (-- &2 * a' + &2 * b + &2 * c - b * c)`);
 446  (ABBREV_TAC `Db = (-- &2 * b + &2 * c + &2 * a' - a' * c)`);
 447  (ABBREV_TAC `Dc = (-- &2 * c + &2 * a' + &2 * b - a' * b)`);
 448  (ABBREV_TAC `D' = ups_x a' b c - a' * b * c`);
 449
 450   (SUBGOAL_THEN `&0 < D'` ASSUME_TAC);
 451   (* Subgoal 3.1 *)
 452
 453   (REPLICATE_TAC 5 UP_ASM_TAC THEN EXPAND_TAC "s");
 454   (PURE_ASM_REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[]);
 455
 456 (* --------------------------------------------------------------------------*)
 457 (*  Subgoal 3.2                                                              *)
 458 (*         Derivative of sqrt (ups_x x b c - x * b * c)                      *)
 459 (* --------------------------------------------------------------------------*)
 460
 461  (ABBREV_TAC `G = (\x.  sqrt (ups_x x b c - x * b * c))`);
 462  (ABBREV_TAC `G' = (-- &2 * a' + &2 * b + &2 * c - b * c) *
 463                     inv (&2 * sqrt (ups_x a' b c - a' * b * c))`);
 464  (SUBGOAL_THEN ` (G has_real_derivative G') (atreal a' within s)` ASSUME_TAC);
 465  (ABBREV_TAC `f = (\x. ups_x x b c - x * b * c)`);
 466
 467   (SUBGOAL_THEN `G = (\x:real. sqrt (f x))` ASSUME_TAC);
 468     (* Subgoal 3.2.1 *)
 469   (EXPAND_TAC "f" THEN ASM_REWRITE_TAC[]);
 470
 471  (ABBREV_TAC `g' = (\x. inv (&2 * sqrt x))`);
 472  (ABBREV_TAC `f' = -- &2 * a' + &2 * b + &2 * c - b * c`);
 473
 474  (SUBGOAL_THEN `G' = f' * (g' ((f:real->real) a'))` ASSUME_TAC);
 475     (* Subgoal 3.2.2 *)
 476   (EXPAND_TAC "G'" THEN EXPAND_TAC "f'");
 477   (EXPAND_TAC "g'" THEN EXPAND_TAC "f" );
 478   (REWRITE_TAC[]);
 479
 480  (ABBREV_TAC `P = {x:real | &0 < x}`);
 481
 482   (SUBGOAL_THEN
 483     `!x. P x ==> (sqrt has_real_derivative (g':real->real) x) (atreal x)`
 484      ASSUME_TAC);
 485     (* Subgoal 3.2.3 *)
 486   (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
 487   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
 488   (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
 489
 490   (SUBGOAL_THEN
 491    `(f has_real_derivative f') (atreal a' within s) /\
 492     (P:real->bool) ((f:real->real) a')`
 493      ASSUME_TAC);
 494     (* Subgoal 3.2.4 *)
 495   CONJ_TAC;
 496
 497     (* Subgoal 3.2.4.1 *)
 498   (EXPAND_TAC "f" THEN EXPAND_TAC "f'");
 499   (REWRITE_TAC[ups_x]);
 500   (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 501     (* Subgoal 3.2.4.2 *)
 502   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
 503
 504     (SUBGOAL_THEN `!x. (x:real) IN s ==> &0 < f x` ASSUME_TAC);
 505       (* Subgoal 3.2.4.1.1 *)
 506     (EXPAND_TAC "s" THEN REWRITE_TAC[IN_ELIM_THM]);
 507     (EXPAND_TAC "f" THEN MESON_TAC[]);
 508     (FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
 509
 510   (ONCE_ASM_REWRITE_TAC[]);
 511     (* End Subgoal 3.2.4 *)
 512
 513  (REPLICATE_TAC 2 UP_ASM_TAC);
 514  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2 THEN MESON_TAC[]);
 515 (* --------------------------------------------------------------------------*)
 516 (*  Subgoal 3.3                                                              *)
 517 (*         Derivative of &2 * sqrt (ups_x x b c - x * b * c)                 *)
 518 (* --------------------------------------------------------------------------*)
 519
 520  (ABBREV_TAC `2G = (\x.  &2 * sqrt (ups_x x b c - x * b * c))`);
 521
 522  (SUBGOAL_THEN
 523   `(2G has_real_derivative &2 * G') (atreal a' within s)` ASSUME_TAC);
 524
 525   (SUBGOAL_THEN `2G = (\x:real. &2 * G x)` ASSUME_TAC);
 526   (EXPAND_TAC "2G" THEN EXPAND_TAC "G" THEN MESON_TAC[]);
 527
 528  (PURE_ONCE_ASM_REWRITE_TAC[]);
 529  (DEL_TAC THEN DEL_TAC );
 530  (FIRST_X_ASSUM MP_TAC);
 531  (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN THEN MESON_TAC[]);
 532
 533 (* --------------------------------------------------------------------------*)
 534 (*  Subgoal 3.4                                                              *)
 535 (*         Derivative of  (-- &2 * x + &2 * b + &2 * c - b * c) /            *)
 536 (*                          &2 * sqrt (ups_x x b c - x * b * c)              *)
 537 (* --------------------------------------------------------------------------*)
 538
 539  (ABBREV_TAC `f1 = (\x. -- &2 * x + &2 * b + &2 * c - b * c)`);
 540  (ABBREV_TAC `F12 = (\x. (-- &2 * x + &2 * b + &2 * c - b * c) /
 541         (&2 * sqrt (ups_x x b c - x * b * c)))`);
 542  (SUBGOAL_THEN
 543   `(F12 has_real_derivative (-- &2 * 2G (a':real) - (f1 a' * &2 * G')) /
 544     2G a' pow 2) (atreal a' within s)`
 545    ASSUME_TAC);
 546
 547   (SUBGOAL_THEN ` F12 = (\x:real. f1 x / 2G x)` ASSUME_TAC);
 548     (* Subgoal 3.4.1 *)
 549   (EXPAND_TAC "F12" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f1");
 550   (ASM_REWRITE_TAC[]);
 551
 552  (ASM_REWRITE_TAC[]);
 553
 554   (SUBGOAL_THEN
 555     `(f1 has_real_derivative -- &2) (atreal a' within s) /\
 556      (2G has_real_derivative &2 * G') (atreal a' within s) /\
 557     ~(2G a' = &0)`
 558     ASSUME_TAC);
 559   (* Subgoal 3.4.2 *)
 560   (ASM_REWRITE_TAC[]);
 561   (REPEAT CONJ_TAC);  (* Break into 2 subgoals *)
 562
 563     (EXPAND_TAC "f1" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 564     (EXPAND_TAC "2G");
 565     (MATCH_MP_TAC
 566       (MESON[REAL_ENTIRE] `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
 567     (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
 568     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
 569     (MATCH_MP_TAC SQRT_POS_LT);
 570     (ASM_REWRITE_TAC[]);
 571
 572  (FIRST_X_ASSUM MP_TAC);
 573  (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
 574  (MESON_TAC[]);
 575
 576 (* --------------------------------------------------------------------------*)
 577 (*  Subgoal 3.5                                                              *)
 578 (*         Derivative of  atn ((-- &2 * a + &2 * b + &2 * c - b * c) /       *)
 579 (*                          &2 * sqrt (ups_x x b c - x * b * c))             *)
 580 (* --------------------------------------------------------------------------*)
 581
 582  (ABBREV_TAC `F1 = (\x. atn ((-- &2 * x + &2 * b + &2 * c - b * c) / (&2 *
 583    sqrt (ups_x x b c - x * b * c))))`);
 584
 585  (SUBGOAL_THEN
 586    `(F1 has_real_derivative
 587     (-- &2 * 2G a' - f1 a' * &2 * G') / 2G a' pow 2 * inv (&1 + F12 a' pow 2))
 588     (atreal a' within s)`
 589   ASSUME_TAC);
 590
 591   (SUBGOAL_THEN `F1 = (\x. atn (F12 (x:real)))` ASSUME_TAC);
 592     (* Subgoal 3.5.1 *)
 593   (EXPAND_TAC "F1" THEN EXPAND_TAC "F12");
 594   (REWRITE_TAC[]);
 595
 596  (PURE_ONCE_ASM_REWRITE_TAC[]);
 597  (REPLICATE_TAC 2 DEL_TAC);
 598  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
 599  (ABBREV_TAC `f' = (-- &2 * 2G (a':real) - f1 a' * &2 * G') / 2G a' pow 2`);
 600
 601   (SUBGOAL_THEN
 602     `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
 603     ASSUME_TAC);
 604     (* Subgoal 3.5.3 *)
 605   (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
 606   (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
 607
 608   (SUBGOAL_THEN `(F12 has_real_derivative f') (atreal a' within s) /\
 609                    (:real) ((F12:real->real) a')`
 610      ASSUME_TAC);
 611   (ASM_REWRITE_TAC[]);
 612   (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
 613
 614   (SUBGOAL_THEN
 615    `inv (&1 + F12 a' pow 2) = g' ((F12:real-> real) a')`
 616      ASSUME_TAC);
 617     (* Subgoal 3.5.2 *)
 618   (EXPAND_TAC "F12" THEN EXPAND_TAC "g'");
 619   (MESON_TAC[]);
 620
 621  (ONCE_ASM_REWRITE_TAC[]);
 622  DEL_TAC ;
 623  (REPLICATE_TAC 2 UP_ASM_TAC);
 624  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
 625  (MESON_TAC[]);
 626
 627 (* ========================================================================= *)
 628 (*           THIS PART TO TO REDUCE THE DERIVATIVE OF F1                     *)
 629 (*             Derivative of  F1 is  -- &1 / sqrt d                          *)
 630 (* ========================================================================= *)
 631
 632 (* --------------------------------------------------------------------------*)
 633 (*     Subgoal 3.6                                                           *)
 634 (*                 (&2 * sqrt D') pow 2 = &4 * D'                            *)
 635 (* --------------------------------------------------------------------------*)
 636
 637   (SUBGOAL_THEN `(&2 * sqrt D') pow 2 = &4 * D'` ASSUME_TAC);
 638   (REWRITE_TAC[REAL_POW_2]);
 639   (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * b = &4 * (a * b)`]);
 640   (REWRITE_TAC[GSYM REAL_POW_2]);
 641   AP_TERM_TAC;
 642   (MATCH_MP_TAC SQRT_POW_2 THEN ASM_REAL_ARITH_TAC);
 643
 644 (* --------------------------------------------------------------------------*)
 645 (*     Subgoal 3.7                                                           *)
 646 (*               Reduce:  inv (&1 + F12 a' pow 2)                            *)
 647 (* --------------------------------------------------------------------------*)
 648
 649   (SUBGOAL_THEN
 650     `inv (&1 + F12 (a':real) pow 2)  = (&4 * D') / (&4 * D' + Da pow 2)`
 651      ASSUME_TAC);
 652   (EXPAND_TAC "F12");
 653   (REWRITE_TAC[REAL_POW_DIV]);
 654   (ASM_REWRITE_TAC[]);
 655   (REWRITE_TAC[MESON[REAL_INV_DIV]
 656      `(&4 * D') / (&4 * D' + Da pow 2) =
 657       inv ((&4 * D' + Da pow 2) / (&4 * D'))`]);
 658   AP_TERM_TAC;
 659   (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
 660   (AP_THM_TAC THEN AP_TERM_TAC);
 661   (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
 662   (REWRITE_TAC[MESON[] `~(a = b) <=> ~(b = a)`;REAL_ENTIRE;
 663                  MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
 664   ASM_REAL_ARITH_TAC;
 665
 666 (* --------------------------------------------------------------------------*)
 667 (*     Subgoal 3.8                                                           *)
 668 (*               Reduce:  Derivative of F1                                   *)
 669 (* --------------------------------------------------------------------------*)
 670
 671  (SUBGOAL_THEN
 672    `(F1 has_real_derivative -- &1 / sqrt D') (atreal a' within s)`
 673    ASSUME_TAC);
 674
 675   (SUBGOAL_THEN `2G (a':real) = &2 * sqrt D'` ASSUME_TAC);
 676     (* Subgoal 3.8.1 *)
 677   (EXPAND_TAC "2G" THEN EXPAND_TAC "D'");
 678   (REWRITE_TAC[]);
 679
 680   (SUBGOAL_THEN `f1 (a':real) = (Da:real)` ASSUME_TAC);
 681     (* Subgoal 3.8.2 *)
 682   (EXPAND_TAC "f1" THEN EXPAND_TAC "Da");
 683   (REWRITE_TAC[]);
 684
 685   (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
 686     (* Subgoal 3.8.3 *)
 687   (MATCH_MP_TAC SQRT_POS_LT);
 688   (ASM_REWRITE_TAC[]);
 689
 690   (SUBGOAL_THEN
 691     `(-- &2 * 2G (a':real) - f1 a' * &2 * G') / 2G a' pow 2 *
 692      inv (&1 + F12 a' pow 2) =
 693      -- &1 / sqrt D'`
 694     ASSUME_TAC);
 695     (* Subgoal 3.8.4 *)
 696   (ASM_REWRITE_TAC[]);
 697   (REWRITE_TAC[REAL_ARITH `(a / b * b / c) = (a / b * b) / c`]);
 698   (SIMP_TAC[REAL_DIV_RMUL]);
 699
 700     (SUBGOAL_THEN `~(&4 * D' = &0)` ASSUME_TAC);
 701       (* Subgoal 3.8.4.1 *)
 702     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 703     (MATCH_MP_TAC REAL_LT_MUL);
 704     ASM_REAL_ARITH_TAC;
 705
 706   (ABBREV_TAC `M = (-- &2 * &2 * sqrt D' - Da * &2 * G')`);
 707
 708     (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);
 709       (* Subgoal 3.8.4.2 *)
 710     (EXPAND_TAC "G'" THEN EXPAND_TAC "Da" THEN EXPAND_TAC "D'");
 711     (AP_THM_TAC THEN AP_TERM_TAC);
 712     (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
 713
 714     (SUBGOAL_THEN `M = -- (&4 * D' + Da pow 2) / sqrt D'` ASSUME_TAC);
 715       (* Subgoal 3.8.4.3 *)
 716     (EXPAND_TAC "M");
 717     (REWRITE_TAC[REAL_ARITH `-- &2 * &2 * x = -- &4 * x`]);
 718     (ONCE_ASM_REWRITE_TAC[]);
 719     (ABBREV_TAC `X = -- &4 * sqrt D' - Da * &2 * Da * inv (&2 * sqrt D')`);
 720     (ABBREV_TAC `Y = --(&4 * D' + Da pow 2)`);
 721     (ABBREV_TAC `Z = sqrt D'`);
 722
 723        (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
 724          (* Subgoal 3.8.4.3.1 *)
 725        (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);
 726
 727     (FIRST_X_ASSUM MATCH_MP_TAC);
 728     (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 729     (REWRITE_TAC[REAL_SUB_RDISTRIB; REAL_NEG_ADD]);
 730     (REWRITE_TAC[REAL_ARITH ` (a * b * a * c) * d = a pow 2 * c * b * d`]);
 731
 732       (SUBGOAL_THEN `inv (&2 * sqrt D') * &2 * sqrt D' = &1` ASSUME_TAC);
 733       (MATCH_MP_TAC REAL_MUL_LINV);
 734       (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
 735       (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
 736       (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 737       (MATCH_MP_TAC SQRT_POS_LT);
 738       (ASM_REWRITE_TAC[]);
 739
 740     (ASM_REWRITE_TAC[]);
 741     (REWRITE_TAC[REAL_ARITH `a - b = a + --b`;REAL_MUL_RID]);
 742     (AP_THM_TAC THEN AP_TERM_TAC);
 743     (REWRITE_TAC[REAL_ARITH `(--a * b) * c = -- (a * (b * c))`]);
 744     (REPEAT AP_TERM_TAC);
 745     (REWRITE_TAC[GSYM REAL_POW_2]);
 746     (EXPAND_TAC "Z");
 747     (MATCH_MP_TAC SQRT_POW_2);
 748     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 749     (ASM_REWRITE_TAC[]);
 750
 751     (SUBGOAL_THEN `M / (&4 * D') * &4 * D' = M` ASSUME_TAC);
 752       (* Subgoal 3.8.4.4 *)
 753     (ASM_MESON_TAC[REAL_DIV_RMUL]);
 754
 755   (ONCE_ASM_REWRITE_TAC[]);
 756   (ONCE_ASM_REWRITE_TAC[]);
 757   (ASM_REWRITE_TAC [REAL_ARITH `a / b / c = a / c / b`]);
 758   (AP_THM_TAC THEN AP_TERM_TAC);
 759   (MATCH_MP_TAC (REAL_ARITH `a / a = &1 ==> -- a / a = -- &1`));
 760   (MATCH_MP_TAC REAL_DIV_REFL);
 761   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 762   (MATCH_MP_TAC REAL_LTE_ADD);
 763   (REWRITE_TAC[REAL_LE_POW_2]);
 764   (MATCH_MP_TAC REAL_LT_MUL);
 765   (ASM_REWRITE_TAC[]);
 766   (REAL_ARITH_TAC);
 767     (* End of subgoal 3.8.4 *)
 768
 769  (ASM_MESON_TAC[]);
 770
 771 (* Delete unnecessary assumptions in assumption list  *)
 772
 773  (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
 774  (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
 775  (REPEAT DISCH_TAC);
 776
 777
 778 (* ================ END DIFF F1 ============================================ *)
 779
 780 (* --------------------------------------------------------------------------*)
 781 (*  Subgoal 3.9                                                              *)
 782 (*         Derivative of  (-- &2 * b + &2 * c + &2 * a - c * a) /            *)
 783 (*                          &2 * sqrt (ups_x x b c - x * b * c)              *)
 784 (* --------------------------------------------------------------------------*)
 785
 786  (ABBREV_TAC `f2 = (\x. -- &2 * b + &2 * c + &2 * x - c * x)`);
 787  (ABBREV_TAC `F22 = (\x. (-- &2 * b + &2 * c + &2 * x - c * x) / (&2 *
 788   sqrt (ups_x x b c - x * b * c)))`);
 789
 790   (SUBGOAL_THEN
 791     `(F22 has_real_derivative ((&2 - c) * 2G (a':real) -
 792      f2 a' * &2 * G') / 2G a' pow 2) (atreal a' within s)`
 793      ASSUME_TAC);
 794
 795     (SUBGOAL_THEN ` F22 = (\x:real. f2 x / 2G x )` ASSUME_TAC);
 796       (* Subgoal 3.9.1 *)
 797     (EXPAND_TAC "F22" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f2");
 798     (ASM_REWRITE_TAC[]);
 799
 800     (SUBGOAL_THEN `(f2 has_real_derivative &2 - c) (atreal a' within s) /\
 801                      (2G has_real_derivative &2 * G') (atreal a' within s) /\
 802                     ~(2G a' = &0)` ASSUME_TAC);
 803       (* Subgoal 3.9.2 *)
 804     (ASM_REWRITE_TAC[]);
 805     (REPEAT CONJ_TAC);  (* Break into 2 subgoals *)
 806
 807     (EXPAND_TAC "f2" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 808     (EXPAND_TAC "2G");
 809     (MATCH_MP_TAC
 810       (MESON[REAL_ENTIRE] `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
 811     (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
 812     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
 813     (MATCH_MP_TAC SQRT_POS_LT);
 814     (ASM_REWRITE_TAC[]);
 815
 816  (ASM_REWRITE_TAC[]);
 817  (FIRST_X_ASSUM MP_TAC);
 818  (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
 819  (MESON_TAC[]);
 820
 821 (* --------------------------------------------------------------------------*)
 822 (*  Subgoal 3.10                                                             *)
 823 (*         Derivative of  atn ((-- &2 * b + &2 * c + &2 * a - c * a) /       *)
 824 (*                          &2 * sqrt (ups_x x b c - x * b * c))             *)
 825 (* --------------------------------------------------------------------------*)
 826
 827  (ABBREV_TAC `F2 = (\x. atn ((-- &2 * b + &2 * c + &2 * x - c * x) /(&2 *
 828    sqrt (ups_x x b c - x * b * c))))`);
 829
 830  (SUBGOAL_THEN `(F2 has_real_derivative
 831   ((&2 - c) * 2G a' - f2 a' * &2 * G') / 2G a' pow 2 * inv (&1 + F22 a' pow 2))
 832   (atreal a' within s)`
 833    ASSUME_TAC);
 834
 835   (SUBGOAL_THEN `F2 = (\x. atn (F22 (x:real)))` ASSUME_TAC);
 836     (* Subgoal 3.10.1 *)
 837   (EXPAND_TAC "F2" THEN EXPAND_TAC "F22");
 838   (REWRITE_TAC[]);
 839
 840  (PURE_ONCE_ASM_REWRITE_TAC[]);
 841  (REPLICATE_TAC 2 DEL_TAC);
 842  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
 843  (ABBREV_TAC `f' = ((&2 - c) * 2G a' - f2 a' * &2 * G') /
 844                     2G (a':real) pow 2`);
 845
 846   (SUBGOAL_THEN
 847     `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
 848     ASSUME_TAC);
 849     (* Subgoal 3.10.2 *)
 850   (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
 851   (REWRITE_TAC[EQ_UNIV;HAS_REAL_DERIVATIVE_ATN]);
 852
 853   (SUBGOAL_THEN `(F22 has_real_derivative f') (atreal a' within s) /\
 854                    (:real) ((F22:real->real) a')`
 855      ASSUME_TAC);
 856   (ASM_REWRITE_TAC[]);
 857   (MESON_TAC[EQ_UNIV;IN_UNIV;IN]);
 858
 859   (SUBGOAL_THEN
 860    `inv (&1 + F22 a' pow 2) = g' ((F22:real-> real) a')`
 861      ASSUME_TAC);
 862     (* Subgoal 3.10.3 *)
 863   (EXPAND_TAC "F22" THEN EXPAND_TAC "g'");
 864   (REWRITE_TAC[]);
 865
 866  (ONCE_ASM_REWRITE_TAC[]);
 867  DEL_TAC ;
 868  (REPLICATE_TAC 2 UP_ASM_TAC);
 869  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
 870  (MESON_TAC[]);
 871
 872 (* ========================================================================= *)
 873 (*           THIS PART TO TO REDUCE THE DERIVATIVE OF F2                     *)
 874 (*             Derivative of  F2 is  ..... / sqrt d                          *)
 875 (* ========================================================================= *)
 876
 877 (* --------------------------------------------------------------------------*)
 878 (*     Subgoal 3.11                                                           *)
 879 (*                 (&2 * sqrt D') pow 2 = &4 * D'                            *)
 880 (* --------------------------------------------------------------------------*)
 881
 882   (SUBGOAL_THEN `(&2 * sqrt D') pow 2 = &4 * D'` ASSUME_TAC);
 883   (REWRITE_TAC[REAL_POW_2]);
 884   (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * b = &4 * (a * b)`]);
 885   (REWRITE_TAC[GSYM REAL_POW_2]);
 886   AP_TERM_TAC;
 887   (MATCH_MP_TAC SQRT_POW_2 THEN ASM_REAL_ARITH_TAC);
 888
 889 (* --------------------------------------------------------------------------*)
 890 (*     Subgoal 3.12                                                           *)
 891 (*               Reduce:  inv (&1 + F22 a' pow 2)                            *)
 892 (* --------------------------------------------------------------------------*)
 893
 894   (SUBGOAL_THEN
 895     `inv (&1 + F22 (a':real) pow 2)  = (&4 * D') / (&4 * D' + Db pow 2)`
 896      ASSUME_TAC);
 897   (EXPAND_TAC "F22");
 898   (REWRITE_TAC[REAL_POW_DIV]);
 899   (ASM_REWRITE_TAC[]);
 900   (REWRITE_TAC[MESON[REAL_INV_DIV]
 901      `(&4 * D') / (&4 * D' + Db pow 2) =
 902       inv ((&4 * D' + Db pow 2) / (&4 * D'))`]);
 903   AP_TERM_TAC;
 904   (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
 905   (EXPAND_TAC "Db");
 906   (REWRITE_TAC[REAL_ARITH `a + b + c - x * y = a + b + c - y * x`]);
 907   (AP_THM_TAC THEN AP_TERM_TAC);
 908   (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
 909   (REWRITE_TAC[MESON[] `~(a = b) <=> ~(b = a)`;REAL_ENTIRE;
 910                  MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
 911   ASM_REAL_ARITH_TAC;
 912
 913
 914 (* --------------------------------------------------------------------------*)
 915 (*     Subgoal 3.13                                                          *)
 916 (*               Reduce:  Derivative of F2                                   *)
 917 (* --------------------------------------------------------------------------*)
 918
 919  (SUBGOAL_THEN
 920    `(F2 has_real_derivative
 921     (-- &2 * c + &2 * a' + &2 * b - a' * b) / (a' * (&4 - a')) / sqrt D')
 922     (atreal a' within s)`
 923    ASSUME_TAC);
 924
 925   (SUBGOAL_THEN `2G (a':real) = &2 * sqrt D'` ASSUME_TAC);
 926     (* Subgoal 3.13.1 *)
 927   (EXPAND_TAC "2G" THEN EXPAND_TAC "D'");
 928   (REWRITE_TAC[]);
 929
 930   (SUBGOAL_THEN `f2 (a':real) = (Db:real)` ASSUME_TAC);
 931     (* Subgoal 3.13.2 *)
 932   (EXPAND_TAC "f2" THEN EXPAND_TAC "Db");
 933   (REAL_ARITH_TAC);
 934
 935   (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
 936     (* Subgoal 3.13.3 *)
 937   (MATCH_MP_TAC SQRT_POS_LT);
 938   (ASM_REWRITE_TAC[]);
 939
 940   (SUBGOAL_THEN `
 941     ((&2 - c) * 2G a' - f2 a' * &2 * G') / 2G a' pow 2 *
 942     inv (&1 + F22 a' pow 2) =
 943     (-- &2 * c + &2 * a' + &2 * b - a' * b) / (a' * (&4 - a')) / sqrt D' `
 944     ASSUME_TAC);
 945     (* Subgoal 3.13.4 *)
 946   (ASM_REWRITE_TAC[]);
 947   (REWRITE_TAC[REAL_ARITH `(a / b * b / c) = (a / b * b) / c`]);
 948   (SIMP_TAC[REAL_DIV_RMUL]);
 949
 950
 951     (SUBGOAL_THEN `~(&4 * D' = &0)` ASSUME_TAC);
 952       (* Subgoal 3.13.4.1 *)
 953     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 954     (MATCH_MP_TAC REAL_LT_MUL);
 955     ASM_REAL_ARITH_TAC;
 956
 957   (ABBREV_TAC `M = (&2 - c) * &2 * sqrt D' - Db * &2 * G'`);
 958
 959     (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);
 960       (* Subgoal 3.13.4.2 *)
 961     (EXPAND_TAC "G'" THEN EXPAND_TAC "Da" THEN EXPAND_TAC "D'");
 962     (REWRITE_TAC[]);
 963
 964     (SUBGOAL_THEN `M = ((&4 - &2 * c) * D' - Da * Db) / sqrt D'` ASSUME_TAC);
 965       (* Subgoal 3.13.4.3 *)
 966     (EXPAND_TAC "M");
 967     (REWRITE_TAC[REAL_ARITH `(&2 - c) * &2 * x = (&4 - &2 * c) * x`]);
 968     (ONCE_ASM_REWRITE_TAC[]);
 969     (ABBREV_TAC `X = (&4 - &2 * c) * sqrt D' -
 970                        Db * &2 * Da * inv (&2 * sqrt D')`);
 971     (ABBREV_TAC `Y = (&4 - &2 * c) * D' - Da * Db`);
 972     (ABBREV_TAC `Z = sqrt D'`);
 973
 974        (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
 975          (* Subgoal 3.13.4.3.1 *)
 976        (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);
 977
 978
 979     (FIRST_X_ASSUM MATCH_MP_TAC);
 980     (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 981     (ABBREV_TAC `m = &4 - &2 * c`);
 982     (REWRITE_TAC[REAL_SUB_RDISTRIB;REAL_NEG_ADD]);
 983     (REWRITE_TAC[REAL_ARITH ` (a * b * c * d) * e = (c * a) * (d * b * e)`]);
 984
 985       (SUBGOAL_THEN `inv (&2 * sqrt D') * &2 * sqrt D' = &1` ASSUME_TAC);
 986          (* Subgoal 3.13.4.3.2 *)
 987       (MATCH_MP_TAC REAL_MUL_LINV);
 988       (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
 989       (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
 990       (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 991       (ASM_REWRITE_TAC[]);
 992
 993     (PURE_ONCE_ASM_REWRITE_TAC[]);
 994     (EXPAND_TAC "Y");
 995     (REWRITE_TAC[REAL_MUL_RID]);
 996     (AP_THM_TAC THEN AP_TERM_TAC);
 997     (EXPAND_TAC "m" THEN EXPAND_TAC "Z");
 998     (REWRITE_TAC[REAL_ARITH `(a * b) * c = a * b * c`]);
 999     (REPEAT AP_TERM_TAC);
1000     (REWRITE_TAC[GSYM REAL_POW_2]);
1001     (MATCH_MP_TAC SQRT_POW_2);
1002     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
1003     (ASM_REWRITE_TAC[]);
1004       (* End of Subgoal 3.13.4.3 *)
1005
1006
1007     (SUBGOAL_THEN `M / (&4 * D') * &4 * D' = M` ASSUME_TAC);
1008       (* Subgoal 3.13.4.4 *)
1009     (ASM_SIMP_TAC[REAL_DIV_RMUL]);
1010
1011   (PURE_ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
1012
1013     (SUBGOAL_THEN
1014       `M = ((-- &2 * c + &2 * a' + &2 * b - a' * b) * (&4 - c) * c)/ sqrt D'`
1015        ASSUME_TAC);
1016       (* Subgoal 3.13.4.5 *)
1017     (ONCE_ASM_REWRITE_TAC[]);
1018     (AP_THM_TAC THEN AP_TERM_TAC);
1019     (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
1020     (EXPAND_TAC "Da" THEN EXPAND_TAC "Db" THEN EXPAND_TAC "f2");
1021     (EXPAND_TAC "Dc");
1022     REAL_ARITH_TAC;
1023
1024   (UP_ASM_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
1025   (ONCE_ASM_REWRITE_TAC[]);
1026   (EXPAND_TAC "Dc");
1027   (REWRITE_TAC[REAL_ARITH `a / b / c = a / c / b`]);
1028   (AP_THM_TAC THEN AP_TERM_TAC);
1029
1030     (SUBGOAL_THEN
1031        `&4 * D' + Db pow 2 = a' * (&4 - a') * (&4 - c) * c` ASSUME_TAC);
1032       (* Subgoal 3.13.4.6 *)
1033     (EXPAND_TAC "Db" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[POW_2] );
1034     (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
1035      REAL_ARITH_TAC;
1036
1037   (ONCE_ASM_REWRITE_TAC[]);
1038   (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);
1039
1040      (* --------------------------------------------------------------- *)
1041      (*       ~ ( c = &4) /\ ~ (c = &0)                                 *)
1042      (* --------------------------------------------------------------- *)
1043
1044       (SUBGOAL_THEN `~ (c = &4) /\ ~ (c = &0)` ASSUME_TAC);
1045       ASM_REAL_ARITH_TAC;
1046       (SUBGOAL_THEN `~ ((&4 - c) * c = &0)` ASSUME_TAC);
1047       (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1048       (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);
1049
1050       (* --------------------------------------------------------------- *)
1051       (*       ~ ( a' = &4) /\ ~ (a' = &0)                               *)
1052       (* --------------------------------------------------------------- *)
1053
1054       (SUBGOAL_THEN `~ (a' = &4) /\ ~ (a' = &0)` ASSUME_TAC);
1055       (REPEAT STRIP_TAC);  (* 2 Subgoals *)
1056
1057         (SUBGOAL_THEN ` D' = -- ((c + b - &4) pow 2)` ASSUME_TAC);
1058         (EXPAND_TAC "D'" );
1059         (REWRITE_TAC[ups_x]);
1060         (ONCE_ASM_REWRITE_TAC[]);
1061         REAL_ARITH_TAC;
1062         (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1063         (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
1064         (MESON_TAC[REAL_LE_POW_2]);
1065         (MP_TAC (ASSUME `&0 < D'`));
1066         (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1067
1068
1069         (SUBGOAL_THEN ` D' = -- ((c - b) pow 2)` ASSUME_TAC);
1070         (EXPAND_TAC "D'" );
1071         (REWRITE_TAC[ups_x]);
1072         (ONCE_ASM_REWRITE_TAC[]);
1073         REAL_ARITH_TAC;
1074         (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1075         (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
1076         (MESON_TAC[REAL_LE_POW_2]);
1077         (MP_TAC (ASSUME `&0 < D'`));
1078         (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1079
1080
1081      (SUBGOAL_THEN `~ (a' * (&4 - a') = &0)` ASSUME_TAC);
1082      (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1083      (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);
1084
1085       (* --------------------------------------------------------------- *)
1086       (*       continue                                                  *)
1087       (* --------------------------------------------------------------- *)
1088
1089   (ABBREV_TAC `x = -- &2 * c + &2 * a' + &2 * b - a' * b`);
1090   (ABBREV_TAC `y = (&4 - c) * c`);
1091   (REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
1092   (ABBREV_TAC `z = a' * (&4 - a')`);
1093   (ASM_SIMP_TAC[REDUCE_WITH_DIV_Euler_lemma]);
1094   (ASM_MESON_TAC[]);
1095
1096  (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
1097  (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN REPEAT DISCH_TAC);
1098
1099 (* ================ END DIFF 2 ============================================= *)
1100
1101
1102
1103 (* --------------------------------------------------------------------------*)
1104 (* Subgoal 14                                                                *)
1105 (*         Derivative of  (-- &2 * c + &2 * a + &2 * b - a * b) /            *)
1106 (*                          &2 * sqrt (ups_x x b c - x * b * c)              *)
1107 (* --------------------------------------------------------------------------*)
1108
1109  (ABBREV_TAC `f3 = (\x. -- &2 * c + &2 * x + &2 * b - x * b)`);
1110  (ABBREV_TAC `F32 = (\x. (-- &2 * c + &2 * x + &2 * b - x * b) /
1111         (&2 * sqrt (ups_x x b c - x * b * c)))`);
1112
1113   (SUBGOAL_THEN
1114     `(F32 has_real_derivative ((&2 - b) * 2G (a':real) -
1115      f3 a' * &2 * G') / 2G a' pow 2) (atreal a' within s)`
1116      ASSUME_TAC);
1117
1118     (SUBGOAL_THEN ` F32 = (\x:real. f3 x / 2G x )` ASSUME_TAC);
1119       (* Subgoal 3.14.1 *)
1120     (EXPAND_TAC "F32" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f3");
1121     (ASM_REWRITE_TAC[]);
1122
1123     (SUBGOAL_THEN `(f3 has_real_derivative &2 - b) (atreal a' within s) /\
1124                      (2G has_real_derivative &2 * G') (atreal a' within s) /\
1125                     ~(2G a' = &0)` ASSUME_TAC);
1126       (* Subgoal 3.14.2 *)
1127     (ASM_REWRITE_TAC[]);
1128     (REPEAT CONJ_TAC);  (* Break into 2 subgoals *)
1129
1130     (EXPAND_TAC "f3" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
1131     (EXPAND_TAC "2G");
1132     (MATCH_MP_TAC
1133       (MESON[REAL_ENTIRE] `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
1134     (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
1135     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
1136     (MATCH_MP_TAC SQRT_POS_LT);
1137     (ASM_REWRITE_TAC[]);
1138
1139  (ASM_REWRITE_TAC[]);
1140  (FIRST_X_ASSUM MP_TAC);
1141  (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
1142  (MESON_TAC[]);
1143
1144
1145 (* --------------------------------------------------------------------------*)
1146 (*  Subgoal 3.15                                                             *)
1147 (*         Derivative of  atn ((-- &2 * c + &2 * a + &2 * b - a * b) /       *)
1148 (*                          &2 * sqrt (ups_x x b c - x * b * c))             *)
1149 (* --------------------------------------------------------------------------*)
1150
1151  (ABBREV_TAC `F3 = (\x. atn ((-- &2 * c + &2 * x + &2 * b - x * b) /(&2 *
1152    sqrt (ups_x x b c - x * b * c))))`);
1153
1154  (SUBGOAL_THEN `(F3 has_real_derivative
1155   ((&2 - b) * 2G a' - f3 a' * &2 * G') / 2G a' pow 2 * inv (&1 + F32 a' pow 2))
1156   (atreal a' within s)`
1157    ASSUME_TAC);
1158
1159   (SUBGOAL_THEN `F3 = (\x. atn (F32 (x:real)))` ASSUME_TAC);
1160     (* Subgoal 3.15.1 *)
1161   (EXPAND_TAC "F3" THEN EXPAND_TAC "F32");
1162   (REWRITE_TAC[]);
1163
1164  (PURE_ONCE_ASM_REWRITE_TAC[]);
1165  (REPLICATE_TAC 2 DEL_TAC);
1166  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
1167  (ABBREV_TAC `f' = ((&2 - b) * 2G a' - f3 a' * &2 * G') /
1168                     2G (a':real) pow 2`);
1169
1170   (SUBGOAL_THEN
1171     `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
1172     ASSUME_TAC);
1173     (* Subgoal 3.15.2 *)
1174   (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
1175   (REWRITE_TAC[EQ_UNIV;HAS_REAL_DERIVATIVE_ATN]);
1176
1177   (SUBGOAL_THEN `(F32 has_real_derivative f') (atreal a' within s) /\
1178                    (:real) ((F32:real->real) a')`
1179      ASSUME_TAC);
1180   (ASM_REWRITE_TAC[]);
1181   (MESON_TAC[EQ_UNIV;IN_UNIV;IN]);
1182
1183   (SUBGOAL_THEN
1184    `inv (&1 + F32 a' pow 2) = g' ((F32:real-> real) a')`
1185      ASSUME_TAC);
1186     (* Subgoal 3.15.3 *)
1187   (EXPAND_TAC "F32" THEN EXPAND_TAC "g'");
1188   (REWRITE_TAC[]);
1189
1190  (ONCE_ASM_REWRITE_TAC[]);
1191     DEL_TAC ;
1192  (REPLICATE_TAC 2 UP_ASM_TAC);
1193  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
1194  (MESON_TAC[]);
1195
1196 (* ========================================================================= *)
1197 (*           THIS PART TO TO REDUCE THE DERIVATIVE OF F3                     *)
1198 (*             Derivative of  F3 is  ..... / sqrt d                          *)
1199 (* ========================================================================= *)
1200
1201
1202 (* --------------------------------------------------------------------------*)
1203 (*     Subgoal 3.16                                                          *)
1204 (*                 (&2 * sqrt D') pow 2 = &4 * D'                            *)
1205 (* --------------------------------------------------------------------------*)
1206
1207   (SUBGOAL_THEN `(&2 * sqrt D') pow 2 = &4 * D'` ASSUME_TAC);
1208   (REWRITE_TAC[REAL_POW_2]);
1209   (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * b = &4 * (a * b)`]);
1210   (REWRITE_TAC[GSYM REAL_POW_2]);
1211       AP_TERM_TAC;
1212   (MATCH_MP_TAC SQRT_POW_2 THEN ASM_REAL_ARITH_TAC);
1213
1214 (* --------------------------------------------------------------------------*)
1215 (*     Subgoal 3.17                                                          *)
1216 (*               Reduce:  inv (&1 + F32 a' pow 2)                            *)
1217 (* --------------------------------------------------------------------------*)
1218
1219   (SUBGOAL_THEN
1220     `inv (&1 + F32 (a':real) pow 2)  = (&4 * D') / (&4 * D' + Dc pow 2)`
1221      ASSUME_TAC);
1222   (EXPAND_TAC "F32");
1223   (REWRITE_TAC[REAL_POW_DIV]);
1224   (ASM_REWRITE_TAC[]);
1225   (REWRITE_TAC[MESON[REAL_INV_DIV]
1226      `(&4 * D') / (&4 * D' + Dc pow 2) =
1227       inv ((&4 * D' + Dc pow 2) / (&4 * D'))`]);
1228       AP_TERM_TAC;
1229   (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
1230   (EXPAND_TAC "Dc");
1231   (REWRITE_TAC[REAL_ARITH `a + b + c - x * y = a + b + c - y * x`]);
1232   (AP_THM_TAC THEN AP_TERM_TAC);
1233   (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
1234   (REWRITE_TAC[MESON[] `~(a = b) <=> ~(b = a)`;REAL_ENTIRE;
1235                  MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1236       ASM_REAL_ARITH_TAC;
1237
1238 (* --------------------------------------------------------------------------*)
1239 (*     Subgoal 3.18                                                          *)
1240 (*               Reduce:  Derivative of F3                                   *)
1241 (* --------------------------------------------------------------------------*)
1242
1243  (SUBGOAL_THEN
1244    `(F3 has_real_derivative
1245     (-- &2 * b + &2 * a' + &2 * c - a' * c) / (a' * (&4 - a')) / sqrt D')
1246     (atreal a' within s)`
1247    ASSUME_TAC);
1248
1249   (SUBGOAL_THEN `2G (a':real) = &2 * sqrt D'` ASSUME_TAC);
1250     (* Subgoal 3.18.1 *)
1251   (EXPAND_TAC "2G" THEN EXPAND_TAC "D'");
1252   (REWRITE_TAC[]);
1253
1254   (SUBGOAL_THEN `f3 (a':real) = (Dc:real)` ASSUME_TAC);
1255     (* Subgoal 3.18.2 *)
1256   (EXPAND_TAC "f3" THEN EXPAND_TAC "Dc");
1257   (REAL_ARITH_TAC);
1258
1259   (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
1260     (* Subgoal 3.18.3 *)
1261   (MATCH_MP_TAC SQRT_POS_LT);
1262   (ASM_REWRITE_TAC[]);
1263
1264   (SUBGOAL_THEN `
1265     ((&2 - b) * 2G a' - f3 a' * &2 * G') / 2G a' pow 2 *
1266     inv (&1 + F32 a' pow 2) =
1267     (-- &2 * b + &2 * a' + &2 * c - a' * c) / (a' * (&4 - a')) / sqrt D' `
1268     ASSUME_TAC);
1269     (* Subgoal 3.18.4 *)
1270   (ASM_REWRITE_TAC[]);
1271   (REWRITE_TAC[REAL_ARITH `(a / b * b / c) = (a / b * b) / c`]);
1272   (SIMP_TAC[REAL_DIV_RMUL]);
1273
1274     (SUBGOAL_THEN `~(&4 * D' = &0)` ASSUME_TAC);
1275       (* Subgoal 3.18.4.1 *)
1276     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1277     (MATCH_MP_TAC REAL_LT_MUL);
1278     (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1279
1280   (ABBREV_TAC `M = (&2 - b) * &2 * sqrt D' - Dc * &2 * G'`);
1281
1282     (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);
1283       (* Subgoal 3.18.4.2 *)
1284     (EXPAND_TAC "G'" THEN EXPAND_TAC "Da" THEN EXPAND_TAC "D'");
1285     (REWRITE_TAC[]);
1286
1287     (SUBGOAL_THEN `M = ((&4 - &2 * b) * D' - Da * Dc) / sqrt D'` ASSUME_TAC);
1288       (* Subgoal 3.18.4.3 *)
1289     (EXPAND_TAC "M");
1290     (REWRITE_TAC[REAL_ARITH `(&2 - b) * &2 * x = (&4 - &2 * b) * x`]);
1291     (ONCE_ASM_REWRITE_TAC[]);
1292     (ABBREV_TAC `X = (&4 - &2 * b) * sqrt D' -
1293                        Dc * &2 * Da * inv (&2 * sqrt D')`);
1294     (ABBREV_TAC `Y = (&4 - &2 * b) * D' - Da * Dc`);
1295     (ABBREV_TAC `Z = sqrt D'`);
1296
1297       (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
1298          (* Subgoal 3.18.4.3.1 *)
1299       (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);
1300
1301     (FIRST_X_ASSUM MATCH_MP_TAC);
1302     (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
1303     (ABBREV_TAC `m = &4 - &2 * b`);
1304     (REWRITE_TAC[REAL_SUB_RDISTRIB;REAL_NEG_ADD]);
1305     (REWRITE_TAC[REAL_ARITH ` (a * b * c * d) * e = (c * a) * (d * b * e)`]);
1306
1307      (SUBGOAL_THEN `inv (&2 * sqrt D') * &2 * sqrt D' = &1` ASSUME_TAC);
1308          (* Subgoal 3.18.4.3.2 *)
1309      (MATCH_MP_TAC REAL_MUL_LINV);
1310      (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1311      (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
1312      (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1313      (ASM_REWRITE_TAC[]);
1314
1315     (PURE_ONCE_ASM_REWRITE_TAC[]);
1316     (EXPAND_TAC "Y");
1317     (REWRITE_TAC[REAL_MUL_RID]);
1318     (AP_THM_TAC THEN AP_TERM_TAC);
1319     (EXPAND_TAC "m" THEN EXPAND_TAC "Z");
1320     (REWRITE_TAC[REAL_ARITH `(a * b) * c = a * b * c`]);
1321     (REPEAT AP_TERM_TAC);
1322     (REWRITE_TAC[GSYM REAL_POW_2]);
1323     (MATCH_MP_TAC SQRT_POW_2);
1324     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
1325     (ASM_REWRITE_TAC[]);
1326       (* End of Subgoal 3.18.4.3 *)
1327
1328     (SUBGOAL_THEN `M / (&4 * D') * &4 * D' = M` ASSUME_TAC);
1329       (* Subgoal 3.18.4.4 *)
1330     (ASM_SIMP_TAC[REAL_DIV_RMUL]);
1331
1332   (PURE_ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
1333
1334     (SUBGOAL_THEN
1335       `M = ((-- &2 * b + &2 * a' + &2 * c - a' * c) * (&4 - b) * b)/ sqrt D'`
1336        ASSUME_TAC);
1337       (* Subgoal 3.18.4.5 *)
1338     (ONCE_ASM_REWRITE_TAC[]);
1339     (AP_THM_TAC THEN AP_TERM_TAC);
1340     (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
1341     (EXPAND_TAC "Da" THEN EXPAND_TAC "Dc" THEN EXPAND_TAC "f3");
1342     REAL_ARITH_TAC;
1343
1344   (UP_ASM_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
1345   (ONCE_ASM_REWRITE_TAC[]);
1346   (EXPAND_TAC "Dc");
1347   (REWRITE_TAC[REAL_ARITH `a / b / c = a / c / b`]);
1348   (AP_THM_TAC THEN AP_TERM_TAC);
1349
1350     (SUBGOAL_THEN
1351        `&4 * D' + f3 a' pow 2 = a' * (&4 - a') * (&4 - b) * b` ASSUME_TAC);
1352       (* Subgoal 3.18.4.6 *)
1353     (EXPAND_TAC "f3" THEN REWRITE_TAC[POW_2] );
1354     (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
1355    REAL_ARITH_TAC;
1356
1357   (ONCE_ASM_REWRITE_TAC[]);
1358   (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);
1359
1360      (* --------------------------------------------------------------- *)
1361      (*       ~ ( b = &4) /\ ~ (b = &0)                                 *)
1362      (* --------------------------------------------------------------- *)
1363
1364     (SUBGOAL_THEN `~ (b = &4) /\ ~ (b = &0)` ASSUME_TAC);
1365     (ASM_REAL_ARITH_TAC);
1366
1367      (SUBGOAL_THEN `~ ((&4 - b) * b = &0)` ASSUME_TAC);
1368      (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1369      (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);
1370
1371       (* --------------------------------------------------------------- *)
1372       (*       ~ ( a' = &4) /\ ~ (a' = &0)                               *)
1373       (* --------------------------------------------------------------- *)
1374
1375      (SUBGOAL_THEN `~ (a' = &4) /\ ~ (a' = &0)` ASSUME_TAC);
1376      (REPEAT STRIP_TAC);  (* 2 Subgoals *)
1377
1378         (SUBGOAL_THEN ` D' = -- ((c + b - &4) pow 2)` ASSUME_TAC);
1379         (EXPAND_TAC "D'" );
1380         (REWRITE_TAC[ups_x]);
1381         (ONCE_ASM_REWRITE_TAC[]);
1382          REAL_ARITH_TAC;
1383         (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1384         (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
1385         (MESON_TAC[REAL_LE_POW_2]);
1386         (MP_TAC (ASSUME `&0 < D'`));
1387         (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1388
1389         (SUBGOAL_THEN ` D' = -- ((c - b) pow 2)` ASSUME_TAC);
1390         (EXPAND_TAC "D'" );
1391         (REWRITE_TAC[ups_x]);
1392         (ONCE_ASM_REWRITE_TAC[]);
1393          REAL_ARITH_TAC;
1394         (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1395         (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
1396         (MESON_TAC[REAL_LE_POW_2]);
1397         (MP_TAC (ASSUME `&0 < D'`));
1398         (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1399
1400      (SUBGOAL_THEN `~ (a' * (&4 - a') = &0)` ASSUME_TAC);
1401      (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1402      (ASM_REWRITE_TAC[REAL_ARITH ` ~(a - b = &0) <=> ~ (a = b)`]);
1403
1404       (* --------------------------------------------------------------- *)
1405       (*       continue                                                  *)
1406       (* --------------------------------------------------------------- *)
1407
1408   (ABBREV_TAC `x = -- &2 * b + &2 * a' + &2 * c - a' * c`);
1409   (ABBREV_TAC `y = (&4 - b) * b`);
1410   (REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);
1411   (ABBREV_TAC `z = a' * (&4 - a')`);
1412   (ASM_SIMP_TAC[REDUCE_WITH_DIV_Euler_lemma]);
1413   (ASM_MESON_TAC[]);
1414
1415  (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
1416  (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN REPEAT DISCH_TAC);
1417
1418 (* ================ END DIFF 3 ============================================= *)
1419
1420
1421 (* --------------------------------------------------------------------------*)
1422 (*    Subgoal 3.19.                                                          *)
1423 (*       Derivative of  (&8 - a - b - c) / sqrt (ups_x a b c - a * b * c)    *)
1424 (* --------------------------------------------------------------------------*)
1425
1426  (ABBREV_TAC `f4 = (\x. (&8 - x - b - c))`);
1427  (ABBREV_TAC `F42 = (\x. (&8 - x - b - c) / sqrt (ups_x x b c - x * b * c))`);
1428
1429  (SUBGOAL_THEN
1430   `(F42 has_real_derivative (-- &1 * G a' - f4 a' * G') / G a' pow 2)
1431    (atreal a' within s)`
1432    ASSUME_TAC);
1433
1434   (SUBGOAL_THEN ` F42 = (\x:real. f4 x / G x)` ASSUME_TAC);
1435     (* Subgoal 3.19.1  *)
1436   (EXPAND_TAC "F42" THEN EXPAND_TAC "G" THEN EXPAND_TAC "f4");
1437   (REWRITE_TAC[]);
1438
1439  (PURE_ONCE_ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 DEL_TAC);
1440
1441   (SUBGOAL_THEN `(f4 has_real_derivative -- &1) (atreal a' within s) /\
1442                    (G has_real_derivative G') (atreal a' within s) /\
1443                    ~(G a' = &0)` ASSUME_TAC);
1444     (* Subgoal 3.19.2 *)
1445   (ASM_REWRITE_TAC[]);
1446   CONJ_TAC;  (* Break into 2 subgoals *)
1447
1448     (EXPAND_TAC "f4" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
1449       (* End one of 2 subgoals *)
1450     (EXPAND_TAC "G");
1451     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1452     (MATCH_MP_TAC SQRT_POS_LT);
1453     (ASM_REWRITE_TAC[]);
1454
1455  (FIRST_X_ASSUM MP_TAC);
1456  (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
1457  (MESON_TAC[]);
1458
1459 (* --------------------------------------------------------------------------*)
1460 (*    Subgoal 3.20.                                                          *)
1461 (*  Derivative of  atn ((&8 - a - b - c) / sqrt (ups_x a b c - a * b * c))   *)
1462 (* --------------------------------------------------------------------------*)
1463
1464  (ABBREV_TAC
1465   `F4 = (\x. atn ((&8 - x - b - c) / (sqrt (ups_x x b c - x * b * c))))`);
1466
1467  (SUBGOAL_THEN
1468   `(F4 has_real_derivative
1469     (-- &1 * G a' - f4 a' * G') / G a' pow 2 * inv (&1 + F42 a' pow 2))
1470    (atreal a' within s)`
1471   ASSUME_TAC);
1472
1473   (SUBGOAL_THEN `F4 = (\x. atn (F42 (x:real)))` ASSUME_TAC);
1474     (* Subgoal 3.20.1 *)
1475   (EXPAND_TAC "F4" THEN EXPAND_TAC "F42");
1476   (REWRITE_TAC[]);
1477
1478  (PURE_ONCE_ASM_REWRITE_TAC[]);
1479  (REPLICATE_TAC 2 DEL_TAC);
1480  (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
1481  (ABBREV_TAC `f' = ( -- &1 * G (a':real) - f4 a' * G') / G  a' pow 2`);
1482
1483   (SUBGOAL_THEN
1484      `inv (&1 + F42 a' pow 2) = g' ((F42:real-> real) a')`
1485      ASSUME_TAC);
1486     (* Subgoal 3.20.2 *)
1487   (EXPAND_TAC "F42" THEN EXPAND_TAC "g'");
1488   (REWRITE_TAC[]);
1489
1490   (SUBGOAL_THEN
1491    `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
1492      ASSUME_TAC);
1493     (* Subgoal 3.20.3 *)
1494   (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
1495   (REWRITE_TAC[EQ_UNIV;HAS_REAL_DERIVATIVE_ATN]);
1496
1497   (SUBGOAL_THEN
1498    `(F42 has_real_derivative f') (atreal a' within s) /\
1499     (:real) ((F42:real->real) a')`
1500     ASSUME_TAC);
1501     (* Subgoal 3.20.4 *)
1502   (ASM_REWRITE_TAC[]);
1503   (MESON_TAC[EQ_UNIV;IN_UNIV;IN]);
1504
1505  (ONCE_ASM_REWRITE_TAC[]);
1506  (REPLICATE_TAC 2 UP_ASM_TAC);
1507  (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
1508  (MESON_TAC[]);
1509
1510
1511 (* ========================================================================= *)
1512 (*           THIS PART TO TO REDUCE THE DERIVATIVE OF F4                     *)
1513 (*             Derivative of  F4 is  ..... ........                          *)
1514 (* ========================================================================= *)
1515 (*          Subgoal 3.21                                                     *)
1516 (* ------------------------------------------------------------------------- *)
1517
1518  (SUBGOAL_THEN
1519    `(F4 has_real_derivative (a' - b - c) / &2 / (&4 - a') / sqrt D')
1520     (atreal a' within s)`
1521   ASSUME_TAC);
1522
1523   (SUBGOAL_THEN `G (a':real) = sqrt D'` ASSUME_TAC);
1524     (* Subgoal 3.21.1 *)
1525   (EXPAND_TAC "G" THEN EXPAND_TAC "D'");
1526   (REWRITE_TAC[]);
1527
1528  (ABBREV_TAC `D4 = &8 - a' - b - c`);
1529
1530   (SUBGOAL_THEN `f4 (a':real) = (D4:real)` ASSUME_TAC);
1531     (* Subgoal 3.21.2 *)
1532   (EXPAND_TAC "f4" THEN EXPAND_TAC "D4");
1533   (REWRITE_TAC[]);
1534
1535   (SUBGOAL_THEN `&0 < sqrt D'` ASSUME_TAC);
1536     (* Subgoal 3.21.3 *)
1537   (MATCH_MP_TAC SQRT_POS_LT);
1538   (ASM_REWRITE_TAC[]);
1539
1540   (SUBGOAL_THEN
1541    `(-- &1 * G a' - f4 a' * G') / G a' pow 2 * inv (&1 + F42 a' pow 2) =
1542     (a' - b - c) / &2 / (&4 - a') / sqrt D'`
1543     ASSUME_TAC);
1544     (* Subgoal 3.21.4 *)
1545   (ASM_REWRITE_TAC[]);
1546
1547     (SUBGOAL_THEN `sqrt D' pow 2 = D'` ASSUME_TAC);
1548       (* Subgoal 3.21.4.1 *)
1549     (MATCH_MP_TAC SQRT_POW_2);
1550     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
1551     (ASM_REWRITE_TAC[]);
1552
1553     (SUBGOAL_THEN
1554       `inv (&1 + F42 (a':real) pow 2)  = D' / (D' + D4 pow 2)` ASSUME_TAC);
1555       (* Subgoal 3.21.4.2 *)
1556     (EXPAND_TAC "F42");
1557     (ONCE_ASM_REWRITE_TAC[]);
1558     (REWRITE_TAC[REAL_POW_DIV]);
1559     (ONCE_ASM_REWRITE_TAC[]);
1560     (PURE_ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
1561     AP_TERM_TAC;
1562     (PURE_ONCE_REWRITE_TAC[REAL_INV_DIV]);
1563     (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
1564     (AP_THM_TAC THEN AP_TERM_TAC);
1565     (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
1566     (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (&0 = a)`));
1567     (ASM_REWRITE_TAC[]);
1568
1569   (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC THEN DEL_TAC);
1570   (PURE_REWRITE_TAC[REAL_ARITH `-- &1 * x = -- x`]);
1571   (ABBREV_TAC `M = -- sqrt D' - D4 * G'`);
1572
1573     (SUBGOAL_THEN
1574       `D' + D4 pow 2 = (&4 - a') * (&4 - b) * (&4 - c)` ASSUME_TAC);
1575       (* Subgoal 3.21.4.3 *)
1576     (EXPAND_TAC "D4");
1577     (EXPAND_TAC "D'" THEN REWRITE_TAC[ups_x]);
1578     (EXPAND_TAC "f4");
1579     REAL_ARITH_TAC;
1580
1581     (SUBGOAL_THEN `G' = Da * inv (&2 * sqrt D')` ASSUME_TAC);
1582       (* Subgoal 3.21.4.4 *)
1583     (EXPAND_TAC "G'" THEN EXPAND_TAC "Da");
1584     (REPEAT AP_TERM_TAC);
1585     (ASM_REWRITE_TAC[]);
1586
1587     (SUBGOAL_THEN
1588      `M = (a' - b - c) * ((&4 - b) * (&4 - c)) / &2 / sqrt D'` ASSUME_TAC);
1589       (* Subgoal 3.21.4.5 *)
1590     (EXPAND_TAC "M");
1591     (UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
1592     (ONCE_ASM_REWRITE_TAC[]);
1593     (ABBREV_TAC `X = --sqrt D' - D4 * Da * inv (&2 * sqrt D') `);
1594     (REWRITE_TAC[REAL_ARITH `a * (b * c) / d / e = ((a * b * c) / d) / e`]);
1595     (ABBREV_TAC `Y = ((a' - b - c) * (&4 - b) * (&4 - c)) / &2`);
1596     (ABBREV_TAC `Z = sqrt D'`);
1597
1598      (SUBGOAL_THEN `X * Z = Y ==> X = Y / Z ` ASSUME_TAC);
1599         (* Subgoal 3.21.4.5.1 *)
1600      (ASM_SIMP_TAC[REAL_EQ_RDIV_EQ]);
1601
1602     (FIRST_ASSUM MATCH_MP_TAC);
1603     (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
1604     (REWRITE_TAC[REAL_SUB_RDISTRIB]);
1605
1606      (SUBGOAL_THEN `--sqrt D' * sqrt D' = -- D'` ASSUME_TAC);
1607         (* Subgoal 3.21.4.5.2 *)
1608      (MATCH_MP_TAC (REAL_ARITH `a * b = c ==> -- a * b = -- c`));
1609      (REWRITE_TAC[GSYM REAL_POW_2]);
1610      (MATCH_MP_TAC SQRT_POW_2);
1611      (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
1612      (ASM_REWRITE_TAC[]);
1613
1614      (SUBGOAL_THEN
1615         `(D4 * Da * inv (&2 * sqrt D')) * sqrt D' = D4 * Da / &2` ASSUME_TAC);
1616         (* Subgoal 3.21.4.5.3 *)
1617      (REWRITE_TAC[REAL_INV_MUL]);
1618      (REWRITE_TAC[REAL_ARITH
1619        `(a * b * c * d) * e = (a * b * c) * (d * e)`]);
1620
1621          (SUBGOAL_THEN `inv (sqrt D') * sqrt D' = &1 ` ASSUME_TAC);
1622          (MATCH_MP_TAC REAL_MUL_LINV);
1623          (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
1624          (MATCH_MP_TAC SQRT_POS_LT);
1625          (ASM_REWRITE_TAC[]);
1626
1627      (ASM_REWRITE_TAC[REAL_MUL_RID]);
1628       REAL_ARITH_TAC;
1629
1630     (ASM_REWRITE_TAC[]);
1631     (EXPAND_TAC "D'" THEN EXPAND_TAC "D4" THEN EXPAND_TAC "Da");
1632     (REWRITE_TAC[ups_x]);
1633     (EXPAND_TAC "f4");
1634     (REAL_ARITH_TAC);
1635    (* End Subgoal 3.21.4.5 *)
1636
1637   (REWRITE_TAC[REAL_ARITH `a / b * c / d = (a / b * c) / d`]);
1638
1639     (SUBGOAL_THEN `(M / D' * D') = M` ASSUME_TAC);
1640     (MATCH_MP_TAC REAL_DIV_RMUL);
1641     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ ( x = &0) `));
1642     (ASM_REWRITE_TAC[]);
1643
1644   (ASM_REWRITE_TAC[]);
1645   (REWRITE_TAC[REAL_ARITH `(a * x / b / c) / d = (a * x / d) / b / c`]);
1646   (AP_THM_TAC THEN AP_TERM_TAC);
1647   (ONCE_REWRITE_TAC[REAL_ARITH ` a/ &2 / b = a / b / &2`]);
1648   (AP_THM_TAC THEN AP_TERM_TAC);
1649   (ABBREV_TAC `S = (&4 - b) * (&4 - c)`);
1650
1651         (* ----------------------------------------------------- *)
1652         (*       ~ ( c = &4)                                     *)
1653         (* ----------------------------------------------------- *)
1654          (SUBGOAL_THEN `~ (&4 - b = &0) /\ ~ (&4 - c = &0)` ASSUME_TAC);
1655           ASM_REAL_ARITH_TAC;
1656
1657         (* ----------------------------------------------------- *)
1658         (*        ~ (a' = &4)                                     *)
1659         (* ----------------------------------------------------- *)
1660
1661          (SUBGOAL_THEN `~ (&4 - a' = &0)` ASSUME_TAC);
1662          (MATCH_MP_TAC (REAL_ARITH `~ (x = &4) ==> ~ (&4 - x = &0)`));
1663           STRIP_TAC;
1664
1665            (SUBGOAL_THEN ` D' = -- ((b + c - &4) pow 2)` ASSUME_TAC);
1666            (EXPAND_TAC "D'" );
1667            (REWRITE_TAC[ups_x]);
1668            (ONCE_ASM_REWRITE_TAC[]);
1669             REAL_ARITH_TAC;
1670
1671            (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1672            (ASM_REWRITE_TAC[REAL_ARITH `-- a <= &0 <=> &0 <= a`]);
1673            (MESON_TAC[REAL_LE_POW_2]);
1674
1675            (MP_TAC (ASSUME `&0 < D'`));
1676            (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1677
1678 (* ===================================================================== *)
1679
1680         (* ----------------------------------------------------- *)
1681         (*        Continue                                       *)
1682         (* ----------------------------------------------------- *)
1683
1684     (SUBGOAL_THEN `~ (S = &0)` ASSUME_TAC);
1685     (EXPAND_TAC "S");
1686     (REWRITE_TAC [REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b `]);
1687     (ASM_REWRITE_TAC[]);
1688
1689   (ASM_MESON_TAC[REDUCE_WITH_DIV_Euler_lemma]);
1690     (* End of subgoal  *)
1691
1692  (ASM_MESON_TAC[]);
1693  (UP_ASM_TAC);
1694  (DEL_TAC THEN UP_ASM_TAC);
1695  (DEL_TAC THEN DEL_TAC THEN DEL_TAC);
1696  (REPEAT DISCH_TAC);
1697
1698
1699 (* ================ END DIFF 4 ============================================== *)
1700
1701
1702 (* ========================================================================= *)
1703 (*               END OF THE FIRST GOAL                                       *)
1704 (* ========================================================================= *)
1705
1706 (* ------------------------------------------------------------------------- *)
1707 (*          Subgoal 3.22                                                     *)
1708 (* ------------------------------------------------------------------------- *)
1709
1710  (ABBREV_TAC `FUNCTION = (\a. --pi / &2 -
1711        atn
1712        ((-- &2 * a + &2 * b + &2 * c - b * c) /
1713         (&2 * sqrt (ups_x a b c - a * b * c))) -
1714        atn
1715        ((-- &2 * b + &2 * c + &2 * a - c * a) /
1716         (&2 * sqrt (ups_x a b c - a * b * c))) -
1717        atn
1718        ((-- &2 * c + &2 * a + &2 * b - a * b) /
1719         (&2 * sqrt (ups_x a b c - a * b * c))) +
1720        &2 * atn ((&8 - a - b - c) / sqrt (ups_x a b c - a * b * c)))`);
1721
1722   (SUBGOAL_THEN
1723     `FUNCTION = (\(a:real). --pi / &2 - F1 a - F2 a - F3 a + &2 * F4 a)`
1724      ASSUME_TAC);
1725   (EXPAND_TAC "FUNCTION");
1726   (EXPAND_TAC "F1" THEN EXPAND_TAC "F2");
1727   (EXPAND_TAC "F3" THEN EXPAND_TAC "F4");
1728   (REWRITE_TAC[]);
1729
1730  (ABBREV_TAC `F1' = -- &1 / sqrt D'`);
1731  (ABBREV_TAC `F2' =
1732   (-- &2 * c + &2 * a' + &2 * b - a' * b) / (a' * (&4 - a')) / sqrt D'`);
1733  (ABBREV_TAC `F3' =
1734   (-- &2 * b + &2 * a' + &2 * c - a' * c) / (a' * (&4 - a')) / sqrt D'`);
1735  (ABBREV_TAC `F4' = (a' - b - c) / &2 / (&4 - a') / sqrt D'`);
1736
1737 (* ------------------------------------------------------------------------- *)
1738 (*          Subgoal 3.23                                                     *)
1739 (* ------------------------------------------------------------------------- *)
1740
1741   (SUBGOAL_THEN ` &0 - F1' - F2' - F3' + &2 * F4' = &0` ASSUME_TAC);
1742   (EXPAND_TAC "F1'" THEN EXPAND_TAC "F2'");
1743   (EXPAND_TAC "F3'" THEN EXPAND_TAC "F4'");
1744   (REWRITE_TAC[REAL_ARITH `&0 - a - b - c + d = &0 <=> a + b + c = d `]);
1745   (REWRITE_TAC[REAL_ARITH `a / x + b / x = (a + b) / x`]);
1746   (REWRITE_TAC[REAL_ARITH `a * b / c / d / e  = ((a * b / c) / d) / e`]);
1747   (AP_THM_TAC THEN AP_TERM_TAC);
1748   (REWRITE_TAC[REAL_ARITH
1749       `(-- &2 * c + &2 * a' + &2 * b - a' * b) +
1750         -- &2 * b + &2 * a' + &2 * c - a' * c =
1751         a' * (&4 - b - c)`]);
1752
1753     (* --------------------------------------------------------------- *)
1754     (*       ~ ( a' = &4) /\ ~ (a' = &0)                               *)
1755     (* --------------------------------------------------------------- *)
1756
1757     (SUBGOAL_THEN `~ (&4 - a' = &0) /\ ~ (a' = &0)` ASSUME_TAC);
1758     (REWRITE_TAC[REAL_ARITH `~ (&4 - a' = &0) <=> ~ (a' = &4)`]);
1759     (REPEAT STRIP_TAC);  (* 2 Subgoals *)
1760
1761      (SUBGOAL_THEN ` D' = -- ((c + b - &4) pow 2)` ASSUME_TAC);
1762      (EXPAND_TAC "D'" );
1763      (REWRITE_TAC[ups_x]);
1764      (ONCE_ASM_REWRITE_TAC[]);
1765       REAL_ARITH_TAC;
1766      (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1767      (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
1768      (MESON_TAC[REAL_LE_POW_2]);
1769      (MP_TAC (ASSUME `&0 < D'`));
1770      (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1771
1772      (SUBGOAL_THEN ` D' = -- ((c - b) pow 2)` ASSUME_TAC);
1773      (EXPAND_TAC "D'" );
1774      (REWRITE_TAC[ups_x]);
1775      (ONCE_ASM_REWRITE_TAC[]);
1776       REAL_ARITH_TAC;
1777      (SUBGOAL_THEN `D' <= &0` ASSUME_TAC);
1778      (ASM_REWRITE_TAC[REAL_ARITH `-- c <= &0 <=> &0 <= c`]);
1779      (MESON_TAC[REAL_LE_POW_2]);
1780      (MP_TAC (ASSUME `&0 < D'`));
1781      (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1782
1783     (SUBGOAL_THEN `~ (a' * (&4 - a') = &0)` ASSUME_TAC);
1784     (REWRITE_TAC[REAL_ENTIRE;MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
1785     (ASM_REWRITE_TAC[]);
1786
1787   (REWRITE_TAC[REAL_ARITH `&2 * x / &2 = x`]);
1788
1789     (SUBGOAL_THEN `-- &1 = -- (&4 - a') / (&4 - a')` ASSUME_TAC);
1790     (MATCH_MP_TAC (REAL_ARITH `(a = b/c) ==> (-- a = -- b/c)`));
1791     (ASM_SIMP_TAC[REAL_DIV_REFL]);
1792
1793   (ASM_REWRITE_TAC[]);
1794   (REWRITE_TAC[REAL_ARITH `(-- x /y + z = t / y) <=> (z = (t + x) / y)`]);
1795   (REWRITE_TAC[REAL_ARITH `a - x - y + z - a = z - x - y`]);
1796   (REWRITE_TAC[REAL_ARITH `(x * y) / (x * z) = y * x / (z * x)`]);
1797   (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
1798   (ASM_REWRITE_TAC[]);
1799
1800  (UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC);
1801  (REPLICATE_TAC 5 (UP_ASM_TAC THEN DEL_TAC));
1802  (REPEAT DISCH_TAC);
1803
1804 (* ------------------------------------------------------------------------- *)
1805 (*          Subgoal 3.24                                                     *)
1806 (* ------------------------------------------------------------------------- *)
1807
1808  (ABBREV_TAC `FUNC1 = (\(a:real). F1 a + F2 a + F3 a)`);
1809  (ABBREV_TAC `FUNC2 = (\(a:real). --pi / &2 + &2 * F4 a)`);
1810
1811   (SUBGOAL_THEN
1812      `(FUNC1 has_real_derivative F1' + F2' + F3') (atreal a' within s)`
1813      ASSUME_TAC);
1814   (ABBREV_TAC `X = (\(a:real). F2 a + F3 a)`);
1815   (ABBREV_TAC `X' = F2' + F3'`);
1816
1817     (SUBGOAL_THEN
1818       `(X has_real_derivative X') (atreal a' within s)` ASSUME_TAC);
1819       (* Subgoal 3.24.1 *)
1820     (EXPAND_TAC "X" THEN EXPAND_TAC "X'");
1821     (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);
1822
1823     (SUBGOAL_THEN `FUNC1 = (\(a:real). F1 a + X a)` ASSUME_TAC);
1824       (* Subgoal 3.24.2 *)
1825     (EXPAND_TAC "X");
1826     (ASM_REWRITE_TAC[]);
1827
1828     (ASM_REWRITE_TAC[]);
1829     (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);
1830
1831 (* ------------------------------------------------------------------------- *)
1832 (*          Subgoal 3.25                                                     *)
1833 (* ------------------------------------------------------------------------- *)
1834
1835   (SUBGOAL_THEN
1836     `(FUNC2 has_real_derivative &0 + &2 * F4') (atreal a' within s)`
1837      ASSUME_TAC);
1838   (ABBREV_TAC `X = (\(a:real). -- pi / &2)`);
1839   (ABBREV_TAC `Y = (\(a:real). &2 * F4 a)`);
1840
1841     (SUBGOAL_THEN
1842      `(X has_real_derivative &0) (atreal a' within s)` ASSUME_TAC);
1843       (* Subgoal 3.25.1 *)
1844     (EXPAND_TAC "X");
1845     (REAL_DIFF_TAC);
1846     (REWRITE_TAC[]);
1847
1848     (SUBGOAL_THEN
1849       `(Y has_real_derivative &2 * F4') (atreal a' within s)` ASSUME_TAC);
1850       (* Subgoal 3.25.2 *)
1851     (EXPAND_TAC "Y");
1852     (MATCH_MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN);
1853     (ASM_REWRITE_TAC[]);
1854
1855     (SUBGOAL_THEN `FUNC2 = (\(a:real). X a + Y a)` ASSUME_TAC);
1856       (* Subgoal 3.25.3 *)
1857     (EXPAND_TAC "X" THEN EXPAND_TAC "Y");
1858     (ASM_REWRITE_TAC[]);
1859
1860   (ASM_REWRITE_TAC[]);
1861   (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);
1862
1863 (* ------------------------------------------------------------------------- *)
1864 (*          Subgoal 3.26                                                     *)
1865 (* ------------------------------------------------------------------------- *)
1866
1867   (SUBGOAL_THEN `FUNCTION = (\(a:real). FUNC2 a - FUNC1 a)` ASSUME_TAC);
1868   (EXPAND_TAC "FUNC1" THEN EXPAND_TAC "FUNC2");
1869   (REWRITE_TAC[REAL_ARITH `(a + b) - (c + d + e) = a - c - d - e + b`]);
1870   (ASM_REWRITE_TAC[]);
1871
1872 (* ------------------------------------------------------------------------- *)
1873 (*          Subgoal 3.27                                                     *)
1874 (* ------------------------------------------------------------------------- *)
1875
1876   (SUBGOAL_THEN
1877    `(FUNCTION has_real_derivative &0 - F1' - F2' - F3' + &2 * F4')
1878     (atreal a' within s)`
1879     ASSUME_TAC);
1880   (REWRITE_TAC[REAL_ARITH `a - c - d - e + b = (a + b) - (c + d + e)`]);
1881   (ASM_MESON_TAC[HAS_REAL_DERIVATIVE_SUB]);
1882
1883  (ASM_MESON_TAC[]);
1884
1885
1886 (* ========================================================================= *)
1887 (*                                                                           *)
1888 (*                 FINISH COMPUTE FIRST DERIVATIVES                          *)
1889 (*                                                                           *)
1890 (* ========================================================================= *)
1891
1892
1893 (* ------------------------------------------------------------------------- *)
1894 (*       SUBGOAL 4.1                                                         *)
1895 (*       ~ ( c = &4) /\ ~ (c = &0)                                           *)
1896 (* ------------------------------------------------------------------------- *)
1897
1898   (SUBGOAL_THEN `~ (c = &4) /\ ~ (c = &0)` ASSUME_TAC);
1899   ASM_REAL_ARITH_TAC;
1900
1901 (* ------------------------------------------------------------------------- *)
1902 (*       SUBGOAL 4.2                                                         *)
1903 (*                     Reduce the expression                                 *)
1904 (* ------------------------------------------------------------------------- *)
1905
1906  (PURE_REWRITE_TAC[REAL_ARITH
1907   `&8 - (b + c - (b * c) / &2) - b - c =
1908    &8 + (b * c) / &2 - &2 * b  - &2 * c`]);
1909  (PURE_REWRITE_TAC[REAL_ARITH
1910     `-- &2 * (b + c - (b * c) / &2) + &2 * b + &2 * c - b * c = &0 `]);
1911  (REWRITE_TAC[REAL_ARITH `&0 * x = &0 /\ &0 / x = &0`;
1912                ATN_0; REAL_ARITH `a - &0 = a`]);
1913  (PURE_REWRITE_TAC[REAL_ARITH
1914   `-- &2 * b + &2 * c + &2 * (b + c - (b * c) / &2) -
1915    c * (b + c - (b * c) / &2) =
1916   (&1 - b / &2) * (&4 - c) * c `]);
1917  (PURE_REWRITE_TAC[REAL_ARITH
1918   `-- &2 * c + &2 * (b + c - (b * c) / &2) +
1919    &2 * b - (b + c - (b * c) / &2) * b =
1920    (&1 - c / &2) * (&4 - b) * b`]);
1921  (PURE_REWRITE_TAC[ups_x]);
1922  (PURE_REWRITE_TAC[REAL_ARITH
1923    `(--(b + c - (b * c) / &2) * (b + c - (b * c) / &2) - b * b - c * c +
1924     &2 * (b + c - (b * c) / &2) * c +
1925     &2 * (b + c - (b * c) / &2) * b +
1926     &2 * b * c) -
1927     (b + c - (b * c) / &2) * b * c =
1928    (((&4 - b) * b) * (&4 - c) * c) / &4`]);
1929
1930
1931 (* ------------------------------------------------------------------------- *)
1932 (*       SUBGOAL 4.                                                           *)
1933 (*                                                                            *)
1934 (* ------------------------------------------------------------------------- *)
1935
1936
1937  (SUBGOAL_THEN
1938   `!r b. c IN r /\
1939      is_realinterval r /\
1940      b IN r /\
1941      (!y. y IN r ==> &0 < ((&4 - y) * y) * (&4 - c) * c)
1942      ==> --pi / &2 -
1943          atn
1944          (((&1 - b / &2) * (&4 - c) * c) /
1945           (&2 * sqrt ((((&4 - b) * b) * (&4 - c) * c) / &4))) -
1946          atn
1947          (((&1 - c / &2) * (&4 - b) * b) /
1948           (&2 * sqrt ((((&4 - b) * b) * (&4 - c) * c) / &4))) +
1949          &2 *
1950          atn
1951          ((&8 + (b * c) / &2 - &2 * b - &2 * c) /
1952           sqrt ((((&4 - b) * b) * (&4 - c) * c) / &4)) =
1953          &0`
1954  ASSUME_TAC);
1955
1956  (REPEAT GEN_TAC  THEN STRIP_TAC);
1957  SWITCH_TAC;
1958  (FIRST_X_ASSUM MP_TAC THEN SPEC_TAC (`b':real`, `x:real`) );
1959  (MATCH_MP_TAC HAS_REAL_DERIVATIVE_ZERO_CONSTANT2 THEN EXISTS_TAC `c:real`);
1960  (ASM_REWRITE_TAC[]);
1961  STRIP_TAC;  (* Break into 2 Subgoals *)
1962
1963   (* The first one *)
1964   (ABBREV_TAC `C = (&4 - c) * c`);
1965   (ABBREV_TAC
1966      `FUNCTION = (\x. --pi / &2 -
1967            atn
1968            (((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4))) -
1969            atn
1970            (((&1 - c / &2) * (&4 - x) * x) /
1971             (&2 * sqrt ((((&4 - x) * x) * C) / &4))) +
1972            &2 *
1973            atn
1974            ((&8 + (x * c) / &2 - &2 * x - &2 * c) /
1975             sqrt ((((&4 - x) * x) * C) / &4)))`);
1976   (ABBREV_TAC
1977     `F1 = (\x. atn
1978     (((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4))))`);
1979   (ABBREV_TAC
1980     `F2 = (\x. atn
1981            (((&1 - c / &2) * (&4 - x) * x) /
1982             (&2 * sqrt ((((&4 - x) * x) * C) / &4))))`);
1983   (ABBREV_TAC
1984     `F3 = (\x. atn
1985            ((&8 + (x * c) / &2 - &2 * x - &2 * c) /
1986             sqrt ((((&4 - x) * x) * C) / &4)))`);
1987
1988   (SUBGOAL_THEN
1989     `FUNCTION = (\(x:real). --pi / &2 - F1 x - F2 x + &2 * F3 x)`
1990      ASSUME_TAC);
1991   (EXPAND_TAC "F1" THEN EXPAND_TAC "F2" THEN EXPAND_TAC "F3");
1992   (EXPAND_TAC "FUNCTION");
1993   (REWRITE_TAC[]);
1994
1995  (GEN_TAC THEN DISCH_TAC);
1996
1997
1998 (* ------------------------------------------------------------------------- *)
1999 (*       SUBGOAL 4.                                                           *)
2000 (*                                                                            *)
2001 (* ------------------------------------------------------------------------- *)
2002
2003  (ABBREV_TAC `D' = (((&4 - x) * x) * C) / &4`);
2004   (SUBGOAL_THEN `&0 < D'` ASSUME_TAC);
2005     (* Subgoal *)
2006   (EXPAND_TAC "D'" THEN DEL_TAC);
2007   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 < a / &4`));
2008    UP_ASM_TAC;
2009   (ASM_MESON_TAC[]);
2010
2011 (* --------------------------------------------------------------------------*)
2012 (*         Derivativ of sqrt ((((&4 - x) * x) * C) / &4)                *)
2013 (* --------------------------------------------------------------------------*)
2014
2015  (ABBREV_TAC `G = (\x.  sqrt ((((&4 - x) * x) * C) / &4))`);
2016  (ABBREV_TAC `G' =
2017   (((&4 - &2 * x) * C) / &4) * inv (&2 * sqrt ((((&4 - x) * x) * C) / &4))`);
2018
2019   (SUBGOAL_THEN `(G has_real_derivative G') (atreal x within r)` ASSUME_TAC);
2020     (* Subgoal *)
2021
2022   (ABBREV_TAC `f = (\x. (((&4 - x) * x) * C) / &4)`);
2023
2024     (SUBGOAL_THEN `G = (\x:real. sqrt (f x))` ASSUME_TAC);
2025       (* Subgoal *)
2026     (EXPAND_TAC "f" THEN ASM_REWRITE_TAC[]);
2027
2028   (ABBREV_TAC `g' = (\x. inv (&2 * sqrt x))`);
2029   (ABBREV_TAC `f' = ((&4 - &2 * x) * C)/ &4 `);
2030   (ABBREV_TAC `P = {x:real | &0 < x}`);
2031
2032     (SUBGOAL_THEN
2033      `!x. P x ==> (sqrt has_real_derivative (g':real->real) x) (atreal x)`
2034       ASSUME_TAC);
2035       (* Subgoal *)
2036     (EXPAND_TAC "g'" THEN REWRITE_TAC[BETA_THM]);
2037     (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
2038     (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
2039
2040     (SUBGOAL_THEN
2041        `(f has_real_derivative f') (atreal x within r) /\
2042         (P:real->bool) (f x)` ASSUME_TAC);
2043       (* Subgoal *)
2044
2045       CONJ_TAC;
2046        (EXPAND_TAC "f" THEN EXPAND_TAC "f'");
2047        (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
2048        (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
2049        (EXPAND_TAC "f");
2050        (ASM_REWRITE_TAC[]);
2051
2052     (SUBGOAL_THEN `G' = f' * (g' ((f:real->real) x))` ASSUME_TAC);
2053       (* Subgoal *)
2054     (EXPAND_TAC "G'" THEN EXPAND_TAC "f'");
2055     (EXPAND_TAC "g'" THEN EXPAND_TAC "f" );
2056     (REWRITE_TAC[]);
2057
2058   (ONCE_ASM_REWRITE_TAC[]);
2059   (DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
2060   (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2 THEN MESON_TAC[]);
2061
2062 (* --------------------------------------------------------------------------*)
2063 (*         Derivative of &2 * sqrt ((((&4 - x) * x) * C) / &4)           *)
2064 (* --------------------------------------------------------------------------*)
2065
2066  (ABBREV_TAC `2G = (\x.  &2 * sqrt ((((&4 - x) * x) * C) / &4))`);
2067   (SUBGOAL_THEN
2068     `(2G has_real_derivative &2 * G') (atreal x within r)` ASSUME_TAC);
2069
2070     (SUBGOAL_THEN `2G = (\x:real. &2 * G x)` ASSUME_TAC);
2071     (EXPAND_TAC "2G" THEN EXPAND_TAC "G" THEN MESON_TAC[]);
2072
2073   (ONCE_ASM_REWRITE_TAC[]);
2074   (DEL_TAC THEN DEL_TAC );
2075   (FIRST_X_ASSUM MP_TAC);
2076   (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN THEN MESON_TAC[]);
2077
2078 (* --------------------------------------------------------------------------*)
2079 (*         Derivative of  ((&1 - x / &2) * C) /                          *)
2080 (*            (&2 * sqrt ((((&4 - x) * x) * C) / &4))                    *)
2081 (* --------------------------------------------------------------------------*)
2082
2083  (ABBREV_TAC `f1 = (\x. (&1 - x / &2) * C)`);
2084  (ABBREV_TAC `F12 =
2085   (\x. ((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4)))`);
2086
2087   (SUBGOAL_THEN
2088     `(F12 has_real_derivative
2089      ((-- &1 / &2 * C) * 2G x - f1 x * &2 * G') / 2G x pow 2)
2090      (atreal x within r)`
2091      ASSUME_TAC);
2092
2093     (SUBGOAL_THEN `F12 = (\x:real.  f1 x / 2G x)` ASSUME_TAC);
2094       (* Subgoal *)
2095     (EXPAND_TAC "F12" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f1");
2096     (REWRITE_TAC[]);
2097
2098   (ASM_REWRITE_TAC[] THEN DEL_TAC);
2099
2100     (SUBGOAL_THEN
2101       `(f1 has_real_derivative (-- &1 / &2) * C) (atreal x within r) /\
2102        (2G has_real_derivative &2 * G') (atreal x within r) /\ ~(2G x = &0)`
2103        ASSUME_TAC);
2104       (*  Subgoal *)
2105     (ASM_REWRITE_TAC[]);
2106      CONJ_TAC;  (* Break into 2 subgoals *)
2107
2108       (EXPAND_TAC "f1" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
2109       (EXPAND_TAC "2G");
2110       (MATCH_MP_TAC (MESON[REAL_ENTIRE]
2111          `~ (x = &0) /\ ~ (y = &0) ==> ~ (x * y = &0)`));
2112       (REWRITE_TAC[REAL_ARITH `~(&2 = &0)`]);
2113       (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
2114       (MATCH_MP_TAC SQRT_POS_LT);
2115       (ASM_REWRITE_TAC[]);
2116
2117    UP_ASM_TAC;
2118    (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
2119    (MESON_TAC[]);
2120
2121 (* --------------------------------------------------------------------------*)
2122 (*         Derivative of  atn ((&1 - x / &2) * C) /                      *)
2123 (*            (&2 * sqrt ((((&4 - x) * x) * C) / &4))                    *)
2124 (* --------------------------------------------------------------------------*)
2125
2126   (SUBGOAL_THEN
2127     `(F1 has_real_derivative
2128      ((-- &1 / &2 * C) * 2G x - f1 x * &2 * G') / 2G x pow 2 *
2129      inv (&1 + F12 x pow 2))
2130      (atreal x within r)`
2131      ASSUME_TAC);
2132
2133     (SUBGOAL_THEN `F1 = (\x:real. atn (F12 x))` ASSUME_TAC);
2134       (* Subgoal *)
2135     (EXPAND_TAC "F1" THEN EXPAND_TAC "F12");
2136     (REWRITE_TAC[]);
2137
2138   (ONCE_ASM_REWRITE_TAC[]);
2139    DEL_TAC;
2140   (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
2141   (ABBREV_TAC `f' =
2142     ((-- &1 / &2 * C) * 2G (x:real) - f1 x * &2 * G') / 2G x pow 2`);
2143
2144     (SUBGOAL_THEN
2145       `inv (&1 + F12 x pow 2) = g' ((F12:real-> real) x)`
2146        ASSUME_TAC);
2147       (* Subgoal *)
2148     (EXPAND_TAC "F12" THEN EXPAND_TAC "g'");
2149     (REWRITE_TAC[]);
2150
2151   (ONCE_ASM_REWRITE_TAC[]);
2152
2153     (SUBGOAL_THEN
2154      `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
2155       ASSUME_TAC);
2156       (* Subgoal *)
2157     (EXPAND_TAC "g'");
2158     (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
2159
2160
2161     (SUBGOAL_THEN
2162       `(F12 has_real_derivative f') (atreal x within r) /\
2163        (:real) (F12 x)` ASSUME_TAC);
2164       (* Subgoal *)
2165     (ASM_REWRITE_TAC[]);
2166     (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
2167
2168   (REPLICATE_TAC 2 UP_ASM_TAC);
2169   (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
2170   (MESON_TAC[]);
2171
2172 (* --------------------------------------------------------------------------*)
2173 (*                                                                           *)
2174 (*                                                                           *)
2175 (* --------------------------------------------------------------------------*)
2176
2177   (ABBREV_TAC `X = (&4 - x) * x`);
2178   (SUBGOAL_THEN `~(X = &0)` ASSUME_TAC);
2179    STRIP_TAC;
2180     (SUBGOAL_THEN `D' = &0` ASSUME_TAC);
2181     (EXPAND_TAC "D'");
2182     (REWRITE_TAC[REAL_ARITH `(a * x)/ &4 = a * (x / &4)`]);
2183     (ONCE_ASM_REWRITE_TAC[]);
2184      REAL_ARITH_TAC;
2185   (MP_TAC (ASSUME `&0 < D'`));
2186   (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2187
2188   (SUBGOAL_THEN `~(&4 - x = &0) /\ ~(x = &0)` ASSUME_TAC);
2189   (UP_ASM_TAC THEN EXPAND_TAC "X");
2190   (REWRITE_TAC[REAL_ENTIRE]);
2191   (MESON_TAC[]);
2192
2193   (SUBGOAL_THEN
2194     `inv (&1 + F12 (x:real) pow 2) = X / (X + C - X * C / &4)`
2195      ASSUME_TAC);
2196   (ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
2197    AP_TERM_TAC;
2198   (REWRITE_TAC[REAL_ARITH `(a + b)/ c = a / c + b / c`]);
2199
2200     (SUBGOAL_THEN `X / X = &1` ASSUME_TAC);
2201     (ASM_SIMP_TAC[REAL_DIV_REFL]);
2202
2203   (ONCE_ASM_REWRITE_TAC[]);
2204   (AP_TERM_TAC);
2205   (EXPAND_TAC "F12");
2206   (REWRITE_TAC[REAL_POW_DIV]);
2207   (REWRITE_TAC[REAL_POW_2]);
2208   (REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * a = &4 * a pow 2`]);
2209   (ONCE_ASM_REWRITE_TAC[]);
2210
2211     (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
2212     (MATCH_MP_TAC SQRT_POW_2);
2213     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2214     (ASM_REWRITE_TAC[]);
2215
2216   (ONCE_ASM_REWRITE_TAC[]);
2217   (REWRITE_TAC[REAL_ARITH `&4 * (X * C) / & 4 = X * C`]);
2218   (REWRITE_TAC[REAL_ARITH
2219     `((&1 - x / &2) * C) * (&1 - x / &2) * C =
2220      ((&1 - ((&4 - x) * x) / &4) * C) * C`]);
2221   (ONCE_ASM_REWRITE_TAC[]);
2222
2223   (SUBGOAL_THEN `~(C = &0)` ASSUME_TAC);
2224    STRIP_TAC;
2225     (SUBGOAL_THEN `D' = &0` ASSUME_TAC);
2226     (EXPAND_TAC "D'");
2227     (REWRITE_TAC[REAL_ARITH `(a * x)/ &4 = (a / &4) * x`]);
2228     (ONCE_ASM_REWRITE_TAC[]);
2229      REAL_ARITH_TAC;
2230   (MP_TAC (ASSUME `&0 < D'`));
2231   (FIRST_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2232
2233     (SUBGOAL_THEN
2234       `(((&1 - X / &4) * C) * C) / (X * C) = ((&1 - X / &4) * C) / X`
2235       ASSUME_TAC);
2236     (ONCE_REWRITE_TAC[REAL_ARITH `((a * b) * c) / d = (a * b) * c / d`]);
2237     (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
2238     (ASM_REWRITE_TAC[]);
2239
2240   (ONCE_ASM_REWRITE_TAC[]);
2241   (AP_THM_TAC THEN AP_TERM_TAC);
2242    REAL_ARITH_TAC;
2243
2244 (* --------------------------------------------------------------------------*)
2245 (*                                                                           *)
2246 (*                                                                           *)
2247 (* --------------------------------------------------------------------------*)
2248
2249 (SUBGOAL_THEN `&2 * sqrt ((X * C) / &4) = sqrt (X * C)` ASSUME_TAC);
2250 (MATCH_MP_TAC (REAL_ARITH
2251     `(&2 * sqrt x = sqrt (&4) * sqrt x) /\ (sqrt (&4) * sqrt x = y)
2252       ==> &2 * sqrt x = y`));
2253 (ASM_REWRITE_TAC[]);
2254  CONJ_TAC;
2255
2256   (AP_THM_TAC THEN AP_TERM_TAC);
2257   (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
2258   (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_MUL]);
2259   (SIMP_TAC[GSYM REAL_POW_2; GSYM SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
2260
2261   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `X * C = &4 * (X * C) / &4`]);
2262   (ASM_REWRITE_TAC[]);
2263   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&4 * (a * b) / &4 = a * b`]);
2264   (MATCH_MP_TAC (GSYM SQRT_MUL));
2265   (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
2266   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
2267   (ASM_REWRITE_TAC[]);
2268
2269 (* --------------------------------------------------------------------------*)
2270 (*                                                                           *)
2271 (* --------------------------------------------------------------------------*)
2272
2273   (SUBGOAL_THEN `2G (x:real) = sqrt (X * C)` ASSUME_TAC);
2274   (EXPAND_TAC "2G");
2275   (ONCE_ASM_REWRITE_TAC[]);
2276   (ASM_REWRITE_TAC[]);
2277
2278   (SUBGOAL_THEN
2279     `G' = ((&4 - &2 * x) * C) / &4 * inv (sqrt (X * C))` ASSUME_TAC);
2280   (EXPAND_TAC "G'");
2281   (REPEAT AP_TERM_TAC);
2282   (ASM_REWRITE_TAC[]);
2283
2284   (SUBGOAL_THEN `&0 < X * C` ASSUME_TAC);
2285   (EXPAND_TAC "X" THEN ASM_MESON_TAC[]);
2286
2287   (SUBGOAL_THEN
2288     `(-- &1 / &2 * C) * 2G (x:real) - f1 x * &2 * G' =
2289       -- &2 * C * C / sqrt (X * C)` ASSUME_TAC);
2290   (ONCE_ASM_REWRITE_TAC[]);
2291   (EXPAND_TAC "f1");
2292   (ONCE_REWRITE_TAC[REAL_ARITH
2293     `a * &2 * b / &4 * c = (a * &2 * b / &4) * c`]);
2294   (ONCE_REWRITE_TAC[REAL_ARITH
2295     `((&1 - x / &2) * C) * &2 * ((&4 - &2 * x) * C) / &4 =
2296      (&4 - (&4 - x) * x) * C * C / &2`]);
2297   (ONCE_ASM_REWRITE_TAC[]);
2298
2299   (SUBGOAL_THEN
2300     `(-- &1 / &2 * C) * sqrt (X * C) = (-- &1 / &2 * C * X * C) / sqrt (X * C)`
2301      ASSUME_TAC);
2302   (REWRITE_TAC[REAL_ARITH
2303     `(-- &1 / &2 * C * X * C) / Y = (-- &1 / &2 * C) * (X * C) / Y `]);
2304    AP_TERM_TAC;
2305
2306
2307     (SUBGOAL_THEN
2308       `sqrt (X * C) * sqrt (X * C) = (X * C) ==>
2309        sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
2310     (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
2311     (MATCH_MP_TAC (GSYM REAL_EQ_RDIV_EQ));
2312     (MATCH_MP_TAC SQRT_POS_LT);
2313     (ASM_REWRITE_TAC[]);
2314
2315   (FIRST_X_ASSUM MATCH_MP_TAC);
2316   (REWRITE_TAC[GSYM REAL_POW_2]);
2317   (MATCH_MP_TAC SQRT_POW_2);
2318   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
2319   (ASM_REWRITE_TAC[]);
2320
2321  (ASM_REWRITE_TAC[]);
2322  (REWRITE_TAC[REAL_ARITH `-- a *  b * c / x = -- (a * b * c) / x`]);
2323  (REWRITE_TAC[REAL_ARITH `a / x - y = -- b / x <=> (a + b) / x = y`]);
2324  (REWRITE_TAC[REAL_ARITH
2325    `-- &1 / &2 * C * X * C + &2 * C * C = (&4 - X) * C * C / &2`]);
2326  (ABBREV_TAC `m = (&4 - X) * C * C / &2`);
2327  (ABBREV_TAC `n = sqrt (X * C)`);
2328
2329     (SUBGOAL_THEN `m = (m * inv n) * n  ==> m / n = m * inv n` ASSUME_TAC);
2330     (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
2331     (MATCH_MP_TAC (GSYM REAL_EQ_LDIV_EQ));
2332     (EXPAND_TAC "n");
2333     (MATCH_MP_TAC SQRT_POS_LT);
2334     (ASM_REWRITE_TAC[]);
2335
2336   (FIRST_X_ASSUM MATCH_MP_TAC);
2337   (REWRITE_TAC[REAL_ARITH `(m * inv n) * n = m * (inv n * n)`]);
2338   (MATCH_MP_TAC (MESON[REAL_MUL_RID]
2339                   `inv n * n = &1 ==> m = m * inv n * n`));
2340   (MATCH_MP_TAC REAL_MUL_LINV);
2341   (MATCH_MP_TAC (REAL_ARITH `&0 < n ==> ~ (n = &0)`));
2342   (EXPAND_TAC "n");
2343   (MATCH_MP_TAC SQRT_POS_LT);
2344   (ASM_REWRITE_TAC[]);
2345
2346 (* --------------------------------------------------------------------------*)
2347 (*                                                                           *)
2348 (*                                                                           *)
2349 (* --------------------------------------------------------------------------*)
2350
2351 (SUBGOAL_THEN
2352  `(F1 has_real_derivative -- &2 * C / (X + C - X * C / &4) / sqrt (X * C))
2353   (atreal x within r)`
2354   ASSUME_TAC);
2355
2356   (SUBGOAL_THEN `2G (x:real) pow 2 = X * C` ASSUME_TAC);
2357   (MATCH_MP_TAC (REAL_ARITH
2358     `2G (x:real) pow 2 = &4 * D' /\ &4 * D' = X * C ==>
2359      2G (x:real) pow 2 = X * C`));
2360   (ASM_REWRITE_TAC[REAL_ARITH `(&4 * z = x * y) <=> ((x * y) / &4 = z)`]);
2361   (EXPAND_TAC "D'");
2362   (REWRITE_TAC[REAL_ARITH `&4 * (X * C) / &4 = X * C`]);
2363   (MATCH_MP_TAC SQRT_POW_2);
2364   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2365   (ASM_REWRITE_TAC[]);
2366
2367   (SUBGOAL_THEN
2368     `((-- &1 / &2 * C) * 2G (x:real) - f1 x * &2 * G') / 2G x pow 2 *
2369      inv (&1 + F12 x pow 2) =
2370      -- &2 * C / (X + C - X * C / &4) / sqrt (X * C)`
2371      ASSUME_TAC);
2372   (ASM_REWRITE_TAC[]);
2373   (ABBREV_TAC `m = X + C - X * C / &4`);
2374   (REWRITE_TAC[REAL_ARITH `-- &2 * C / m / n = (-- &2 * C) / m / n`]);
2375   (REWRITE_TAC[REAL_ARITH
2376     `(-- a * b * c / d) / e * f / g = (-- a * b * c * f) / e / g / d`]);
2377   (REPEAT (AP_THM_TAC THEN AP_TERM_TAC));
2378   (REWRITE_TAC[REAL_ARITH
2379     `(-- a * b * c * d) / e = (-- a * b) * (d * c) / e`]);
2380   (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> (y * x = y)`));
2381   (MATCH_MP_TAC REAL_DIV_REFL);
2382   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
2383   (ASM_REWRITE_TAC[]);
2384
2385 (ASM_MESON_TAC[]);
2386
2387 (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC);
2388 (REPLICATE_TAC 3 UP_ASM_TAC THEN REPLICATE_TAC 4 DEL_TAC);
2389 (REPEAT DISCH_TAC);
2390
2391 (* --------------------------------------------------------------------------*)
2392 (*                                                                           *)
2393 (*                                                                           *)
2394 (* --------------------------------------------------------------------------*)
2395
2396 (ABBREV_TAC `f2 = (\x. (&1 - c / &2) * (&4 - x) * x)`);
2397 (ABBREV_TAC
2398    `F22 = (\x. ((&1 - c / &2) * (&4 - x) * x) /
2399           (&2 * sqrt ((((&4 - x) * x) * C) / &4)))`);
2400
2401   (SUBGOAL_THEN
2402     `(F22 has_real_derivative
2403      (((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2)
2404      (atreal x within r)`
2405      ASSUME_TAC);
2406
2407     (SUBGOAL_THEN `F22 = (\x:real.  f2 x / 2G x)` ASSUME_TAC);
2408       (* Subgoal *)
2409     (EXPAND_TAC "F22" THEN EXPAND_TAC "2G" THEN EXPAND_TAC "f2");
2410     (REWRITE_TAC[]);
2411
2412   (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
2413
2414     (SUBGOAL_THEN
2415       `(f2 has_real_derivative (&1 - c / &2) * (&4 - &2 * x))
2416        (atreal x within r) /\
2417        (2G has_real_derivative &2 * G') (atreal x within r) /\ ~(2G x = &0)`
2418        ASSUME_TAC);
2419       (*  Subgoal *)
2420     (ASM_REWRITE_TAC[]);
2421      CONJ_TAC;  (* Break into 2 subgoals *)
2422
2423       (EXPAND_TAC "f2" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
2424       (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
2425       (EXPAND_TAC "2G");
2426       (MATCH_MP_TAC (REAL_ARITH `&0 < &2 /\ &0 < x ==> &0 < &2 * x`));
2427       (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
2428       (MATCH_MP_TAC SQRT_POS_LT);
2429       (MATCH_MP_TAC (REAL_ARITH `&0 < x  ==> &0 < x / &4`));
2430       (ASM_REWRITE_TAC[]);
2431
2432    UP_ASM_TAC;
2433   (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
2434   (MESON_TAC[]);
2435
2436
2437 (* --------------------------------------------------------------------------*)
2438 (*         Derivative of  atn ((&1 - c / &2) * (&4 - x) * x) /               *)
2439 (*            (&2 * sqrt ((((&4 - x) * x) * C) / &4))                        *)
2440 (* --------------------------------------------------------------------------*)
2441
2442   (SUBGOAL_THEN
2443     `(F2 has_real_derivative
2444      (((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2 *
2445      inv (&1 + F22 x pow 2))
2446      (atreal x within r)`
2447      ASSUME_TAC);
2448
2449     (SUBGOAL_THEN `F2 = (\x:real. atn (F22 x))` ASSUME_TAC);
2450       (* Subgoal *)
2451     (EXPAND_TAC "F2" THEN EXPAND_TAC "F22");
2452     (REWRITE_TAC[]);
2453
2454   (ONCE_ASM_REWRITE_TAC[]);
2455    DEL_TAC;
2456   (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
2457   (ABBREV_TAC `f' =
2458     (((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2`);
2459
2460     (SUBGOAL_THEN
2461       `inv (&1 + F22 x pow 2) = g' ((F22:real-> real) x)`
2462        ASSUME_TAC);
2463       (* Subgoal *)
2464     (EXPAND_TAC "F22" THEN EXPAND_TAC "g'");
2465     (MESON_TAC[]);
2466
2467   (ONCE_ASM_REWRITE_TAC[]);
2468
2469     (SUBGOAL_THEN
2470      `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
2471       ASSUME_TAC);
2472       (* Subgoal *)
2473     (EXPAND_TAC "g'");
2474     (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
2475
2476
2477     (SUBGOAL_THEN
2478       `(F22 has_real_derivative f') (atreal x within r) /\
2479        (:real) (F22 x)` ASSUME_TAC);
2480       (* Subgoal *)
2481     (ASM_REWRITE_TAC[]);
2482     (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
2483
2484   (REPLICATE_TAC 2 UP_ASM_TAC);
2485   (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
2486   (MESON_TAC[]);
2487
2488 (* --------------------------------------------------------------------------*)
2489 (*                                                                           *)
2490 (*                                                                           *)
2491 (* --------------------------------------------------------------------------*)
2492
2493   (SUBGOAL_THEN
2494     `inv (&1 + F22 (x:real) pow 2) = C / (X + C - X * C / &4)`
2495      ASSUME_TAC);
2496   (ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
2497    AP_TERM_TAC;
2498   (REWRITE_TAC[REAL_ARITH `(a + b - d)/ c = b / c + (a - d) / c`]);
2499
2500     (SUBGOAL_THEN `C / C = &1` ASSUME_TAC);
2501     (MATCH_MP_TAC REAL_DIV_REFL);
2502     (EXPAND_TAC "C");
2503     (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
2504     (ASM_REWRITE_TAC[REAL_ARITH `~ (&4 - x = &0) <=> ~(x = &4)`]);
2505
2506   (ONCE_ASM_REWRITE_TAC[]);
2507   (AP_TERM_TAC);
2508   (EXPAND_TAC "F22");
2509   (REWRITE_TAC[REAL_POW_DIV]);
2510   (REWRITE_TAC[REAL_POW_2]);
2511   (REWRITE_TAC[REAL_ARITH `(x * a) * x * a = x pow 2 * a pow 2`]);
2512   (ONCE_ASM_REWRITE_TAC[]);
2513
2514     (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
2515     (MATCH_MP_TAC SQRT_POW_2);
2516     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2517     (ASM_REWRITE_TAC[]);
2518
2519   (ONCE_ASM_REWRITE_TAC[]);
2520   (REWRITE_TAC[REAL_ARITH `&2 pow 2 * (X * C) / & 4 = X * C`]);
2521
2522     (SUBGOAL_THEN
2523       `((&1 - c / &2) pow 2 * X pow 2) / (X * C) =
2524        ((&1 - C / &4) * X) * X / (C * X)` ASSUME_TAC);
2525     (EXPAND_TAC "C");
2526     (REWRITE_TAC[REAL_ARITH
2527                   `(&1 - c / &2) pow 2 = &1 - ((&4 - c) * c) / &4`]);
2528     (REWRITE_TAC[REAL_ARITH `a * b pow 2 = (a * b) * b`]);
2529     (ONCE_REWRITE_TAC[REAL_ARITH `((a * d) * b) / c = (a * d) * (b / c)`]);
2530     (REPEAT AP_TERM_TAC);
2531     (REWRITE_TAC[REAL_MUL_SYM]);
2532
2533   (ONCE_ASM_REWRITE_TAC[]);
2534   (REWRITE_TAC[REAL_ARITH `(a - a * b) / c = ((&1 - b) * a) / c`]);
2535   (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
2536   (ASM_REWRITE_TAC[]);
2537   (EXPAND_TAC "C");
2538   (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
2539   (ASM_REWRITE_TAC[REAL_ARITH `~ (&4 - x = &0) <=> ~(x = &4)`]);
2540
2541 (* --------------------------------------------------------------------------*)
2542 (*                                                                           *)
2543 (*                                                                           *)
2544 (* --------------------------------------------------------------------------*)
2545
2546 (SUBGOAL_THEN `&2 * sqrt ((X * C) / &4) = sqrt (X * C)` ASSUME_TAC);
2547 (MATCH_MP_TAC (REAL_ARITH
2548     `(&2 * sqrt x = sqrt (&4) * sqrt x) /\ (sqrt (&4) * sqrt x = y)
2549       ==> &2 * sqrt x = y`));
2550 (ASM_REWRITE_TAC[]);
2551  CONJ_TAC;
2552
2553   (AP_THM_TAC THEN AP_TERM_TAC);
2554   (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
2555   (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_MUL]);
2556   (SIMP_TAC[GSYM REAL_POW_2; GSYM SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
2557
2558   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `X * C = &4 * (X * C) / &4`]);
2559   (ASM_REWRITE_TAC[]);
2560   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&4 * (a * b) / &4 = a * b`]);
2561   (MATCH_MP_TAC (GSYM SQRT_MUL));
2562   (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
2563   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
2564   (ASM_REWRITE_TAC[]);
2565
2566 (* --------------------------------------------------------------------------*)
2567 (*                                                                           *)
2568 (* --------------------------------------------------------------------------*)
2569
2570   (SUBGOAL_THEN `2G (x:real) = sqrt (X * C)` ASSUME_TAC);
2571   (EXPAND_TAC "2G");
2572   (ONCE_ASM_REWRITE_TAC[]);
2573   (ASM_REWRITE_TAC[]);
2574
2575   (SUBGOAL_THEN
2576     `G' = ((&4 - &2 * x) * C) / &4 * inv (sqrt (X * C))` ASSUME_TAC);
2577   (EXPAND_TAC "G'");
2578   (REPEAT AP_TERM_TAC);
2579   (ASM_REWRITE_TAC[]);
2580
2581   (SUBGOAL_THEN
2582     `((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G' =
2583      ((&1 - c / &2) * (&4 - &2 * x)) * (X * C) / &2 / sqrt (X * C)`
2584       ASSUME_TAC);
2585
2586   (ONCE_ASM_REWRITE_TAC[]);
2587   (EXPAND_TAC "f2");
2588   (ONCE_REWRITE_TAC[REAL_ARITH
2589     `(a * b) * &2 * (c * d) / &4 * e = (a * c) * (b * d * e) / &2`]);
2590   (ABBREV_TAC `m = (&1 - c / &2) * (&4 - &2 * x)`);
2591   (ONCE_REWRITE_TAC[REAL_ARITH `m * x - m * y = m * (x - y)`]);
2592    AP_TERM_TAC;
2593   (ONCE_ASM_REWRITE_TAC[]);
2594
2595   (SUBGOAL_THEN `sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
2596     (SUBGOAL_THEN
2597       `sqrt (X * C) * sqrt (X * C) = (X * C) ==>
2598        sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
2599     (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
2600     (MATCH_MP_TAC (GSYM REAL_EQ_RDIV_EQ));
2601     (MATCH_MP_TAC SQRT_POS_LT);
2602     (ASM_REWRITE_TAC[]);
2603
2604   (FIRST_X_ASSUM MATCH_MP_TAC);
2605   (REWRITE_TAC[GSYM REAL_POW_2]);
2606   (MATCH_MP_TAC SQRT_POW_2);
2607   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
2608   (ASM_REWRITE_TAC[]);
2609
2610  (ABBREV_TAC `n = (X * C) / &2 / sqrt (X * C)`);
2611  (ABBREV_TAC `n' = inv (sqrt (X * C))`);
2612  (PURE_ONCE_ASM_REWRITE_TAC[]);
2613  (EXPAND_TAC "n" THEN EXPAND_TAC "n'");
2614  (REWRITE_TAC[REAL_ARITH `a / x - y = a / &2 / x <=> a / & 2 / x = y`]);
2615  (REWRITE_TAC[REAL_ARITH `(a *  b * c) / x = (a * b) / x  * c`]);
2616  (ABBREV_TAC `t = (X * C) / &2`);
2617  (ABBREV_TAC `r' = sqrt (X * C)`);
2618
2619     (SUBGOAL_THEN `t = (t * inv r') * r'  ==> t / r' = t * inv r'`
2620        ASSUME_TAC);
2621     (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
2622     (MATCH_MP_TAC (GSYM REAL_EQ_LDIV_EQ));
2623     (EXPAND_TAC "r'");
2624     (MATCH_MP_TAC SQRT_POS_LT);
2625     (ASM_REWRITE_TAC[]);
2626
2627   (FIRST_X_ASSUM MATCH_MP_TAC);
2628   (REWRITE_TAC[REAL_ARITH `(m * inv n) * n = m * (inv n * n)`]);
2629   (MATCH_MP_TAC (MESON[REAL_MUL_RID]
2630                   `inv r' * r' = &1 ==> m = m * inv r' * r'`));
2631   (MATCH_MP_TAC REAL_MUL_LINV);
2632   (MATCH_MP_TAC (REAL_ARITH `&0 < n ==> ~ (n = &0)`));
2633   (EXPAND_TAC "r'");
2634   (MATCH_MP_TAC SQRT_POS_LT);
2635   (ASM_REWRITE_TAC[]);
2636
2637
2638 (* --------------------------------------------------------------------------*)
2639 (*                                                                           *)
2640 (*                                                                           *)
2641 (* --------------------------------------------------------------------------*)
2642
2643 (SUBGOAL_THEN
2644   `(F2 has_real_derivative
2645    ((&2 - c) * (&2 - x)) * C / &2 / (X + C - X * C / &4) / sqrt (X * C))
2646    (atreal x within r)`
2647    ASSUME_TAC);
2648
2649   (SUBGOAL_THEN `2G (x:real) pow 2 = X * C` ASSUME_TAC);
2650   (MATCH_MP_TAC (REAL_ARITH
2651     `2G (x:real) pow 2 = &4 * D' /\ &4 * D' = X * C ==>
2652      2G (x:real) pow 2 = X * C`));
2653   (ASM_REWRITE_TAC[REAL_ARITH `(&4 * z = x * y) <=> ((x * y) / &4 = z)`]);
2654   (EXPAND_TAC "D'");
2655   (REWRITE_TAC[REAL_ARITH `&4 * (X * C) / &4 = X * C`]);
2656   (MATCH_MP_TAC SQRT_POW_2);
2657   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2658   (ASM_REWRITE_TAC[]);
2659
2660   (SUBGOAL_THEN
2661     `(((&1 - c / &2) * (&4 - &2 * x)) * 2G x - f2 x * &2 * G') / 2G x pow 2 *
2662        inv (&1 + F22 x pow 2) =
2663      ((&2 - c) * (&2 - x)) * C / &2 / (X + C - X * C / &4) / sqrt (X * C)`
2664      ASSUME_TAC);
2665   (ASM_REWRITE_TAC[]);
2666   (ABBREV_TAC `m = X + C - X * C / &4`);
2667   (REWRITE_TAC[REAL_ARITH
2668     `(a * b / c / d) / e * f / g = (a * f * (b / e)) / c / g / d`]);
2669   (REWRITE_TAC[REAL_ARITH
2670     `(a * b / c / d / e)= (a * b) / c / d / e`]);
2671
2672   (REPEAT(AP_THM_TAC THEN AP_TERM_TAC));
2673   (REWRITE_TAC[REAL_ARITH
2674     `((&1 - c / &2) * (&4 - &2 * x)) = ((&2 - c) * (&2 - x))`]);
2675    AP_TERM_TAC;
2676   (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> (y * x = y)`));
2677   (MATCH_MP_TAC REAL_DIV_REFL);
2678   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~(x = &0)`));
2679   (ASM_REWRITE_TAC[]);
2680
2681 (ASM_MESON_TAC[]);
2682 (UP_ASM_TAC THEN REPLICATE_TAC 9 DEL_TAC);
2683 (REPEAT DISCH_TAC);
2684
2685 (* Begin Diff 3 *)
2686
2687 (ABBREV_TAC `f3 = (\x. (&8 + (x * c) / &2 - &2 * x - &2 * c))`);
2688 (ABBREV_TAC
2689    `F32 = (\x.(&8 + (x * c) / &2 - &2 * x - &2 * c) /
2690             sqrt ((((&4 - x) * x) * C) / &4))`);
2691
2692   (SUBGOAL_THEN
2693     `(F32 has_real_derivative
2694      ((c / &2 - &2) * G x - f3 x * G') / G x pow 2) (atreal x within r)`
2695      ASSUME_TAC);
2696
2697     (SUBGOAL_THEN `F32 = (\x:real.  f3 x / G x)` ASSUME_TAC);
2698       (* Subgoal *)
2699     (EXPAND_TAC "F32" THEN EXPAND_TAC "G" THEN EXPAND_TAC "f3");
2700     (REWRITE_TAC[]);
2701
2702   (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
2703
2704     (SUBGOAL_THEN
2705       `(f3 has_real_derivative (c / &2 - &2))
2706        (atreal x within r) /\
2707        (G has_real_derivative G') (atreal x within r) /\ ~(G x = &0)`
2708        ASSUME_TAC);
2709       (*  Subgoal *)
2710     (ASM_REWRITE_TAC[]);
2711      CONJ_TAC;  (* Break into 2 subgoals *)
2712
2713       (EXPAND_TAC "f3" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
2714       (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
2715       (EXPAND_TAC "G");
2716       (MATCH_MP_TAC SQRT_POS_LT);
2717       (ASM_REWRITE_TAC[]);
2718
2719    UP_ASM_TAC;
2720   (MP_TAC HAS_REAL_DERIVATIVE_DIV_WITHIN);
2721   (MESON_TAC[]);
2722
2723
2724 (* --------------------------------------------------------------------------*)
2725 (*         Derivative of  atn (....)                                         *)
2726 (* --------------------------------------------------------------------------*)
2727
2728   (SUBGOAL_THEN
2729     `(F3 has_real_derivative
2730      ((c / &2 - &2) * G x - f3 x * G') / G x pow 2 * inv (&1 + F32 x pow 2))
2731      (atreal x within r)`
2732      ASSUME_TAC);
2733
2734     (SUBGOAL_THEN `F3 = (\x:real. atn (F32 x))` ASSUME_TAC);
2735       (* Subgoal *)
2736     (EXPAND_TAC "F3" THEN EXPAND_TAC "F32");
2737     (REWRITE_TAC[]);
2738
2739   (ONCE_ASM_REWRITE_TAC[]);
2740    DEL_TAC;
2741   (ABBREV_TAC `g' = (\x. inv (&1 + x pow 2))`);
2742   (ABBREV_TAC `f' = ((c / &2 - &2) * G (x:real) - f3 x * G') / G x pow 2`);
2743
2744     (SUBGOAL_THEN
2745       `inv (&1 + F32 x pow 2) = g' ((F32:real-> real) x)`
2746        ASSUME_TAC);
2747       (* Subgoal *)
2748     (EXPAND_TAC "F32" THEN EXPAND_TAC "g'");
2749     (MESON_TAC[]);
2750
2751   (ONCE_ASM_REWRITE_TAC[]);
2752
2753     (SUBGOAL_THEN
2754      `!x. (:real) x ==> (atn has_real_derivative (g':real->real) x) (atreal x)`
2755       ASSUME_TAC);
2756       (* Subgoal *)
2757     (EXPAND_TAC "g'");
2758     (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
2759
2760     (SUBGOAL_THEN
2761       `(F32 has_real_derivative f') (atreal x within r) /\
2762        (:real) (F32 x)` ASSUME_TAC);
2763       (* Subgoal *)
2764     (ASM_REWRITE_TAC[]);
2765     (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
2766
2767   (REPLICATE_TAC 2 UP_ASM_TAC);
2768   (MP_TAC HAS_REAL_DERIVATIVE_CHAIN2);
2769   (MESON_TAC[]);
2770
2771 (* --------------------------------------------------------------------------*)
2772 (*                                                                           *)
2773 (*                                                                           *)
2774 (* --------------------------------------------------------------------------*)
2775
2776   (SUBGOAL_THEN
2777     `inv (&1 + F32 (x:real) pow 2) = (x * c) / (x * c + (&4 - x) * (&4 - c))`
2778      ASSUME_TAC);
2779   (ONCE_REWRITE_TAC[GSYM REAL_INV_DIV]);
2780    AP_TERM_TAC;
2781   (REWRITE_TAC[REAL_ARITH `(a + b) / c = a / c + b / c`]);
2782
2783     (SUBGOAL_THEN `(x * c) / (x * c) = &1` ASSUME_TAC);
2784     (MATCH_MP_TAC REAL_DIV_REFL);
2785     (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
2786     (ASM_REWRITE_TAC[]);
2787
2788   (ONCE_ASM_REWRITE_TAC[]);
2789   (AP_TERM_TAC);
2790   (EXPAND_TAC "F32");
2791   (REWRITE_TAC[REAL_POW_DIV]);
2792   (ONCE_ASM_REWRITE_TAC[]);
2793
2794     (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
2795     (MATCH_MP_TAC SQRT_POW_2);
2796     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2797     (ASM_REWRITE_TAC[]);
2798   (ONCE_ASM_REWRITE_TAC[]);
2799   (REWRITE_TAC[REAL_ARITH `(x * a) * x * a = x pow 2 * a pow 2`]);
2800   (REWRITE_TAC[REAL_ARITH
2801      `&8 + (x * c) / &2 - &2 * x - &2 * c = ((&4 - x) * (&4 - c)) / &2`]);
2802   (REWRITE_TAC[REAL_POW_DIV]);
2803   (REWRITE_TAC[REAL_ARITH `&2 pow 2 = &4`]);
2804   (ABBREV_TAC `m = ((&4 - x) * (&4 - c)) pow 2 / &4`);
2805   (ABBREV_TAC `n = ((X * C) / &4)`);
2806   (ABBREV_TAC `p = ((&4 - x) * (&4 - c)) / (x * c)`);
2807
2808     (SUBGOAL_THEN `m = p * n ==> (m / n = p)` ASSUME_TAC);
2809     (MATCH_MP_TAC (MESON[] `(b <=> a) ==> (a ==> b)`));
2810     (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
2811     (EXPAND_TAC "n");
2812     (ASM_REWRITE_TAC[]);
2813
2814   (FIRST_X_ASSUM MATCH_MP_TAC);
2815   (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN EXPAND_TAC "p");
2816   (REWRITE_TAC[REAL_ARITH `(a / x) * (b / y) = (a * b) / x / y`]);
2817   (AP_THM_TAC THEN AP_TERM_TAC);
2818   (REWRITE_TAC[REAL_ARITH `(a * b * c) / x = a * (b * c) / x`]);
2819   (REWRITE_TAC[REAL_POW_2]);
2820    AP_TERM_TAC;
2821   (EXPAND_TAC "X" THEN EXPAND_TAC "C");
2822   (REWRITE_TAC[REAL_ARITH `((a * b) * c * d) / e = (a * c) * (b * d) / e`]);
2823   (MATCH_MP_TAC (MESON[REAL_MUL_RID] `y = &1 ==> x = x * y`));
2824   (MATCH_MP_TAC REAL_DIV_REFL);
2825   (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=> ~a /\ ~b`]);
2826   (ASM_REWRITE_TAC[]);
2827
2828 (* --------------------------------------------------------------------------*)
2829 (*                                                                           *)
2830 (*                                                                           *)
2831 (* --------------------------------------------------------------------------*)
2832
2833
2834   (SUBGOAL_THEN `G (x:real) = sqrt ((X * C) / &4)` ASSUME_TAC);
2835   (EXPAND_TAC "G");
2836   (ONCE_ASM_REWRITE_TAC[]);
2837   (ASM_REWRITE_TAC[]);
2838
2839   (SUBGOAL_THEN
2840     `G' = ((&4 - &2 * x) * C) / &4 * inv (sqrt (X * C))` ASSUME_TAC);
2841   (EXPAND_TAC "G'");
2842   (REPEAT AP_TERM_TAC);
2843   (MATCH_MP_TAC (REAL_ARITH
2844     `(&2 * sqrt x = sqrt (&4) * sqrt x) /\ (sqrt (&4) * sqrt x = y)
2845       ==> &2 * sqrt x = y`));
2846   (ASM_REWRITE_TAC[]);
2847    CONJ_TAC;
2848
2849   (AP_THM_TAC THEN AP_TERM_TAC);
2850   (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
2851   (SIMP_TAC[REAL_ARITH `&0 <= &2`; SQRT_MUL]);
2852   (SIMP_TAC[GSYM REAL_POW_2; GSYM SQRT_POW_2; REAL_ARITH `&0 <= &2`]);
2853
2854   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `X * C = &4 * (X * C) / &4`]);
2855   (ASM_REWRITE_TAC[]);
2856   (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&4 * (a * b) / &4 = a * b`]);
2857   (MATCH_MP_TAC (GSYM SQRT_MUL));
2858   (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
2859   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2860   (ASM_REWRITE_TAC[]);
2861
2862   (SUBGOAL_THEN
2863     `(c / &2 - &2) * G x - f3 x * G' =
2864      (--C * ((&4 - x) * (&4 - c))) / &2 / sqrt (X * C)` ASSUME_TAC);
2865
2866   (ONCE_ASM_REWRITE_TAC[]);
2867   (EXPAND_TAC "f3");
2868
2869   (SUBGOAL_THEN `sqrt ((X * C) / &4) = sqrt (X * C) / &2` ASSUME_TAC);
2870     (SUBGOAL_THEN `&2 = sqrt (&4) ` ASSUME_TAC);
2871     (MATCH_MP_TAC (REAL_ARITH
2872       `(&2) = sqrt (&2) * sqrt (&2) /\ sqrt (&2) * sqrt (&2) = sqrt (&4) ==>
2873        &2 = sqrt (&4)`));
2874      CONJ_TAC;
2875       (REWRITE_TAC[GSYM REAL_POW_2]);
2876       (MATCH_MP_TAC (GSYM SQRT_POW_2));
2877        REAL_ARITH_TAC;
2878
2879       (REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`]);
2880       (MESON_TAC[SQRT_MUL; REAL_ARITH `&0 <= &2`]);
2881   (ONCE_ASM_REWRITE_TAC[]);
2882   (EXPAND_TAC "D'");
2883   (MATCH_MP_TAC SQRT_DIV);
2884   (REWRITE_TAC[REAL_ARITH `&0 <= &4`]);
2885   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2886   (ASM_REWRITE_TAC[]);
2887
2888 (ONCE_ASM_REWRITE_TAC[]);
2889 (REWRITE_TAC[REAL_ARITH
2890   `(c / &2 - &2) * x / &2 = --(&4 - c) / &4 * x`]);
2891 (REWRITE_TAC[REAL_ARITH
2892   `(&8 + (x * c) / &2 - &2 * x - &2 * c) * s / &4 * r =
2893    ((&4 - x) * (&4 - c)) * s / &8 * r`]);
2894
2895   (SUBGOAL_THEN `--(&4 - c) / &4 * sqrt (X * C) =
2896     (--(&4 - c) / &4 * (X * C)) / sqrt (X * C)` ASSUME_TAC);
2897
2898   (REWRITE_TAC[REAL_ARITH
2899     `(--(&4 - c) / &4 * X * C) / Y = (--(&4 - c) / &4) * (X * C) / Y `]);
2900    AP_TERM_TAC;
2901
2902     (SUBGOAL_THEN
2903       `sqrt (X * C) * sqrt (X * C) = (X * C) ==>
2904        sqrt (X * C) = (X * C) / sqrt (X * C)` ASSUME_TAC);
2905     (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
2906     (MATCH_MP_TAC (GSYM REAL_EQ_RDIV_EQ));
2907     (MATCH_MP_TAC SQRT_POS_LT);
2908     (ASM_REWRITE_TAC[]);
2909
2910   (FIRST_X_ASSUM MATCH_MP_TAC);
2911   (REWRITE_TAC[GSYM REAL_POW_2]);
2912   (MATCH_MP_TAC SQRT_POW_2);
2913   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2914   (ASM_REWRITE_TAC[]);
2915
2916  (PURE_ONCE_ASM_REWRITE_TAC[]);
2917  (REWRITE_TAC[REAL_ARITH `a / x - y = b / x <=> (a - b) / x = y`]);
2918  (EXPAND_TAC "X" THEN EXPAND_TAC "C");
2919  (REWRITE_TAC[REAL_ARITH
2920    `((&4 - x) * (&4 - c)) *
2921     ((&4 - &2 * x) * (&4 - c) * c) / &8 * N = (((&4 - x) * (&4 - c)) *
2922     ((&4 - &2 * x) * (&4 - c) * c) / &8) * N `]);
2923 (ABBREV_TAC
2924   `m = ((&4 - x) * (&4 - c)) * ((&4 - &2 * x) * (&4 - c) * c) / &8`);
2925 (ASM_REWRITE_TAC[]);
2926 (ABBREV_TAC `n = sqrt (X * C)`);
2927
2928   (SUBGOAL_THEN
2929     `(--(&4 - c) / &4 * X * C - (--C * (&4 - x) * (&4 - c)) / &2) = m`
2930     ASSUME_TAC);
2931   (EXPAND_TAC "X" THEN EXPAND_TAC "C" THEN EXPAND_TAC "m");
2932    REAL_ARITH_TAC;
2933
2934 (ONCE_ASM_REWRITE_TAC[]);
2935
2936   (SUBGOAL_THEN `m = (m * inv n) * n  ==> m / n = m * inv n` ASSUME_TAC);
2937   (MATCH_MP_TAC (MESON[] `(a <=> b) ==> (a ==> b)`));
2938   (MATCH_MP_TAC (GSYM REAL_EQ_LDIV_EQ));
2939   (EXPAND_TAC "n");
2940   (MATCH_MP_TAC SQRT_POS_LT);
2941   (ASM_REWRITE_TAC[]);
2942
2943   (FIRST_X_ASSUM MATCH_MP_TAC);
2944   (REWRITE_TAC[REAL_ARITH `(m * inv n) * n = m * (inv n * n)`]);
2945   (MATCH_MP_TAC (MESON[REAL_MUL_RID]
2946                   `inv r' * r' = &1 ==> m = m * inv r' * r'`));
2947   (MATCH_MP_TAC REAL_MUL_LINV);
2948   (MATCH_MP_TAC (REAL_ARITH `&0 < n ==> ~ (n = &0)`));
2949   (EXPAND_TAC "n");
2950   (MATCH_MP_TAC SQRT_POS_LT);
2951    ASM_REAL_ARITH_TAC;
2952   (ASM_REWRITE_TAC[]);
2953
2954 (* --------------------------------------------------------------------------*)
2955 (*                                                                           *)
2956 (*                                                                           *)
2957 (* --------------------------------------------------------------------------*)
2958
2959
2960 (ABBREV_TAC `F12 =
2961   (\x. ((&1 - x / &2) * C) / (&2 * sqrt ((((&4 - x) * x) * C) / &4)))`);
2962
2963     (SUBGOAL_THEN `sqrt ((X * C) / &4) pow 2 = (X * C) / &4` ASSUME_TAC);
2964     (MATCH_MP_TAC SQRT_POW_2);
2965     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
2966     (ASM_REWRITE_TAC[]);
2967
2968   (SUBGOAL_THEN
2969     `X + C - X * C / &4 = (&1 + F12 (x:real) pow 2 ) * X` ASSUME_TAC);
2970
2971   (EXPAND_TAC "X" THEN EXPAND_TAC "C" THEN EXPAND_TAC "F12");
2972   (ONCE_ASM_REWRITE_TAC[]);
2973   (ONCE_REWRITE_TAC[REAL_POW_DIV]);
2974   (ONCE_REWRITE_TAC[REAL_POW_2]);
2975   (ONCE_REWRITE_TAC[REAL_ARITH `(&2 * a) * &2 * a = &4 * a pow 2`]);
2976   (ONCE_ASM_REWRITE_TAC[]);
2977   (ONCE_REWRITE_TAC[REAL_ARITH `&4 * x / &4 = x`]);
2978   (ONCE_REWRITE_TAC[REAL_ARITH
2979     `((&1 - x / &2) * C) * (&1 - x / &2) * C =
2980      (&1 - ((&4 - x) * x) / &4) * C * C`]);
2981   (ONCE_ASM_REWRITE_TAC[]);
2982
2983     (SUBGOAL_THEN `&1 = (X * C) / (X * C)` ASSUME_TAC);
2984     (REWRITE_TAC[EQ_SYM_EQ]);
2985     (MATCH_MP_TAC REAL_DIV_REFL);
2986     (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
2987     (ASM_REWRITE_TAC[]);
2988
2989   (ONCE_REWRITE_TAC[REAL_ARITH `(&1 - x) * y = y - x * y`]);
2990   (ONCE_ASM_REWRITE_TAC[]);
2991   (ONCE_REWRITE_TAC[REAL_ARITH `a / x + b / x = (a + b) / x`]);
2992   (ONCE_REWRITE_TAC[REAL_ARITH
2993     `X * C + C * C - X / &4 * C * C = (X + C - X * C / &4) * C`]);
2994   (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c * d = a * (d * b) / c`]);
2995   (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> (a = a * x)`));
2996   (MATCH_MP_TAC REAL_DIV_REFL);
2997   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
2998   (ASM_REWRITE_TAC[]);
2999
3000   (SUBGOAL_THEN `~ (X + C - X * C / &4 = &0)` ASSUME_TAC);
3001   (ONCE_ASM_REWRITE_TAC[]);
3002   (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~ a /\ ~ b`]);
3003   (ASM_REWRITE_TAC[]);
3004   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> ~ (x = &0)`));
3005   (MATCH_MP_TAC (REAL_ARITH `&0 <= x ==> &0 < &1 + x`));
3006   (REWRITE_TAC[REAL_LE_POW_2]);
3007
3008   (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN REPEAT DISCH_TAC);
3009
3010 (* --------------------------------------------------------------------------*)
3011 (*                                                                           *)
3012 (*                                                                           *)
3013 (* --------------------------------------------------------------------------*)
3014
3015
3016 (SUBGOAL_THEN
3017   `(F3 has_real_derivative
3018    (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8 / (X + C - X * C / &4) /
3019     sqrt (X * C)) (atreal x within r)`
3020    ASSUME_TAC);
3021
3022   (SUBGOAL_THEN `G (x:real) pow 2 = (X * C) / &4` ASSUME_TAC);
3023   (EXPAND_TAC "G");
3024   (ASM_REWRITE_TAC[]);
3025   (MATCH_MP_TAC SQRT_POW_2);
3026   (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`));
3027   (ASM_REWRITE_TAC[]);
3028
3029   (SUBGOAL_THEN
3030     `((c / &2 - &2) * G x - f3 x * G') / G x pow 2 * inv (&1 + F32 x pow 2) =
3031      (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8 / (X + C - X * C / &4) /
3032      sqrt (X * C)` ASSUME_TAC);
3033   (ONCE_ASM_REWRITE_TAC[] THEN DEL_TAC);
3034   (REWRITE_TAC[REAL_ARITH
3035     `(a / b / c / d) * f / g = (a * f) / b / d / g / c `]);
3036   (REPEAT(AP_THM_TAC THEN AP_TERM_TAC));
3037
3038   (ABBREV_TAC
3039     `x1 = (x * c + (&4 - x) * (&4 - c))`);
3040   (ABBREV_TAC
3041     `x2 = &2 * x + &2 * c - x * c`);
3042
3043   (SUBGOAL_THEN
3044     `X + C - X * C / &4 = x1 * x2 / &8` ASSUME_TAC);
3045   (EXPAND_TAC "X" THEN EXPAND_TAC "C" THEN EXPAND_TAC "x1" THEN EXPAND_TAC "x2");
3046   (REAL_ARITH_TAC);
3047
3048 (ONCE_ASM_REWRITE_TAC[]);
3049 (REWRITE_TAC[REAL_ARITH `(--x * a * b) * c * d = --x * (a * c) * (b * d)`]);
3050 (ASM_REWRITE_TAC[]);
3051
3052 (SUBGOAL_THEN `~ (x1 = &0) /\ ~ (x2 = &0)` ASSUME_TAC);
3053 (REPEAT STRIP_TAC);
3054
3055   (SUBGOAL_THEN `X + C - X * C / &4 = &0` ASSUME_TAC);
3056   (MATCH_MP_TAC
3057   (MESON[REAL_MUL_LZERO] `(x = x1 * x2 / &8) /\ (x1 = &0) ==> (x = &0)`));
3058   (ASM_REWRITE_TAC[]);
3059   (MP_TAC (ASSUME `~(X + C - X * C / &4 = &0)`));
3060   (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
3061
3062   (SUBGOAL_THEN `X + C - X * C / &4 = &0` ASSUME_TAC);
3063   (MATCH_MP_TAC
3064     (MESON[REAL_MUL_RZERO; REAL_ARITH `&0 / x = &0`]
3065     `(x = x1 * x2 / &8) /\ (x2 = &0) ==> (x = &0)`));
3066   (ASM_REWRITE_TAC[]);
3067   (MP_TAC (ASSUME `~(X + C - X * C / &4 = &0)`));
3068   (FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
3069
3070 (REWRITE_TAC[EQ_SYM_EQ]);
3071 (REWRITE_TAC[REAL_ARITH `(-- &2 * C * x2) / &8 / (x1 * x2 / &8) =
3072                            (-- &2 * C) * (x2 / &8) / (x1 * x2 / &8)`]);
3073 (SUBGOAL_THEN
3074   `(-- &2 * C) * x2 / &8 / (x1 * x2 / &8) = (-- &2 * C) / x1 ` ASSUME_TAC);
3075 (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
3076 (ASM_REWRITE_TAC[]);
3077 (MATCH_MP_TAC (REAL_ARITH `~(x = &0) ==> ~(x / &8 = &0)`));
3078 (ASM_REWRITE_TAC[]);
3079 (ASM_REWRITE_TAC[]);
3080 (EXPAND_TAC "D'");
3081 (AP_THM_TAC THEN AP_TERM_TAC);
3082 (REWRITE_TAC[REAL_ARITH `x / &2  = (x * &2) / &4 `]);
3083 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `a / (b / &4) = a / (&1 * b / &4) `]);
3084 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `((--C * X * C) * &2) / &4 =
3085                                      (-- &2 * C) * (X * C) / &4 `]);
3086 (PURE_REWRITE_TAC[EQ_SYM_EQ]);
3087 (PURE_REWRITE_TAC[REAL_ARITH `(a * b / c) / d = a * (b/ c/ d)`]);
3088 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a = b / &1`]);
3089 (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
3090 (REWRITE_TAC[REAL_ARITH `~(&1 = &0)`]);
3091 (MATCH_MP_TAC (REAL_ARITH `&0 < x  ==> ~ (x / &4 = &0)`));
3092 (ASM_REWRITE_TAC[]);
3093
3094 (ASM_MESON_TAC[]);
3095 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPLICATE_TAC 8 DEL_TAC THEN REPEAT DISCH_TAC);
3096
3097
3098 (ABBREV_TAC `F1' = -- &2 * C / (X + C - X * C / &4) / sqrt (X * C)`);
3099 (ABBREV_TAC `F2' =
3100   ((&2 - c) * (&2 - x)) * C / &2 / (X + C - X * C / &4) / sqrt (X * C)`);
3101
3102 (ABBREV_TAC `F3' =
3103    (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8 /
3104    (X + C - X * C / &4) / sqrt (X * C)`);
3105
3106
3107 (SUBGOAL_THEN `&0 - (F1' + F2') + &2 * F3' = &0` ASSUME_TAC);
3108 (REWRITE_TAC[REAL_ARITH `&0 - (a + b) + c = &0 <=> a + b - c = &0`]);
3109 (EXPAND_TAC "F1'" THEN EXPAND_TAC "F2'" THEN EXPAND_TAC "F3'");
3110 (ONCE_REWRITE_TAC[REAL_ARITH `--a / x + b / x - &2 * c / x = (--a + b - &2 * c) / x`]);
3111
3112
3113 (ABBREV_TAC `m = sqrt (X * C)`);
3114 (ABBREV_TAC `n = X + C - X * C / &4`);
3115 (REWRITE_TAC[REAL_ARITH `-- &2 * x / a  + y * z / a - &2 * t / a =
3116 (-- &2 * x + y * z - &2 * t) / a `]);
3117
3118 (SUBGOAL_THEN `(-- &2 * C +
3119   ((&2 - c) * (&2 - x)) * C / &2 -
3120   &2 * (-- &2 * C * (&2 * x + &2 * c - x * c)) / &8) = &0 ` ASSUME_TAC);
3121 (EXPAND_TAC "C");
3122  REAL_ARITH_TAC;
3123 (ASM_REWRITE_TAC[]);
3124
3125 (SUBGOAL_THEN `&0 / n = &0 ` ASSUME_TAC);
3126 (MATCH_MP_TAC (REAL_ARITH `~(x = &0) ==> &0 / x = &0`));
3127 (ASM_REWRITE_TAC[]);
3128
3129 (ASM_REWRITE_TAC[]);
3130  (MATCH_MP_TAC (REAL_ARITH `~(x = &0) ==> &0 / x = &0`));
3131  (EXPAND_TAC "m");
3132  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
3133  (MATCH_MP_TAC SQRT_POS_LT);
3134  (ASM_REWRITE_TAC[]);
3135
3136  (ABBREV_TAC `FUN1 = (\x:real. --pi / &2 - F1 x - F2 x)`);
3137  (ABBREV_TAC `FUN2 = (\x:real. F1 x + F2 x)`);
3138
3139  (SUBGOAL_THEN `(FUN2 has_real_derivative F1' + F2') (atreal x within r)` ASSUME_TAC);
3140  (EXPAND_TAC "FUN2");
3141  (ASM_SIMP_TAC[HAS_REAL_DERIVATIVE_ADD]);
3142
3143  (SUBGOAL_THEN `(FUN1 has_real_derivative &0 - (F1' + F2')) (atreal x within r)` ASSUME_TAC);
3144     (SUBGOAL_THEN `FUN1 = (\x:real. --pi / &2 - FUN2 x)` ASSUME_TAC);
3145     (EXPAND_TAC "FUN1" THEN EXPAND_TAC "FUN2");
3146     (REWRITE_TAC[REAL_ARITH `a - (b + c) = a - b - c`]);
3147
3148  (ASM_REWRITE_TAC[]);
3149
3150  (SUBGOAL_THEN `((\x:real. --pi / &2) has_real_derivative &0 )
3151                  (atreal x within r)` ASSUME_TAC);
3152 (REAL_DIFF_TAC);
3153  (MESON_TAC[]);
3154
3155  (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC);
3156  (MP_TAC HAS_REAL_DERIVATIVE_SUB THEN MESON_TAC[]);
3157
3158  (ABBREV_TAC `FUN3 = (\x:real. &2 * F3 x)`);
3159  (SUBGOAL_THEN `(FUN3 has_real_derivative &2 * F3') (atreal x within r)` ASSUME_TAC);
3160  (EXPAND_TAC "FUN3");
3161  (MP_TAC (ASSUME `(F3 has_real_derivative F3') (atreal x within r)`));
3162  (MP_TAC HAS_REAL_DERIVATIVE_LMUL_WITHIN THEN MESON_TAC[]);
3163
3164
3165  (SUBGOAL_THEN `(FUNCTION has_real_derivative &0 - (F1' + F2') + &2 * F3') (atreal x within r)` ASSUME_TAC);
3166
3167     (SUBGOAL_THEN `(\x. --pi / &2 - F1 x - F2 x + &2 * F3 x) = (\x:real. FUN1 x + FUN3 x)` ASSUME_TAC);
3168     (EXPAND_TAC "FUN1" THEN EXPAND_TAC "FUN3");
3169     (MESON_TAC[]);
3170
3171     (ASM_REWRITE_TAC[]);
3172  (ASM_MESON_TAC[HAS_REAL_DERIVATIVE_ADD]);
3173  (ASM_MESON_TAC[]);
3174
3175 (* ========================================================================= *)
3176
3177  (SUBGOAL_THEN `&0 < (&4 - c) * c` ASSUME_TAC);
3178  (MATCH_MP_TAC REAL_LT_MUL);
3179  ASM_REAL_ARITH_TAC;
3180
3181  (SUBGOAL_THEN `sqrt ((((&4 - c) * c) * (&4 - c) * c) / &4) =
3182                  ((&4 - c) * c) / &2` ASSUME_TAC);
3183  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
3184  (MATCH_MP_TAC SQRT_RULE_Euler_lemma);
3185  ASM_REAL_ARITH_TAC;
3186
3187  (ASM_REWRITE_TAC[REAL_ARITH `&2 * x / &2 = x`]);
3188  (REWRITE_TAC[REAL_ARITH
3189  `&8 + (c * c) / &2 - &2 * c - &2 * c = (&4 - c) * ((&4 - c) / &2)`]);
3190  (REWRITE_TAC[REAL_ARITH `((&4 - c) * c) / &2 = c * ((&4 - c) / &2)`]);
3191  (REWRITE_TAC[REAL_ARITH `(a * b) / (c * d) = a * b / (c * d)`]);
3192
3193  (SUBGOAL_THEN `(&4 - c) * (&4 - c) / &2 / (c * (&4 - c) / &2) = (&4 - c) / c` ASSUME_TAC);
3194
3195  (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
3196  (ASM_REWRITE_TAC[]);
3197  ASM_REAL_ARITH_TAC;
3198
3199  (ONCE_ASM_REWRITE_TAC[]);
3200
3201  (SUBGOAL_THEN `(&1 - c / &2) * (&4 - c) * c / ((&4 - c) * c) = (&1 - c / &2)` ASSUME_TAC);
3202  (REWRITE_TAC[REAL_ARITH `a * b * c / d = a * (b * c) / d`]);
3203  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> a * x = a`));
3204  (MATCH_MP_TAC REAL_DIV_REFL);
3205  (REWRITE_TAC[REAL_ENTIRE; MESON[] `~ (a \/ b) <=>  ~a /\ ~b`]);
3206  ASM_REAL_ARITH_TAC;
3207
3208  (ASM_REWRITE_TAC[REAL_ARITH `a - b - b = a - &2 * b`]);
3209
3210  (ABBREV_TAC `P = {x| &0 < x /\ x < &4}`);
3211
3212  (SUBGOAL_THEN `is_realinterval P` ASSUME_TAC);
3213  (EXPAND_TAC "P");
3214  (MP_TAC REAL_INTERVAL_Euler_lemma);
3215  (REPEAT LET_TAC);
3216  (UP_ASM_TAC THEN MESON_TAC[]);
3217
3218  (SUBGOAL_THEN `&2 IN P` ASSUME_TAC);
3219  (EXPAND_TAC "P");
3220  (REWRITE_TAC [IN_ELIM_THM]);
3221  REAL_ARITH_TAC;
3222
3223  (SUBGOAL_THEN `!x. x IN P ==> ~(x = &0) /\ ~(&4 - x = &0)` ASSUME_TAC);
3224  (GEN_TAC THEN EXPAND_TAC "P");
3225  (REWRITE_TAC [IN_ELIM_THM]);
3226  REAL_ARITH_TAC;
3227
3228  (SUBGOAL_THEN `(c:real) IN P` ASSUME_TAC);
3229  (EXPAND_TAC "P");
3230  (ASM_REWRITE_TAC [IN_ELIM_THM]);
3231
3232  (REPLICATE_TAC 4 UP_ASM_TAC);
3233  (MP_TAC DERIVATIVE_WRT_C1_Euler_lemma);
3234  (MESON_TAC[DERIVATIVE_WRT_C1_Euler_lemma]);
3235
3236  (ABBREV_TAC `R = {x:real| &0 < x /\ x < &4}`);
3237
3238  (SUBGOAL_THEN `(c:real) IN R` ASSUME_TAC);
3239  (EXPAND_TAC"R" THEN ASM_REWRITE_TAC[IN_ELIM_THM]);
3240  (SUBGOAL_THEN `is_realinterval R` ASSUME_TAC);
3241  (EXPAND_TAC"R" THEN REWRITE_TAC[is_realinterval]);
3242  (REWRITE_TAC[IN_ELIM_THM]);
3243  (REPEAT STRIP_TAC);
3244   (MATCH_MP_TAC (REAL_ARITH `&0 < a' /\ a' <= c ==> &0 < c`));
3245   (ASM_REWRITE_TAC[]);
3246   (MATCH_MP_TAC (REAL_ARITH `c' <= b' /\ b' < &4 ==> c' < &4`));
3247   (ASM_REWRITE_TAC[]);
3248
3249  (SUBGOAL_THEN `!y. y IN R ==> &0 < ((&4 - y) * y) * (&4 - c) * c` ASSUME_TAC);
3250
3251  (GEN_TAC THEN EXPAND_TAC "R" THEN REWRITE_TAC[IN_ELIM_THM]);
3252  STRIP_TAC;
3253  (MATCH_MP_TAC REAL_LT_MUL);
3254   STRIP_TAC;
3255  (MATCH_MP_TAC REAL_LT_MUL);
3256  ASM_REAL_ARITH_TAC;
3257  (MATCH_MP_TAC REAL_LT_MUL);
3258 ASM_REAL_ARITH_TAC;
3259
3260  (SUBGOAL_THEN `(b:real) IN R` ASSUME_TAC);
3261  (EXPAND_TAC"R" THEN ASM_REWRITE_TAC[IN_ELIM_THM]);
3262
3263  (REPLICATE_TAC 4 UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC);
3264  (MESON_TAC[]);
3265
3266
3267  (EXPAND_TAC "d");
3268  (FIRST_X_ASSUM MATCH_MP_TAC);
3269  (EXPAND_TAC "s" THEN ASM_REWRITE_TAC[IN_ELIM_THM])
3270 ]);;
3271
3272 end;;