development/thales/chaff/august9_2011_session.hl

   1 (* Code from Carnegie Library Session with
   2    Tom Hales and Nick Volker, August 9, 2011
   3
   4 *)
   5
   6
   7 Trigonometry1.ATN2_BREAKDOWN;;
   8
   9 (* modify Calc_derivative module to remove signature,
  10    reload, then open *)
  11
  12 open Calc_derivative;;
  13
  14
  15 let test_aug9_2011 = prove_by_refinement(
  16   `!x. (x > &0) ==> (?eps. abs(x - eps) > &0)`,
  17   (* {{{ proof *)
  18   [
  19   REPEAT STRIP_TAC;
  20 EXISTS_TAC `x / &2`;
  21 ASM_REAL_ARITH_TAC
  22   ]);;
  23   (* }}} *)
  24
  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'))`,
  28   (* {{{ proof *)
  29   [
  30 REWRITE_TAC[Calc_derivative.derived_form];
  31 REWRITE_TAC[TAUT `(a /\ (a ==> b) /\ c) <=> (a /\ b /\ c)`];
  32 REPEAT STRIP_TAC;
  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`));
  36 ASM_REWRITE_TAC[];
  37 STRIP_TAC;
  38 EXISTS_TAC `d:real`;
  39 ASM_REWRITE_TAC[];
  40 REPEAT STRIP_TAC;
  41 FIRST_X_ASSUM (MP_TAC o (SPEC `x':real`));
  42 ASM_REWRITE_TAC[];
  43 ASM_REAL_ARITH_TAC;
  44   ]);;
  45   (* }}} *)
  46
  47
  48 let derived_form_chain_simple = prove_by_refinement(
  49   `!x s g g' f f' p p'.
  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`,
  53   (* {{{ proof *)
  54   [
  55   MESON_TAC[derived_form_chain]
  56   ]);;
  57   (* }}} *)
  58
  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`,
  61   (* {{{ proof *)
  62   [
  63 REPEAT STRIP_TAC;
  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;
  69 ASM_REWRITE_TAC[];
  70 ASM_REWRITE_TAC[derived_form];
  71 REPEAT STRIP_TAC;
  72 FIRST_X_ASSUM MATCH_MP_TAC;
  73 ASM_REWRITE_TAC[]
  74   ]);;
  75   (* }}} *)
  76
  77
  78 (* UNFINISHED
  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`,
  81   (* {{{ proof *)
  82   [
  83 REPEAT STRIP_TAC
  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)`
  86 ASM_REWRITE_TAC[]
  87 REPEAT STRIP_TAC
  88   ]);;
  89   (* }}} *)
  90
  91 *)
  92
  93 (* UNFINISHED
  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')))`,
  98   (* {{{ proof *)
  99   [
 100 REPEAT GEN_TAC;
 101     DISCH_THEN (MP_TAC o (MATCH_MP derived_imp_pos_open))
 102   ]);;
 103   (* }}} *)
 104 *)
 105