text_formalization/nonlinear/calc_derivative.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Counting Spheres                                                             *)
   4 (* Chapter: packing                                                           *)
   5 (* Author: Thomas C. Hales                                  *)
   6 (* Date: 2011-06-22                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* Example:
  10     to put all terms over a common denominator :
  11
  12    rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;
  13
  14    To prove a rational identity, modulo accumulated side conditions:
  15
  16    rational_identity `&1 / (x + y) - &1 / (x - y) = -- &2 * y / (x pow 2 - y pow 2)`;;
  17 *)
  18
  19
  20 (*
  21
  22   written to automate the calculation of derivatives, with accumulating side conditions.
  23   It implements --, -, +, *, /, inv, pow, sqrt, sin, cos, atn, asn, acs, chain rule.
  24
  25   To recover results without "within" use:
  26
  27   "WITHINREAL_UNIV", |- !a. atreal x within (:real) = atreal x)
  28
  29    derived_form p f f' x s   means:
  30    Under the assumption p, the derivative of the function f evaluated at x,
  31    on the interval s
  32    is equal to the real number f'.
  33
  34   Apply REWRITE_RULE[derived_form] to express the result back in terms of
  35   has_real_derivative.
  36
  37   (* A rational inequality implies a polynomial ineq with
  38   denominators cleared.  Allowed ops <,>, <=,>=,=,~=,*)
  39
  40   val rational_ineq_rule  : thm -> thm
  41
  42 *)
  43
  44
  45
  46 (* Example:
  47
  48 To calculate the derivative of tm with respect to q, evaluated at x, on the interval s:
  49
  50   let th1 =
  51     let x = `x:real` in
  52     let s = `{t | t > &0}` in
  53     let tm = `(\q:real. (q  - sin(q pow 3) + q pow 7 + y)/(q pow 2  + q pow 4 *(&33 + &43 * q)) +  (q pow 3) *  ((q pow 2) / (-- (q pow 3))))` in
  54       differentiate tm x s;;
  55
  56 *)
  57
  58
  59 module Calc_derivative
  60
  61 (*: sig
  62
  63   val ratform : thm
  64   val rationalize_ratform: term -> thm
  65
  66   val rationalize: term -> thm
  67   val rational_identity:term -> thm
  68   val rational_ineq_rule  : thm -> thm
  69
  70   val invert_den_lt :thm
  71   val invert_den_le: thm
  72
  73   val derived_form:thm
  74   val differentiate:term -> term -> term -> thm
  75
  76  end *) = struct
  77
  78
  79 (* ========================================================================== *)
  80 (* RATIONALIZE CONVERSION                                              *)
  81
  82
  83 (*
  84 rationalize puts everything over a common denominator, accumulating
  85 assumptions as it goes.
  86 *)
  87
  88
  89 let ratform  = new_definition `ratform p r a b = (p ==> ~(b = &0) /\ (r = a/b))`;;
  90
  91 let ratform_tac =   REWRITE_TAC [ratform] THEN
  92     REPEAT STRIP_TAC THENL
  93     [ASM_MESON_TAC[REAL_ENTIRE] ;
  94     REPEAT (FIRST_X_ASSUM (fun t -> MP_TAC t THEN ANTS_TAC THEN
  95                              ASM_REWRITE_TAC[])) THEN
  96     REPEAT STRIP_TAC THEN
  97     ASM_REWRITE_TAC[] THEN
  98     REPEAT (POP_ASSUM MP_TAC) THEN
  99     CONV_TAC REAL_FIELD];;
 100
 101 let REAL_POW_NEQ_0 = prove_by_refinement(
 102   `!x n. ~(x pow n = &0) <=> ~(x = &0) \/ (n = 0)`,
 103   (* {{{ proof *)
 104   [
 105   MESON_TAC[REAL_POW_EQ_0];
 106   ]);;
 107   (* }}} *)
 108
 109 let ratform_pow = prove_by_refinement(
 110   `ratform p1 r1 a1 b1 ==> ratform p1 (r1 pow n) (a1 pow n) (b1 pow n)`,
 111   (* {{{ proof *)
 112   [
 113     REWRITE_TAC[GSYM REAL_POW_DIV;ratform];
 114     MESON_TAC[REAL_POW_NEQ_0;];
 115   ]);;
 116   (* }}} *)
 117
 118 let ratform_add = prove_by_refinement(
 119   `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2) (r1 + r2) (a1 * b2 + b1 * a2) (b1 * b2)`,
 120   (* {{{ proof *)
 121   [
 122   ratform_tac;
 123   ]);;
 124   (* }}} *)
 125
 126 let ratform_sub = prove_by_refinement(
 127   `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2) (r1 - r2) (a1 * b2 - b1 * a2) (b1 * b2)`,
 128   (* {{{ proof *)
 129   [
 130     ratform_tac;
 131   ]);;
 132   (* }}} *)
 133
 134 let ratform_neg = prove_by_refinement(
 135   `ratform p1 r1 a1 b1 ==> ratform p1 (-- r1 ) (-- a1 ) (b1)`,
 136   (* {{{ proof *)
 137   [
 138     ratform_tac;
 139   ]);;
 140   (* }}} *)
 141
 142 let ratform_mul = prove_by_refinement(
 143   `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2) (r1 * r2) (a1 * a2) (b1 * b2)`,
 144   (* {{{ proof *)
 145   [
 146     ratform_tac;
 147   ]);;
 148   (* }}} *)
 149
 150 let ratform_div = prove_by_refinement(
 151   `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2 /\ ~(a2 = &0)) (r1 / r2) (a1 * b2) (b1 * a2)`,
 152   (* {{{ proof *)
 153   [
 154   ratform_tac;
 155   ]);;
 156   (* }}} *)
 157
 158 let ratform_inv = prove_by_refinement(
 159   `ratform p1 r1 a1 b1 ==> ratform (p1 /\ ~(a1= &0)) (inv r1) b1 a1`,
 160   (* {{{ proof *)
 161   [
 162   REWRITE_TAC [ratform;];
 163     REPEAT STRIP_TAC;
 164     ASM_MESON_TAC[REAL_ENTIRE];
 165     REPEAT (FIRST_X_ASSUM (fun t -> MP_TAC t THEN ANTS_TAC THEN ASM_REWRITE_TAC[]));
 166     REPEAT STRIP_TAC;
 167     ASM_REWRITE_TAC[REAL_INV_DIV];
 168   ]);;
 169   (* }}} *)
 170
 171 let trivial_ratform = prove_by_refinement(
 172   `!t. ratform T t t (&1)`,
 173   (* {{{ proof *)
 174   [
 175   REWRITE_TAC[ratform];
 176     REAL_ARITH_TAC;
 177   ]);;
 178   (* }}} *)
 179
 180 let pre_rationalize =
 181   let   binop_assoc = [(`(+)`,ratform_add);
 182                        (`( * )`,ratform_mul);(`( - )`,ratform_sub);
 183                        (`( / )`,ratform_div)] in
 184   let unary_assoc = [(` ( -- )`,ratform_neg);(`inv`,ratform_inv)] in
 185   let rec pre_rationalize tm =
 186     try (
 187       let (x,y) = dest_binop `(pow)` tm in
 188         MATCH_MP (INST [y,`n:num`] ratform_pow) (pre_rationalize x)
 189     )
 190     with _ ->
 191     try (
 192       let h = fst (strip_comb tm) in
 193       let bin_th = assoc h binop_assoc in
 194       let (x,y) = dest_binop h tm in
 195         MATCH_MP bin_th (CONJ (pre_rationalize x) (pre_rationalize y))
 196     )
 197     with _ -> (
 198       try (
 199         let (h,x) = dest_comb tm in
 200         let un_th = assoc h unary_assoc in
 201           MATCH_MP un_th (pre_rationalize x)
 202       )
 203       with _ -> SPEC tm trivial_ratform) in
 204     pre_rationalize;;
 205
 206 let clean_conv =
 207   let ra = REAL_ARITH `&1 * x = x /\ x * &1 = x /\ &0 * x = &0 /\
 208     x * &0 = &0 /\ &0+x = x /\ x + &0 = x /\ x - &0 = x /\ &0 - x = -- x ` in
 209     REWRITE_CONV[REAL_POW_NEQ_0;GSYM CONJ_ASSOC;
 210                  TAUT `~(p \/ q) <=> ~p /\ ~q`;
 211                               REAL_POW_POW;REAL_POW_1;real_pow;REAL_POW_ONE;
 212                               REAL_ENTIRE;
 213                               ra]
 214   THENC NUM_REDUCE_CONV;;
 215
 216 let dest_ratform rf =  snd(strip_comb rf);;
 217
 218 let rationalize_ratform =
 219   let rc = clean_conv in
 220   let clean_ratform = MESON[]
 221     `ratform p r a b /\ (p = p') /\ (a = a') /\ (b = b') ==> ratform p' r a' b'` in
 222   fun tm ->
 223     let pr = pre_rationalize tm in
 224     let [p;_;a;b] = dest_ratform (concl pr) in
 225     let p' = rc p in
 226     let a' = rc a in
 227     let b' = rc b in
 228       MATCH_MP clean_ratform (end_itlist CONJ [pr;p';a';b']);;
 229
 230 let rationalize =
 231   REWRITE_RULE[ratform] o rationalize_ratform;;
 232
 233 (* example:
 234 rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;
 235 *)
 236
 237
 238 let lite_imp = prove_by_refinement(
 239   `ratform p (u - v) a b /\ (p = p') /\ (a = &0) ==> (p' ==> (u = v))`,
 240   (* {{{ proof *)
 241   [
 242   REWRITE_TAC[ratform];
 243   ASM_MESON_TAC[REAL_ARITH `(u = v) <=> u - v = &0 /b`];
 244   ]);;
 245   (* }}} *)
 246
 247 let lite_imp2 = prove_by_refinement(
 248   `ratform p (u - v) a b /\ (p = p') /\ (a = a') ==> ((p' /\ (a' = &0)) ==> (u = v))`,
 249   (* {{{ proof *)
 250   [
 251   REWRITE_TAC[ratform];
 252   ASM_MESON_TAC[REAL_ARITH `(u = v) <=> u - v = &0 /b`];
 253   ]);;
 254   (* }}} *)
 255
 256 let rational_identity  =
 257   let sub = `( - )` in
 258     fun tm ->
 259       let (lhs,rhs) = dest_eq tm in
 260       let diff =     mk_binop sub lhs rhs in
 261       let rf = pre_rationalize diff in
 262       let [p;_;a;_]=dest_ratform (concl rf) in
 263       let p' = clean_conv p in
 264       let a' = clean_conv a in
 265         try (
 266           let zero = REAL_FIELD (mk_eq (a,`&0`)) in
 267             MATCH_MP (lite_imp) (end_itlist CONJ [rf ;p';zero])
 268         )
 269         with _ -> MATCH_MP (lite_imp2) (end_itlist CONJ [rf;p';a']);;
 270
 271 let CALC_ID_TAC gl =  (MATCH_MP_TAC (rational_identity (goal_concl gl))) gl;;
 272
 273 let invert_den_lt = prove_by_refinement(
 274   `!a b. &0 < a/b <=> &0 < a*b`,
 275   (* {{{ proof *)
 276 [
 277   REPEAT GEN_TAC;
 278 REWRITE_TAC  [real_div];
 279 REWRITE_TAC  [REAL_MUL_POS_LT];
 280 REWRITE_TAC  [REAL_ARITH `inv x < &0 <=> &0 < -- inv x`];
 281 REWRITE_TAC  [GSYM REAL_INV_NEG];
 282 REWRITE_TAC  [REAL_LT_INV_EQ];
 283 REAL_ARITH_TAC
 284  ]);;
 285   (* }}} *)
 286
 287 let invert_den_le = prove_by_refinement(
 288   `!a b. &0 <= a/b <=> &0 <= a*b`,
 289   (* {{{ proof *)
 290 [
 291   REPEAT GEN_TAC;
 292 REWRITE_TAC  [real_div];
 293 REWRITE_TAC  [REAL_MUL_POS_LE];
 294 REWRITE_TAC  [REAL_ARITH `inv x < &0 <=> &0 < -- inv x`];
 295 REWRITE_TAC  [GSYM REAL_INV_NEG];
 296 REWRITE_TAC  [REAL_LT_INV_EQ;Real_ext.REAL_PROP_ZERO_INV];
 297 REAL_ARITH_TAC
 298  ]);;
 299   (* }}} *)
 300
 301 let invert_den_eq = prove_by_refinement(
 302   `!a b. (a/b = &0)  <=> ( a*b = &0)`,
 303   (* {{{ proof *)
 304 [
 305   REPEAT GEN_TAC;
 306 REWRITE_TAC  [real_div];
 307 REWRITE_TAC  [REAL_ENTIRE];
 308 REWRITE_TAC  [REAL_LT_INV_EQ;Real_ext.REAL_PROP_ZERO_INV];
 309  ]);;
 310   (* }}} *)
 311
 312 let imp_lt = prove_by_refinement(
 313   `!p p' x a a' b b'. (&0 < x) /\ (ratform p x a b) /\ (p = p') /\ (a = a') /\ (b = b') ==> (p' ==> &0 < a' * b')`,
 314   (* {{{ proof *)
 315 [
 316 REWRITE_TAC [ratform];
 317 REPEAT STRIP_TAC ;
 318 ASM_MESON_TAC [invert_den_lt]
 319 ]);;
 320   (* }}} *)
 321
 322
 323 let imp_le = prove_by_refinement(
 324   `!p p' x a a' b b'. (&0 <= x) /\ (ratform p x a b) /\ (p = p') /\ (a = a') /\ (b = b') ==> (p' ==> &0 <= a' * b')`,
 325   (* {{{ proof *)
 326 [
 327 REWRITE_TAC [ratform];
 328 REPEAT STRIP_TAC ;
 329 ASM_MESON_TAC [invert_den_le]
 330 ]);;
 331   (* }}} *)
 332
 333 let imp_eq = prove_by_refinement(
 334   `!p p' x a a' b b'. (x= &0) /\ (ratform p x a b) /\ (p = p') /\ (a = a') /\ (b = b') ==> (p' /\ ~(b' = &0) ==>  (a'= &0 ))`,
 335   (* {{{ proof *)
 336 [
 337 REWRITE_TAC [ratform];
 338 REPEAT STRIP_TAC ;
 339 ASM_MESON_TAC [invert_den_eq;REAL_ENTIRE]
 340 ]);;
 341   (* }}} *)
 342
 343
 344 let imp_nz = prove_by_refinement(
 345   `!p p' x a a' b b'. ~(x= &0) /\ (ratform p x a b) /\ (p = p') /\ (a = a') /\ (b = b') ==> (p' ==>  (~(a' = &0) /\ ~(b' = &0)))`,
 346   (* {{{ proof *)
 347 [
 348 REWRITE_TAC [ratform];
 349 REPEAT STRIP_TAC THEN ASM_MESON_TAC [invert_den_eq;REAL_ENTIRE]
 350 ]);;
 351   (* }}} *)
 352
 353 let dest_nz  =
 354   let neg = `(~)` in
 355     fun tm ->
 356       let (a,b) = dest_comb tm in
 357       let _ = (a = neg) or failwith "not a negation" in
 358         dest_eq b;;
 359
 360 (* clear the denominator of an inequality *)
 361
 362 let rational_ineq_rule  =
 363   let lt = `(<)` in
 364   let le = `(<=)` in
 365   let ra1 = REAL_ARITH `a < b <=> &0 < b - a` in
 366   let ra2 = REAL_ARITH `a <= b <=> &0 <= b - a` in
 367   let ra3 = REAL_ARITH `(x = y) <=> (x - y = &0)` in
 368   let ineq_types =
 369     [snd o (dest_binop lt ), imp_lt;
 370      snd o (dest_binop le ), imp_le;
 371      fst o (dest_eq ), imp_eq;
 372      fst o (dest_nz), imp_nz] in
 373     fun thm ->
 374       let thm' = REWRITE_RULE[real_gt;real_ge] thm  in
 375       let thm' = ONCE_REWRITE_RULE [ra1] thm' in
 376       let thm' = ONCE_REWRITE_RULE [ra2] thm' in
 377       let thm' = ONCE_REWRITE_RULE [ra3] thm' in
 378       let (diff,imp) = tryfind (fun (d,imp) -> (d(concl thm'),imp)) ineq_types in
 379       let rf = pre_rationalize diff in
 380       let [p;_;a;b]=dest_ratform (concl rf) in
 381       let p' = clean_conv p in
 382       let a' = clean_conv a in
 383       let b' = clean_conv b in
 384       let thm' = MATCH_MP (imp) (end_itlist CONJ [thm';rf ;p';a';b']) in
 385         thm';;
 386
 387 (* Example:
 388
 389 rational_identity `(&1 / u  - &1/v) pow 2  = inv u pow 2 - &2 * inv (u * v) + inv v pow 2`;;
 390
 391 rational_identity `&1 / (x + y) - &1 / (x - y) = -- &2 * y / (x pow 2 - y pow 2)`;;
 392
 393 rational_ineq_rule (ASSUME `a / (b * e) <  c / (&2 * b)`);;
 394
 395 *)
 396
 397
 398 (* ========================================================================== *)
 399 (* DERIV FORM                                              *)
 400
 401
 402   let derived_form = new_definition
 403     `derived_form p f f' x s = (p ==> (f has_real_derivative f') (atreal x within s))`;;
 404
 405   let deriv_tac =   REWRITE_TAC[derived_form] THEN
 406 (*    REPEAT GEN_TAC THEN
 407     COND_CASES_TAC THEN
 408     REWRITE_TAC[] THEN     *)
 409     REPEAT STRIP_TAC  THEN
 410     ASM_REWRITE_TAC[]  THEN
 411     FIRST (map MATCH_MP_TAC [
 412              HAS_REAL_DERIVATIVE_ADD;
 413              HAS_REAL_DERIVATIVE_SUB;
 414              HAS_REAL_DERIVATIVE_MUL_ATREAL;
 415              HAS_REAL_DERIVATIVE_MUL_WITHIN;
 416              HAS_REAL_DERIVATIVE_DIV_ATREAL;
 417              HAS_REAL_DERIVATIVE_DIV_WITHIN;
 418              HAS_REAL_DERIVATIVE_NEG;
 419              HAS_REAL_DERIVATIVE_POW_WITHIN;
 420              HAS_REAL_DERIVATIVE_POW_ATREAL
 421            ]) THEN
 422     ASM_MESON_TAC[];;
 423
 424
 425 (* OLD u versions:
 426
 427   let derived_form_add = prove_by_refinement(
 428   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s /\ (u =  (\x. f1 x + f2 x)) ==> derived_form (p1 /\ p2) u (f1'+f2') x s`,
 429   (* {{{ proof *)
 430   [
 431   deriv_tac;
 432   ]);;
 433   (* }}} *)
 434
 435   let derived_form_sub = prove_by_refinement(
 436   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s /\ (u = (\x. f1 x - f2 x)) ==> derived_form (p1 /\ p2) u (f1'-f2') x s`,
 437   (* {{{ proof *)
 438   [
 439     deriv_tac;
 440   ]);;
 441   (* }}} *)
 442
 443   let derived_form_mul = prove_by_refinement(
 444   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s /\ (u = (\x. f1 x * f2 x)) ==> derived_form (p1 /\ p2) u  (f1 x * f2' + f1' * f2 x) x s`,
 445   (* {{{ proof *)
 446   [
 447     deriv_tac;
 448   ]);;
 449   (* }}} *)
 450
 451   let derived_form_div = prove_by_refinement(
 452   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s /\ (u =  (\x. f1 x / f2 x) ) ==> derived_form (p1 /\ p2 /\ ~(f2 x = &0)) u  ((f1'  * f2 x - f1 x * f2')/(f2 x pow 2)) x s`,
 453   (* {{{ proof *)
 454   [
 455     deriv_tac;
 456   ]);;
 457   (* }}} *)
 458
 459   let derived_form_neg = prove_by_refinement(
 460   `!x s. derived_form p1 f1 f1' x s /\ (u = (\x.  -- f1 x))  ==> derived_form p1 u (-- f1') x s`,
 461   (* {{{ proof *)
 462   [
 463   deriv_tac;
 464   ]);;
 465   (* }}} *)
 466
 467   let derived_form_pow = prove_by_refinement(
 468   `!x s.  derived_form p f f' x s /\ (u = (\x.  f x pow n)) ==> derived_form p u (&n * f x pow (n-1)* f') x s`,
 469   (* {{{ proof *)
 470   [
 471     deriv_tac;
 472   ]);;
 473   (* }}} *)
 474
 475   let deriv_fn_tac =     REPEAT STRIP_TAC THEN
 476   ASM_REWRITE_TAC[derived_form] THEN
 477   (* COND_CASES_TAC THEN  *)
 478   ASM_MESON_TAC[ HAS_REAL_DERIVATIVE_CONST;
 479                  HAS_REAL_DERIVATIVE_ATREAL_WITHIN;
 480                  HAS_REAL_DERIVATIVE_SIN;
 481                  HAS_REAL_DERIVATIVE_COS;
 482                  HAS_REAL_DERIVATIVE_SQRT;
 483                  HAS_REAL_DERIVATIVE_ATN;
 484                  HAS_REAL_DERIVATIVE_ACS;
 485                  HAS_REAL_DERIVATIVE_ASN;
 486                  HAS_REAL_DERIVATIVE_INV_BASIC;
 487                ];;
 488
 489   let derived_form_const = prove_by_refinement(
 490   `!x s. (u = \x. c) ==> derived_form T u (&0) x s`,
 491   (* {{{ proof *)
 492   [
 493     deriv_fn_tac;
 494   ]);;
 495   (* }}} *)
 496
 497   let derived_form_sin = prove_by_refinement(
 498   `!x s.  derived_form T sin (cos x) x s`,
 499   (* {{{ proof *)
 500   [
 501     deriv_fn_tac;
 502   ]);;
 503   (* }}} *)
 504
 505   let derived_form_cos = prove_by_refinement(
 506   `!x s.  derived_form T cos (-- sin x) x s`,
 507   (* {{{ proof *)
 508   [
 509     deriv_fn_tac;
 510   ]);;
 511   (* }}} *)
 512
 513   let derived_form_sqrt = prove_by_refinement(
 514   `!x s.  derived_form (&0 < x) sqrt (inv (&2 * sqrt x)) x s`,
 515   (* {{{ proof *)
 516     [
 517       deriv_fn_tac;
 518   ]);;
 519   (* }}} *)
 520
 521   let derived_form_atn = prove_by_refinement(
 522   `!x s.  derived_form T atn (inv (&1 + x pow 2)) x s`,
 523   (* {{{ proof *)
 524   [
 525     deriv_fn_tac;
 526   ]);;
 527   (* }}} *)
 528
 529   let derived_form_acs = prove_by_refinement(
 530   `!x s.  derived_form (abs x < &1) acs (-- inv (sqrt(&1 - x pow 2))) x s`,
 531   (* {{{ proof *)
 532   [
 533     deriv_fn_tac;
 534   ]);;
 535   (* }}} *)
 536
 537   let derived_form_asn = prove_by_refinement(
 538   `!x s.  derived_form (abs x < &1) asn ( inv (sqrt(&1 - x pow 2))) x s`,
 539   (* {{{ proof *)
 540   [
 541     deriv_fn_tac;
 542   ]);;
 543   (* }}} *)
 544
 545
 546   let derived_form_inv = prove_by_refinement(
 547   `!x s.  derived_form (~(x = &0)) inv  (-- inv (x pow 2)) x s`,
 548   (* {{{ proof *)
 549   [
 550     deriv_fn_tac;
 551   ]);;
 552   (* }}} *)
 553
 554   let derived_form_id = prove_by_refinement(
 555   `!x s. (u = (\x. x)) ==>derived_form T u  (&1) x s`,
 556   (* {{{ proof *)
 557   [
 558     REPEAT STRIP_TAC;
 559   ASM_REWRITE_TAC[derived_form;HAS_REAL_DERIVATIVE_ID];
 560   ]);;
 561   (* }}} *)
 562
 563   let derived_form_chain = prove_by_refinement(
 564   `!x s.  derived_form p g g' (f x) (:real) /\ derived_form p' f f' x s /\ (u = (\x.  g(f x))) ==> derived_form (p /\ p' ) u  (f' * g') x s`,
 565   (* {{{ proof *)
 566   [
 567     REWRITE_TAC[derived_form];
 568     REPEAT STRIP_TAC;
 569     MP_TAC (SPECL [`(\t. ((t = (f:real->real) x) /\ p))`;`(f:real->real)`;`(g:real->real)`] (INST [`(\(t:real). (g':real))`,`g':real->real`] HAS_REAL_DERIVATIVE_CHAIN));
 570     ANTS_TAC;
 571     GEN_TAC;
 572     BETA_TAC;
 573     ASM_MESON_TAC[WITHINREAL_UNIV];
 574     REPEAT (POP_ASSUM MP_TAC);
 575     (* *)
 576     ASM_MESON_TAC[];
 577   ]);;
 578   (* }}} *)
 579
 580
 581   *)
 582 (* REDO *)
 583
 584
 585   let derived_form_add = prove_by_refinement(
 586   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s ==> derived_form (p1 /\ p2)  (\x. f1 x + f2 x)  (f1'+f2') x s`,
 587   (* {{{ proof *)
 588   [
 589   deriv_tac;
 590   ]);;
 591   (* }}} *)
 592
 593   let derived_form_sub = prove_by_refinement(
 594   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s  ==> derived_form (p1 /\ p2)  (\x. f1 x - f2 x) (f1'-f2') x s`,
 595   (* {{{ proof *)
 596   [
 597     deriv_tac;
 598   ]);;
 599   (* }}} *)
 600
 601   let derived_form_mul = prove_by_refinement(
 602   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s  ==> derived_form (p1 /\ p2)  (\x. f1 x * f2 x)  (f1 x * f2' + f1' * f2 x) x s`,
 603   (* {{{ proof *)
 604   [
 605     deriv_tac;
 606   ]);;
 607   (* }}} *)
 608
 609   let derived_form_div = prove_by_refinement(
 610   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s ==> derived_form (p1 /\ p2 /\ ~(f2 x = &0))  (\x. f1 x / f2 x)    ((f1'  * f2 x - f1 x * f2')/(f2 x pow 2)) x s`,
 611   (* {{{ proof *)
 612   [
 613     deriv_tac;
 614   ]);;
 615   (* }}} *)
 616
 617 (* moved to function section.
 618   let derived_form_neg = prove_by_refinement(
 619   `!x s. derived_form p1 f1 f1' x s   ==> derived_form p1 (\x.  -- f1 x) (-- f1') x s`,
 620   (* {{{ proof *)
 621   [
 622   deriv_tac;
 623   ]);;
 624   (* }}} *)
 625 *)
 626
 627   let derived_form_pow = prove_by_refinement(
 628   `!n x s.  derived_form p f f' x s ==> derived_form p (\x.  f x pow n)  (&n * f x pow (n-1)* f') x s`,
 629   (* {{{ proof *)
 630   [
 631     deriv_tac;
 632   ]);;
 633   (* }}} *)
 634
 635   let deriv_fn_tac =     REPEAT STRIP_TAC THEN
 636   ASM_REWRITE_TAC[derived_form] THEN
 637   (* COND_CASES_TAC THEN  *)
 638   ASM_MESON_TAC[ HAS_REAL_DERIVATIVE_CONST;
 639                  HAS_REAL_DERIVATIVE_ATREAL_WITHIN;
 640                  HAS_REAL_DERIVATIVE_SIN;
 641                  HAS_REAL_DERIVATIVE_COS;
 642                  HAS_REAL_DERIVATIVE_SQRT;
 643                  HAS_REAL_DERIVATIVE_ATN;
 644                  HAS_REAL_DERIVATIVE_ACS;
 645                  HAS_REAL_DERIVATIVE_ASN;
 646                  HAS_REAL_DERIVATIVE_INV_BASIC;
 647                ];;
 648
 649   let derived_form_neg = prove_by_refinement(
 650   `!x s. derived_form T ( -- )  (-- &1) x s`,
 651   (* {{{ proof *)
 652   [
 653     REPEAT STRIP_TAC;
 654     REWRITE_TAC[derived_form];
 655     SUBGOAL_THEN `( -- ) = (\x. --x)`  SUBST1_TAC;
 656     MATCH_MP_TAC EQ_EXT;
 657     MESON_TAC[];
 658     BETA_TAC;
 659     MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
 660     REWRITE_TAC[HAS_REAL_DERIVATIVE_ID];
 661   ]);;
 662   (* }}} *)
 663
 664   let derived_form_const = prove_by_refinement(
 665   `!c x s. derived_form T  (\x. c)  (&0) x s`,
 666   (* {{{ proof *)
 667   [
 668     deriv_fn_tac;
 669   ]);;
 670   (* }}} *)
 671
 672   let derived_form_sin = prove_by_refinement(
 673   `!x s.  derived_form T sin (cos x) x s`,
 674   (* {{{ proof *)
 675   [
 676     deriv_fn_tac;
 677   ]);;
 678   (* }}} *)
 679
 680   let derived_form_cos = prove_by_refinement(
 681   `!x s.  derived_form T cos (-- sin x) x s`,
 682   (* {{{ proof *)
 683   [
 684     deriv_fn_tac;
 685   ]);;
 686   (* }}} *)
 687
 688   let derived_form_sqrt = prove_by_refinement(
 689   `!x s.  derived_form (&0 < x) sqrt (inv (&2 * sqrt x)) x s`,
 690   (* {{{ proof *)
 691     [
 692       deriv_fn_tac;
 693   ]);;
 694   (* }}} *)
 695
 696   let derived_form_atn = prove_by_refinement(
 697   `!x s.  derived_form T atn (inv (&1 + x pow 2)) x s`,
 698   (* {{{ proof *)
 699   [
 700     deriv_fn_tac;
 701   ]);;
 702   (* }}} *)
 703
 704   let derived_form_acs = prove_by_refinement(
 705   `!x s.  derived_form (abs x < &1) acs (-- inv (sqrt(&1 - x pow 2))) x s`,
 706   (* {{{ proof *)
 707   [
 708     deriv_fn_tac;
 709   ]);;
 710   (* }}} *)
 711
 712   let derived_form_asn = prove_by_refinement(
 713   `!x s.  derived_form (abs x < &1) asn ( inv (sqrt(&1 - x pow 2))) x s`,
 714   (* {{{ proof *)
 715   [
 716     deriv_fn_tac;
 717   ]);;
 718   (* }}} *)
 719
 720
 721   let derived_form_inv = prove_by_refinement(
 722   `!x s.  derived_form (~(x = &0)) inv  (-- inv (x pow 2)) x s`,
 723   (* {{{ proof *)
 724   [
 725     deriv_fn_tac;
 726   ]);;
 727   (* }}} *)
 728
 729   let derived_form_id = prove_by_refinement(
 730   `!x s. derived_form T (\x. x)  (&1) x s`,
 731   (* {{{ proof *)
 732   [
 733     REPEAT STRIP_TAC;
 734   ASM_REWRITE_TAC[derived_form;HAS_REAL_DERIVATIVE_ID];
 735   ]);;
 736   (* }}} *)
 737
 738   let derived_form_chain = prove_by_refinement(
 739   `!x s.  derived_form p g g' (f1 x) (:real) /\ derived_form p' f2 f' x s /\ (f1=f2) ==> derived_form (p /\ p' )  (\x.  g(f1 x))  (f' * g') x s`,
 740   (* {{{ proof *)
 741   [
 742     REWRITE_TAC[derived_form];
 743     REPEAT STRIP_TAC;
 744     MP_TAC (SPECL [`(\t. ((t = (f1:real->real) x) /\ p))`;`(f1:real->real)`;`(g:real->real)`] (INST [`(\(t:real). (g':real))`,`g':real->real`] HAS_REAL_DERIVATIVE_CHAIN));
 745     ANTS_TAC;
 746     GEN_TAC;
 747     BETA_TAC;
 748     ASM_MESON_TAC[WITHINREAL_UNIV];
 749     REPEAT (POP_ASSUM MP_TAC);
 750     (* *)
 751     ASM_MESON_TAC[];
 752   ]);;
 753   (* }}} *)
 754
 755
 756 let derived_form_generic = prove_by_refinement(
 757   `!f f' x s. derived_form   (derived_form T f (f') x s) f (f') x s`,
 758   (* {{{ proof *)
 759   [
 760     REWRITE_TAC[derived_form];
 761   ]);;
 762
 763
 764 (* START OF NICK VOLKER'S CODE *)
 765
 766
 767 let region_conv = prove_by_refinement(
 768   `!(x:real) (y:real). ~(y = &0 /\ x <= &0) ==> (x > &0) \/ (y < &0) \/ (y > &0)`,
 769   (* {{{ proof *)
 770   [
 771   REAL_ARITH_TAC;
 772   ]);;
 773
 774  let x2notless0 = prove_by_refinement(`!x:real. ~(x pow 2 < &0)`,
 775                                        [
 776 STRIP_TAC;
 777 SUBGOAL_THEN `x = &0 ==> ~(x pow 2 < &0)` MP_TAC;
 778 STRIP_TAC;
 779 MP_TAC (SPECL[`x:real`] Trigonometry2.POW2_EQ_0);
 780 ASM_REWRITE_TAC[];
 781 REAL_ARITH_TAC;
 782 SUBGOAL_THEN `~(x = &0) ==> ~(x pow 2 < &0)` MP_TAC;
 783 STRIP_TAC;
 784 MP_TAC (SPECL[`x:real`] (GENL[`a:real`] Trigonometry2.NOT_ZERO_EQ_POW2_LT));
 785 ASM_REWRITE_TAC[];
 786 STRIP_TAC;
 787 MP_TAC (REAL_FIELD `&0 < x pow 2 ==> ~(x pow 2 < &0)`);
 788 ASM_MESON_TAC[];
 789 ASM_MESON_TAC[];
 790                                        ]);;
 791
 792   let x2notlesseq0 = prove_by_refinement(`!x:real. ~(x = &0) ==> ~(x pow 2 <= &0)`,
 793                                          [
 794 STRIP_TAC;
 795 STRIP_TAC;
 796 MP_TAC (SPECL[`x:real`] (GENL[`a:real`] Trigonometry2.NOT_ZERO_EQ_POW2_LT));
 797 ASM_REWRITE_TAC[];
 798 STRIP_TAC;
 799 MP_TAC (REAL_FIELD `&0 < x pow 2 ==> ~(x pow 2 <= &0)`);
 800 ASM_MESON_TAC[];
 801                                          ]);;
 802
 803   let sumsquaresnot0 = prove_by_refinement(`!x:real y:real. ~(x = &0) ==> ~(x pow 2 + y pow 2 <= &0)`,
 804                                            [
 805 STRIP_TAC;
 806 STRIP_TAC;
 807 STRIP_TAC;
 808 MP_TAC (SPECL[`x:real`] x2notlesseq0);
 809 ASM_REWRITE_TAC[];
 810 STRIP_TAC;
 811 MP_TAC (SPECL[`y:real`] x2notless0);
 812 STRIP_TAC;
 813 MP_TAC (REAL_ARITH `~(x pow 2 <= &0) /\ ~(y pow 2 < &0) ==> ~(x pow 2 + y pow 2 <= &0)`);
 814 ASM_MESON_TAC[];
 815                                            ]);;
 816
 817  let notzerodenom = prove_by_refinement(`!a:real b:real c:real d:real. (~(b = &0) ==> (a*b - c*d)/(b pow 2) * inv (&1 + (c/b) pow 2) = (a*b - c*d)/(b pow 2 + c pow 2))`,
 818                                          [
 819 REPEAT STRIP_TAC;
 820 MP_TAC (SPECL [`b:real`;`c:real`] sumsquaresnot0);
 821 ASM_REWRITE_TAC[];
 822 STRIP_TAC;
 823 MP_TAC (REAL_FIELD `~(b = &0) /\ ~(b pow 2 + c pow 2 <= &0) ==> (a*b - c*d)/(b pow 2) * inv (&1 + (c/b) pow 2) = (a*b - c*d)/(b pow 2 + c pow 2)`);
 824 ASM_MESON_TAC[];
 825                                          ]);;
 826
 827  let notzerodenom2 = prove_by_refinement(`!a:real b:real c:real d:real. (~(c = &0) ==> (a*b - c*d)/(c pow 2) * inv (&1 + (b/c) pow 2) = (a*b - c*d)/(b pow 2 + c pow 2))`,
 828                                          [
 829 REPEAT STRIP_TAC;
 830 MP_TAC (SPECL [`c:real`;`b:real`] sumsquaresnot0);
 831 ASM_REWRITE_TAC[];
 832 STRIP_TAC;
 833 MP_TAC (REAL_FIELD `~(c = &0) /\ ~(c pow 2 + b pow 2 <= &0) ==> (a*b - c*d)/(c pow 2) * inv (&1 + (b/c) pow 2) = (a*b - c*d)/(b pow 2 + c pow 2)`);
 834 ASM_MESON_TAC[];
 835                                          ]);;
 836
 837
 838 let derived_imp_pos_open = prove_by_refinement(
 839   `!p f f' x s.  p /\ derived_form p f f' x s /\ &0 < f x ==>
 840      (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 < f x'))`,
 841   (* {{{ proof *)
 842   [
 843 REWRITE_TAC[derived_form];
 844 REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`];
 845 REPEAT STRIP_TAC;
 846 FIRST_X_ASSUM (MP_TAC o (  MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL ));
 847 REWRITE_TAC[real_continuous_withinreal];
 848 DISCH_THEN (MP_TAC o (SPEC `(f:real->real) x`));
 849 ASM_REWRITE_TAC[];
 850 STRIP_TAC;
 851 EXISTS_TAC `d:real`;
 852 ASM_REWRITE_TAC[];
 853 REPEAT STRIP_TAC;
 854 FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`));
 855 ASM_REWRITE_TAC[];
 856 ASM_REAL_ARITH_TAC;
 857   ]);;
 858
 859 let derived_imp_pos_open_2 = prove_by_refinement(
 860   `!p g g' x s.  p /\ derived_form p g g' x s /\ &0 < g x ==>
 861      (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 < g x'))`,
 862   (* {{{ proof *)
 863   [
 864 REWRITE_TAC[derived_form];
 865 REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`];
 866 REPEAT STRIP_TAC;
 867 FIRST_X_ASSUM (MP_TAC o (  MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL ));
 868 REWRITE_TAC[real_continuous_withinreal];
 869 DISCH_THEN (MP_TAC o (SPEC `(g:real->real) x`));
 870 ASM_REWRITE_TAC[];
 871 STRIP_TAC;
 872 EXISTS_TAC `d:real`;
 873 ASM_REWRITE_TAC[];
 874 REPEAT STRIP_TAC;
 875 FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`));
 876 ASM_REWRITE_TAC[];
 877 ASM_REAL_ARITH_TAC;
 878   ]);;
 879
 880 let derived_imp_pos_open_3 = prove_by_refinement(
 881   `!p g g' x s.  p /\ derived_form p g g' x s /\ &0 > g x==>
 882      (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 > g x' ))`,
 883   (* {{{ proof *)
 884   [
 885 REWRITE_TAC[REAL_ARITH ` &0 > g x <=> &0 < --(g x)`];
 886 REWRITE_TAC[derived_form];
 887 REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`];
 888 REPEAT STRIP_TAC;
 889 FIRST_X_ASSUM (MP_TAC o (  MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL ));
 890 REWRITE_TAC[real_continuous_withinreal];
 891 DISCH_THEN (MP_TAC o (SPEC `--(g:real->real) x`));
 892 ASM_REWRITE_TAC[];
 893 STRIP_TAC;
 894 EXISTS_TAC `d:real`;
 895 ASM_REWRITE_TAC[];
 896 REPEAT STRIP_TAC;
 897 FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`));
 898 ASM_REWRITE_TAC[];
 899 ASM_REAL_ARITH_TAC;
 900   ]);;
 901
 902 let deriv_pi = prove_by_refinement(
 903   `!(x:real) s. derived_form T (\x. (pi / &2)) (&0) x s`,
 904   [
 905     MP_TAC (SPECL [`(pi / &2)`] derived_form_const);
 906     ASM_MESON_TAC[];
 907   ]);;
 908
 909 let deriv_pi_minus = prove_by_refinement(
 910   `!(x:real) pf f f' s. derived_form pf f f' x s ==> derived_form (T /\pf) (\x. (pi / &2) - f x) (&0 - f') x s`,
 911   [
 912     REPEAT GEN_TAC;
 913     MP_TAC (SPECL[`x:real`;`s:real->bool`] deriv_pi);
 914     REPEAT STRIP_TAC;
 915     MATCH_MP_TAC derived_form_sub;
 916     ASM_MESON_TAC[];
 917 ]);;
 918
 919 let deriv_minus_pi = prove_by_refinement(
 920   `!(x:real) s. derived_form T (\x. --(pi / &2)) (&0) x s`,
 921   [
 922     MP_TAC (SPECL [`--(pi / &2)`] derived_form_const);
 923     ASM_MESON_TAC[];
 924   ]);;
 925
 926 let deriv_minus_pi_minus = prove_by_refinement(
 927   `!(x:real) pf f f' s. derived_form pf f f' x s ==> derived_form (T /\pf) (\x. --(pi / &2) - f x) (&0 - f') x s`,
 928   [
 929     REPEAT GEN_TAC;
 930     MP_TAC (SPECL[`x:real`;`s:real->bool`] deriv_minus_pi);
 931     REPEAT STRIP_TAC;
 932     MATCH_MP_TAC derived_form_sub;
 933     ASM_MESON_TAC[];
 934 ]);;
 935
 936 let derived_form_chain_simple = prove_by_refinement(
 937   `!x s g g' f f' p p'.
 938          derived_form p g g' (f x) (:real) /\
 939          derived_form p' f f' x s
 940          ==> derived_form (p /\ p') (\x. g (f x)) (f' * g') x s`,
 941   (* {{{ proof *)
 942   [
 943   MESON_TAC[derived_form_chain]
 944   ]);;
 945
 946 let atn_lemma = prove_by_refinement(
 947   `!x pf f f' pg g g' s.  (&0 < f x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form (T /\ (pg /\ pf)) (\x. atn( g x / f x)) ((g' * f x - g x * f')/(f x pow 2) *inv (&1 + (g x / f x) pow 2)) x s`,
 948   (* {{{ proof *)
 949   [
 950 REPEAT STRIP_TAC;
 951 MATCH_MP_TAC derived_form_chain_simple;
 952 REWRITE_TAC[derived_form_atn];
 953 MP_TAC (REAL_ARITH `&0 < (f:real->real) x ==> ~(f x = &0)`);
 954 SUBGOAL_THEN `derived_form (pg /\ pf /\ ~(f x = &0)) (\x. g x / f x)      ((g' * f x - g x * f') / f x pow 2)      x      s` MP_TAC;
 955 MATCH_MP_TAC derived_form_div;
 956 ASM_REWRITE_TAC[];
 957 ASM_REWRITE_TAC[derived_form];
 958 REPEAT STRIP_TAC;
 959 FIRST_X_ASSUM MATCH_MP_TAC;
 960 ASM_REWRITE_TAC[]
 961   ]);;
 962
 963 let atn_notpi_lemma = prove_by_refinement(
 964   `!x pf f f' pg g g' s.  (&0 < g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form (T /\ (pf /\ pg)) (\x. atn( f x / g x)) ((f' * g x - f x * g')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
 965   (* {{{ proof *)
 966   [
 967 REPEAT STRIP_TAC;
 968 MATCH_MP_TAC derived_form_chain_simple;
 969 REWRITE_TAC[derived_form_atn];
 970 MP_TAC (REAL_ARITH `&0 < (g:real->real) x ==> ~(g x = &0)`);
 971 SUBGOAL_THEN `derived_form (pf /\ pg /\ ~(g x = &0)) (\x. f x / g x)      ((f' * g x - f x * g') / g x pow 2)      x      s` MP_TAC;
 972 MATCH_MP_TAC derived_form_div;
 973 ASM_REWRITE_TAC[];
 974 ASM_REWRITE_TAC[derived_form];
 975 REPEAT STRIP_TAC;
 976 FIRST_X_ASSUM MATCH_MP_TAC;
 977 ASM_REWRITE_TAC[]
 978   ]);;
 979
 980 let atn_notnegpi_lemma = prove_by_refinement(
 981   `!x pf f f' pg g g' s.  (&0 > g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form (T /\ (pf /\ pg)) (\x. atn( f x / g x)) ((f' * g x - f x * g')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
 982   (* {{{ proof *)
 983   [
 984 REPEAT STRIP_TAC;
 985 MATCH_MP_TAC derived_form_chain_simple;
 986 REWRITE_TAC[derived_form_atn];
 987 MP_TAC (REAL_ARITH `&0 > (g:real->real) x ==> ~(g x = &0)`);
 988 SUBGOAL_THEN `derived_form (pf /\ pg /\ ~(g x = &0)) (\x. f x / g x)      ((f' * g x - f x * g') / g x pow 2)      x      s` MP_TAC;
 989 MATCH_MP_TAC derived_form_div;
 990 ASM_REWRITE_TAC[];
 991 ASM_REWRITE_TAC[derived_form];
 992 REPEAT STRIP_TAC;
 993 FIRST_X_ASSUM MATCH_MP_TAC;
 994 ASM_REWRITE_TAC[]
 995   ]);;
 996
 997 let atn_lemma_2 = prove_by_refinement (
 998   `!x pf f f' pg g g' s.  (&0 < g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form (T /\ (pf /\ pg)) (\x. (pi / &2) - atn( f x / g x)) ((g' * f x - g x * f')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
 999   [
1000     REPEAT STRIP_TAC;
1001     MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn_notpi_lemma);
1002     ASM_REWRITE_TAC[];
1003     REPEAT STRIP_TAC;
1004     UNDISCH_THEN `derived_form (pf /\ pg) (\x. atn (f x / g x)) ((f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2)) x s` (MP_TAC o (MATCH_MP deriv_pi_minus));
1005 (*REWRITE_TAC[REAL_ARITH `(&0 - (a*d -b*c))/u*v = (c*b - d*a)/u*v`]; *)
1006     UNDISCH_TAC `derived_form pf f f' x s`;
1007     UNDISCH_TAC `derived_form pg g g' x s`;
1008     REWRITE_TAC[derived_form];
1009     REPEAT STRIP_TAC;
1010     SUBGOAL_THEN `((\x. pi / &2 - atn (f x / g x)) has_real_derivative
1011            &0 -
1012            (f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2))
1013           (atreal x within s)` MP_TAC;
1014     ASM_MESON_TAC[];
1015     SUBGOAL_THEN `!(f:real->real) (g:real->real). (&0 - (f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2)) = ((g' * f x - g x * f') / g x pow 2 * inv (&1 + (f x / g x) pow 2))` MP_TAC;
1016     REPEAT STRIP_TAC;
1017     REAL_ARITH_TAC;
1018     STRIP_TAC;
1019     ASM_MESON_TAC[];
1020   ]);;
1021
1022 let atn_lemma_3 = prove_by_refinement (
1023   `!x pf f f' pg g g' s.  (&0 > g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form (T /\ (pf /\ pg)) (\x. --(pi / &2) - atn( f x / g x)) ((g' * f x - g x * f')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
1024   [
1025     REPEAT STRIP_TAC;
1026     MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn_notnegpi_lemma);
1027     ASM_REWRITE_TAC[];
1028     REPEAT STRIP_TAC;
1029     UNDISCH_THEN `derived_form (pf /\ pg) (\x. atn (f x / g x)) ((f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2)) x s` (MP_TAC o (MATCH_MP deriv_minus_pi_minus));
1030 (*REWRITE_TAC[REAL_ARITH `(&0 - (a*d -b*c))/u*v = (c*b - d*a)/u*v`]; *)
1031     UNDISCH_TAC `derived_form pf f f' x s`;
1032     UNDISCH_TAC `derived_form pg g g' x s`;
1033     REWRITE_TAC[derived_form];
1034     REPEAT STRIP_TAC;
1035     SUBGOAL_THEN `((\x. --(pi / &2) - atn (f x / g x)) has_real_derivative
1036            &0 -
1037            (f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2))
1038           (atreal x within s)` MP_TAC;
1039     ASM_MESON_TAC[];
1040     SUBGOAL_THEN `!(f:real->real) (g:real->real). (&0 - (f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2)) = ((g' * f x - g x * f') / g x pow 2 * inv (&1 + (f x / g x) pow 2))` MP_TAC;
1041     REPEAT STRIP_TAC;
1042     REAL_ARITH_TAC;
1043     STRIP_TAC;
1044     ASM_MESON_TAC[];
1045   ]);;
1046
1047 let atn2_atn_open = prove_by_refinement(
1048   `!p f f' g x s.  p /\ derived_form p f f' x s /\ (&0 < f x)==>
1049     (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==>
1050         atn2 (f x', g x') = atn(g x' / f x')))`,
1051   (* {{{ proof *)
1052   [
1053 (REPEAT GEN_TAC);
1054 (DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open)));
1055 (REPEAT STRIP_TAC);
1056 (EXISTS_TAC `d:real`);
1057 (ASM_REWRITE_TAC[]);
1058 (REPEAT STRIP_TAC);
1059 (SUBGOAL_THEN `&0 < ((f:real->real) x')` MP_TAC);
1060 (ASM_MESON_TAC[]);
1061 (MP_TAC (MATCH_MP (TAUT `a /\ b /\ c /\ d ==> a`)  (SPECL [`((f:real->real) x')`;`((g:real->real) x')`] Trigonometry1.ATN2_BREAKDOWN)));
1062 (REPEAT STRIP_TAC);
1063   ]);;
1064
1065 let atn2_atn_open_2 = prove_by_refinement(
1066   `!p g g' f x s.  p /\ derived_form p g g' x s /\ (&0 < g x)==>
1067     (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==>
1068         atn2 (f x', g x') = (pi / &2 - atn(f x' / g x'))))`,
1069   (* {{{ proof *)
1070   [
1071 (REPEAT GEN_TAC);
1072 (DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open)));
1073 (REPEAT STRIP_TAC);
1074 (EXISTS_TAC `d:real`);
1075 (ASM_REWRITE_TAC[]);
1076 (REPEAT STRIP_TAC);
1077 (SUBGOAL_THEN `&0 < ((g:real->real) x')` MP_TAC);
1078 (ASM_MESON_TAC[]);
1079 (MP_TAC (MATCH_MP (TAUT `a /\ b /\ c /\ d ==> b`)  (SPECL [`((f:real->real) x')`;`((g:real->real) x')`] Trigonometry1.ATN2_BREAKDOWN)));
1080 (REPEAT STRIP_TAC);
1081   ]);;
1082
1083 let atn2_atn_open_3 = prove_by_refinement(
1084   `!p g g' f x s.  p /\ derived_form p g g' x s /\ (&0 > g x)==>
1085     (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==>
1086         atn2 (f x', g x') = (--(pi / &2) - atn(f x' / g x'))))`,
1087   (* {{{ proof *)
1088   [
1089 (REPEAT GEN_TAC);
1090 (DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open_3)));
1091 (REPEAT STRIP_TAC);
1092 (EXISTS_TAC `d:real`);
1093 (ASM_REWRITE_TAC[]);
1094 (REPEAT STRIP_TAC);
1095 (SUBGOAL_THEN `&0 > ((g:real->real) x')` MP_TAC);
1096 (ASM_MESON_TAC[]);
1097 (REWRITE_TAC[REAL_ARITH `a > b <=> b < a`]);
1098 (MP_TAC (MATCH_MP (TAUT `a /\ b /\ c /\ d ==> c`)  (SPECL [`((f:real->real) x')`;`((g:real->real) x')`] Trigonometry1.ATN2_BREAKDOWN)));
1099 (REPEAT STRIP_TAC);
1100   ]);;
1101
1102 (*//////////////////////////////////*)
1103
1104 let atn2_final_1 =  prove_by_refinement( `!x pf (f:real->real) f' pg (g:real->real) g' s.  (&0 < f x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(f x pow 2) *inv (&1 + (g x / f x) pow 2)) x s`,
1105   (* {{{ proof *)
1106   [
1107  REPEAT GEN_TAC;
1108  REWRITE_TAC[derived_form];
1109  REPEAT STRIP_TAC;
1110  SUBGOAL_THEN `pf /\ derived_form pf f f' x s /\ (&0 < (f:real->real) x)` MP_TAC;
1111  REWRITE_TAC[derived_form];
1112  ASM_MESON_TAC[];
1113  DISCH_THEN (MP_TAC o (MATCH_MP atn2_atn_open));
1114  STRIP_TAC;
1115  SUBGOAL_THEN `derived_form (T /\ (pg /\ pf)) (\x. atn( g x / f x)) ((g' * f x - g x * f')/(f x pow 2) *inv (&1 + (g x / f x) pow 2)) x s` MP_TAC;
1116  MP_TAC atn_lemma;
1117  REWRITE_TAC[derived_form];
1118  REPEAT STRIP_TAC;
1119  ASM_MESON_TAC[];
1120  REWRITE_TAC[derived_form];
1121  STRIP_TAC;
1122  MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN;
1123  ASM_MESON_TAC[];
1124   ]);;
1125
1126 let atn2_final_2 = prove_by_refinement (
1127   `!x pf (f:real->real) f' pg (g:real->real) g' s.  (&0 < g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
1128   [
1129         REPEAT GEN_TAC;
1130         REWRITE_TAC[derived_form];
1131         REPEAT STRIP_TAC;
1132         SUBGOAL_THEN `pg /\ derived_form pg g g' x s /\ (&0 < (g:real->real) x)` MP_TAC;
1133         REWRITE_TAC[derived_form];
1134         ASM_MESON_TAC[];
1135         DISCH_THEN (MP_TAC o (MATCH_MP atn2_atn_open_2));
1136         STRIP_TAC;
1137         SUBGOAL_THEN `derived_form (T /\ (pg /\ pf)) (\x. (pi / &2) - atn( f x / g x)) ((g' * f x - g x * f')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s` MP_TAC;
1138         MP_TAC atn_lemma_2;
1139         REWRITE_TAC[derived_form];
1140         REPEAT STRIP_TAC;
1141         ASM_MESON_TAC[];
1142         REWRITE_TAC[derived_form];
1143         STRIP_TAC;
1144         MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN;
1145         ASM_MESON_TAC[];
1146   ]);;
1147
1148 let atn2_final_3 = prove_by_refinement (
1149   `!x pf (f:real->real) f' pg (g:real->real) g' s.  (&0 > g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
1150   [
1151         REPEAT GEN_TAC;
1152         REWRITE_TAC[derived_form];
1153         REPEAT STRIP_TAC;
1154         SUBGOAL_THEN `pg /\ derived_form pg g g' x s /\ (&0 > (g:real->real) x)` MP_TAC;
1155         REWRITE_TAC[derived_form];
1156         ASM_MESON_TAC[];
1157         DISCH_THEN (MP_TAC o (MATCH_MP atn2_atn_open_3));
1158         STRIP_TAC;
1159         SUBGOAL_THEN `derived_form (T /\ (pg /\ pf)) (\x. --(pi / &2) - atn( f x / g x)) ((g' * f x - g x * f')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s` MP_TAC;
1160         MP_TAC atn_lemma_3;
1161         REWRITE_TAC[derived_form];
1162         REPEAT STRIP_TAC;
1163         ASM_MESON_TAC[];
1164         REWRITE_TAC[derived_form];
1165         STRIP_TAC;
1166         MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN;
1167         ASM_MESON_TAC[];
1168   ]);;
1169
1170 let atn2_deriv_simple1 = prove_by_refinement(`!x pf (f:real->real) f' pg (g:real->real) g' s.  (&0 < f x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(f x pow 2 + g x pow 2)) x s`,
1171                                              [
1172 REPEAT STRIP_TAC;
1173 MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn2_final_1);
1174 ASM_REWRITE_TAC[];
1175 STRIP_TAC;
1176 MP_TAC (REAL_ARITH `&0 < (f:real->real) x ==> ~(f x = &0)`);
1177 ASM_REWRITE_TAC[];
1178 STRIP_TAC;
1179 MP_TAC (SPECL[`(f:real->real) x`;`(g:real->real) x`;] sumsquaresnot0);
1180 ASM_REWRITE_TAC[];
1181 STRIP_TAC;
1182 MP_TAC (SPECL[`g':real`;`(f:real->real) x`;`(g:real->real) x`;`f':real`] notzerodenom);
1183 ASM_REWRITE_TAC[];
1184 ASM_MESON_TAC[];
1185                                              ]);;
1186
1187 let atn2_deriv_simple2 = prove_by_refinement(`!x pf (f:real->real) f' pg (g:real->real) g' s.  (&0 < g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(f x pow 2 + g x pow 2)) x s`,
1188                                              [
1189 REPEAT STRIP_TAC;
1190 MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn2_final_2);
1191 ASM_REWRITE_TAC[];
1192 STRIP_TAC;
1193 MP_TAC (REAL_ARITH `&0 < (g:real->real) x ==> ~(g x = &0)`);
1194 ASM_REWRITE_TAC[];
1195 STRIP_TAC;
1196 MP_TAC (SPECL[`(f:real->real) x`;`(g:real->real) x`;] sumsquaresnot0);
1197 ASM_REWRITE_TAC[];
1198 STRIP_TAC;
1199 MP_TAC (SPECL[`g':real`;`(f:real->real) x`;`(g:real->real) x`;`f':real`] notzerodenom2);
1200 ASM_REWRITE_TAC[];
1201 ASM_MESON_TAC[];
1202                                              ]);;
1203
1204 let atn2_deriv_simple3 = prove_by_refinement(`!x pf (f:real->real) f' pg (g:real->real) g' s.  (&0 > g x) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(f x pow 2 + g x pow 2)) x s`,
1205                                              [
1206 REPEAT STRIP_TAC;
1207 MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn2_final_3);
1208 ASM_REWRITE_TAC[];
1209 STRIP_TAC;
1210 MP_TAC (REAL_ARITH `&0 > (g:real->real) x ==> ~(g x = &0)`);
1211 ASM_REWRITE_TAC[];
1212 STRIP_TAC;
1213 MP_TAC (SPECL[`(f:real->real) x`;`(g:real->real) x`;] sumsquaresnot0);
1214 ASM_REWRITE_TAC[];
1215 STRIP_TAC;
1216 MP_TAC (SPECL[`g':real`;`(f:real->real) x`;`(g:real->real) x`;`f':real`] notzerodenom2);
1217 ASM_REWRITE_TAC[];
1218 ASM_MESON_TAC[];
1219                                              ]);;
1220
1221 let atn2_derivative = prove_by_refinement(`!x pf (f:real->real) f' pg (g:real->real) g' s.  (~((g x = &0) /\ (f x <= &0))) /\ derived_form pf f f' x s /\ derived_form pg g g' x s ==> derived_form ((x IN s) /\ (pg /\ pf)) (\x. atn2( f x , g x)) ((g' * f x - g x * f')/(f x pow 2 + g x pow 2)) x s`,
1222                                          [
1223 REPEAT GEN_TAC;
1224 REWRITE_TAC[REAL_ARITH `(~((y = &0) /\ (x <= &0)) <=> (&0 < x) \/ (&0 < y) \/ (&0 > y))`];
1225 REPEAT STRIP_TAC;
1226 MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn2_deriv_simple1);
1227 ASM_MESON_TAC[];
1228 MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn2_deriv_simple2);
1229 ASM_MESON_TAC[];
1230 MP_TAC (SPECL[`x:real`;`pf:bool`;`f:real->real`;`f':real`;`pg:bool`;`g:real->real`;`g':real`;`s:real->bool`] atn2_deriv_simple3);
1231 ASM_MESON_TAC[];
1232                                          ]);;
1233
1234
1235 (* END OF NICK VOLKER'S ATAN2 CODE *)
1236
1237
1238
1239   let atn2curry = new_definition `atn2curry x y = atn2(x,y)`;;
1240
1241   let derived_form_atn2curry = prove_by_refinement(
1242   `!x s. derived_form p1 f1 f1' x s /\ derived_form p2 f2 f2' x s ==> derived_form (p1 /\ p2 /\ (~((f2 x = &0) /\ (f1 x <= &0))) /\ (x IN s))  (\x. atn2curry (f1 x)  (f2 x))   ( (f2' * f1 x - f2 x * f1')/ (f1 x pow 2 + f2 x pow 2)) x s`,
1243   (* {{{ proof *)
1244   [
1245   REWRITE_TAC[atn2curry];
1246   REPEAT STRIP_TAC;
1247   MP_TAC (SPECL [`x:real`;`p1:bool`;`f1:real->real`;`f1':real`;`p2:bool`;`f2:real->real`;`f2':real`;`s:real->bool`] atn2_derivative);
1248   ASM_REWRITE_TAC[];
1249   REWRITE_TAC[derived_form];
1250   ASM_MESON_TAC[];
1251   ]);;
1252   (* }}} *)
1253
1254 (* apply chain only when head is a named constant, sqrt, cos, sin,... *)
1255
1256
1257   let differentiate =
1258     let real_univ = `(:real)` in
1259     let real_ty = `:real` in
1260     let pow  = `(pow)` in
1261     let c = ref 0 in
1262     let get_var() =
1263       let _ = (c:= !c+1) in
1264         mk_var("F"^(string_of_int !c),real_ty) in
1265     let curryl = [atn2curry] in
1266     let uncurry = REWRITE_CONV curryl in
1267     let curry = REWRITE_CONV (map GSYM curryl) in
1268     let binop = [(`( / )`,derived_form_div);(`( * )`,derived_form_mul);
1269                  (`( + )`,derived_form_add); (`( - )`,derived_form_sub);
1270                 (`atn2curry`,derived_form_atn2curry)] in
1271     let unop = [] in
1272     let fns = [((` -- `), derived_form_neg);
1273                (`sin`,derived_form_sin);
1274                (`cos`,derived_form_cos);
1275                (`sqrt`,derived_form_sqrt);
1276                (`inv`,derived_form_inv);
1277                (`acs`,derived_form_acs);
1278                (`asn`,derived_form_asn);
1279                (`atn`,derived_form_atn);
1280               ] in
1281     let rc = clean_conv   in
1282     let check thm = ((* print_thm thm; *) thm) in
1283     let mate f g = try (MATCH_MP f g) with e ->
1284       (
1285         print_string "ERROR: derivative MATCH_MP:\n\n" ;
1286         print_thm f;
1287         print_thm g;
1288         print_string "END ERROR\n";
1289         raise e;
1290       ) in
1291     let clean_derived_form = MESON[]
1292       `derived_form p f f' x s /\ (p = p') /\ (f = tm) /\ (f' = f'') /\ (x = x') /\ (s = s') ==>
1293       derived_form p' tm f'' x' s'` in
1294
1295     let cleanup_derived_form th tm s =
1296       let (_,[p;f;f';x;s']) = strip_comb (concl th) in
1297       let p' = rc p in
1298       let f'' = (rc THENC uncurry) f' in
1299       let tm1 = ((REDEPTH_CONV BETA_CONV) THENC curry) tm in
1300       let f1 = ((REDEPTH_CONV BETA_CONV) THENC curry) f in
1301       let u = try (prove(mk_eq (f,tm),REWRITE_TAC[tm1;f1] THEN MESON_TAC[]))
1302       with _ ->
1303         (print_term tm; print_string" "; print_thm tm1; print_thm f1; failwith "cdfm")  in
1304         mate (clean_derived_form) (end_itlist CONJ [th;p';u;f'';REFL x;REFL s]) in
1305
1306     let rec derivative'  tm x s =
1307       let hyp r = end_itlist CONJ ((map (fun t->derivative' t x s) r)) in
1308       let SPECM xs (dd,msg) =
1309         try SPECL xs dd
1310         with e ->
1311           (
1312             print_string("\n\n unexpected \n"^msg^"\n");
1313             map print_term xs;
1314           raise e ;
1315           ) in
1316
1317       let m r (dd,msg) =
1318         try (
1319           if (r=[]) then SPECL [x;s] dd else (mate (SPECL [x;s] dd) (hyp r))
1320         )
1321         with e -> (
1322           print_string("\n\n unexpected failure on ops\n"^msg^"\n");
1323           map (fun u ->print_term u; print_string "\n") r;
1324           print_thm (SPECL [x;s] dd);
1325           print_string "-------\n\n";
1326           raise e
1327         ) in
1328       let d_fns tm =
1329         let derived_form_fn = assoc tm fns in
1330           (SPECM[x;s] (derived_form_fn,"fns")) in
1331       let d_const tm =
1332         let (v,bod) = dest_abs tm in
1333         let _ = not(mem v (frees bod)) or failwith "constant" in
1334           (SPECM[bod;x;s]  (derived_form_const,"const"))  in
1335       let d_id tm =
1336         let (v,bod) = dest_abs tm in
1337         let _ = (v=bod) or failwith "id" in
1338           (m [] (derived_form_id,"id"))  in
1339       let d_pow tm =
1340         let (v,bod) = dest_abs tm in
1341         let (t,n) = dest_binop pow bod in
1342         let r = mk_abs (v,t) in
1343           (m [r] (SPEC n derived_form_pow,"pow")) in
1344       let d_op tm =
1345         let (v,bod) = dest_abs tm in
1346         let (h,b) = strip_comb bod in
1347           if (List.length b = 1) then
1348             let _ = failwith "no unary ops exist" in
1349             let derived_form_unary = assoc h unop in
1350             let r = mk_abs (v,hd b) in
1351               (m [r] (derived_form_unary,"unary"))
1352           else
1353             let _ = (List.length b = 2) or failwith "not a binary op" in
1354             let [f1;f2] = b in
1355             let derived_form_op = (assoc h binop) in
1356             let r1 = mk_abs (v,f1) in
1357             let r2 = mk_abs (v,f2) in
1358               (m [r1;r2] (derived_form_op,"binary")) in
1359       let d_chain tm =
1360         let (v,bod) = dest_abs tm in
1361         let (h,br) = strip_comb bod in
1362         let _ = List.length br = 1 or failwith "not a chain" in
1363         let fs = mk_abs(v,hd br) in
1364         let r1 = derivative' h (mk_comb (fs,x)) real_univ in
1365         let r2 = derivative' fs x s in
1366 (*      let b1 = ABS v (AP_TERM h (SYM(BETA (mk_comb (fs,v))))) in *)
1367         let f1 =
1368           let  (_,[_;_;_;f1x;_]) = strip_comb (concl r1) in
1369           let (f1,_) = dest_comb f1x in
1370             f1 in
1371         let f2 =
1372           let (_,[_;f2;_;_;_]) = strip_comb(concl r2) in f2 in
1373         let rd = REDEPTH_CONV BETA_CONV in
1374         let b1 = prove(mk_eq(f1,f2),REWRITE_TAC[rd f1;rd f2] THEN MESON_TAC[]) in
1375         let spec = SPECM [x;s] (derived_form_chain,"chain") in
1376           (mate (spec)  (end_itlist CONJ [r1;r2;b1])) in
1377
1378       let d_hyp tm =
1379         SPECM [tm;get_var();x;s] (derived_form_generic,"generic") in
1380
1381         tryfind (fun t ->  check(t tm))  [d_fns;d_const;d_id;d_pow;d_op;d_chain;d_hyp] in
1382
1383       fun tm x s ->
1384         let tm' = rhs (concl (curry tm)) in
1385           cleanup_derived_form  (derivative' tm' x s) tm s;;
1386
1387
1388 (*
1389   let differentiate tm x s =
1390     let th =  (REWRITE_CONV [GSYM atn2curry] tm) in
1391     let tm1 = rhs (concl th) in
1392     let d = differentiate_prelim tm1 x s in
1393     let ans = REWRITE_RULE[SYM th] d in
1394       ans;;
1395 *)
1396
1397
1398 (* Examples *)
1399
1400 (*
1401
1402 let th1 =
1403   let x = `x:real` in
1404   let s = `(:real)` in
1405   let tm = `\x:real. &1` in
1406     differentiate tm x s;;
1407
1408
1409 let th1 =
1410   let x = `x:real` in
1411   let s = `(:real)` in
1412   let tm = `\x:real. x` in
1413     differentiate tm x s;;
1414
1415 let th1 =
1416   let x = `x:real` in
1417   let s = `(:real)` in
1418   let tm = `sin` in
1419     differentiate tm x s;;
1420
1421 let th1 =
1422   let x = `x:real` in
1423   let s = `(:real)` in
1424   let tm = `( -- )` in
1425     differentiate tm x s;;
1426
1427
1428 let th1 =
1429   let x = `x:real` in
1430   let s = `(:real)` in
1431   let tm = `\x. &1 + x` in
1432     differentiate tm x s;;
1433
1434
1435 let th1 =
1436   let x = `x:real` in
1437   let s = `(:real)` in
1438   let tm = `\x. x + &1` in
1439     differentiate tm x s;;
1440
1441 let th1 =
1442   let x = `x:real` in
1443   let s = `(:real)` in
1444   let tm = `\x. -- (x pow 2)` in
1445     differentiate tm x s;;
1446
1447   let th1 =
1448     let x = `x:real` in
1449     let s = `{t | t > &0}` in
1450     let tm = `(\q:real. (q  - sin(q pow 3) + q pow 7 + y)/(q pow 2  + q pow 4 *(&33 + &43 * q)) +  (q pow 3) *  ((q pow 2) / (-- (q pow 3))))` in
1451       time(differentiate tm x) s;;
1452
1453   let th2 =
1454     let x = `x:real` in
1455     let s = `(:real)` in
1456     let tm = `\q.  cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in
1457       time(differentiate tm x) s;;
1458
1459   let th3 =
1460     let x = `r:real` in
1461     let s = `(:real)` in
1462     let tm = `\q.  cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in
1463       time(differentiate tm x) s;;
1464
1465   let th3 =
1466     let x = `t:real` in
1467     let s = `(:real)` in
1468     let tm = `\q.  (\x.  x pow 5 + x* y - cos x) (&1 + q pow 2) ` in
1469       differentiate tm x s;;
1470
1471  let th3 =
1472     let x = `t:real` in
1473     let s = `(:real)` in
1474     let tm = `\q.  (\x.  x pow 5 + &1 - cos x) q` in
1475       differentiate tm x s;;
1476
1477 let th3 =
1478     let x = `t:real` in
1479     let s = `(:real)` in
1480     let tm = `\q.  (\x.  &2 + sin x + &1) q` in
1481       differentiate tm x s;;
1482
1483   let th3 =
1484     let x = `x:real` in
1485     let s = `(:real)` in
1486     let tm = `\q.  ((f:real->real) ((g:real->real) q))  + (g:real->real) q ` in
1487       differentiate tm x s;;
1488
1489 *)
1490
1491 (*
1492 let real_interval_nonempty = prove_by_refinement(
1493   `!a b. (a<=b) ==> ~(real_interval[a,b]={})`,
1494   (* {{{ proof *)
1495   [
1496   REWRITE_TAC[real_interval];
1497    REPEAT GEN_TAC;
1498    DISCH_TAC;
1499    REWRITE_TAC[GSYM MEMBER_NOT_EMPTY;IN_ELIM_THM];
1500    EXISTS_TAC `a:real`;
1501    POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1502   ]);;
1503   (* }}} *)
1504 *)
1505
1506
1507
1508 end;;