text_formalization/jordan/real_ext_geom_series.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10 (* needs tactics_ext.ml *)
  11
  12 module Real_ext_geom_series = struct
  13
  14 open Tactics_jordan;;
  15
  16 prioritize_real();;
  17
  18 let (TRY_RULE:(thm->thm) -> (thm->thm)) =
  19         fun rl t -> try (rl t) with _ -> t;;
  20
  21
  22 let REAL_MUL_RTIMES =
  23         prove ((`!x a b.
  24                 (((~(x=(&0))==>(a*x = b*x)) /\ ~(x=(&0))) ==>  (a = b))`),
  25                 MESON_TAC[REAL_EQ_MUL_RCANCEL]);;
  26
  27 (*
  28 let GEOMETRIC_SUM = prove(
  29         `!m n x.(~(x=(&1)) ==>
  30         (sum(m,n) (\k.(x pow k)) = ((x pow m) - (x pow (m+n)))/((&1)-x)))`,
  31         let tac1 =
  32         GEN_TAC
  33         THEN INDUCT_TAC
  34         THEN GEN_TAC
  35         THEN DISCH_TAC
  36         THEN (REWRITE_TAC
  37           [sum_DEF;real_pow;ADD_CLAUSES;real_div;REAL_SUB_RDISTRIB;
  38                 REAL_SUB_REFL]) in
  39         let tac2 =
  40          (RULE_ASSUM_TAC (TRY_RULE (SPEC (`x:real`))))
  41         THEN (UNDISCH_EL_TAC 1)
  42         THEN (UNDISCH_EL_TAC 0)
  43         THEN (TAUT_TAC (`(A==>(B==>C))    ==> (A ==> ((A==>B) ==>C))`))
  44         THEN (REPEAT DISCH_TAC)
  45         THEN (ASM_REWRITE_TAC[real_div])
  46         THEN (ABBREV_TAC (`a:real = x pow m`))
  47         THEN (ABBREV_TAC (`b:real = x pow (m+n)`)) in
  48         let tac3 =
  49              (MATCH_MP_TAC (SPEC (`&1 - x`) REAL_MUL_RTIMES))
  50         THEN CONJ_TAC
  51         THENL [ALL_TAC; (UNDISCH_TAC (`~(x = (&1))`))
  52           THEN (ACCEPT_TAC (REAL_ARITH (`~(x=(&1)) ==> ~((&1 - x = (&0)))`)))]
  53         THEN (REWRITE_TAC
  54           [GSYM REAL_MUL_ASSOC;REAL_ADD_RDISTRIB;REAL_SUB_RDISTRIB])
  55         THEN (SIMP_TAC[REAL_MUL_LINV])
  56         THEN DISCH_TAC
  57         THEN (REWRITE_TAC
  58           [REAL_SUB_LDISTRIB;REAL_MUL_LID;REAL_MUL_RID;REAL_MUL_ASSOC])
  59         THEN (ACCEPT_TAC (REAL_ARITH (`a - b + b - b*x = a - x*b`))) in
  60         (tac1 THEN tac2 THEN tac3));;
  61
  62
  63 (* pop_priority();; *)
  64 *)
  65
  66 end;;