(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*               SOME USEFUL TACTICS AND LEMMAS                              *)
(*                                                                           *)
(*      Authour : VU KHAC KY                                                 *)
(*                                                                           *)
(* ========================================================================= *)

(* ========================================================================= *)
(*                        SOME TACTICS                                       *)
(* ========================================================================= *)

module Vukhacky_tactics = struct 

let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;

let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;

let SWITCH_TAC = 
   FIRST_X_ASSUM MP_TAC THEN 
   FIRST_X_ASSUM MP_TAC THEN 
   MATCH_MP_TAC (MESON[] `(a ==> b ==> c) ==> (b ==> a ==> c)`) THEN 
   DISCH_TAC THEN 
   DISCH_TAC;;

let REWRITE_ONLY_TAC thm = REWRITE_TAC[thm];;
let REWRITE_WITH thm = SUBGOAL_THEN thm REWRITE_ONLY_TAC;;
let NEW_GOAL s1 = SUBGOAL_THEN s1 ASSUME_TAC;;

let KY_CHOOSE_TAC thm s = 
UNDISCH_TAC thm THEN DISCH_THEN (LABEL_TAC "temp_ky") THEN 
(USE_THEN "temp_ky" (MP_TAC o SPEC s)) THEN DISCH_TAC;;

(* ========================================================================= *)
(*                        SOME LEMMAS                                        *)
(* ========================================================================= *)

let HAS_REAL_DERIVATIVE_CHAIN2 = 
prove
  (`!P f g x s.
         (!x. P x ==> (g has_real_derivative g' x) (atreal x))
         ==> (f has_real_derivative f') (atreal x within s) /\ P (f x)
         ==> ((\x. g (f x)) has_real_derivative f' * g' (f x))
             (atreal x within s)`,

   REPEAT GEN_TAC THEN 
   MP_TAC HAS_REAL_DERIVATIVE_CHAIN THEN
   MESON_TAC[]);;
let REDUCE_WITH_DIV_Euler_lemma = 
prove_by_refinement (
 `!x y z . ~ (y = &0) /\ ~ (z = &0) ==> x * y / (z * y) = x / z`,

 [(REPEAT STRIP_TAC);
 (MATCH_MP_TAC REAL_EQ_LCANCEL_IMP);
 (EXISTS_TAC `z:real`);
 (ASM_REWRITE_TAC[]);
 (REWRITE_TAC[REAL_ARITH `a * b * (c:real) = (a * c) * b`]);
 (SUBGOAL_THEN `z * x / z = x` ASSUME_TAC);
 (MATCH_MP_TAC REAL_DIV_LMUL);
 (ASM_REWRITE_TAC[]);
 (PURE_ONCE_ASM_REWRITE_TAC[]);
 (MATCH_MP_TAC (MESON[REAL_MUL_LID] `a = &1 ==> a * b = b`));
 (REWRITE_TAC[REAL_ARITH `a * b / c = (a * b) / c`]);
 (MATCH_MP_TAC REAL_DIV_REFL);
 (REWRITE_TAC[REAL_ENTIRE; MESON[] `~(a \/ b) <=> ~a /\ ~b`]);
 (ASM_REWRITE_TAC[])]);;
 
end;;