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