blob: 18d4901f6bb48e4aebb424624f94494fc66fb361 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
# let LEMMA_1 = prove
(`!x n. x pow (n + 1) - (&n + &1) * x + &n =
(x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
[REAL_ARITH_TAC; REWRITE_TAC[ARITH_RULE `1 <= SUC n`]] THEN
SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN
ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC);;
val ( LEMMA_1 ) : thm =
|- !x n.
x pow (n + 1) - (&n + &1) * x + &n =
(x - &1) pow 2 * sum (1..n) (\k. &k * x pow (n - k))
# print_executed_proof ();;
e ((CONV_TAC (ONCE_DEPTH_CONV SYM_CONV)) THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]) THENL [REAL_ARITH_TAC; REWRITE_TAC [ARITH_RULE `1 <= SUC n`]] THEN (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]) THEN (REWRITE_TAC [real_pow;REAL_MUL_RID]) THEN (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]) THEN (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]) THEN (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]) THEN REAL_ARITH_TAC);;
val it : unit = ()
# print_flat_proof ();;
e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));;
e (GEN_TAC);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
e (REAL_ARITH_TAC);;
e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);;
e (REWRITE_TAC [real_pow;REAL_MUL_RID]);;
e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);;
e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);;
e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);;
e (REAL_ARITH_TAC);;
|
