(* Code from Carnegie Library Session with 
   Tom Hales and Nick Volker, August 9, 2011

*)


Trigonometry1.ATN2_BREAKDOWN;;

(* modify Calc_derivative module to remove signature, 
   reload, then open *)

open Calc_derivative;;


let test_aug9_2011 = prove_by_refinement(
  `!x. (x > &0) ==> (?eps. abs(x - eps) > &0)`,
  (* {{{ proof *)
  [
  REPEAT STRIP_TAC;
EXISTS_TAC `x / &2`;
ASM_REAL_ARITH_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[Calc_derivative.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_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 atn2_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[]
  ]);;
  (* }}} *)


(* UNFINISHED
let atn2_derived_form_pos = 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 (pf /\ pg) (\x. atn( g x / f x)) ((g' * f x - g x * f')*inv (f x pow 2 + g x pow 2)) x s`,
  (* {{{ proof *)
  [
REPEAT STRIP_TAC
UNDISCH_TAC `pf ==> (f has_real_derivative f') (atreal x within s)`
UNDISCH_TAC `pg ==> (g has_real_derivative g') (atreal x within s)`
ASM_REWRITE_TAC[]
REPEAT STRIP_TAC
  ]);;
  (* }}} *)

*)

(* UNFINISHED
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))
  ]);;
  (* }}} *)
*)