(* ========================================================================== *)
(* 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;;