text_formalization/nonlinear/vukhacky_tactics.hl

   1 (* ========================================================================= *)
   2 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   3 (*               SOME USEFUL TACTICS AND LEMMAS                              *)
   4 (*                                                                           *)
   5 (*      Authour : VU KHAC KY                                                 *)
   6 (*                                                                           *)
   7 (* ========================================================================= *)
   8
   9 (* ========================================================================= *)
  10 (*                        SOME TACTICS                                       *)
  11 (* ========================================================================= *)
  12
  13 module Vukhacky_tactics = struct
  14
  15 let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;
  16
  17 let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;
  18
  19 let SWITCH_TAC =
  20    FIRST_X_ASSUM MP_TAC THEN
  21    FIRST_X_ASSUM MP_TAC THEN
  22    MATCH_MP_TAC (MESON[] `(a ==> b ==> c) ==> (b ==> a ==> c)`) THEN
  23    DISCH_TAC THEN
  24    DISCH_TAC;;
  25
  26 let REWRITE_ONLY_TAC thm = REWRITE_TAC[thm];;
  27 let REWRITE_WITH thm = SUBGOAL_THEN thm REWRITE_ONLY_TAC;;
  28 let NEW_GOAL s1 = SUBGOAL_THEN s1 ASSUME_TAC;;
  29
  30 let KY_CHOOSE_TAC thm s =
  31 UNDISCH_TAC thm THEN DISCH_THEN (LABEL_TAC "temp_ky") THEN
  32 (USE_THEN "temp_ky" (MP_TAC o SPEC s)) THEN DISCH_TAC;;
  33
  34 (* ========================================================================= *)
  35 (*                        SOME LEMMAS                                        *)
  36 (* ========================================================================= *)
  37
  38 let HAS_REAL_DERIVATIVE_CHAIN2 = prove
  39   (`!P f g x s.
  40          (!x. P x ==> (g has_real_derivative g' x) (atreal x))
  41          ==> (f has_real_derivative f') (atreal x within s) /\ P (f x)
  42          ==> ((\x. g (f x)) has_real_derivative f' * g' (f x))
  43              (atreal x within s)`,
  44    REPEAT GEN_TAC THEN
  45    MP_TAC HAS_REAL_DERIVATIVE_CHAIN THEN
  46    MESON_TAC[]);;
  47
  48 let REDUCE_WITH_DIV_Euler_lemma = prove_by_refinement (
  49  `!x y z . ~ (y = &0) /\ ~ (z = &0) ==> x * y / (z * y) = x / z`,
  50  [(REPEAT STRIP_TAC);
  51  (MATCH_MP_TAC REAL_EQ_LCANCEL_IMP);
  52  (EXISTS_TAC `z:real`);
  53  (ASM_REWRITE_TAC[]);
  54  (REWRITE_TAC[REAL_ARITH `a * b * (c:real) = (a * c) * b`]);
  55  (SUBGOAL_THEN `z * x / z = x` ASSUME_TAC);
  56  (MATCH_MP_TAC REAL_DIV_LMUL);
  57  (ASM_REWRITE_TAC[]);
  58  (PURE_ONCE_ASM_REWRITE_TAC[]);
  59  (MATCH_MP_TAC (MESON[REAL_MUL_LID] `a = &1 ==> a * b = b`));
  60  (REWRITE_TAC[REAL_ARITH `a * b / c = (a * b) / c`]);
  61  (MATCH_MP_TAC REAL_DIV_REFL);
  62  (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
  63  (ASM_REWRITE_TAC[])]);;
  64
  65 end;;