text_formalization/nonlinear/compute_2158872499.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*                                                                           *)
   4 (*                                                                           *)
   5 (*      Author : TRIEU THI DIEP                                             *)
   6 (* Date: 2010-05-14                                                           *)
   7 (*      Number  : 2158872499                                                 *)
   8 (*                                                                           *)
   9 (* ========================================================================= *)
  10
  11 (*
  12 This contains the second derivative calculation of  g(t) in calculation 2158872499.
  13 *)
  14
  15 (*
  16 changes: extension changed from .ml to .hl,
  17 wrapped all files in a module.
  18 needs -> flyspeck_needs.
  19 merged two compute files,
  20 open Sphere,
  21 open Vukhacky_tactics,
  22 replaced h0 with hz to avoid conflict with constant h0.
  23 *)
  24
  25 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  26
  27 module Compute_2158872499 = struct
  28
  29
  30   open Sphere;;
  31   open Vukhacky_tactics;;
  32   open Trigonometry1;;
  33   open Trigonometry2;;
  34
  35 (* ========================================================================== *)
  36
  37 let ATN_UPS_X_BREAKDOWN1 = prove_by_refinement (
  38  `!a b c.
  39      &0 < (a + b + c) * (a + b - c) * (b + c - a) * (c + a - b)
  40      ==> arclength a b c =
  41          pi / &2 +
  42          atn
  43          ((c * c - a * a - b * b) /
  44           sqrt ((a + b + c) * (a + b - c) * (b + c - a) * (c + a - b)))`,
  45
  46 [(REPEAT STRIP_TAC);
  47  (SUBGOAL_THEN `ups_x (a * a) (b * b) (c * c) = (a + b + c) * (a + b - c) *
  48   (b + c - a) * (c + a - b)` ASSUME_TAC);
  49  (REWRITE_TAC[ups_x]);
  50  (REAL_ARITH_TAC);
  51  (REWRITE_TAC[arclength]);
  52  AP_TERM_TAC;
  53  (ASM_REWRITE_TAC[]);
  54  (ABBREV_TAC `S = (a + b + c) * (a + b - c) * (b + c - a) * (c + a - b)`);
  55  (SUBGOAL_THEN `&0 < sqrt S` ASSUME_TAC);
  56  (MATCH_MP_TAC SQRT_POS_LT);
  57  (ASM_REWRITE_TAC[]);
  58  (ASM_MESON_TAC[ATN2_BREAKDOWN])]);;
  59
  60 (* ========================================================================== *)
  61
  62 let compute_one_first = prove_by_refinement (
  63  `!y1 y2 s hz g x.
  64      &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
  65      &2 <= y2 /\ y2 <= &2 * hz /\
  66      s = {t | y1 - &4 < t /\ t < &4 - y2} /\
  67      g = (\t. arclength y1 (y2 + t) (&2)) /\ x IN s /\
  68      g' = (\x. --((y2 + x) pow 2 - y1 pow 2 + &4) /
  69        ((y2 + x) *
  70         sqrt
  71         ((y1 + (y2 + x) + &2) *
  72          (y1 + (y2 + x) - &2) *
  73          ((y2 + x) + &2 - y1) *
  74          (&2 + y1 - (y2 + x)))))
  75      ==> (g has_real_derivative g' x) (atreal x within s)`,
  76
  77 [(REPEAT STRIP_TAC);
  78  REWRITE_TAC[ASSUME `g' = (\x. --((y2 + x) pow 2 - y1 pow 2 + &4) /
  79        ((y2 + x) *
  80         sqrt
  81         ((y1 + (y2 + x) + &2) *
  82          (y1 + (y2 + x) - &2) *
  83          ((y2 + x) + &2 - y1) *
  84          (&2 + y1 - (y2 + x)))))`];
  85   (SUBGOAL_THEN `!t. t IN s ==>
  86      &0 < (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
  87           ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))` ASSUME_TAC);
  88
  89   (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
  90
  91    (SUBGOAL_THEN
  92       `&0 < y1 + (y2 + t) - &2 /\ &0 < y1 + (y2 + t) + &2 /\
  93        &0 < (y2 + t) + &2 - y1 /\ &0 < &2 + y1 - (y2 + t)` ASSUME_TAC);
  94     ASM_REAL_ARITH_TAC;
  95   (ASM_MESON_TAC[REAL_LT_MUL]);
  96
  97 (* ========================================================================== *)
  98 (*         SUBGOAL 3                                                          *)
  99 (* ========================================================================== *)
 100
 101  (ABBREV_TAC `f1 = (\t. (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 102                          ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))`);
 103  (ABBREV_TAC `f1' = &4 * (y2 + x) * (y1 pow 2 - (y2 + x) pow 2 + &4)`);
 104  (ABBREV_TAC `P ={x| &0 < x}`);
 105  (ABBREV_TAC `f2 = (\t. sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 106                               ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))))`);
 107
 108   (SUBGOAL_THEN `f2 = (\t:real. sqrt (f1 t))` ASSUME_TAC);
 109   (EXPAND_TAC "f1" THEN EXPAND_TAC "f2" THEN MESON_TAC[]);
 110
 111  (ABBREV_TAC `g2' = (\x. inv (&2 * sqrt x))`);
 112  (ABBREV_TAC `f2' = f1' * g2' ((f1:real->real) x)`);
 113
 114  (SUBGOAL_THEN `(f2 has_real_derivative f2') (atreal x within s)`ASSUME_TAC);
 115  (EXPAND_TAC "f2'" THEN PURE_REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 116
 117   (SUBGOAL_THEN `(f1 has_real_derivative f1') (atreal x within s) /\ P (f1 x)`
 118    ASSUME_TAC);
 119    STRIP_TAC;
 120   (EXPAND_TAC "f1" THEN EXPAND_TAC "f1'");
 121   (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 122   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM] THEN EXPAND_TAC "f1");
 123   (MP_TAC (ASSUME `(x:real) IN s`) THEN ASM_REWRITE_TAC[]);
 124   (FIRST_X_ASSUM MP_TAC);
 125
 126   (SUBGOAL_THEN `!x. P x ==>
 127     (sqrt has_real_derivative (g2':real->real) x) (atreal x)` ASSUME_TAC);
 128   (EXPAND_TAC "g2'" THEN REWRITE_TAC[BETA_THM]);
 129   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
 130   (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
 131   (FIRST_X_ASSUM MP_TAC);
 132
 133  (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 134
 135 (* ------------------------------------------------------------------------- *)
 136
 137  (ABBREV_TAC `f3 = (\t. (&2 * &2 - y1 * y1 - (y2 + t) * (y2 + t)) /
 138                       sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 139                             ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))))`);
 140  (ABBREV_TAC `h = (\t. (&2 * &2 - y1 * y1 - (y2 + t) * (y2 + t)))`);
 141
 142  (SUBGOAL_THEN `f3 = (\t:real. h t / f2 t)` ASSUME_TAC);
 143  (EXPAND_TAC "f2" THEN EXPAND_TAC "h" THEN EXPAND_TAC "f3");
 144  (REWRITE_TAC[]);
 145
 146  (SUBGOAL_THEN `(h has_real_derivative -- &2 * (y2 + x)) (atreal x within s) /\
 147                 (f2 has_real_derivative f2') (atreal x within s) /\
 148                ~(f2 x = &0)` ASSUME_TAC);
 149  (REPEAT CONJ_TAC);
 150
 151   (EXPAND_TAC "h" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 152   (ASM_REWRITE_TAC[]);
 153   (ASM_REWRITE_TAC[]);
 154   (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 155   (MATCH_MP_TAC SQRT_POS_LT);
 156   (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 157
 158  (SUBGOAL_THEN `(f3 has_real_derivative
 159                  ((-- &2 * (y2 + x)) * f2 x - h x * f2') / f2 x pow 2)
 160                  (atreal x within s)` ASSUME_TAC);
 161  (PURE_REWRITE_TAC[ASSUME `f3 = (\t:real. h t / f2 t)`]);
 162  (FIRST_X_ASSUM MP_TAC);
 163  (REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);
 164
 165 (* --------------------------------------------------------------------------*)
 166
 167  (ABBREV_TAC `F1 = (\t. atn ((&2 * &2 - y1 * y1 - (y2 + t) * (y2 + t)) /
 168                            sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 169                             ((y2 + t) + &2 - y1)  * (&2 + y1 - (y2 + t)))))`);
 170  (ABBREV_TAC `f3' = ((-- &2 * (y2 + x)) * f2 x - h x * f2') / f2 x pow 2`);
 171  (ABBREV_TAC `h' = (\x. inv (&1 + x pow 2))`);
 172
 173  (SUBGOAL_THEN `F1 = (\t:real. atn (f3 t))` ASSUME_TAC);
 174  (EXPAND_TAC "f3" THEN EXPAND_TAC "F1" THEN ASM_REWRITE_TAC[]);
 175
 176  (SUBGOAL_THEN `(F1 has_real_derivative f3' * inv (&1 + f3 x pow 2))
 177                  (atreal x within s)` ASSUME_TAC);
 178  (REWRITE_TAC[ASSUME `F1 = (\t:real. atn (f3 t))`]);
 179
 180   (SUBGOAL_THEN `(f3 has_real_derivative f3') (atreal x within s) /\
 181                    (:real) (f3 x)` ASSUME_TAC);
 182   (ASM_REWRITE_TAC[]);
 183   (MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
 184   (FIRST_X_ASSUM MP_TAC);
 185
 186   (SUBGOAL_THEN `!x. (:real) x ==> (atn has_real_derivative (h':real->real) x)
 187                                      (atreal x)` ASSUME_TAC);
 188   (EXPAND_TAC "h'" THEN REWRITE_TAC[BETA_THM]);
 189   (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
 190   (FIRST_X_ASSUM MP_TAC);
 191
 192   (SUBGOAL_THEN `inv (&1 + f3 (x:real) pow 2) = h' (f3 x)` ASSUME_TAC);
 193   (EXPAND_TAC "h'" THEN REWRITE_TAC[]);
 194
 195  (REWRITE_TAC[ASSUME `inv (&1 + f3 (x:real) pow 2) = h'( f3 x)`]);
 196  (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 197
 198 (* --------------------------------------------------------------------------*)
 199
 200  (SUBGOAL_THEN `f1 x = &4 * (y1 * (y2 + x)) pow 2 -
 201                  (&2 * &2 - y1 * y1 - (y2 + x) * (y2 + x)) pow 2` ASSUME_TAC);
 202  (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
 203
 204  (SUBGOAL_THEN `inv (&1 + f3 x pow 2) =
 205                 (f1 x) / (&4 * (y1 * (y2 + x)) pow 2)` ASSUME_TAC);
 206  (EXPAND_TAC "f3");
 207  (REWRITE_TAC[REAL_POW_DIV]);
 208
 209  (SUBGOAL_THEN `&0 <= (y1 + (y2 + x) + &2) * (y1 + (y2 + x) - &2) *
 210                       ((y2 + x) + &2 - y1) * (&2 + y1 - (y2 + x))` ASSUME_TAC);
 211  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 212  (MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 213
 214  (SUBGOAL_THEN `sqrt ((y1 + (y2 + x) + &2) * (y1 + (y2 + x) - &2) *
 215         ((y2 + x) + &2 - y1) * (&2 + y1 - (y2 + x))) pow 2 = f1 x` ASSUME_TAC);
 216  (EXPAND_TAC "f1" THEN ASM_SIMP_TAC [SQRT_POW_2]);
 217
 218  (PURE_ONCE_ASM_REWRITE_TAC[]);
 219  (ONCE_ASM_REWRITE_TAC[GSYM REAL_INV_DIV]);
 220  (AP_TERM_TAC);
 221  (ONCE_ASM_REWRITE_TAC[REAL_INV_DIV] THEN PURE_ONCE_ASM_REWRITE_TAC[]);
 222
 223  (MATCH_MP_TAC (REAL_ARITH `&1 = x - y ==> &1 + y = x `));
 224  (REWRITE_TAC [REAL_ARITH `x / y - z / y = (x - z) / y`]);
 225  (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
 226  (REWRITE_TAC[GSYM (ASSUME `f1 x = &4 * (y1 * (y2 + x)) pow 2 -
 227    (&2 * &2 - y1 * y1 - (y2 + x) * (y2 + x)) pow 2`)]);
 228  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(&0 = a)`));
 229  (MP_TAC (ASSUME `x:real IN s`));
 230  (EXPAND_TAC "f1" THEN ASM_REWRITE_TAC[]);
 231
 232 (* ========================================================================== *)
 233
 234  (SUBGOAL_THEN ` ((-- &2 * (y2 + x)) * f2 x - h x * f2') =
 235    -- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4) / f2 x`
 236  ASSUME_TAC);
 237
 238  (ABBREV_TAC `X = ((-- &2 * (y2 + x)) * f2 x - h x * f2')`);
 239  (REWRITE_TAC[REAL_ARITH `x * y / z = (x * y) / z`]);
 240  (ABBREV_TAC
 241    `Y = (-- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4))`);
 242  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 243
 244  (SUBGOAL_THEN `Y / f2 (x:real) = X <=> Y = X * f2 x` ASSUME_TAC);
 245  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 246  (REPLICATE_TAC 2 (ONCE_ASM_REWRITE_TAC[]) THEN MATCH_MP_TAC SQRT_POS_LT);
 247  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 248  (ONCE_ASM_REWRITE_TAC[]);
 249
 250  (EXPAND_TAC "X" THEN EXPAND_TAC "Y");
 251  (EXPAND_TAC "f2'" THEN EXPAND_TAC "h" THEN EXPAND_TAC "g2'");
 252  (ONCE_REWRITE_TAC[REAL_ARITH `(a - b) * c = a * c - b * c`]);
 253
 254  (SUBGOAL_THEN `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2` ASSUME_TAC);
 255  (REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 256  (ONCE_REWRITE_TAC[REAL_ARITH `a * sqrt b = (a * (&2 * sqrt b)) / &2`]);
 257  (AP_THM_TAC THEN AP_TERM_TAC);
 258  (MATCH_MP_TAC REAL_MUL_LINV);
 259  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 260  (MATCH_MP_TAC REAL_LT_MUL);
 261  (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
 262  (MATCH_MP_TAC SQRT_POS_LT);
 263  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 264
 265  (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b) * c * d`]);
 266  (PURE_REWRITE_TAC[ASSUME `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2`]);
 267  (REWRITE_TAC[REAL_ARITH `(a * f2 x) * f2 x = a * (f2 (x:real) pow 2)`]);
 268
 269  (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 270  (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 271  (MATCH_MP_TAC SQRT_POW_2);
 272  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 273  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 274
 275  (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);
 276  (ASM_REWRITE_TAC[]);
 277  (EXPAND_TAC "Y" THEN EXPAND_TAC "f1'");
 278  REAL_ARITH_TAC;
 279
 280 (* ========================================================================= *)
 281
 282  (SUBGOAL_THEN
 283   `f3' * inv (&1 + f3 x pow 2) =
 284    -- ((y2 + x) pow 2 - y1 pow 2 + &4) / ((y2 + x) * f2 x)` ASSUME_TAC);
 285  (EXPAND_TAC "f3'");
 286  (REWRITE_TAC[ASSUME
 287   `inv (&1 + f3 x pow 2) = f1 x / (&4 * (y1 * (y2 + x)) pow 2)`]);
 288  (REWRITE_TAC[ASSUME `(-- &2 * (y2 + x)) * f2 x - h x * f2' =
 289       -- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4) / f2 x`]);
 290
 291  (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 292  (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 293  (MATCH_MP_TAC SQRT_POW_2);
 294  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 295  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 296  (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);
 297
 298  (ONCE_REWRITE_TAC [REAL_ARITH `a / b * c / d = (a / d) * c / b`]);
 299  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 /\ x = y ==> x * a = y`));
 300  STRIP_TAC;
 301  (MATCH_MP_TAC REAL_DIV_REFL);
 302  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 303  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 304
 305  (ABBREV_TAC `X =
 306   (-- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4) / f2 x)`);
 307  (ABBREV_TAC
 308    `Y = --((y2 + x) pow 2 - y1 pow 2 + &4) / ((y2 + x) * f2 x)`);
 309  (ABBREV_TAC `Z = (&4 * (y1 * (y2 + x)) pow 2)`);
 310
 311  (SUBGOAL_THEN `X / Z = Y <=> X = Y * Z` ASSUME_TAC);
 312  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 313  (EXPAND_TAC "Z");
 314  (MATCH_MP_TAC REAL_LT_MUL);
 315  (REWRITE_TAC[REAL_ARITH `&0 < &4`]);
 316  (MATCH_MP_TAC REAL_POW_LT);
 317  (MATCH_MP_TAC REAL_LT_MUL);
 318  STRIP_TAC;
 319  (ASM_REAL_ARITH_TAC);
 320  (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + y2 - &4 /\ y1 + y2 - &4 < s ==> &0 < s`));
 321  (STRIP_TAC);
 322  (MATCH_MP_TAC (REAL_ARITH `&2 <= y1 /\ &2 <= y2 ==> &0 <= y1 + y2 - &4`));
 323  (ASM_REWRITE_TAC[]);
 324  (MATCH_MP_TAC (REAL_ARITH `y1 - &4 < x ==> y1 + y2 - &4 < y2 + x`));
 325  (MP_TAC (ASSUME `x:real IN s`));
 326  (REWRITE_TAC[ASSUME `s = {t | y1 - &4 < t /\ t < &4 - y2}`]);
 327  (PURE_REWRITE_TAC[IN_ELIM_THM]);
 328  (STRIP_TAC THEN ASM_REWRITE_TAC[]);
 329  (ONCE_ASM_REWRITE_TAC[]);
 330
 331  (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 332  (REWRITE_TAC [REAL_ARITH `a * b / c = (a * b) / c`]);
 333  (REWRITE_TAC[REAL_ARITH
 334   `--((y2 + x) pow 2 - y1 pow 2 + &4) / ((y2 + x) * f2 x) *
 335    &4 *  (y1 * (y2 + x)) pow 2 =
 336    (-- &4 * y1 * y1 * (y2 + x) * ((y2 + x) pow 2 - y1 pow 2 + &4)) * (y2 + x)
 337    / (f2 x * (y2 + x))`]);
 338  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 339  (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
 340  CONJ_TAC;
 341  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 342  (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + y2 - &4 /\ y1 + y2 - &4 < s ==> &0 < s`));
 343  (STRIP_TAC);
 344  (MATCH_MP_TAC (REAL_ARITH `&2 <= y1 /\ &2 <= y2 ==> &0 <= y1 + y2 - &4`));
 345  (ASM_REWRITE_TAC[]);
 346  (MATCH_MP_TAC (REAL_ARITH `y1 - &4 < x ==> y1 + y2 - &4 < y2 + x`));
 347  (MP_TAC (ASSUME `x:real IN s`));
 348  (REWRITE_TAC[ASSUME `s = {t | y1 - &4 < t /\ t < &4 - y2}`]);
 349  (PURE_REWRITE_TAC[IN_ELIM_THM]);
 350  (STRIP_TAC THEN ASM_REWRITE_TAC[]);
 351
 352  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 353  (ONCE_ASM_REWRITE_TAC[]);
 354  (ONCE_ASM_REWRITE_TAC[]);
 355  (MATCH_MP_TAC SQRT_POS_LT);
 356  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 357
 358 (* ========================================================================== *)
 359
 360  (SUBGOAL_THEN
 361   `(F1 has_real_derivative --((y2 + x) pow 2 - y1 pow 2 + &4) /
 362    ((y2 + x) * f2 x)) (atreal x within s)` ASSUME_TAC);
 363  (ASM_MESON_TAC[]);
 364
 365  (SUBGOAL_THEN `
 366   (F1 has_real_derivative --((y2 + x) pow 2 - y1 pow 2 + &4) /
 367   ((y2 + x) * sqrt
 368            ((y1 + (y2 + x) + &2) *
 369             (y1 + (y2 + x) - &2) *
 370             ((y2 + x) + &2 - y1) *
 371             (&2 + y1 - (y2 + x)))))
 372       (atreal x within s)` ASSUME_TAC);
 373  (FIRST_X_ASSUM MP_TAC THEN EXPAND_TAC "f2");
 374  (REWRITE_TAC[]);
 375
 376  (ABBREV_TAC `F2 = (\x:real. pi / &2 + F1 x)`);
 377  (ABBREV_TAC `pi_2 = (\x:real. pi / &2 )`);
 378
 379  (SUBGOAL_THEN `(F2 has_real_derivative --((y2 + x) pow 2 - y1 pow 2 + &4) /
 380   ((y2 + x) *
 381    sqrt
 382    ((y1 + (y2 + x) + &2) *
 383     (y1 + (y2 + x) - &2) *
 384     ((y2 + x) + &2 - y1) *
 385     (&2 + y1 - (y2 + x)))))
 386  (atreal x within s)` ASSUME_TAC);
 387
 388  (SUBGOAL_THEN `F2 = (\x:real. pi_2 x + F1 x)` ASSUME_TAC);
 389  (EXPAND_TAC "F2" THEN EXPAND_TAC "F1" THEN EXPAND_TAC "pi_2");
 390  (REWRITE_TAC[]);
 391
 392  (REWRITE_TAC[ASSUME `F2 = (\x:real. pi_2 x + F1 x)`]);
 393  (ABBREV_TAC `F1' = (--((y2 + x) pow 2 - y1 pow 2 + &4) /
 394   ((y2 + x) *
 395    sqrt
 396    ((y1 + (y2 + x) + &2) *
 397     (y1 + (y2 + x) - &2) *
 398     ((y2 + x) + &2 - y1) *
 399     (&2 + y1 - (y2 + x)))))`);
 400
 401  (SUBGOAL_THEN `((\x. pi_2 x + F1 x) has_real_derivative &0 + F1')
 402  (atreal x within s)` ASSUME_TAC);
 403
 404  (SUBGOAL_THEN `(pi_2 has_real_derivative (&0)) (atreal x within s)`
 405    ASSUME_TAC);
 406  (EXPAND_TAC "pi_2");
 407  (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 408
 409  (FIRST_X_ASSUM MP_TAC);
 410  (MP_TAC (ASSUME `(F1 has_real_derivative F1') (atreal x within s)`));
 411  (REWRITE_TAC[MESON[] `(a ==> b ==> c) <=> (b /\ a ==> c)`]);
 412  (MESON_TAC[HAS_REAL_DERIVATIVE_ADD]);
 413  (ASM_MESON_TAC[REAL_ARITH `&0 + a = a`]);
 414
 415
 416  (ABBREV_TAC `F1' = (--((y2 + x) pow 2 - y1 pow 2 + &4) /
 417   ((y2 + x) *
 418    sqrt
 419    ((y1 + (y2 + x) + &2) *
 420     (y1 + (y2 + x) - &2) *
 421     ((y2 + x) + &2 - y1) *
 422     (&2 + y1 - (y2 + x)))))`);
 423
 424  (SUBGOAL_THEN
 425   `(!x':real. (x':real) IN s /\ abs (x' - x) < &1 ==>
 426    (F2:real -> real) x' = g x')` ASSUME_TAC);
 427  (REPEAT STRIP_TAC);
 428  (ASM_REWRITE_TAC[]);
 429  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 430  (EXPAND_TAC "F2");
 431  (EXPAND_TAC "F1");
 432  (MATCH_MP_TAC ATN_UPS_X_BREAKDOWN1);
 433  (MP_TAC (ASSUME `x':real IN s`));
 434  (ASM_REWRITE_TAC[]);
 435  (MP_TAC (ASSUME `(F2 has_real_derivative F1') (atreal x within s)`));
 436  (MP_TAC (ASSUME `!x'. x' IN s /\ abs (x' - x) < &1 ==> (F2:real->real) x' = g x'`));
 437  (MP_TAC (ASSUME `x:real IN s`));
 438  (MP_TAC (REAL_ARITH `&0 < &1`));
 439  (MESON_TAC[HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN])]);;
 440
 441 (* ========================================================================= *)
 442
 443
 444 let compute_one_second = prove_by_refinement (
 445  `!y1 y2 s hz g x.
 446      &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
 447      &2 <= y2 /\ y2 <= &2 * hz /\
 448      s = {t | y1 - &4 < t /\ t < &4 - y2} /\
 449      g = (\t. --((y2 + t) pow 2 - y1 pow 2 + &4) /
 450            ((y2 + t) *
 451             sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 452             ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))))
 453      ==> (g has_real_derivative
 454           (-- &64 + &48 * y1 pow 2 - &12 * y1 pow 4 + y1 pow 6 +
 455           &80 * y2 pow 2 - &8 * y1 pow 2 * y2 pow 2 - &3 * y1 pow 4 * y2 pow 2 -
 456           &12 * y2 pow 4 + &3 * y1 pow 2 * y2 pow 4 - y2 pow 6) /
 457           (y2 pow 2 *  sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
 458           ups_x (y1 pow 2) (y2 pow 2) (&4)))
 459          (atreal (&0) within s)`,
 460 [ REPEAT STRIP_TAC;
 461
 462    (SUBGOAL_THEN `&0 IN s` ASSUME_TAC);
 463    (PURE_ASM_REWRITE_TAC[IN_ELIM_THM]);
 464    CONJ_TAC;
 465      (REWRITE_TAC[REAL_ARITH `a - b < &0 <=> a < b`]);
 466      (MATCH_MP_TAC (REAL_ARITH `y1 <= &2 * hz /\ &2 * hz < &4 ==> y1 < &4`));
 467      (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
 468      ASM_REAL_ARITH_TAC;
 469
 470 (* ========================================================================== *)
 471
 472   (SUBGOAL_THEN
 473     `!t. t IN s ==>  &0 < (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 474          ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t))` ASSUME_TAC);
 475   (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
 476
 477     (SUBGOAL_THEN `&0 < y1 + (y2 + t) - &2 /\ &0 < y1 + (y2 + t) + &2 /\
 478           &0 < (y2 + t) + &2 - y1 /\ &0 < &2 + y1 - (y2 + t)` ASSUME_TAC);
 479     (ASM_REAL_ARITH_TAC);
 480     (ASM_MESON_TAC[REAL_LT_MUL]);
 481
 482  (ABBREV_TAC `f1 = (\t. --((y2 + t) pow 2 - y1 pow 2 + &4))`);
 483  (ABBREV_TAC `f2 = (\t. (y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 484              ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))`);
 485  (ABBREV_TAC `f3 = (\t:real. sqrt (f2 t))`);
 486  (ABBREV_TAC `f4 = (\t:real. y2 + t)`);
 487  (ABBREV_TAC `f5 = (\t:real. f4 t * f3 t )`);
 488
 489 (SUBGOAL_THEN `&0 < f2 (&0)` ASSUME_TAC);
 490 (EXPAND_TAC "f2" THEN MP_TAC (ASSUME`((&0):real) IN s`) THEN ASM_REWRITE_TAC[]);
 491
 492 (SUBGOAL_THEN `(f1 has_real_derivative -- &2 * y2) (atreal (&0) within s)`
 493   ASSUME_TAC);
 494 (EXPAND_TAC "f1" THEN REAL_DIFF_TAC);
 495 (REWRITE_TAC[ARITH_RULE `2 - 1 = 1`] THEN REAL_ARITH_TAC);
 496
 497 (ABBREV_TAC `f2' = &4 * y2 * (y1 pow 2 - y2 pow 2 + &4)`);
 498 (ABBREV_TAC `P ={x| &0 < x}`);
 499 (ABBREV_TAC `g3' = (\x. inv (&2 * sqrt x))`);
 500 (ABBREV_TAC `f3' = f2' * g3' ((f2:real->real) (&0))`);
 501
 502  (SUBGOAL_THEN
 503     `(f3 has_real_derivative f3') (atreal (&0) within s)` ASSUME_TAC);
 504  (EXPAND_TAC "f3'" THEN EXPAND_TAC "f3");
 505
 506 (SUBGOAL_THEN `(f2 has_real_derivative f2') (atreal (&0) within s) /\
 507                P (f2 (&0))` MP_TAC);
 508   STRIP_TAC;
 509
 510   (EXPAND_TAC "f2" THEN EXPAND_TAC "f2'");
 511   (REAL_DIFF_TAC THEN REWRITE_TAC[POW_2] THEN REAL_ARITH_TAC);
 512   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
 513   (ASM_REWRITE_TAC[]);
 514
 515  (SUBGOAL_THEN
 516     `!x. P x ==> (sqrt has_real_derivative (g3':real->real) x) (atreal x)`
 517      MP_TAC);
 518  (EXPAND_TAC "g3'" THEN REWRITE_TAC[BETA_THM]);
 519  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
 520  (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
 521
 522 (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 523
 524 (* ========================================================================== *)
 525
 526 (SUBGOAL_THEN `(f5 has_real_derivative f4 (&0) * f3' + &1 * f3 (&0))
 527   (atreal (&0) within s)` ASSUME_TAC);
 528
 529 (SUBGOAL_THEN
 530   `(f4 has_real_derivative &1) (atreal (&0) within s) /\
 531    (f3 has_real_derivative f3') (atreal (&0) within s)` MP_TAC);
 532 (ASM_REWRITE_TAC[]);
 533 (EXPAND_TAC "f4" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 534
 535 (EXPAND_TAC "f5");
 536 (REWRITE_TAC[HAS_REAL_DERIVATIVE_MUL_WITHIN]);
 537
 538 (* ========================================================================= *)
 539 (*          Derivative of f1 / f5                                            *)
 540 (* ========================================================================= *)
 541
 542 (SUBGOAL_THEN `g = (\t:real. f1 t / f5 t)` ASSUME_TAC);
 543 (ASM_REWRITE_TAC[] THEN EXPAND_TAC "f5" THEN EXPAND_TAC "f1");
 544 (EXPAND_TAC "f4" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f2" THEN REWRITE_TAC[]);
 545
 546 (REWRITE_TAC[ASSUME `g = (\t:real. f1 t / f5 t)`] THEN DEL_TAC);
 547
 548 (SUBGOAL_THEN `((\t. f1 t / f5 t) has_real_derivative
 549   ((-- &2 * y2) * f5 (&0) - f1 (&0) * (f4 (&0) * f3' + &1 * f3 (&0))) /
 550   f5 (&0) pow 2) (atreal (&0) within s)` ASSUME_TAC);
 551
 552 (SUBGOAL_THEN
 553   `(f1 has_real_derivative -- &2 * y2) (atreal (&0) within s) /\
 554    (f5 has_real_derivative f4 (&0) * f3' + &1 * f3 (&0))
 555     (atreal (&0) within s) /\ ~(f5 (&0) = &0)` MP_TAC);
 556 (ASM_REWRITE_TAC[]);
 557 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 558 (EXPAND_TAC "f5" THEN MATCH_MP_TAC REAL_LT_MUL);
 559 STRIP_TAC;
 560
 561 (EXPAND_TAC "f4" THEN ASM_REAL_ARITH_TAC);
 562 (EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
 563
 564 (REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);
 565
 566 (* ========================================================================= *)
 567
 568 (SUBGOAL_THEN
 569 `((-- &2 * y2) * f5 (&0) - f1 (&0) * (f4 (&0) * f3' + &1 * f3 (&0))) /
 570  f5 (&0) pow 2 =
 571 (-- &64 + &48 * y1 pow 2 - &12 * y1 pow 4 + y1 pow 6 +
 572     &80 * y2 pow 2 - &8 * y1 pow 2 * y2 pow 2 - &3 * y1 pow 4 * y2 pow 2 -
 573     &12 * y2 pow 4 + &3 * y1 pow 2 * y2 pow 4 - y2 pow 6) /
 574     (y2 pow 2 *  sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
 575     ups_x (y1 pow 2) (y2 pow 2) (&4))` ASSUME_TAC);
 576
 577 (EXPAND_TAC "f5");
 578
 579 (SUBGOAL_THEN `f4 (&0) = (y2:real)` ASSUME_TAC);
 580 (EXPAND_TAC "f4" THEN REAL_ARITH_TAC);
 581 (ASM_REWRITE_TAC[]);
 582 (REWRITE_TAC[REAL_ARITH `a pow 4 = a pow 2 * a pow 2`]);
 583 (REWRITE_TAC[REAL_ARITH `a pow 6 = a pow 2 * a pow 2 * a pow 2`]);
 584 (REWRITE_TAC[REAL_MUL_LID]);
 585 (REWRITE_TAC[REAL_ARITH `a - b * (c + d) = a - b * c - b * d`]);
 586 (REWRITE_TAC[REAL_ARITH `(-- &2 * y2) * y2 * x = ((-- &2 * y2) * y2) * x`]);
 587 (REWRITE_TAC[REAL_ARITH `a * f3 (&0) - b - c * f3 (&0) = (a - c) * f3 (&0) - b`]);
 588
 589 (SUBGOAL_THEN `(-- &2 * y2) * y2 - f1 (&0) = (&4 - y1 pow 2 - y2 pow 2)` ASSUME_TAC);
 590 (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
 591 (ASM_REWRITE_TAC[]);
 592
 593 (EXPAND_TAC "f3'" THEN EXPAND_TAC "g3'");
 594
 595 (SUBGOAL_THEN `sqrt (f2 (&0)) = f3 (&0)` ASSUME_TAC);
 596 (EXPAND_TAC "f3" THEN REWRITE_TAC[]);
 597 (REWRITE_TAC[ASSUME `sqrt (f2 (&0)) = f3 (&0)`]);
 598
 599 (SUBGOAL_THEN
 600 `(&4 - y1 pow 2 - y2 pow 2) * f3 (&0) -
 601  f1 (&0) * y2 * f2' * inv (&2 * f3 (&0)) =
 602  ((&4 - y1 pow 2 - y2 pow 2) * f3 (&0) pow 2 -
 603   f1 (&0) * &2 * y2 pow 2 * (y1 pow 2 - y2 pow 2 + &4)) /
 604  f3 (&0)` ASSUME_TAC);
 605
 606 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a - b) / c = a / c - b / c`]);
 607 (MATCH_MP_TAC (REAL_ARITH `a = b /\ c = d ==> a - c = b - d`));
 608 STRIP_TAC;
 609
 610 (REWRITE_TAC[REAL_POW_2; REAL_ARITH `(a * b * c) / d = (a * b) * c / d`]);
 611 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b = b * a`));
 612 (MATCH_MP_TAC REAL_DIV_REFL);
 613 (EXPAND_TAC "f3");
 614 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 615 (MATCH_MP_TAC SQRT_POS_LT);
 616 (ASM_REWRITE_TAC[]);
 617
 618 (EXPAND_TAC "f2'" THEN REWRITE_TAC[REAL_POW_2]);
 619 (REWRITE_TAC[REAL_ARITH
 620  `f1 (&0) * y2 * (&4 * y2 * (y1 * y1 - y2 * y2 + &4)) * inv (&2 * f3 (&0)) =
 621   (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) * &2 *
 622  inv (&2 * f3 (&0))`]) ;
 623
 624 (ABBREV_TAC `X = (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) *
 625  &2 * inv (&2 * f3 (&0))`);
 626 (ABBREV_TAC `Y = (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4))`);
 627 (ABBREV_TAC `Z = (f3:real->real) (&0)`);
 628
 629 (SUBGOAL_THEN `X = Y / Z <=> X * Z = Y` ASSUME_TAC);
 630 (MATCH_MP_TAC REAL_EQ_RDIV_EQ THEN EXPAND_TAC "Z" THEN EXPAND_TAC "f3");
 631 (MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
 632 (ASM_REWRITE_TAC[]);
 633
 634 (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 635 (REWRITE_TAC[REAL_ARITH
 636   `((f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) * &2 *
 637     inv (&2 * f3 (&0))) * f3 (&0) =
 638     (f1 (&0) * &2 * (y2 * y2) * (y1 * y1 - y2 * y2 + &4)) *
 639     (&2 * f3 (&0)) * inv (&2 * f3 (&0))`]);
 640
 641 (MATCH_MP_TAC( MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
 642 (MATCH_MP_TAC REAL_MUL_RINV);
 643 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
 644 (MATCH_MP_TAC REAL_LT_MUL);
 645 (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
 646 (EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
 647 (ASM_REWRITE_TAC[]);
 648
 649 (ABBREV_TAC `a = y1 pow 2`);
 650 (ABBREV_TAC `b = y2 pow 2`);
 651
 652 (SUBGOAL_THEN
 653  `((&4 - a - b) * f3 (&0) pow 2 - f1 (&0) * &2 * b * (a - b + &4)) =
 654   -- &64 + &48 * a - &12 * a * a + a * a * a + &80 * b - &8 * a * b -
 655   &3 * (a * a) * b - &12 * b * b + &3 * a * b * b - b * b * b` ASSUME_TAC);
 656
 657 (EXPAND_TAC "f3");
 658 (SUBGOAL_THEN `sqrt (f2 (&0)) pow 2 = f2 (&0)` ASSUME_TAC);
 659 (MATCH_MP_TAC SQRT_POW_2);
 660 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);
 661 (ASM_REWRITE_TAC[]);
 662
 663 (SUBGOAL_THEN `f2 (&0) = &4 * a * b - (&4 - a - b) pow 2` ASSUME_TAC);
 664 (EXPAND_TAC "f2" THEN EXPAND_TAC "a" THEN EXPAND_TAC "b");
 665 REAL_ARITH_TAC;
 666 (ASM_REWRITE_TAC[]);
 667
 668 (EXPAND_TAC "f1");
 669 (REWRITE_TAC[REAL_ARITH `y + &0 = y`; ASSUME `y2 pow 2 = b`]);
 670 REAL_ARITH_TAC;
 671
 672 (ASM_REWRITE_TAC[]);
 673
 674 (ABBREV_TAC `X' = (-- &64 + &48 * a - &12 * a * a +  a * a * a +  &80 * b -
 675   &8 * a * b - &3 * (a * a) * b - &12 * b * b + &3 * a * b * b - b * b * b)`);
 676
 677 (SUBGOAL_THEN `ups_x a b (&4) = f2 (&0)` ASSUME_TAC);
 678 (EXPAND_TAC "f2" THEN REWRITE_TAC[ups_x]);
 679 (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN REAL_ARITH_TAC);
 680 (ASM_REWRITE_TAC[]);
 681
 682 (ABBREV_TAC `Z' = X' / f3 (&0) / (y2 * f3 (&0)) pow 2`);
 683 (ABBREV_TAC `Y' = (b * f3 (&0) * f2 (&0))`);
 684
 685 (SUBGOAL_THEN `Z' = X' / Y' <=> Z' * Y' = X'` ASSUME_TAC);
 686 (MATCH_MP_TAC REAL_EQ_RDIV_EQ THEN EXPAND_TAC "Y'");
 687 (MATCH_MP_TAC REAL_LT_MUL);
 688 STRIP_TAC;
 689 (EXPAND_TAC "b" THEN MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC);
 690 (MATCH_MP_TAC REAL_LT_MUL THEN EXPAND_TAC "f3");
 691 (ASM_SIMP_TAC [SQRT_POS_LT]);
 692 (ASM_REWRITE_TAC[]);
 693
 694 (EXPAND_TAC "Z'" THEN EXPAND_TAC "Y'");
 695 (REWRITE_TAC[REAL_ARITH `a / b * c = (a * c) / b`]);
 696
 697 (SUBGOAL_THEN `(X' * b * f3 (&0) * f2 (&0)) / f3 (&0) = X' * b * f2 (&0)` ASSUME_TAC);
 698 (REWRITE_TAC[REAL_ARITH `(a * b * c * d) / f = (a * b * d) * (c / f)`] );
 699 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
 700 (MATCH_MP_TAC REAL_DIV_REFL);
 701 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 702 (EXPAND_TAC "f3");
 703 (MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
 704
 705 (ASM_REWRITE_TAC[]);
 706 (REWRITE_TAC[REAL_POW_2]);
 707 (REWRITE_TAC[REAL_ARITH `(a * b) * a * b = a pow 2 * b pow 2`]);
 708 (SUBGOAL_THEN `f3 (&0) pow 2 = f2 (&0)` ASSUME_TAC);
 709 (EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POW_2);
 710 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);
 711
 712 (ASM_REWRITE_TAC[]);
 713 (REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]);
 714 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
 715 (REWRITE_TAC[REAL_ARITH `a * b / c = (a * b) / c`]);
 716 (MATCH_MP_TAC REAL_DIV_REFL);
 717 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 718 (MATCH_MP_TAC REAL_LT_MUL);
 719 (ASM_REWRITE_TAC[]);
 720 (EXPAND_TAC "b" THEN MATCH_MP_TAC REAL_POW_LT THEN ASM_REAL_ARITH_TAC);
 721
 722 (ASM_MESON_TAC[])]);;
 723
 724 (* ========================================================================= *)
 725
 726 let COMPUTE_DERIVATIVE_ONE = prove_by_refinement (
 727  `!y1 y2 s hz g x f.
 728      &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
 729      &2 <= y2 /\ y2 <= &2 * hz /\
 730      s = {t | y1 - &4 < t /\ t < &4 - y2} /\
 731      g = (\t. arclength y1 (y2 + t) (&2)) /\
 732      g' = (\t. --((y2 + t) pow 2 - y1 pow 2 + &4) /
 733                 ((y2 + t) *
 734                 sqrt ((y1 + (y2 + t) + &2) * (y1 + (y2 + t) - &2) *
 735                ((y2 + t) + &2 - y1) * (&2 + y1 - (y2 + t)))))
 736 ==>  (!x. x IN s ==> (g has_real_derivative g' x) (atreal x within s)) /\
 737      (g' has_real_derivative
 738           (-- &64 + &48 * y1 pow 2 - &12 * y1 pow 4 + y1 pow 6 +
 739           &80 * y2 pow 2 - &8 * y1 pow 2 * y2 pow 2 - &3 * y1 pow 4 * y2 pow 2 -
 740           &12 * y2 pow 4 + &3 * y1 pow 2 * y2 pow 4 - y2 pow 6) /
 741           (y2 pow 2 *  sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
 742           ups_x (y1 pow 2) (y2 pow 2) (&4)))
 743          (atreal (&0) within s)`,
 744
 745 [(REPEAT STRIP_TAC);
 746  (ASM_MESON_TAC[compute_one_first]);
 747  (ASM_MESON_TAC[compute_one_second])]);;
 748
 749
 750 let compute_two_first = prove_by_refinement (
 751  `!y1 y2 s hz g x.
 752    &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
 753    &2 <= y2 /\ y2 <= &2 * hz /\
 754    s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1} /\
 755    g = (\t. arclength (y1 + t) (y2 - t) (&2)) /\ x IN s /\
 756    g' = (\x. ((y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) /
 757              ((y1 + x) * (y2 - x) * sqrt ((y1 + y2 + &2) * (y1 + y2 - &2) *
 758              (y2 - &2 * x + &2 - y1) * (&2 + y1 + &2 * x - y2))))
 759      ==> (g has_real_derivative g' x) (atreal x within s)`,
 760
 761 [(REPEAT STRIP_TAC);
 762  (SUBGOAL_THEN `!t. t IN s ==>
 763        &0 < ((y1 + t)+ (y2 - t) + &2) * ((y1 + t)+ (y2 - t) - &2) *
 764        ((y2 - t) + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t))`   ASSUME_TAC);
 765  (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
 766  (SUBGOAL_THEN
 767      `&0 < (y1 + t) + y2 - t + &2 /\ &0 < (y1 + t) + y2 - t - &2 /\
 768       &0 < y2 - t + &2 - (y1 + t) /\ &0 < &2 + (y1 + t) - (y2 - t)`ASSUME_TAC);
 769  (ASM_REAL_ARITH_TAC);
 770  (ASM_MESON_TAC[REAL_LT_MUL]);
 771  (ABBREV_TAC
 772   `f1 = (\t. ((y1 + t) + y2 - t + &2) * ((y1 + t) + y2 - t - &2) *
 773               (y2 - t + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t)))`);
 774  (ABBREV_TAC
 775   `f1' = &4 * (y1 + y2 + &2) * (y1 + y2 - &2) * (y2 - y1 - &2 * x)`);
 776  (ABBREV_TAC `P ={x| &0 < x}`);
 777  (ABBREV_TAC
 778   `f2 = (\t. sqrt (((y1 + t) + y2 - t + &2) * ((y1 + t) + y2 - t - &2) *
 779                    (y2 - t + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t))))`);
 780  (SUBGOAL_THEN `f2 = (\t:real. sqrt (f1 t))` ASSUME_TAC);
 781  (EXPAND_TAC "f1"  THEN EXPAND_TAC "f2" THEN MESON_TAC[]);
 782  (ABBREV_TAC `g2' = (\x. inv (&2 * sqrt x))`);
 783  (ABBREV_TAC `f2' = f1' * g2' ((f1:real->real) x)`);
 784  (SUBGOAL_THEN`(f2 has_real_derivative f2') (atreal x within s)` ASSUME_TAC);
 785  (EXPAND_TAC "f2'" THEN REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 786  (SUBGOAL_THEN `(f1 has_real_derivative f1')(atreal x within s) /\ P (f1 x)`
 787   MP_TAC);
 788   STRIP_TAC;
 789  (EXPAND_TAC "f1'" THEN EXPAND_TAC "f1");
 790  (REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 791  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM] THEN EXPAND_TAC "f1");
 792  (MP_TAC (ASSUME `(x:real) IN s`) THEN ASM_REWRITE_TAC[]);
 793
 794  (SUBGOAL_THEN `!x. P x ==> (sqrt has_real_derivative g2' x) (atreal x)`MP_TAC);
 795  (EXPAND_TAC "g2'" THEN REWRITE_TAC[BETA_THM]);
 796  (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
 797  (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
 798  (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 799
 800  (ABBREV_TAC `f3 = (\t. (&2 * &2 - (y1 + t) * (y1 + t) - (y2 - t) * (y2 - t)) /
 801     sqrt (((y1 + t) + (y2 - t) + &2) * ((y1 + t) + (y2 - t) - &2) *
 802            ((y2 - t) + &2 - (y1 + t)) * (&2 + (y1 + t) - (y2 - t))))`);
 803  (ABBREV_TAC
 804    `h = (\t. (&2 * &2 - (y1 + t) * (y1 + t) - (y2 - t) * (y2 - t)))`);
 805
 806  (SUBGOAL_THEN `(f3 has_real_derivative
 807                  ((&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2') / f2 x pow 2)
 808                  (atreal x within s)` ASSUME_TAC);
 809
 810  (SUBGOAL_THEN `f3 = (\t:real. h t / f2 t)` ASSUME_TAC);
 811  (EXPAND_TAC "f2" THEN EXPAND_TAC "h" THEN EXPAND_TAC "f3");
 812  (ASM_REWRITE_TAC[]);
 813
 814  (SUBGOAL_THEN
 815  `(h has_real_derivative &2 * (y2 - y1 - &2 * x)) (atreal x within s) /\
 816   (f2 has_real_derivative f2') (atreal x within s) /\ ~(f2 x = &0)` MP_TAC);
 817  (ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC);
 818  (EXPAND_TAC "h" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
 819  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 820  (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SQRT_POS_LT);
 821  (EXPAND_TAC "f1" THEN MP_TAC(ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 822
 823  (PURE_REWRITE_TAC[ASSUME `f3 = (\t:real. h t / f2 t)`]);
 824  (REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);
 825
 826  (ABBREV_TAC `F1 = (\t. atn
 827                        ((&2 * &2 - (y1 + t) * (y1 + t) - (y2 - t) * (y2 - t)) /
 828                       sqrt
 829                         (((y1 + t) + (y2 - t) + &2) *
 830                         ((y1 + t) + (y2 - t) - &2) *
 831                         ((y2 - t) + &2 - (y1 + t)) *
 832                         (&2 + (y1 + t) - (y2 - t)))))`);
 833  (SUBGOAL_THEN `F1 = (\t:real. atn (f3 t))` ASSUME_TAC);
 834  (EXPAND_TAC "f3" THEN EXPAND_TAC "F1" THEN ASM_REWRITE_TAC[]);
 835
 836  (ABBREV_TAC
 837   `f3' = ((&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2') / f2 x pow 2`);
 838  (SUBGOAL_THEN
 839  `(F1 has_real_derivative f3' * inv (&1 + f3 x pow 2)) (atreal x within s)`
 840  ASSUME_TAC);
 841  (REWRITE_TAC[ASSUME `F1 = (\t:real. atn (f3 t))`]);
 842  (SUBGOAL_THEN `(f3 has_real_derivative f3') (atreal x within s) /\
 843                  (:real) (f3 x)` MP_TAC);
 844  (ASM_REWRITE_TAC[] THEN MESON_TAC[EQ_UNIV;IN_UNIV; IN]);
 845  (ABBREV_TAC `h' = (\x. inv (&1 + x pow 2))`);
 846
 847  (SUBGOAL_THEN `!x. (:real) x ==> (atn has_real_derivative (h':real->real) x)
 848   (atreal x)` MP_TAC);
 849  (EXPAND_TAC "h'" THEN REWRITE_TAC[BETA_THM]);
 850  (REWRITE_TAC[EQ_UNIV; HAS_REAL_DERIVATIVE_ATN]);
 851
 852  (SUBGOAL_THEN `inv (&1 + f3 (x:real) pow 2) = h' (f3 x)` ASSUME_TAC);
 853  (EXPAND_TAC "h'" THEN REWRITE_TAC[]);
 854  (REWRITE_TAC[ASSUME `inv (&1 + f3 (x:real) pow 2) = h'( f3 x)`]);
 855
 856  (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
 857
 858 (* --------------------------------------------------------------------------*)
 859 (*                  REDUCE derivative of F1                                  *)
 860 (* --------------------------------------------------------------------------*)
 861
 862  (SUBGOAL_THEN `f1 x = (y1 + y2 + &2) *
 863                         (y1 + y2 - &2) *
 864                         (y2 - &2 * x + &2 - y1) *
 865                         (&2 + y1 + &2 * x - y2)`ASSUME_TAC);
 866  (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
 867  (SUBGOAL_THEN `inv (&1 + f3 x pow 2) =
 868                 (f1 x) / (&4 * ((y1 + x) * (y2 - x)) pow 2)` ASSUME_TAC);
 869  (EXPAND_TAC "f3" THEN REWRITE_TAC[REAL_POW_DIV]);
 870
 871  (SUBGOAL_THEN `&0 <= ((y1 + x) + y2 - x + &2) * ((y1 + x) + y2 - x - &2) *
 872   (y2 - x + &2 - (y1 + x)) * (&2 + (y1 + x) - (y2 - x))` ASSUME_TAC);
 873  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 874  (MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 875
 876  (SUBGOAL_THEN `sqrt (((y1 + x) + y2 - x + &2) * ((y1 + x) + y2 - x - &2) *
 877    (y2 - x + &2 - (y1 + x)) * (&2 + (y1 + x) - (y2 - x))) pow 2 = f1 x`
 878  ASSUME_TAC);
 879  (EXPAND_TAC "f1" THEN ASM_SIMP_TAC [SQRT_POW_2]);
 880
 881  (PURE_ONCE_ASM_REWRITE_TAC[]);
 882  (ONCE_ASM_REWRITE_TAC[GSYM REAL_INV_DIV]);
 883  (AP_TERM_TAC);
 884  (ONCE_ASM_REWRITE_TAC[REAL_INV_DIV] THEN PURE_ONCE_ASM_REWRITE_TAC[]);
 885  (MATCH_MP_TAC (REAL_ARITH `&1 = x - y ==> &1 + y = x `));
 886  (REWRITE_TAC [REAL_ARITH `x / y - z / y = (x - z) / y`]);
 887  (REWRITE_TAC[REAL_ARITH `&4 * ((y1 + x) * (y2 - x)) pow 2 -
 888   (&2 * &2 - (y1 + x) * (y1 + x) - (y2 - x) * (y2 - x)) pow 2 =
 889   (y1 + y2 + &2) * (y1 + y2 - &2) * (y2 - &2 * x + &2 - y1) *
 890   (&2 + y1 + &2 * x - y2)`]);
 891  (MATCH_MP_TAC (GSYM REAL_DIV_REFL));
 892  (REWRITE_TAC[GSYM (ASSUME `f1 x = (y1 + y2 + &2) * (y1 + y2 - &2) *
 893       (y2 - &2 * x + &2 - y1) * (&2 + y1 + &2 * x - y2)`)]);
 894  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(&0 = a)`));
 895  (MP_TAC (ASSUME `x:real IN s`) THEN EXPAND_TAC "f1" THEN ASM_REWRITE_TAC[]);
 896
 897 (* ========================================================================== *)
 898
 899  (SUBGOAL_THEN `(&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2' =
 900   &4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) *
 901   ((y2 + y1) pow 2 - &4) / f2 x` ASSUME_TAC);
 902  (ABBREV_TAC `X = (&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2'`);
 903  (REWRITE_TAC[REAL_ARITH `x * y / z = (x * y) / z`]);
 904  (ABBREV_TAC `Y = &4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) *
 905                    ((y2 + y1) pow 2 - &4)`);
 906  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 907
 908  (SUBGOAL_THEN `Y / f2 (x:real) = X <=> Y = X * f2 x` ASSUME_TAC);
 909  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 910  (REPLICATE_TAC 2 (ONCE_ASM_REWRITE_TAC[]) THEN MATCH_MP_TAC SQRT_POS_LT);
 911  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 912
 913  (ONCE_ASM_REWRITE_TAC[]);
 914  (EXPAND_TAC "X" THEN EXPAND_TAC "Y");
 915  (EXPAND_TAC "f2'" THEN EXPAND_TAC "h" THEN EXPAND_TAC "g2'");
 916  (ONCE_REWRITE_TAC[REAL_ARITH `(a - b) * c = a * c - b * c`]);
 917
 918  (SUBGOAL_THEN `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2` ASSUME_TAC);
 919  (REWRITE_TAC[ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 920  (ONCE_REWRITE_TAC[REAL_ARITH `a * sqrt b = (a * (&2 * sqrt b)) / &2`]);
 921  (AP_THM_TAC THEN AP_TERM_TAC);
 922  (MATCH_MP_TAC REAL_MUL_LINV);
 923  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 924  (MATCH_MP_TAC REAL_LT_MUL);
 925  (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
 926  (MATCH_MP_TAC SQRT_POS_LT);
 927  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 928
 929  (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b) * c * d`]);
 930  (PURE_REWRITE_TAC[ASSUME `inv (&2 * sqrt (f1 x)) * f2 (x:real) = &1 / &2`]);
 931  (REWRITE_TAC[REAL_ARITH `(a * f2 x) * f2 x = a * (f2 (x:real) pow 2)`]);
 932
 933  (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 934  (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 935  (MATCH_MP_TAC SQRT_POW_2);
 936  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 937  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 938
 939  (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);
 940  (ASM_REWRITE_TAC[] THEN EXPAND_TAC "f1'" THEN REAL_ARITH_TAC);
 941
 942  (SUBGOAL_THEN
 943   `f3' * inv (&1 + f3 x pow 2) =
 944    (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4) / ((y1 + x) * (y2 - x) * f2 x)` ASSUME_TAC);
 945  (EXPAND_TAC "f3'");
 946  (REWRITE_TAC[ASSUME `inv (&1 + f3 x pow 2) =
 947                        f1 x / (&4 * ((y1 + x) * (y2 - x)) pow 2)`]);
 948  (REWRITE_TAC[ASSUME
 949  `(&2 * (y2 - y1 - &2 * x)) * f2 x - h x * f2' = &4 * (y1 + x) * (y2 - x) *
 950   (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4) / f2 x`]);
 951
 952  (SUBGOAL_THEN `f2 (x:real) pow 2 = f1 x` ASSUME_TAC);
 953  (REWRITE_TAC [ASSUME `f2 = (\t:real. sqrt (f1 t))`]);
 954  (MATCH_MP_TAC SQRT_POW_2);
 955  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
 956  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 957  (REWRITE_TAC[ASSUME `f2 (x:real) pow 2 = f1 x`]);
 958
 959  (ONCE_REWRITE_TAC [REAL_ARITH `a / b * c / d = (a / d) * c / b`]);
 960  (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 /\ x = y ==> x * a = y`));
 961   STRIP_TAC;
 962
 963  (MATCH_MP_TAC REAL_DIV_REFL);
 964  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
 965  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
 966
 967  (ABBREV_TAC `X = (&4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) *
 968                    ((y2 + y1) pow 2 - &4) / f2 x)`);
 969  (ABBREV_TAC `Y = (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4) /
 970                    ((y1 + x) * (y2 - x) * f2 x)`);
 971  (ABBREV_TAC `Z = (&4 * ((y1 + x) * (y2 - x)) pow 2)`);
 972
 973  (SUBGOAL_THEN `X / Z = Y <=> X = Y * Z` ASSUME_TAC);
 974  (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
 975  (EXPAND_TAC "Z" THEN MATCH_MP_TAC REAL_LT_MUL);
 976  (REWRITE_TAC[REAL_ARITH `&0 < &4`] THEN MATCH_MP_TAC REAL_POW_LT);
 977  (MATCH_MP_TAC REAL_LT_MUL);
 978  (MP_TAC (ASSUME `x:real IN s`));
 979  (PURE_REWRITE_TAC[ASSUME
 980   `s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1}`]);
 981  (REWRITE_TAC[IN_ELIM_THM]);
 982  (REPEAT STRIP_TAC);
 983
 984  (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + &2 * x /\ &2 <= y1 ==> &0 < y1 + x`));
 985  (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
 986  (MATCH_MP_TAC (REAL_ARITH `&2 * x < &2 * y ==> &0 < y - x`));
 987  (MATCH_MP_TAC (REAL_ARITH
 988    `a < y2 + &2 - y1 /\ y2 + &2 - y1 <= b ==> a < b`));
 989  (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
 990
 991  (ONCE_ASM_REWRITE_TAC[]);
 992  (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
 993  (REWRITE_TAC [REAL_ARITH `a * b / c = (a * b) / c`]);
 994  (REWRITE_TAC[REAL_ARITH `((y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) /
 995   ((y1 + x) * (y2 - x) * f2 x) * &4 * ((y1 + x) * (y2 - x)) pow 2 =
 996   (&4 * (y1 + x) * (y2 - x) * (y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) *
 997   ((y1 + x) * (y2 - x)) / (f2 x * (y1 + x) * (y2 - x))`]);
 998  (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
 999  (MATCH_MP_TAC REDUCE_WITH_DIV_Euler_lemma);
1000  CONJ_TAC;
1001  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1002  (MATCH_MP_TAC REAL_LT_MUL THEN MP_TAC (ASSUME `x:real IN s`));
1003  (PURE_REWRITE_TAC[ASSUME
1004   `s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1}`]);
1005  (REWRITE_TAC[IN_ELIM_THM]);
1006  (REPEAT STRIP_TAC);
1007
1008  (MATCH_MP_TAC (REAL_ARITH `&0 <= y1 + &2 * x /\ &2 <= y1 ==> &0 < y1 + x`));
1009  (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
1010  (MATCH_MP_TAC (REAL_ARITH `&2 * x < &2 * y ==> &0 < y - x`));
1011  (MATCH_MP_TAC (REAL_ARITH
1012    `a < y2 + &2 - y1 /\ y2 + &2 - y1 <= b ==> a < b`));
1013  (ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC);
1014
1015  (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1016  (ONCE_ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[]);
1017  (MATCH_MP_TAC SQRT_POS_LT);
1018  (EXPAND_TAC "f1" THEN MP_TAC (ASSUME `x:real IN s`) THEN ASM_REWRITE_TAC[]);
1019
1020 (* ========================================================================== *)
1021
1022  (SUBGOAL_THEN
1023   `(F1 has_real_derivative ((y2 - y1 - &2 * x) *
1024       ((y2 + y1) pow 2 - &4)) / ((y1 + x) * (y2 - x) * f2 x))
1025       (atreal x within s)` ASSUME_TAC);
1026  (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);
1027  (ASM_MESON_TAC[]);
1028
1029  (SUBGOAL_THEN
1030   `(F1 has_real_derivative g' x) (atreal x within s)` ASSUME_TAC);
1031  (REWRITE_TAC[ASSUME
1032   `g' = (\x. ((y2 - y1 - &2 * x) * ((y2 + y1) pow 2 - &4)) /
1033            ((y1 + x) * (y2 - x) *
1034             sqrt
1035             ((y1 + y2 + &2) *
1036              (y1 + y2 - &2) *
1037              (y2 - &2 * x + &2 - y1) *
1038              (&2 + y1 + &2 * x - y2))))`]);
1039  (FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]);
1040
1041  (ABBREV_TAC `F2 = (\x:real. pi / &2 + F1 x)`);
1042  (ABBREV_TAC `pi_2 = (\x:real. pi / &2 )`);
1043
1044  (SUBGOAL_THEN `(F2 has_real_derivative g' x)(atreal x within s)` MP_TAC);
1045  (SUBGOAL_THEN `F2 = (\x:real. pi_2 x + F1 x)` ASSUME_TAC);
1046  (EXPAND_TAC "F2" THEN EXPAND_TAC "F1" THEN EXPAND_TAC "pi_2");
1047  (REWRITE_TAC[]);
1048  (REWRITE_TAC[ASSUME `F2 = (\x:real. pi_2 x + F1 x)`]);
1049  (SUBGOAL_THEN `((\x. pi_2 x + F1 x) has_real_derivative &0 + g' x)
1050  (atreal x within s)` ASSUME_TAC);
1051
1052  (SUBGOAL_THEN `(pi_2 has_real_derivative (&0)) (atreal x within s)` MP_TAC);
1053  (EXPAND_TAC "pi_2" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
1054
1055  (MP_TAC (ASSUME `(F1 has_real_derivative g' x) (atreal x within s)`));
1056  (REWRITE_TAC[MESON[] `(a ==> b ==> c) <=> (b /\ a ==> c)`]);
1057  (MESON_TAC[HAS_REAL_DERIVATIVE_ADD]);
1058  (ASM_MESON_TAC[REAL_ARITH `&0 + a = a`]);
1059
1060  (SUBGOAL_THEN `(!x':real. (x':real) IN s /\ abs (x' - x) < &1 ==>
1061                             (F2:real -> real) x' = g x')` MP_TAC);
1062  (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
1063  (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN EXPAND_TAC "F2" THEN EXPAND_TAC "F1");
1064  (MATCH_MP_TAC ATN_UPS_X_BREAKDOWN1);
1065  (MP_TAC (ASSUME `x':real IN s`) THEN ASM_REWRITE_TAC[]);
1066
1067  (MP_TAC (ASSUME `x:real IN s`));
1068  (MP_TAC (REAL_ARITH `&0 < &1`));
1069  (MESON_TAC[HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN])]);;
1070
1071 (* ========================================================================== *)
1072 (*        SECOND LEMMA                                                        *)
1073 (* ========================================================================== *)
1074
1075 let compute_two_second = prove_by_refinement (
1076  `!y1 y2 s hz g x.
1077      &1 <= hz /\ hz < &2 /\
1078      &2 <= y1 /\ y1 <= &2 * hz /\
1079      &2 <= y2 /\ y2 <= &2 * hz /\
1080      s = {t | y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1} /\
1081      g =
1082      (\t. ((y2 - y1 - &2 * t) * ((y2 + y1) pow 2 - &4)) /
1083           ((y1 + t) *
1084            (y2 - t) *
1085            sqrt
1086            ((y1 + y2 + &2) *
1087             (y1 + y2 - &2) *
1088             (y2 - &2 * t + &2 - y1) *
1089             (&2 + y1 + &2 * t - y2))))
1090      ==> (g has_real_derivative
1091           (sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
1092            (-- &4 * y1 pow 2 +
1093             y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
1094             &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
1095             y2 pow 4)) /
1096           (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2))
1097          (atreal (&0) within s)`,
1098
1099 [(REWRITE_TAC[REAL_ARITH `a * b * sqrt c = (a * b) * sqrt c`]);
1100  (REPEAT STRIP_TAC);
1101
1102   (SUBGOAL_THEN `&0 IN s` ASSUME_TAC);
1103   (PURE_ASM_REWRITE_TAC[IN_ELIM_THM; REAL_MUL_RZERO]);
1104    ASM_REAL_ARITH_TAC;
1105
1106 (* ========================================================================== *)
1107
1108   (SUBGOAL_THEN  `!t. t IN s ==>  &0 < (y1 + y2 + &2) * (y1 + y2 - &2) *
1109                           (y2 - &2 * t + &2 - y1) * (&2 + y1 + &2 * t - y2)`
1110      ASSUME_TAC);
1111
1112   (GEN_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC);
1113
1114     (SUBGOAL_THEN `&0 < y1 + y2 - &2 /\ &0 < y1 + y2 + &2 /\
1115        &0 < y2 - &2 * t + &2 - y1 /\ &0 < &2 + y1 + &2 * t - y2` ASSUME_TAC);
1116      ASM_REAL_ARITH_TAC;
1117     (ASM_MESON_TAC[REAL_LT_MUL]);
1118
1119 (* -------------------------------------------------------------------------- *)
1120
1121 (ABBREV_TAC `f1 = (\t. (y2 - y1 - &2 * t) * ((y2 + y1) pow 2 - &4))`);
1122 (ABBREV_TAC `f2 = (\t. (y1 + y2 + &2) * (y1 + y2 - &2) *
1123              (y2 - &2 * t + &2 - y1) * (&2 + y1 + &2 * t - y2))`);
1124 (ABBREV_TAC `f3 = (\t:real. sqrt (f2 t))`);
1125 (ABBREV_TAC `f4 = (\t:real. (y1 + t) * (y2 - t))`);
1126 (ABBREV_TAC `f5 = (\t:real. f4 t * f3 t )`);
1127
1128 (SUBGOAL_THEN `&0 < f2 (&0)` ASSUME_TAC);
1129 (EXPAND_TAC "f2" THEN MP_TAC (ASSUME `((&0):real) IN s`));
1130 (ASM_REWRITE_TAC[]);
1131
1132 (SUBGOAL_THEN `(f1 has_real_derivative -- &2 * ((y2 + y1) pow 2 - &4))
1133                  (atreal (&0) within s)` ASSUME_TAC);
1134 (EXPAND_TAC "f1" THEN REAL_DIFF_TAC);
1135  REAL_ARITH_TAC;
1136
1137 (ABBREV_TAC `f2' = &4 * (y2 - y1) * ((y2 + y1) pow 2 - &4)`);
1138 (ABBREV_TAC `P ={x| &0 < x}`);
1139 (ABBREV_TAC `g3' = (\x. inv (&2 * sqrt x))`);
1140 (ABBREV_TAC `f3' = f2' * g3' ((f2:real->real) (&0))`);
1141
1142   (SUBGOAL_THEN
1143     `(f3 has_real_derivative f3') (atreal (&0) within s)` ASSUME_TAC);
1144   (EXPAND_TAC "f3'" THEN EXPAND_TAC "f3");
1145
1146   (SUBGOAL_THEN
1147      `(f2 has_real_derivative f2') (atreal (&0) within s) /\ P (f2 (&0))`
1148    MP_TAC);
1149    STRIP_TAC;
1150
1151   (EXPAND_TAC "f2" THEN EXPAND_TAC "f2'");
1152   (REAL_DIFF_TAC THEN REWRITE_TAC[POW_2] THEN REAL_ARITH_TAC);
1153   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
1154   (ASM_REWRITE_TAC[]);
1155
1156   (SUBGOAL_THEN
1157     `!x. P x ==> (sqrt has_real_derivative (g3':real->real) x) (atreal x)`
1158      MP_TAC);
1159   (EXPAND_TAC "g3'" THEN REWRITE_TAC[BETA_THM]);
1160   (EXPAND_TAC "P" THEN REWRITE_TAC[IN_ELIM_THM]);
1161   (REWRITE_TAC[HAS_REAL_DERIVATIVE_SQRT]);
1162
1163 (REWRITE_TAC[HAS_REAL_DERIVATIVE_CHAIN2]);
1164
1165 (* ========================================================================== *)
1166
1167 (SUBGOAL_THEN `(f5 has_real_derivative f4 (&0) * f3' + (y2 - y1) * f3 (&0))
1168   (atreal (&0) within s)` ASSUME_TAC);
1169 (EXPAND_TAC "f5");
1170
1171 (SUBGOAL_THEN
1172   `(f4 has_real_derivative y2 - y1) (atreal (&0) within s) /\
1173    (f3 has_real_derivative f3') (atreal (&0) within s)` MP_TAC);
1174 (ASM_REWRITE_TAC[]);
1175 (EXPAND_TAC "f4" THEN REAL_DIFF_TAC THEN REAL_ARITH_TAC);
1176
1177 (REWRITE_TAC[HAS_REAL_DERIVATIVE_MUL_WITHIN]);
1178
1179 (* ========================================================================= *)
1180 (*          Derivative of f1 / f5                                            *)
1181 (* ========================================================================= *)
1182
1183 (SUBGOAL_THEN `g = (\t:real. f1 t / f5 t)` ASSUME_TAC);
1184 (ASM_REWRITE_TAC[]);
1185 (EXPAND_TAC "f5" THEN EXPAND_TAC "f1");
1186 (EXPAND_TAC "f4" THEN EXPAND_TAC "f3" THEN EXPAND_TAC "f2");
1187 (REWRITE_TAC[]);
1188
1189 (REWRITE_TAC[ASSUME `g = (\t:real. f1 t / f5 t)`] THEN DEL_TAC);
1190
1191 (SUBGOAL_THEN `((\t. f1 t / f5 t) has_real_derivative
1192   ((-- &2 * ((y2 + y1) pow 2 - &4)) * f5 (&0) - f1 (&0) *
1193   (f4 (&0) * f3' + (y2 - y1) * f3 (&0))) /
1194   f5 (&0) pow 2) (atreal (&0) within s)` ASSUME_TAC);
1195
1196 (SUBGOAL_THEN
1197   `(f1 has_real_derivative -- &2 * ((y2 + y1) pow 2 - &4))
1198    (atreal (&0) within s) /\
1199    (f5 has_real_derivative f4 (&0) * f3' + (y2 - y1) * f3 (&0))
1200     (atreal (&0) within s) /\ ~(f5 (&0) = &0)` MP_TAC);
1201
1202 (ASM_REWRITE_TAC[]);
1203 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`));
1204 (EXPAND_TAC "f5" THEN MATCH_MP_TAC REAL_LT_MUL);
1205  STRIP_TAC;
1206
1207 (EXPAND_TAC "f4" THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REAL_ARITH_TAC);
1208 (EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
1209
1210 (REWRITE_TAC[HAS_REAL_DERIVATIVE_DIV_WITHIN]);
1211
1212 (* ========================================================================= *)
1213
1214 (SUBGOAL_THEN
1215 `((-- &2 * ((y2 + y1) pow 2 - &4)) * f5 (&0) -
1216   f1 (&0) * (f4 (&0) * f3' + (y2 - y1) * f3 (&0))) /
1217  f5 (&0) pow 2 =
1218  (sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
1219   (-- &4 * y1 pow 2 +
1220    y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
1221    &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
1222    y2 pow 4)) /
1223  (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2)` ASSUME_TAC);
1224
1225 (REWRITE_WITH `ups_x (y1 pow 2) (y2 pow 2) (&4) = f2 (&0)`);
1226 (REWRITE_TAC[ups_x] THEN EXPAND_TAC "f2");
1227  REAL_ARITH_TAC;
1228
1229 (EXPAND_TAC "f5");
1230
1231 (SUBGOAL_THEN `f4 (&0) = y1 * y2` ASSUME_TAC);
1232 (EXPAND_TAC "f4" THEN REAL_ARITH_TAC);
1233 (ASM_REWRITE_TAC[]);
1234
1235
1236 (REWRITE_TAC[REAL_ARITH `a - b * (c + d) = a - b * c - b * d`]);
1237 (REWRITE_TAC[REAL_ARITH `(-- &2 * m) * n * x = ((-- &2 * m) * n) * x`]);
1238 (REWRITE_TAC[REAL_ARITH `f1 (&0) * (y2 - y1) * f3 (&0) =
1239                           (f1 (&0) * (y2 - y1)) * f3 (&0)`]);
1240 (REWRITE_TAC[REAL_ARITH `a * f3 (&0) - b - c * f3 (&0) = (a - c) * f3 (&0) - b`]);
1241 (SUBGOAL_THEN
1242   `((-- &2 * ((y2 + y1) pow 2 - &4)) * y1) * y2 - f1 (&0) * (y2 - y1) =
1243     -- (y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)` ASSUME_TAC);
1244 (EXPAND_TAC "f1" THEN REAL_ARITH_TAC);
1245
1246 (ASM_REWRITE_TAC[]);
1247 (EXPAND_TAC "f3'" THEN EXPAND_TAC "g3'");
1248
1249 (SUBGOAL_THEN `sqrt (f2 (&0)) = f3 (&0)` ASSUME_TAC);
1250 (EXPAND_TAC "f3" THEN REWRITE_TAC[]);
1251 (REWRITE_TAC[ASSUME `sqrt (f2 (&0)) = f3 (&0)`]);
1252
1253 (SUBGOAL_THEN
1254 `(--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * f3 (&0) -
1255   f1 (&0) * (y1 * y2) * f2' * inv (&2 * f3 (&0)) =
1256  ((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * f3 (&0) pow 2 -
1257   f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) /
1258  f3 (&0)` ASSUME_TAC);
1259
1260 (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a - b) / c = a / c - b / c`]);
1261 (MATCH_MP_TAC (REAL_ARITH `a = b /\ c = d ==> a - c = b - d`));
1262  STRIP_TAC;
1263
1264 (REWRITE_TAC[REAL_POW_2; REAL_ARITH `(a * b * c) / d = (a * b) * c / d`]);
1265 (MATCH_MP_TAC (MESON[REAL_MUL_RID] `a = &1 ==> b = b * a`));
1266 (MATCH_MP_TAC REAL_DIV_REFL);
1267 (EXPAND_TAC "f3");
1268 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1269 (MATCH_MP_TAC SQRT_POS_LT);
1270 (ASM_REWRITE_TAC[]);
1271
1272 (EXPAND_TAC "f2'");
1273 (REWRITE_TAC[REAL_ARITH
1274  `f1 (&0) * (y1 * y2) * (&4 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) *
1275   inv (&2 * f3 (&0)) =
1276   f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4) * &2 *
1277   inv (&2 * f3 (&0))`]) ;
1278 (ABBREV_TAC
1279   `X =  f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4) * &2 *
1280   inv (&2 * f3 (&0))`);
1281 (ABBREV_TAC
1282  `Y = f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)`);
1283 (ABBREV_TAC `Z = (f3:real->real) (&0)`);
1284
1285 (SUBGOAL_THEN `X = Y / Z <=> X * Z = Y` ASSUME_TAC);
1286 (MATCH_MP_TAC REAL_EQ_RDIV_EQ THEN EXPAND_TAC "Z" THEN EXPAND_TAC "f3");
1287 (MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
1288 (ASM_REWRITE_TAC[]);
1289
1290 (EXPAND_TAC "X" THEN EXPAND_TAC "Y" THEN EXPAND_TAC "Z");
1291 (REWRITE_TAC[REAL_ARITH `(x1 * x2 * x3 * x4 * x5 * &2 * b) * c  =
1292                            (x1 * x2 * x3 * x4 * x5) * (&2 * c) * b`]);
1293 (MATCH_MP_TAC( MESON[REAL_MUL_RID] `a = &1 ==> b * a = b`));
1294 (MATCH_MP_TAC REAL_MUL_RINV);
1295 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a = &0)`));
1296 (MATCH_MP_TAC REAL_LT_MUL);
1297 (REWRITE_TAC[REAL_ARITH `&0 < &2`]);
1298 (EXPAND_TAC "f3" THEN MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
1299
1300 (ASM_REWRITE_TAC[]);
1301 (REWRITE_TAC[REAL_POW_MUL]);
1302 (EXPAND_TAC "f3");
1303 (REWRITE_WITH `sqrt (f2 (&0)) pow 2 = f2 (&0)`);
1304 (MATCH_MP_TAC SQRT_POW_2);
1305 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);
1306
1307 (REWRITE_TAC[REAL_ARITH `a / b / c = a / c / b`]);
1308 (ABBREV_TAC `A = ((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) *
1309    f2 (&0) - f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) /
1310   ((y1 pow 2 * y2 pow 2) * f2 (&0))`);
1311 (ABBREV_TAC `B = (sqrt (f2 (&0)) * (-- &4 * y1 pow 2 +
1312    y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
1313    &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
1314    y2 pow 4)) /
1315    (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2)`);
1316
1317 (SUBGOAL_THEN `A/ sqrt (f2 (&0)) = B <=> A = B * sqrt (f2 (&0))` ASSUME_TAC);
1318 (MATCH_MP_TAC REAL_EQ_LDIV_EQ);
1319 (MATCH_MP_TAC SQRT_POS_LT THEN ASM_REWRITE_TAC[]);
1320 (ONCE_ASM_REWRITE_TAC[]);
1321 (EXPAND_TAC "A" THEN EXPAND_TAC "B");
1322 (REWRITE_TAC[REAL_ARITH `(a * b) / c * d = (b * a * d) / c`]);
1323 (ONCE_REWRITE_TAC[GSYM REAL_POW_2]);
1324 (REWRITE_WITH `sqrt (f2 (&0)) pow 2 = f2 (&0)`);
1325 (MATCH_MP_TAC SQRT_POW_2);
1326 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`) THEN ASM_REWRITE_TAC[]);
1327
1328
1329 (ABBREV_TAC `C = ((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) *
1330    f2 (&0) - f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) /
1331   ((y1 pow 2 * y2 pow 2) * f2 (&0))`);
1332 (ABBREV_TAC `D = ((-- &4 * y1 pow 2 +
1333    y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
1334    &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
1335    y2 pow 4) *
1336   f2 (&0))`);
1337 (ABBREV_TAC `E = (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2)`);
1338
1339
1340 (SUBGOAL_THEN `C = D / E <=> C * E = D` ASSUME_TAC);
1341 (MATCH_MP_TAC REAL_EQ_RDIV_EQ);
1342 (EXPAND_TAC "E");
1343 (MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
1344 (MATCH_MP_TAC REAL_POW_LT);
1345 (ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
1346 (MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
1347 (MATCH_MP_TAC REAL_POW_LT);
1348 (ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
1349 (MATCH_MP_TAC REAL_POW_LT);
1350 (MATCH_MP_TAC (REAL_ARITH `b < a ==> &0 < a - b`));
1351 (SUBGOAL_THEN ` -- &2 < y1 - y2 /\ y1 - y2 < &2` ASSUME_TAC);
1352 (ASM_REAL_ARITH_TAC);
1353 (REWRITE_TAC[REAL_ARITH `&4 = (&2) pow 2`]);
1354 (REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]);
1355 (ASM_REAL_ARITH_TAC);
1356
1357 (ONCE_ASM_REWRITE_TAC[]);
1358 (EXPAND_TAC "C" THEN EXPAND_TAC "D" THEN EXPAND_TAC "E");
1359 (REWRITE_TAC[REAL_ARITH `a / b * c = (a * c) / b`]);
1360
1361 (REWRITE_WITH `(((--(y1 pow 2 + y2 pow 2) * ((y2 + y1) pow 2 - &4)) * f2 (&0) -
1362    f1 (&0) * (y1 * y2) * &2 * (y2 - y1) * ((y2 + y1) pow 2 - &4)) *
1363   y1 pow 2 *
1364   y2 pow 2 *
1365   (&4 - (y1 - y2) pow 2) pow 2) = ((-- &4 * y1 pow 2 +
1366   y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
1367   &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
1368   y2 pow 4) *
1369  f2 (&0)) * ((y1 pow 2 * y2 pow 2) * f2 (&0))`);
1370
1371 (EXPAND_TAC "f2" THEN EXPAND_TAC "f1");
1372 (REAL_ARITH_TAC);
1373
1374 (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);
1375 (MATCH_MP_TAC (MESON [REAL_MUL_RID] `a = &1 ==> b * a = b`));
1376 (MATCH_MP_TAC REAL_DIV_REFL);
1377 (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~ (a =  &0)`));
1378
1379
1380 (MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
1381 (MATCH_MP_TAC REAL_LT_MUL THEN STRIP_TAC);
1382 (MATCH_MP_TAC REAL_POW_LT);
1383 (ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
1384 (MATCH_MP_TAC REAL_POW_LT);
1385 (ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 < a`]);
1386 (ASM_REWRITE_TAC[]);
1387
1388 (ASM_MESON_TAC[])]);;
1389
1390 (* ========================================================================= *)
1391
1392 let COMPUTE_DERIVATIVE_TWO = prove_by_refinement (
1393  `!y1 y2 s hz g x f.
1394      &1 <= hz /\ hz < &2 /\ &2 <= y1 /\ y1 <= &2 * hz /\
1395      &2 <= y2 /\ y2 <= &2 * hz /\
1396    s = {t |  y2 - &2 - y1 < &2 * t /\ &2 * t < y2 + &2 - y1} /\
1397    g = (\t. arclength (y1 + t) (y2 - t) (&2)) /\ x IN s /\
1398    g' =
1399      (\t. ((y2 - y1 - &2 * t) * ((y2 + y1) pow 2 - &4)) /
1400           ((y1 + t) *
1401            (y2 - t) *
1402            sqrt
1403            ((y1 + y2 + &2) *
1404             (y1 + y2 - &2) *
1405             (y2 - &2 * t + &2 - y1) *
1406             (&2 + y1 + &2 * t - y2))))
1407 ==>  (!x. x IN s ==> (g has_real_derivative g' x) (atreal x within s)) /\
1408      (g' has_real_derivative
1409           (sqrt (ups_x (y1 pow 2) (y2 pow 2) (&4)) *
1410            (-- &4 * y1 pow 2 +
1411             y1 pow 4 - &4 * y1 pow 3 * y2 - &4 * y2 pow 2 +
1412             &6 * y1 pow 2 * y2 pow 2 - &4 * y1 * y2 pow 3 +
1413             y2 pow 4)) /
1414           (y1 pow 2 * y2 pow 2 * (&4 - (y1 - y2) pow 2) pow 2))
1415          (atreal (&0) within s)`,
1416
1417 [(REPEAT STRIP_TAC);
1418  (ASM_MESON_TAC[compute_two_first]);
1419  (ASM_MESON_TAC[compute_two_second])]);;
1420
1421
1422 end;;