(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Counting Spheres                                                             *)
(* Chapter: packing                                                           *)
(* Author: Thomas C. Hales                                  *)
(* Date: 2011-06-22                                                           *)
(* ========================================================================== *)

(* Example:
    to put all terms over a common denominator :

   rationalize `-- (v/ u pow 3)/(&1/x  + &3 * (-- (u /( v * inv (w)))))`;;

   To prove a rational identity, modulo accumulated side conditions:

   rational_identity `&1 / (x + y) - &1 / (x - y) = -- &2 * y / (x pow 2 - y pow 2)`;;
*)


(*

  written to automate the calculation of derivatives, with accumulating side conditions.
  It implements --, -, +, *, /, inv, pow, sqrt, sin, cos, atn, asn, acs, chain rule. 

  To recover results without "within" use:

  "WITHINREAL_UNIV", |- !a. atreal x within (:real) = atreal x)

   derived_form p f f' x s   means:
   Under the assumption p, the derivative of the function f evaluated at x, 
   on the interval s
   is equal to the real number f'.

  Apply REWRITE_RULE[derived_form] to express the result back in terms of
  has_real_derivative.

  (* A rational inequality implies a polynomial ineq with
  denominators cleared.  Allowed ops <,>, <=,>=,=,~=,*)

  val rational_ineq_rule  : thm -> thm

*)



(* Example:

To calculate the derivative of tm with respect to q, evaluated at x, on the interval s:

  let th1 = 
    let x = `x:real` in
    let s = `{t | t > &0}` in
    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
      differentiate tm x s;;

*)


module Calc_derivative 

(*: sig

  val ratform : thm
  val rationalize_ratform: term -> thm

  val rationalize: term -> thm
  val rational_identity:term -> thm
  val rational_ineq_rule  : thm -> thm

  val invert_den_lt :thm
  val invert_den_le: thm

  val derived_form:thm
  val differentiate:term -> term -> term -> thm

 end *) = struct


(* ========================================================================== *)
(* RATIONALIZE CONVERSION                                              *)


(*
rationalize puts everything over a common denominator, accumulating
assumptions as it goes.
*)


