Update from HH
[hl193./.git] / Jordan / real_ext_geom_series.ml
1
2 prioritize_real();;
3
4 let (TRY_RULE:(thm->thm) -> (thm->thm)) = 
5         fun rl t -> try (rl t) with _ -> t;;
6
7
8 let REAL_MUL_RTIMES =
9         prove ((`!x a b. 
10                 (((~(x=(&0))==>(a*x = b*x)) /\ ~(x=(&0))) ==>  (a = b))`),
11                 MESON_TAC[REAL_EQ_MUL_RCANCEL]);;
12
13
14 let GEOMETRIC_SUM = prove(
15         `!m n x.(~(x=(&1)) ==> 
16         (sum(m,n) (\k.(x pow k)) = ((x pow m) - (x pow (m+n)))/((&1)-x)))`,
17         let tac1 = 
18         GEN_TAC
19         THEN INDUCT_TAC
20         THEN GEN_TAC
21         THEN DISCH_TAC
22         THEN (REWRITE_TAC
23           [sum_DEF;real_pow;ADD_CLAUSES;real_div;REAL_SUB_RDISTRIB; 
24                 REAL_SUB_REFL]) in
25         let tac2 = 
26          (RULE_ASSUM_TAC (TRY_RULE (SPEC (`x:real`))))
27         THEN (UNDISCH_EL_TAC 1)
28         THEN (UNDISCH_EL_TAC 0)
29         THEN (TAUT_TAC (`(A==>(B==>C))    ==> (A ==> ((A==>B) ==>C))`))
30         THEN (REPEAT DISCH_TAC)
31         THEN (ASM_REWRITE_TAC[real_div])
32         THEN (ABBREV_TAC (`a:real = x pow m`))
33         THEN (ABBREV_TAC (`b:real = x pow (m+n)`)) in
34         let tac3 =
35              (MATCH_MP_TAC (SPEC (`&1 - x`) REAL_MUL_RTIMES))
36         THEN CONJ_TAC 
37         THENL [ALL_TAC; (UNDISCH_TAC (`~(x = (&1))`))
38           THEN (ACCEPT_TAC (REAL_ARITH (`~(x=(&1)) ==> ~((&1 - x = (&0)))`)))]
39         THEN (REWRITE_TAC
40           [GSYM REAL_MUL_ASSOC;REAL_ADD_RDISTRIB;REAL_SUB_RDISTRIB])
41         THEN (SIMP_TAC[REAL_MUL_LINV])
42         THEN DISCH_TAC
43         THEN (REWRITE_TAC
44           [REAL_SUB_LDISTRIB;REAL_MUL_LID;REAL_MUL_RID;REAL_MUL_ASSOC])
45         THEN (ACCEPT_TAC (REAL_ARITH (`a - b + b - b*x = a - x*b`))) in
46         (tac1 THEN tac2 THEN tac3));;
47
48
49 pop_priority();;