1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* SOME USEFUL TACTICS AND LEMMAS *)
5 (* Authour : VU KHAC KY *)
7 (* ========================================================================= *)
9 (* ========================================================================= *)
11 (* ========================================================================= *)
13 module Vukhacky_tactics = struct
15 let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;
17 let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;
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
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;;
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;;
34 (* ========================================================================= *)
36 (* ========================================================================= *)
38 let HAS_REAL_DERIVATIVE_CHAIN2 = prove
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))
45 MP_TAC HAS_REAL_DERIVATIVE_CHAIN THEN
48 let REDUCE_WITH_DIV_Euler_lemma = prove_by_refinement (
49 `!x y z . ~ (y = &0) /\ ~ (z = &0) ==> x * y / (z * y) = x / z`,
51 (MATCH_MP_TAC REAL_EQ_LCANCEL_IMP);
52 (EXISTS_TAC `z:real`);
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);
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[])]);;