let ratform  = new_definition `ratform p r a b = (p ==> ~(b = &0) /\ (r = a/b))`;;
let ratform_tac = REWRITE_TAC [ratform] THEN REPEAT STRIP_TAC THENL [ASM_MESON_TAC[REAL_ENTIRE] ; REPEAT (FIRST_X_ASSUM (fun t -> MP_TAC t THEN ANTS_TAC THEN ASM_REWRITE_TAC[])) THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD];;
let REAL_POW_NEQ_0 = 
prove_by_refinement( `!x n. ~(x pow n = &0) <=> ~(x = &0) \/ (n = 0)`,
(* {{{ proof *) [ MESON_TAC[REAL_POW_EQ_0]; ]);;
(* }}} *)
let ratform_pow = 
prove_by_refinement( `ratform p1 r1 a1 b1 ==> ratform p1 (r1 pow n) (a1 pow n) (b1 pow n)`,
(* {{{ proof *) [ REWRITE_TAC[GSYM REAL_POW_DIV;ratform]; MESON_TAC[REAL_POW_NEQ_0;]; ]);;
(* }}} *)
let ratform_add = 
prove_by_refinement( `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2) (r1 + r2) (a1 * b2 + b1 * a2) (b1 * b2)`,
(* {{{ proof *) [ ratform_tac; ]);;
(* }}} *)
let ratform_sub = 
prove_by_refinement( `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2) (r1 - r2) (a1 * b2 - b1 * a2) (b1 * b2)`,
(* {{{ proof *) [ ratform_tac; ]);;
(* }}} *)
let ratform_neg = 
prove_by_refinement( `ratform p1 r1 a1 b1 ==> ratform p1 (-- r1 ) (-- a1 ) (b1)`,
(* {{{ proof *) [ ratform_tac; ]);;
(* }}} *)
let ratform_mul = 
prove_by_refinement( `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2) (r1 * r2) (a1 * a2) (b1 * b2)`,
(* {{{ proof *) [ ratform_tac; ]);;
(* }}} *)
let ratform_div = 
prove_by_refinement( `ratform p1 r1 a1 b1 /\ ratform p2 r2 a2 b2 ==> ratform (p1 /\ p2 /\ ~(a2 = &0)) (r1 / r2) (a1 * b2) (b1 * a2)`,
(* {{{ proof *) [ ratform_tac; ]);;
(* }}} *)
let ratform_inv = 
prove_by_refinement( `ratform p1 r1 a1 b1 ==> ratform (p1 /\ ~(a1= &0)) (inv r1) b1 a1`,
(* {{{ proof *) [ REWRITE_TAC [ratform;]; REPEAT STRIP_TAC; ASM_MESON_TAC[REAL_ENTIRE]; REPEAT (FIRST_X_ASSUM (fun t -> MP_TAC t THEN ANTS_TAC THEN ASM_REWRITE_TAC[])); REPEAT STRIP_TAC; ASM_REWRITE_TAC[REAL_INV_DIV]; ]);;
(* }}} *)
let trivial_ratform = 
prove_by_refinement( `!t. ratform T t t (&1)`,
(* {{{ proof *) [ REWRITE_TAC[ratform]; REAL_ARITH_TAC; ]);;
(* }}} *) let pre_rationalize = let binop_assoc = [(`(+)`,ratform_add); (`( * )`,ratform_mul);(`( - )`,ratform_sub); (`( / )`,ratform_div)] in let unary_assoc = [(` ( -- )`,ratform_neg);(`inv`,ratform_inv)] in let rec pre_rationalize tm = try ( let (x,y) = dest_binop `(pow)` tm in MATCH_MP (INST [y,`n:num`] ratform_pow) (pre_rationalize x) ) with _ -> try ( let h = fst (strip_comb tm) in let bin_th = assoc h binop_assoc in let (x,y) = dest_binop h tm in MATCH_MP bin_th (CONJ (pre_rationalize x) (pre_rationalize y)) ) with _ -> ( try ( let (h,x) = dest_comb tm in let un_th = assoc h unary_assoc in MATCH_MP un_th (pre_rationalize x) ) with _ -> SPEC tm trivial_ratform) in pre_rationalize;; let clean_conv = let ra = REAL_ARITH `&1 * x = x /\ x * &1 = x /\ &0 * x = &0 /\ x * &0 = &0 /\ &0+x = x /\ x + &0 = x /\ x - &0 = x /\ &0 - x = -- x ` in REWRITE_CONV[REAL_POW_NEQ_0;GSYM CONJ_ASSOC; TAUT `~(p \/ q) <=> ~p /\ ~q`; REAL_POW_POW;REAL_POW_1;real_pow;REAL_POW_ONE; REAL_ENTIRE; ra] THENC NUM_REDUCE_CONV;; let dest_ratform rf = snd(strip_comb rf);; let rationalize_ratform = let rc = clean_conv in let clean_ratform = MESON[] `ratform p r a b /\ (p = p') /\ (a = a') /\ (b = b') ==> ratform p' r a' b'` in fun tm -> let pr = pre_rationalize tm in let [p;_;a;b] = dest_ratform (concl pr) in let p' = rc p in let a' = rc a in let b' = rc b in MATCH_MP clean_ratform (end_itlist CONJ [pr;p';a';b']);; let rationalize = REWRITE_RULE[ratform] o rationalize_ratform;; (* example: rationalize `-- (v/ u pow 3)/(&1/x + &3 * (-- (u /( v * inv (w)))))`;; *)
let lite_imp = 
prove_by_refinement( `ratform p (u - v) a b /\ (p = p') /\ (a = &0) ==> (p' ==> (u = v))`,
(* {{{ proof *) [ REWRITE_TAC[ratform]; ASM_MESON_TAC[REAL_ARITH `(u = v) <=> u - v = &0 /b`]; ]);;
(* }}} *)
let lite_imp2 = 
prove_by_refinement( `ratform p (u - v) a b /\ (p = p') /\ (a = a') ==> ((p' /\ (a' = &0)) ==> (u = v))`,
(* {{{ proof *) [ REWRITE_TAC[ratform]; ASM_MESON_TAC[REAL_ARITH `(u = v) <=> u - v = &0 /b`]; ]);;
(* }}} *) let rational_identity = let sub = `( - )` in fun tm -> let (lhs,rhs) = dest_eq tm in let diff = mk_binop sub lhs rhs in let rf = pre_rationalize diff in let [p;_;a;_]=dest_ratform (concl rf) in let p' = clean_conv p in let a' = clean_conv a in try ( let zero = REAL_FIELD (mk_eq (a,`&0`)) in MATCH_MP (lite_imp) (end_itlist CONJ [rf ;p';zero]) ) with _ -> MATCH_MP (lite_imp2) (end_itlist CONJ [rf;p';a']);; let CALC_ID_TAC gl = (MATCH_MP_TAC (rational_identity (goal_concl gl))) gl;;
let invert_den_lt = 
prove_by_refinement( `!a b. &0 < a/b <=> &0 < a*b`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC [real_div]; REWRITE_TAC [REAL_MUL_POS_LT]; REWRITE_TAC [REAL_ARITH `inv x < &0 <=> &0 < -- inv x`]; REWRITE_TAC [GSYM REAL_INV_NEG]; REWRITE_TAC [REAL_LT_INV_EQ]; REAL_ARITH_TAC ]);;
(* }}} *)
let invert_den_le = 
prove_by_refinement( `!a b. &0 <= a/b <=> &0 <= a*b`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC [real_div]; REWRITE_TAC [REAL_MUL_POS_LE]; REWRITE_TAC [REAL_ARITH `inv x < &0 <=> &0 < -- inv x`]; REWRITE_TAC [GSYM REAL_INV_NEG]; REWRITE_TAC [REAL_LT_INV_EQ;Real_ext.REAL_PROP_ZERO_INV]; REAL_ARITH_TAC ]);;
(* }}} *)
let invert_den_eq = 
prove_by_refinement( `!a b. (a/b = &0) <=> ( a*b = &0)`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC [real_div]; REWRITE_TAC [REAL_ENTIRE]; REWRITE_TAC [REAL_LT_INV_EQ;Real_ext.REAL_PROP_ZERO_INV]; ]);;
(* }}} *)
let imp_lt = 
prove_by_refinement( `!p p' x a a' b b'. (&0 < x) /\ (ratform p x a b) /\ (p = p') /\ (a = a') /\ (b = b') ==> (p' ==> &0 < a' * b')`,
(* {{{ proof *) [ REWRITE_TAC [ratform]; REPEAT STRIP_TAC ; ASM_MESON_TAC [invert_den_lt] ]);;
(* }}} *)
let imp_le = 
prove_by_refinement( `!p p' x a a' b b'. (&0 <= x) /\ (ratform p x a b) /\ (p = p') /\ (a = a') /\ (b = b') ==> (p' ==> &0 <= a' * b')`,
(* {{{ proof *) [ REWRITE_TAC [ratform]; REPEAT STRIP_TAC ; ASM_MESON_TAC [invert_den_le] ]);;
(* }}} *)
let imp_eq = 
prove_by_refinement( `!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 ))`,
(* {{{ proof *) [ REWRITE_TAC [ratform]; REPEAT STRIP_TAC ; ASM_MESON_TAC [invert_den_eq;REAL_ENTIRE] ]);;
(* }}} *)
let imp_nz = 
prove_by_refinement( `!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)))`,
(* {{{ proof *) [ REWRITE_TAC [ratform]; REPEAT STRIP_TAC THEN ASM_MESON_TAC [invert_den_eq;REAL_ENTIRE] ]);;
(* }}} *) let dest_nz = let neg = `(~)` in fun tm -> let (a,b) = dest_comb tm in let _ = (a = neg) or failwith "not a negation" in dest_eq b;; (* clear the denominator of an inequality *) let rational_ineq_rule = let lt = `(<)` in let le = `(<=)` in let ra1 = REAL_ARITH `a < b <=> &0 < b - a` in let ra2 = REAL_ARITH `a <= b <=> &0 <= b - a` in let ra3 = REAL_ARITH `(x = y) <=> (x - y = &0)` in let ineq_types = [snd o (dest_binop lt ), imp_lt; snd o (dest_binop le ), imp_le; fst o (dest_eq ), imp_eq; fst o (dest_nz), imp_nz] in fun thm -> let thm' = REWRITE_RULE[real_gt;real_ge] thm in let thm' = ONCE_REWRITE_RULE [ra1] thm' in let thm' = ONCE_REWRITE_RULE [ra2] thm' in let thm' = ONCE_REWRITE_RULE [ra3] thm' in let (diff,imp) = tryfind (fun (d,imp) -> (d(concl thm'),imp)) ineq_types in let rf = pre_rationalize diff in let [p;_;a;b]=dest_ratform (concl rf) in let p' = clean_conv p in let a' = clean_conv a in let b' = clean_conv b in let thm' = MATCH_MP (imp) (end_itlist CONJ [thm';rf ;p';a';b']) in thm';; (* Example: rational_identity `(&1 / u - &1/v) pow 2 = inv u pow 2 - &2 * inv (u * v) + inv v pow 2`;; rational_identity `&1 / (x + y) - &1 / (x - y) = -- &2 * y / (x pow 2 - y pow 2)`;; rational_ineq_rule (ASSUME `a / (b * e) < c / (&2 * b)`);; *) (* ========================================================================== *) (* DERIV FORM *)
let derived_form = new_definition
    `derived_form p f f' x s = (p ==> (f has_real_derivative f') (atreal x within s))`;;
