1 let ARITHMETIC_PROGRESSION_SIMPLE = prove
2 (`!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2`,
3 INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
9 !n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2
11 nsum(0..0) (\i. i) = 0 by NSUM_CLAUSES_NUMSEG;
12 .= (0*(0 + 1)) DIV 2 [A1] by ARITH_TAC;
14 assume nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2;
15 nsum(0..SUC n) (\i. i) = (n*(n + 1)) DIV 2 + SUC n
16 by NSUM_CLAUSES_NUMSEG,ARITH_RULE (parse_term "0 <= SUC n");
17 thus .= ((SUC n)*(SUC n + 1)) DIV 2 by ARITH_TAC;
19 qed by INDUCT_TAC,A1`;;
23 (if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 [A1] by ARITH_TAC;
24 nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2 [A2]
25 by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A1;
28 assume nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A4];
29 (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =
30 (SUC n * (SUC n + 1)) DIV 2 [A5] by ARITH_TAC;
31 thus nsum (1..SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2 [A6]
32 by REWRITE_TAC,NSUM_CLAUSES_NUMSEG,A4,A5;
34 thus !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A7] by INDUCT_TAC,A2,A3;
37 let EXAMPLE = ref None;;
40 !n. nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2
42 nsum(0..0) (\i. i) = (0*(0 + 1)) DIV 2;
44 assume nsum(0..n) (\i. i) = (n*(n + 1)) DIV 2;
45 thus nsum(0..SUC n) (\i. i) = ((SUC n)*(SUC n + 1)) DIV 2 by #;
50 !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
52 (if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 by ARITH_TAC;
53 nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2 [A1]
54 by ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG];
55 !n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
56 ==> nsum (1..SUC n) (\i .i) = (SUC n * (SUC n + 1)) DIV 2
59 assume nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2 [A2];
60 (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else (n * (n + 1)) DIV 2) =
61 (SUC n * (SUC n + 1)) DIV 2 by ARITH_TAC;
62 qed by ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG],A2;
63 qed by INDUCT_TAC,A1`;;
65 let NSUM_CLAUSES_NUMSEG' = thm `;
66 !s. nsum(0..0) s = s 0 /\ !n. nsum(0..n + 1) s = nsum(0..n) s + s (n + 1)
68 !n. 0 <= SUC n by ARITH_TAC;
69 qed by NSUM_CLAUSES_NUMSEG,ADD1`;;
71 let num_INDUCTION' = REWRITE_RULE[ADD1] num_INDUCTION;;
74 !s. (!i. s i = i) ==> !n. nsum(0..n) s = (n*(n + 1)) DIV 2
77 assume !i. s i = i [A1];
78 set X = \n. (nsum(0..n) s = (n*(n + 1)) DIV 2);
79 nsum(0..0) s = s 0 by NSUM_CLAUSES_NUMSEG';
81 .= (0*(0 + 1)) DIV 2 by ARITH_TAC;
83 now [A3] let n be num;
85 nsum(0..n + 1) s = (n*(n + 1)) DIV 2 + s (n + 1) by NSUM_CLAUSES_NUMSEG';
86 .= (n*(n + 1)) DIV 2 + (n + 1) by A1;
87 thus X (n + 1) by ARITH_TAC;
89 !n. X n by MATCH_MP_TAC,num_INDUCTION',A2,A3;