1 (* Code from Carnegie Library Session with
2 Tom Hales and Nick Volker, August 9, 2011
7 Trigonometry1.ATN2_BREAKDOWN;;
9 (* modify Calc_derivative module to remove signature,
12 open Calc_derivative;;
15 let test_aug9_2011 = prove_by_refinement(
16 `!x. (x > &0) ==> (?eps. abs(x - eps) > &0)`,
25 let derived_imp_pos_open = prove_by_refinement(
26 `!p f f' x s. p /\ derived_form p f f' x s /\ &0 < f x ==>
27 (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==> &0 < f x'))`,
30 REWRITE_TAC[Calc_derivative.derived_form];
31 REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`];
33 FIRST_X_ASSUM (MP_TAC o ( MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_WITHINREAL ));
34 REWRITE_TAC[real_continuous_withinreal];
35 DISCH_THEN (MP_TAC o (SPEC `(f:real->real) x`));
41 FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`));
48 let derived_form_chain_simple = prove_by_refinement(
50 derived_form p g g' (f x) (:real) /\
51 derived_form p' f f' x s
52 ==> derived_form (p /\ p') (\x. g (f x)) (f' * g') x s`,
55 MESON_TAC[derived_form_chain]
59 let atn2_lemma = prove_by_refinement(
60 `!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`,
64 MATCH_MP_TAC derived_form_chain_simple;
65 REWRITE_TAC[derived_form_atn];
66 MP_TAC (REAL_ARITH `&0 < (f:real->real) x ==> ~(f x = &0)`);
67 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;
68 MATCH_MP_TAC derived_form_div;
70 ASM_REWRITE_TAC[derived_form];
72 FIRST_X_ASSUM MATCH_MP_TAC;
79 let atn2_derived_form_pos = prove_by_refinement(
80 `!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`,
84 UNDISCH_TAC `pf ==> (f has_real_derivative f') (atreal x within s)`
85 UNDISCH_TAC `pg ==> (g has_real_derivative g') (atreal x within s)`
94 let atn2_atn_open = prove_by_refinement(
95 `!p f f' g x s. p /\ derived_form p f f' x s /\ (&0 < f x)==>
96 (?d. &0 < d /\ (!x'. x' IN s /\ abs (x' - x) < d ==>
97 atn2 (f x', g x') = atn(g x' / f x')))`,
101 DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open))