let deriv_tac = REWRITE_TAC[derived_form] THEN (* REPEAT GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN *) REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST (map MATCH_MP_TAC [ HAS_REAL_DERIVATIVE_ADD; HAS_REAL_DERIVATIVE_SUB; HAS_REAL_DERIVATIVE_MUL_ATREAL; HAS_REAL_DERIVATIVE_MUL_WITHIN; HAS_REAL_DERIVATIVE_DIV_ATREAL; HAS_REAL_DERIVATIVE_DIV_WITHIN; HAS_REAL_DERIVATIVE_NEG; HAS_REAL_DERIVATIVE_POW_WITHIN; HAS_REAL_DERIVATIVE_POW_ATREAL ]) THEN ASM_MESON_TAC[];; (* OLD u versions: let derived_form_add = prove_by_refinement( `!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`, (* {{{ proof *) [ deriv_tac; ]);; (* }}} *)
let derived_form_sub = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_mul = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_div = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_neg = 
prove_by_refinement( `!x s. derived_form p1 f1 f1' x s /\ (u = (\x. -- f1 x)) ==> derived_form p1 u (-- f1') x s`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_pow = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *) let deriv_fn_tac = REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[derived_form] THEN (* COND_CASES_TAC THEN *) ASM_MESON_TAC[ HAS_REAL_DERIVATIVE_CONST; HAS_REAL_DERIVATIVE_ATREAL_WITHIN; HAS_REAL_DERIVATIVE_SIN; HAS_REAL_DERIVATIVE_COS; HAS_REAL_DERIVATIVE_SQRT; HAS_REAL_DERIVATIVE_ATN; HAS_REAL_DERIVATIVE_ACS; HAS_REAL_DERIVATIVE_ASN; HAS_REAL_DERIVATIVE_INV_BASIC; ];;
let derived_form_const = 
prove_by_refinement( `!x s. (u = \x. c) ==> derived_form T u (&0) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_sin = 
prove_by_refinement( `!x s. derived_form T sin (cos x) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_cos = 
prove_by_refinement( `!x s. derived_form T cos (-- sin x) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_sqrt = 
prove_by_refinement( `!x s. derived_form (&0 < x) sqrt (inv (&2 * sqrt x)) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_atn = 
prove_by_refinement( `!x s. derived_form T atn (inv (&1 + x pow 2)) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_acs = 
prove_by_refinement( `!x s. derived_form (abs x < &1) acs (-- inv (sqrt(&1 - x pow 2))) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_asn = 
prove_by_refinement( `!x s. derived_form (abs x < &1) asn ( inv (sqrt(&1 - x pow 2))) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_inv = 
prove_by_refinement( `!x s. derived_form (~(x = &0)) inv (-- inv (x pow 2)) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_id = 
prove_by_refinement( `!x s. (u = (\x. x)) ==>derived_form T u (&1) x s`,
(* {{{ proof *) [ REPEAT STRIP_TAC; ASM_REWRITE_TAC[derived_form;HAS_REAL_DERIVATIVE_ID]; ]);;
(* }}} *)
let derived_form_chain = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; 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)); ANTS_TAC; GEN_TAC; BETA_TAC; ASM_MESON_TAC[WITHINREAL_UNIV]; REPEAT (POP_ASSUM MP_TAC); (* *) ASM_MESON_TAC[]; ]);;
(* }}} *) *) (* REDO *)
let derived_form_add = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_sub = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_mul = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *)
let derived_form_div = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *) (* moved to function section. let derived_form_neg = prove_by_refinement( `!x s. derived_form p1 f1 f1' x s ==> derived_form p1 (\x. -- f1 x) (-- f1') x s`, (* {{{ proof *) [ deriv_tac; ]);; (* }}} *) *)
let derived_form_pow = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ deriv_tac; ]);;
(* }}} *) let deriv_fn_tac = REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[derived_form] THEN (* COND_CASES_TAC THEN *) ASM_MESON_TAC[ HAS_REAL_DERIVATIVE_CONST; HAS_REAL_DERIVATIVE_ATREAL_WITHIN; HAS_REAL_DERIVATIVE_SIN; HAS_REAL_DERIVATIVE_COS; HAS_REAL_DERIVATIVE_SQRT; HAS_REAL_DERIVATIVE_ATN; HAS_REAL_DERIVATIVE_ACS; HAS_REAL_DERIVATIVE_ASN; HAS_REAL_DERIVATIVE_INV_BASIC; ];;
let derived_form_neg = 
prove_by_refinement( `!x s. derived_form T ( -- ) (-- &1) x s`,
(* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[derived_form]; SUBGOAL_THEN `( -- ) = (\x. --x)` SUBST1_TAC; MATCH_MP_TAC EQ_EXT; MESON_TAC[]; BETA_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG; REWRITE_TAC[HAS_REAL_DERIVATIVE_ID]; ]);;
(* }}} *)
let derived_form_const = 
prove_by_refinement( `!c x s. derived_form T (\x. c) (&0) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_sin = 
prove_by_refinement( `!x s. derived_form T sin (cos x) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_cos = 
prove_by_refinement( `!x s. derived_form T cos (-- sin x) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_sqrt = 
prove_by_refinement( `!x s. derived_form (&0 < x) sqrt (inv (&2 * sqrt x)) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_atn = 
prove_by_refinement( `!x s. derived_form T atn (inv (&1 + x pow 2)) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_acs = 
prove_by_refinement( `!x s. derived_form (abs x < &1) acs (-- inv (sqrt(&1 - x pow 2))) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_asn = 
prove_by_refinement( `!x s. derived_form (abs x < &1) asn ( inv (sqrt(&1 - x pow 2))) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_inv = 
prove_by_refinement( `!x s. derived_form (~(x = &0)) inv (-- inv (x pow 2)) x s`,
(* {{{ proof *) [ deriv_fn_tac; ]);;
(* }}} *)
let derived_form_id = 
prove_by_refinement( `!x s. derived_form T (\x. x) (&1) x s`,
(* {{{ proof *) [ REPEAT STRIP_TAC; ASM_REWRITE_TAC[derived_form;HAS_REAL_DERIVATIVE_ID]; ]);;
(* }}} *)
let derived_form_chain = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; 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)); ANTS_TAC; GEN_TAC; BETA_TAC; ASM_MESON_TAC[WITHINREAL_UNIV]; REPEAT (POP_ASSUM MP_TAC); (* *) ASM_MESON_TAC[]; ]);;
(* }}} *)
let derived_form_generic = 
prove_by_refinement( `!f f' x s. derived_form (derived_form T f (f') x s) f (f') x s`,
(* {{{ proof *) [ REWRITE_TAC[derived_form]; ]);;
(* START OF NICK VOLKER'S CODE *)
let region_conv = 
prove_by_refinement( `!(x:real) (y:real). ~(y = &0 /\ x <= &0) ==> (x > &0) \/ (y < &0) \/ (y > &0)`,
(* {{{ proof *) [ REAL_ARITH_TAC; ]);;
let x2notless0 = 
prove_by_refinement(`!x:real. ~(x pow 2 < &0)`,
[ STRIP_TAC; SUBGOAL_THEN `x = &0 ==> ~(x pow 2 < &0)` MP_TAC; STRIP_TAC; MP_TAC (SPECL[`x:real`] Trigonometry2.POW2_EQ_0); ASM_REWRITE_TAC[]; REAL_ARITH_TAC; SUBGOAL_THEN `~(x = &0) ==> ~(x pow 2 < &0)` MP_TAC; STRIP_TAC; MP_TAC (SPECL[`x:real`] (GENL[`a:real`] Trigonometry2.NOT_ZERO_EQ_POW2_LT)); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (REAL_FIELD `&0 < x pow 2 ==> ~(x pow 2 < &0)`); ASM_MESON_TAC[]; ASM_MESON_TAC[]; ]);;
let x2notlesseq0 = 
prove_by_refinement(`!x:real. ~(x = &0) ==> ~(x pow 2 <= &0)`,
[ STRIP_TAC; STRIP_TAC; MP_TAC (SPECL[`x:real`] (GENL[`a:real`] Trigonometry2.NOT_ZERO_EQ_POW2_LT)); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (REAL_FIELD `&0 < x pow 2 ==> ~(x pow 2 <= &0)`); ASM_MESON_TAC[]; ]);;
let sumsquaresnot0 = 
prove_by_refinement(`!x:real y:real. ~(x = &0) ==> ~(x pow 2 + y pow 2 <= &0)`,
[ STRIP_TAC; STRIP_TAC; STRIP_TAC; MP_TAC (SPECL[`x:real`] x2notlesseq0); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`y:real`] x2notless0); STRIP_TAC; MP_TAC (REAL_ARITH `~(x pow 2 <= &0) /\ ~(y pow 2 < &0) ==> ~(x pow 2 + y pow 2 <= &0)`); ASM_MESON_TAC[]; ]);;
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))`,
[ REPEAT STRIP_TAC; MP_TAC (SPECL [`b:real`;`c:real`] sumsquaresnot0); ASM_REWRITE_TAC[]; STRIP_TAC; 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)`); ASM_MESON_TAC[]; ]);;
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))`,
[ REPEAT STRIP_TAC; MP_TAC (SPECL [`c:real`;`b:real`] sumsquaresnot0); ASM_REWRITE_TAC[]; STRIP_TAC; 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)`); ASM_MESON_TAC[]; ]);;
let derived_imp_pos_open = 
prove_by_refinement( `!p f f' x s. p /\ derived_form p f f' x s /\ &0 < f x ==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 < f x'))`,
(* {{{ proof *) [ REWRITE_TAC[derived_form]; REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`]; REPEAT STRIP_TAC; FIRST_X_ASSUM (MP_TAC o ( MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL )); REWRITE_TAC[real_continuous_withinreal]; DISCH_THEN (MP_TAC o (SPEC `(f:real->real) x`)); ASM_REWRITE_TAC[]; STRIP_TAC; EXISTS_TAC `d:real`; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`)); ASM_REWRITE_TAC[]; ASM_REAL_ARITH_TAC; ]);;
let derived_imp_pos_open_2 = 
prove_by_refinement( `!p g g' x s. p /\ derived_form p g g' x s /\ &0 < g x ==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 < g x'))`,
(* {{{ proof *) [ REWRITE_TAC[derived_form]; REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`]; REPEAT STRIP_TAC; FIRST_X_ASSUM (MP_TAC o ( MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL )); REWRITE_TAC[real_continuous_withinreal]; DISCH_THEN (MP_TAC o (SPEC `(g:real->real) x`)); ASM_REWRITE_TAC[]; STRIP_TAC; EXISTS_TAC `d:real`; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`)); ASM_REWRITE_TAC[]; ASM_REAL_ARITH_TAC; ]);;
let derived_imp_pos_open_3 = 
prove_by_refinement( `!p g g' x s. p /\ derived_form p g g' x s /\ &0 > g x==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 > g x' ))`,
(* {{{ proof *) [ REWRITE_TAC[REAL_ARITH ` &0 > g x <=> &0 < --(g x)`]; REWRITE_TAC[derived_form]; REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`]; REPEAT STRIP_TAC; FIRST_X_ASSUM (MP_TAC o ( MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL )); REWRITE_TAC[real_continuous_withinreal]; DISCH_THEN (MP_TAC o (SPEC `--(g:real->real) x`)); ASM_REWRITE_TAC[]; STRIP_TAC; EXISTS_TAC `d:real`; ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`)); ASM_REWRITE_TAC[]; ASM_REAL_ARITH_TAC; ]);;
let deriv_pi = 
prove_by_refinement( `!(x:real) s. derived_form T (\x. (pi / &2)) (&0) x s`,
[ MP_TAC (SPECL [`(pi / &2)`] derived_form_const); ASM_MESON_TAC[]; ]);;
let deriv_pi_minus = 
prove_by_refinement( `!(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`,
[ REPEAT GEN_TAC; MP_TAC (SPECL[`x:real`;`s:real->bool`] deriv_pi); REPEAT STRIP_TAC; MATCH_MP_TAC derived_form_sub; ASM_MESON_TAC[]; ]);;
let deriv_minus_pi = 
prove_by_refinement( `!(x:real) s. derived_form T (\x. --(pi / &2)) (&0) x s`,
[ MP_TAC (SPECL [`--(pi / &2)`] derived_form_const); ASM_MESON_TAC[]; ]);;
let deriv_minus_pi_minus = 
prove_by_refinement( `!(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`,
[ REPEAT GEN_TAC; MP_TAC (SPECL[`x:real`;`s:real->bool`] deriv_minus_pi); REPEAT STRIP_TAC; MATCH_MP_TAC derived_form_sub; ASM_MESON_TAC[]; ]);;
let derived_form_chain_simple = 
prove_by_refinement( `!x s g g' f f' p p'. derived_form p g g' (f x) (:real) /\ derived_form p' f f' x s ==> derived_form (p /\ p') (\x. g (f x)) (f' * g') x s`,
(* {{{ proof *) [ MESON_TAC[derived_form_chain] ]);;
let atn_lemma = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ REPEAT STRIP_TAC; MATCH_MP_TAC derived_form_chain_simple; REWRITE_TAC[derived_form_atn]; MP_TAC (REAL_ARITH `&0 < (f:real->real) x ==> ~(f x = &0)`); 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; MATCH_MP_TAC derived_form_div; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[] ]);;
let atn_notpi_lemma = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ REPEAT STRIP_TAC; MATCH_MP_TAC derived_form_chain_simple; REWRITE_TAC[derived_form_atn]; MP_TAC (REAL_ARITH `&0 < (g:real->real) x ==> ~(g x = &0)`); 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; MATCH_MP_TAC derived_form_div; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[] ]);;
let atn_notnegpi_lemma = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ REPEAT STRIP_TAC; MATCH_MP_TAC derived_form_chain_simple; REWRITE_TAC[derived_form_atn]; MP_TAC (REAL_ARITH `&0 > (g:real->real) x ==> ~(g x = &0)`); 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; MATCH_MP_TAC derived_form_div; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[] ]);;
let atn_lemma_2 = 
prove_by_refinement ( `!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`,
[ REPEAT STRIP_TAC; 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); ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; 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)); (*REWRITE_TAC[REAL_ARITH `(&0 - (a*d -b*c))/u*v = (c*b - d*a)/u*v`]; *) UNDISCH_TAC `derived_form pf f f' x s`; UNDISCH_TAC `derived_form pg g g' x s`; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; SUBGOAL_THEN `((\x. pi / &2 - atn (f x / g x)) has_real_derivative &0 - (f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2)) (atreal x within s)` MP_TAC; ASM_MESON_TAC[]; 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; REPEAT STRIP_TAC; REAL_ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[]; ]);;
let atn_lemma_3 = 
prove_by_refinement ( `!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`,
[ REPEAT STRIP_TAC; 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); ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; 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)); (*REWRITE_TAC[REAL_ARITH `(&0 - (a*d -b*c))/u*v = (c*b - d*a)/u*v`]; *) UNDISCH_TAC `derived_form pf f f' x s`; UNDISCH_TAC `derived_form pg g g' x s`; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; SUBGOAL_THEN `((\x. --(pi / &2) - atn (f x / g x)) has_real_derivative &0 - (f' * g x - f x * g') / g x pow 2 * inv (&1 + (f x / g x) pow 2)) (atreal x within s)` MP_TAC; ASM_MESON_TAC[]; 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; REPEAT STRIP_TAC; REAL_ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[]; ]);;
let atn2_atn_open = 
prove_by_refinement( `!p f f' g x s. p /\ derived_form p f f' x s /\ (&0 < f x)==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> atn2 (f x', g x') = atn(g x' / f x')))`,
(* {{{ proof *) [ (REPEAT GEN_TAC); (DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open))); (REPEAT STRIP_TAC); (EXISTS_TAC `d:real`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (SUBGOAL_THEN `&0 < ((f:real->real) x')` MP_TAC); (ASM_MESON_TAC[]); (MP_TAC (MATCH_MP (TAUT `a /\ b /\ c /\ d ==> a`) (SPECL [`((f:real->real) x')`;`((g:real->real) x')`] Trigonometry1.ATN2_BREAKDOWN))); (REPEAT STRIP_TAC); ]);;
let atn2_atn_open_2 = 
prove_by_refinement( `!p g g' f x s. p /\ derived_form p g g' x s /\ (&0 < g x)==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> atn2 (f x', g x') = (pi / &2 - atn(f x' / g x'))))`,
(* {{{ proof *) [ (REPEAT GEN_TAC); (DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open))); (REPEAT STRIP_TAC); (EXISTS_TAC `d:real`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (SUBGOAL_THEN `&0 < ((g:real->real) x')` MP_TAC); (ASM_MESON_TAC[]); (MP_TAC (MATCH_MP (TAUT `a /\ b /\ c /\ d ==> b`) (SPECL [`((f:real->real) x')`;`((g:real->real) x')`] Trigonometry1.ATN2_BREAKDOWN))); (REPEAT STRIP_TAC); ]);;
let atn2_atn_open_3 = 
prove_by_refinement( `!p g g' f x s. p /\ derived_form p g g' x s /\ (&0 > g x)==> (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> atn2 (f x', g x') = (--(pi / &2) - atn(f x' / g x'))))`,
(* {{{ proof *) [ (REPEAT GEN_TAC); (DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open_3))); (REPEAT STRIP_TAC); (EXISTS_TAC `d:real`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (SUBGOAL_THEN `&0 > ((g:real->real) x')` MP_TAC); (ASM_MESON_TAC[]); (REWRITE_TAC[REAL_ARITH `a > b <=> b < a`]); (MP_TAC (MATCH_MP (TAUT `a /\ b /\ c /\ d ==> c`) (SPECL [`((f:real->real) x')`;`((g:real->real) x')`] Trigonometry1.ATN2_BREAKDOWN))); (REPEAT STRIP_TAC); ]);;
(*//////////////////////////////////*)
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`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; SUBGOAL_THEN `pf /\ derived_form pf f f' x s /\ (&0 < (f:real->real) x)` MP_TAC; REWRITE_TAC[derived_form]; ASM_MESON_TAC[]; DISCH_THEN (MP_TAC o (MATCH_MP atn2_atn_open)); STRIP_TAC; 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; MP_TAC atn_lemma; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; ASM_MESON_TAC[]; REWRITE_TAC[derived_form]; STRIP_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN; ASM_MESON_TAC[]; ]);;
let atn2_final_2 = 
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')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
[ REPEAT GEN_TAC; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; SUBGOAL_THEN `pg /\ derived_form pg g g' x s /\ (&0 < (g:real->real) x)` MP_TAC; REWRITE_TAC[derived_form]; ASM_MESON_TAC[]; DISCH_THEN (MP_TAC o (MATCH_MP atn2_atn_open_2)); STRIP_TAC; 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; MP_TAC atn_lemma_2; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; ASM_MESON_TAC[]; REWRITE_TAC[derived_form]; STRIP_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN; ASM_MESON_TAC[]; ]);;
let atn2_final_3 = 
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')/(g x pow 2) *inv (&1 + (f x / g x) pow 2)) x s`,
[ REPEAT GEN_TAC; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; SUBGOAL_THEN `pg /\ derived_form pg g g' x s /\ (&0 > (g:real->real) x)` MP_TAC; REWRITE_TAC[derived_form]; ASM_MESON_TAC[]; DISCH_THEN (MP_TAC o (MATCH_MP atn2_atn_open_3)); STRIP_TAC; 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; MP_TAC atn_lemma_3; REWRITE_TAC[derived_form]; REPEAT STRIP_TAC; ASM_MESON_TAC[]; REWRITE_TAC[derived_form]; STRIP_TAC; MATCH_MP_TAC HAS_REAL_DERIVATIVE_TRANSFORM_WITHIN; ASM_MESON_TAC[]; ]);;
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`,
[ REPEAT STRIP_TAC; 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); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (REAL_ARITH `&0 < (f:real->real) x ==> ~(f x = &0)`); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`(f:real->real) x`;`(g:real->real) x`;] sumsquaresnot0); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`g':real`;`(f:real->real) x`;`(g:real->real) x`;`f':real`] notzerodenom); ASM_REWRITE_TAC[]; ASM_MESON_TAC[]; ]);;
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`,
[ REPEAT STRIP_TAC; 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); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (REAL_ARITH `&0 < (g:real->real) x ==> ~(g x = &0)`); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`(f:real->real) x`;`(g:real->real) x`;] sumsquaresnot0); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`g':real`;`(f:real->real) x`;`(g:real->real) x`;`f':real`] notzerodenom2); ASM_REWRITE_TAC[]; ASM_MESON_TAC[]; ]);;
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`,
[ REPEAT STRIP_TAC; 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); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (REAL_ARITH `&0 > (g:real->real) x ==> ~(g x = &0)`); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`(f:real->real) x`;`(g:real->real) x`;] sumsquaresnot0); ASM_REWRITE_TAC[]; STRIP_TAC; MP_TAC (SPECL[`g':real`;`(f:real->real) x`;`(g:real->real) x`;`f':real`] notzerodenom2); ASM_REWRITE_TAC[]; ASM_MESON_TAC[]; ]);;
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`,
[ REPEAT GEN_TAC; REWRITE_TAC[REAL_ARITH `(~((y = &0) /\ (x <= &0)) <=> (&0 < x) \/ (&0 < y) \/ (&0 > y))`]; REPEAT STRIP_TAC; 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); ASM_MESON_TAC[]; 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); ASM_MESON_TAC[]; 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); ASM_MESON_TAC[]; ]);;
(* END OF NICK VOLKER'S ATAN2 CODE *)
let atn2curry = new_definition `atn2curry x y = atn2(x,y)`;;
let derived_form_atn2curry = 
prove_by_refinement( `!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`,
(* {{{ proof *) [ REWRITE_TAC[atn2curry]; REPEAT STRIP_TAC; MP_TAC (SPECL [`x:real`;`p1:bool`;`f1:real->real`;`f1':real`;`p2:bool`;`f2:real->real`;`f2':real`;`s:real->bool`] atn2_derivative); ASM_REWRITE_TAC[]; REWRITE_TAC[derived_form]; ASM_MESON_TAC[]; ]);;
(* }}} *) (* apply chain only when head is a named constant, sqrt, cos, sin,... *) let differentiate = let real_univ = `(:real)` in let real_ty = `:real` in let pow = `(pow)` in let c = ref 0 in let get_var() = let _ = (c:= !c+1) in mk_var("F"^(string_of_int !c),real_ty) in let curryl = [atn2curry] in let uncurry = REWRITE_CONV curryl in let curry = REWRITE_CONV (map GSYM curryl) in let binop = [(`( / )`,derived_form_div);(`( * )`,derived_form_mul); (`( + )`,derived_form_add); (`( - )`,derived_form_sub); (`atn2curry`,derived_form_atn2curry)] in let unop = [] in let fns = [((` -- `), derived_form_neg); (`sin`,derived_form_sin); (`cos`,derived_form_cos); (`sqrt`,derived_form_sqrt); (`inv`,derived_form_inv); (`acs`,derived_form_acs); (`asn`,derived_form_asn); (`atn`,derived_form_atn); ] in let rc = clean_conv in let check thm = ((* print_thm thm; *) thm) in let mate f g = try (MATCH_MP f g) with e -> ( print_string "ERROR: derivative MATCH_MP:\n\n" ; print_thm f; print_thm g; print_string "END ERROR\n"; raise e; ) in let clean_derived_form = MESON[] `derived_form p f f' x s /\ (p = p') /\ (f = tm) /\ (f' = f'') /\ (x = x') /\ (s = s') ==> derived_form p' tm f'' x' s'` in let cleanup_derived_form th tm s = let (_,[p;f;f';x;s']) = strip_comb (concl th) in let p' = rc p in let f'' = (rc THENC uncurry) f' in let tm1 = ((REDEPTH_CONV BETA_CONV) THENC curry) tm in let f1 = ((REDEPTH_CONV BETA_CONV) THENC curry) f in let u = try (prove(mk_eq (f,tm),REWRITE_TAC[tm1;f1] THEN MESON_TAC[])) with _ -> (print_term tm; print_string" "; print_thm tm1; print_thm f1; failwith "cdfm") in mate (clean_derived_form) (end_itlist CONJ [th;p';u;f'';REFL x;REFL s]) in let rec derivative' tm x s = let hyp r = end_itlist CONJ ((map (fun t->derivative' t x s) r)) in let SPECM xs (dd,msg) = try SPECL xs dd with e -> ( print_string("\n\n unexpected \n"^msg^"\n"); map print_term xs; raise e ; ) in let m r (dd,msg) = try ( if (r=[]) then SPECL [x;s] dd else (mate (SPECL [x;s] dd) (hyp r)) ) with e -> ( print_string("\n\n unexpected failure on ops\n"^msg^"\n"); map (fun u ->print_term u; print_string "\n") r; print_thm (SPECL [x;s] dd); print_string "-------\n\n"; raise e ) in let d_fns tm = let derived_form_fn = assoc tm fns in (SPECM[x;s] (derived_form_fn,"fns")) in let d_const tm = let (v,bod) = dest_abs tm in let _ = not(mem v (frees bod)) or failwith "constant" in (SPECM[bod;x;s] (derived_form_const,"const")) in let d_id tm = let (v,bod) = dest_abs tm in let _ = (v=bod) or failwith "id" in (m [] (derived_form_id,"id")) in let d_pow tm = let (v,bod) = dest_abs tm in let (t,n) = dest_binop pow bod in let r = mk_abs (v,t) in (m [r] (SPEC n derived_form_pow,"pow")) in let d_op tm = let (v,bod) = dest_abs tm in let (h,b) = strip_comb bod in if (List.length b = 1) then let _ = failwith "no unary ops exist" in let derived_form_unary = assoc h unop in let r = mk_abs (v,hd b) in (m [r] (derived_form_unary,"unary")) else let _ = (List.length b = 2) or failwith "not a binary op" in let [f1;f2] = b in let derived_form_op = (assoc h binop) in let r1 = mk_abs (v,f1) in let r2 = mk_abs (v,f2) in (m [r1;r2] (derived_form_op,"binary")) in let d_chain tm = let (v,bod) = dest_abs tm in let (h,br) = strip_comb bod in let _ = List.length br = 1 or failwith "not a chain" in let fs = mk_abs(v,hd br) in let r1 = derivative' h (mk_comb (fs,x)) real_univ in let r2 = derivative' fs x s in (* let b1 = ABS v (AP_TERM h (SYM(BETA (mk_comb (fs,v))))) in *) let f1 = let (_,[_;_;_;f1x;_]) = strip_comb (concl r1) in let (f1,_) = dest_comb f1x in f1 in let f2 = let (_,[_;f2;_;_;_]) = strip_comb(concl r2) in f2 in let rd = REDEPTH_CONV BETA_CONV in
let b1 = prove(mk_eq(f1,f2),REWRITE_TAC[rd f1;rd f2] THEN MESON_TAC[]) in
	let spec = SPECM [x;s] (derived_form_chain,"chain") in
	  (mate (spec)  (end_itlist CONJ [r1;r2;b1])) in
 
      let d_hyp tm = 
	SPECM [tm;get_var();x;s] (derived_form_generic,"generic") in

	tryfind (fun t ->  check(t tm))  [d_fns;d_const;d_id;d_pow;d_op;d_chain;d_hyp] in
      
      fun tm x s -> 
	let tm' = rhs (concl (curry tm)) in
	  cleanup_derived_form  (derivative' tm' x s) tm s;;
(* let differentiate tm x s = let th = (REWRITE_CONV [GSYM atn2curry] tm) in let tm1 = rhs (concl th) in let d = differentiate_prelim tm1 x s in let ans = REWRITE_RULE[SYM th] d in ans;; *) (* Examples *) (* let th1 = let x = `x:real` in let s = `(:real)` in let tm = `\x:real. &1` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `(:real)` in let tm = `\x:real. x` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `(:real)` in let tm = `sin` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `(:real)` in let tm = `( -- )` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `(:real)` in let tm = `\x. &1 + x` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `(:real)` in let tm = `\x. x + &1` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `(:real)` in let tm = `\x. -- (x pow 2)` in differentiate tm x s;; let th1 = let x = `x:real` in let s = `{t | t > &0}` in 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 time(differentiate tm x) s;; let th2 = let x = `x:real` in let s = `(:real)` in let tm = `\q. cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in time(differentiate tm x) s;; let th3 = let x = `r:real` in let s = `(:real)` in let tm = `\q. cos(&1 + q pow 2) * acs (q pow 4) + atn(cos q) + inv (q + &1)` in time(differentiate tm x) s;; let th3 = let x = `t:real` in let s = `(:real)` in let tm = `\q. (\x. x pow 5 + x* y - cos x) (&1 + q pow 2) ` in differentiate tm x s;; let th3 = let x = `t:real` in let s = `(:real)` in let tm = `\q. (\x. x pow 5 + &1 - cos x) q` in differentiate tm x s;; let th3 = let x = `t:real` in let s = `(:real)` in let tm = `\q. (\x. &2 + sin x + &1) q` in differentiate tm x s;; let th3 = let x = `x:real` in let s = `(:real)` in let tm = `\q. ((f:real->real) ((g:real->real) q)) + (g:real->real) q ` in differentiate tm x s;; *) (* let real_interval_nonempty = prove_by_refinement( `!a b. (a<=b) ==> ~(real_interval[a,b]={})`, (* {{{ proof *) [ REWRITE_TAC[real_interval]; REPEAT GEN_TAC; DISCH_TAC; REWRITE_TAC[GSYM MEMBER_NOT_EMPTY;IN_ELIM_THM]; EXISTS_TAC `a:real`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);; (* }}} *) *) end;;