1open HolKernel Parse boolLib
2
3(* interactive mode
4app load ["bossLib", "arithmeticTheory", "numLib"];
5*)
6
7open bossLib arithmeticTheory numLib;
8
9infix THEN THENC THENL;
10infix 8 by;
11val ARW = RW_TAC arith_ss;
12
13val _ = new_theory "summation";
14
15val SUMMATION =
16 Define
17     `(summation j 0 f       = 0)
18   /\ (summation j (SUC i) f = f j + summation (SUC j) i f)`;
19
20
21val SUMMATION_1 = store_thm("SUMMATION_1",
22Term `!i j f. summation j (SUC i) f = f j + summation (SUC j) i f`,
23  ARW[SUMMATION]);
24
25
26val SUMMATION_2 = store_thm("SUMMATION_2",
27Term `!i j f. summation j (SUC i) f = summation j i f + f (i + j)`,
28  Induct_on `i`
29    THEN ONCE_REWRITE_TAC[SUMMATION]
30    THEN ARW[ADD_CLAUSES] THEN ARW[SUMMATION]);
31
32
33val SUMMATION_EXT = store_thm("SUMMATION_EXT",
34Term `!i j f g.
35        (!k. k < i ==> (f (j + k) = g (j + k)))
36          ==>
37        (summation j i f = summation j i g)`,
38Induct_on `i`
39  THEN ARW[SUMMATION]
40  THEN `f j:num = f (j+0)` by REWRITE_TAC[ADD_CLAUSES]
41  THEN ARW[]
42  THEN `!k. k < i ==> (f (SUC j + k):num = g (SUC j + k))`
43     by (ARW[ADD_CLAUSES]
44           THEN `f (SUC (j+k)):num = f (j + SUC k)` by REWRITE_TAC[ADD_CLAUSES]
45           THEN ARW[ADD_CLAUSES])
46  THEN RES_TAC);
47
48
49val SUMMATION_ADD = store_thm("SUMMATION_ADD",
50Term `!i j f g.
51  summation j i f + summation j i g = summation j i (\n. (f n) + g n)`,
52Induct_on `i` THEN ARW [SUMMATION]);
53
54
55val SUMMATION_TIMES = store_thm("SUMMATION_TIMES",
56Term `!i j k f. k * summation j i f = summation j i (\n.  k * f n)`,
57  Induct_on `i` THEN ARW[SUMMATION,LEFT_ADD_DISTRIB]);
58
59
60val INV_SUMMATION = store_thm("INV_SUMMATION",
61Term `!i j f P.
62       P 0 /\
63       (! a b. (P a) /\ (P b) ==> P (a + b)) /\
64       (!k. k < i ==> P (f (k + j)))
65       ==>
66          P (summation j i f)`,
67Induct_on `i` THEN ARW[SUMMATION]
68  THEN sg `P (f (j:num):num) : bool`
69  THENL [
70   `f j:num = f (j+0)` by REWRITE_TAC[ADD_CLAUSES]
71     THEN ASM_REWRITE_TAC[] THEN ARW[],
72   Q.PAT_ASSUM `!a b. Q a b` (fn th => MATCH_MP_TAC th THEN ASSUME_TAC th)
73   THEN ARW[]
74   THEN Q.PAT_ASSUM `!j f P. Q j f P` MATCH_MP_TAC
75   THEN ARW[]
76   THEN `SUC k < SUC i` by DECIDE_TAC
77   THEN `P (f (j + SUC k))` by RES_TAC
78   THEN POP_ASSUM MP_TAC
79   THEN POP_ASSUM_LIST (K ALL_TAC)
80   THEN PROVE_TAC [ADD_CLAUSES, ADD_COMM]]);
81
82
83val SUMMATION_SHIFT = store_thm("SUMMATION_SHIFT",
84Term `!i j f. summation j i f = summation (SUC j) i (\n. f (n - 1))`,
85 Induct_on `i`
86  THEN  REWRITE_TAC[SUMMATION]
87  THEN BETA_TAC THEN REWRITE_TAC[SUC_SUB1]
88  THEN POP_ASSUM (fn thm => REWRITE_TAC[GSYM thm]));
89
90val SUMMATION_SHIFT_P = store_thm("SUMMATION_SHIFT_P",
91Term `!i j f. summation (SUC j) i f = summation j i (\n. f (n + 1))`,
92  Induct_on `i` THEN ARW[SUMMATION,ADD1]);
93
94
95val _ = export_theory();
96