sum_numScript.sml
1(* ========================================================================= *)
2(* FILE : sum_numScript.sml *)
3(* DESCRIPTION : Defines a big-sigma (sum) function for the *)
4(* natural numbers. *)
5(* AUTHOR : (c) Anthony Fox, University of Cambridge *)
6(* DATE : 2002 *)
7(* ========================================================================= *)
8Theory sum_num
9Ancestors
10 rich_list[qualified] (* for COUNT_LIST *)
11 arithmetic
12Libs
13 Q
14
15
16(* ------------------------------------------------------------------------- *)
17
18Definition GSUM_def:
19 (GSUM (n,0) f = 0) /\
20 (GSUM (n,SUC m) f = GSUM (n,m) f + f (n + m))
21End
22
23Theorem GSUM_1:
24 !m f. GSUM (m,1) f = f m
25Proof REWRITE_TAC [ONE,GSUM_def,ADD_CLAUSES]
26QED
27
28Theorem GSUM_ADD:
29 !p m n f. GSUM (p,m + n) f = GSUM (p,m) f + GSUM (p + m,n) f
30Proof
31 Induct_on `n` THEN1 REWRITE_TAC [GSUM_def,ADD_CLAUSES]
32 THEN ASM_SIMP_TAC arith_ss [GSYM ADD_SUC,GSUM_def]
33QED
34
35Theorem GSUM_ZERO:
36 !p n f. (!m. p <= m /\ m < p + n ==> (f m = 0)) = (GSUM (p,n) f = 0)
37Proof
38 Induct_on `n`
39 THEN ASM_SIMP_TAC arith_ss [GSUM_def] THEN NTAC 2 STRIP_TAC
40 THEN POP_ASSUM (fn th => REWRITE_TAC [GSYM th])
41 THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC arith_ss []
42 THEN PAT_ASSUM `!m. P` (SPEC_THEN `m` IMP_RES_TAC)
43 THEN Cases_on `m < p + n` THEN1 PROVE_TAC []
44 THEN `m = n + p` by DECIDE_TAC
45 THEN ASM_REWRITE_TAC []
46QED
47
48Theorem GSUM_MONO:
49 !p m n f. m <= n /\ ~(f (p + n) = 0) ==> GSUM (p,m) f < GSUM (p,SUC n) f
50Proof
51 RW_TAC arith_ss [GSUM_def]
52 THEN IMP_RES_TAC LESS_EQUAL_ADD
53 THEN FULL_SIMP_TAC arith_ss [GSUM_ADD]
54QED
55
56Theorem GSUM_MONO2[local]:
57 !p m n f. GSUM (p,m) f < GSUM (p,n) f ==> m < n
58Proof
59 Induct_on `n` THEN1 REWRITE_TAC [prim_recTheory.NOT_LESS_0,GSUM_def]
60 THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC
61 THEN RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS,GSYM LESS_EQ])
62 THEN IMP_RES_TAC LESS_ADD_1 THEN POP_ASSUM (K ALL_TAC)
63 THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (REWRITE_RULE [GSUM_ADD,
64 REWRITE_RULE [DECIDE (Term `!a b. a + (b + 1) = SUC a + b`)] th]))
65 THEN DECIDE_TAC
66QED
67
68Theorem GSUM_LESS:
69 !p m n f.
70 (?q. m + p <= q /\ q < n + p /\ ~(f q = 0)) <=>
71 GSUM (p,m) f < GSUM (p,n) f
72Proof
73 Induct_on `n` THEN1 SIMP_TAC arith_ss [GSUM_def]
74 THEN REPEAT STRIP_TAC
75 THEN EQ_TAC THEN REPEAT STRIP_TAC
76 THENL [
77 Cases_on `GSUM (p,m) f < GSUM (p,n) f`
78 THEN1 ASM_SIMP_TAC arith_ss [GSUM_def]
79 THEN PAT_ASSUM `!p m f. P` (fn th => FULL_SIMP_TAC arith_ss [GSYM th])
80 THEN Cases_on `q < n + p` THEN1 PROVE_TAC []
81 THEN `m <= n /\ (q = n + p)` by DECIDE_TAC
82 THEN IMP_RES_TAC (ONCE_REWRITE_RULE [ADD_COMM] GSUM_MONO)
83 THEN PROVE_TAC [],
84 Cases_on `GSUM (p,m) f < GSUM (p,n) f`
85 THENL [
86 PAT_ASSUM `!p m f. P` IMP_RES_TAC
87 THEN `q < SUC n + p` by DECIDE_TAC
88 THEN PROVE_TAC [],
89 FULL_SIMP_TAC bool_ss [GSUM_def]
90 THEN `~(f (p + n) = 0)` by DECIDE_TAC
91 THEN EXISTS_TAC `p + n`
92 THEN ASM_SIMP_TAC arith_ss []
93 THEN FULL_SIMP_TAC bool_ss [GSYM GSUM_def]
94 THEN IMP_RES_TAC GSUM_MONO2
95 THEN DECIDE_TAC]]
96QED
97
98Theorem GSUM_EQUAL_LEM[local]:
99 !p m n f. n < m /\ (!q. p + n <= q /\ q < p + m ==> (f q = 0)) ==>
100 (GSUM (p,m) f = GSUM (p,n) f)
101Proof
102 REPEAT STRIP_TAC THEN IMP_RES_TAC LESS_ADD
103 THEN POP_ASSUM (fn th => FULL_SIMP_TAC arith_ss [GSUM_ADD,GSUM_ZERO,SYM th])
104 THEN Induct_on `p'` THEN RW_TAC arith_ss [GSUM_def]
105 THEN Cases_on `p'` THEN FULL_SIMP_TAC arith_ss [GSUM_def]
106QED
107
108Theorem GSUM_EQUAL_LEM2[local]:
109 !p m n f. (GSUM (p,m) f = GSUM (p,n) f) =
110 ((m = n) \/
111 (m < n /\ (!q. p + m <= q /\ q < p + n ==> (f q = 0))) \/
112 (n < m /\ (!q. p + n <= q /\ q < p + m ==> (f q = 0))))
113Proof
114 REPEAT STRIP_TAC THEN Tactical.REVERSE EQ_TAC
115 THEN1 PROVE_TAC [GSUM_EQUAL_LEM]
116 THEN Cases_on `m = n` THEN1 ASM_REWRITE_TAC []
117 THEN IMP_RES_TAC (DECIDE (Term `!(a:num) b. ~(a = b) ==> (a < b) \/ (b < a)`))
118 THEN ASM_SIMP_TAC arith_ss []
119 THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC
120 THEN IMP_RES_TAC GSUM_LESS THEN DECIDE_TAC
121QED
122
123Theorem GSUM_EQUAL:
124 !p m n f. (GSUM (p,m) f = GSUM (p,n) f) =
125 ((m <= n /\ (!q. p + m <= q /\ q < p + n ==> (f q = 0))) \/
126 (n < m /\ (!q. p + n <= q /\ q < p + m ==> (f q = 0))))
127Proof
128 RW_TAC arith_ss [GSUM_EQUAL_LEM2]
129 THEN Cases_on `m = n` THEN1 ASM_SIMP_TAC arith_ss []
130 THEN IMP_RES_TAC (DECIDE (Term `!(a:num) b. ~(a = b) ==> (a < b) \/ (b < a)`))
131 THEN ASM_SIMP_TAC arith_ss []
132QED
133
134Theorem GSUM_FUN_EQUAL:
135 !p n f g. (!x. p <= x /\ x < p + n ==> (f x = g x)) ==>
136 (GSUM (p,n) f = GSUM (p,n) g)
137Proof
138 Induct_on `n` THEN RW_TAC arith_ss [GSUM_def]
139QED
140
141(* ------------------------------------------------------------------------- *)
142
143Definition SUM_def:
144 (SUM 0 f = 0) /\
145 (SUM (SUC m) f = SUM m f + f m)
146End
147
148Theorem SUM:
149 !m f. SUM m f = GSUM (0,m) f
150Proof
151 Induct THEN ASM_SIMP_TAC arith_ss [SUM_def,GSUM_def]
152QED
153
154val SYM_SUM = GSYM SUM;
155
156Theorem SUM_1 =
157 (REWRITE_RULE [SYM_SUM] o SPEC `0`) GSUM_1;
158
159Theorem SUM_MONO =
160 (REWRITE_RULE [SYM_SUM,ADD] o SPEC `0`) GSUM_MONO;
161
162Theorem SUM_LESS =
163 (REWRITE_RULE [SYM_SUM,ADD_CLAUSES] o SPEC `0`) GSUM_LESS;
164
165Theorem SUM_EQUAL =
166 (SIMP_RULE arith_ss [SYM_SUM] o SPEC `0`) GSUM_EQUAL;
167
168Theorem SUM_FUN_EQUAL =
169 (SIMP_RULE arith_ss [SYM_SUM] o SPECL [`0`,`n`]) GSUM_FUN_EQUAL;
170
171Theorem SUM_ZERO =
172 (SIMP_RULE arith_ss [SYM_SUM] o SPEC `0`) GSUM_ZERO;
173
174Theorem SUM_FOLDL:
175 !n f. SUM n f = FOLDL (\x n. f n + x) 0 (COUNT_LIST n)
176Proof
177 Induct
178 THEN SRW_TAC [ARITH_ss]
179 [SUM_def, rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC]
180QED
181
182(* ------------------------------------------------------------------------- *)