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(* ========================================================================= *)
8
9open HolKernel Parse boolLib bossLib
10open Q arithmeticTheory;
11
12val _ = new_theory "sum_num";
13val _ = set_grammar_ancestry ["rich_list" (* for COUNT_LIST *) ]
14
15(* ------------------------------------------------------------------------- *)
16
17val GSUM_def = Define`
18  (GSUM (n,0) f = 0) /\
19  (GSUM (n,SUC m) f = GSUM (n,m) f + f (n + m))`;
20
21val GSUM_1 = store_thm("GSUM_1",
22  `!m f. GSUM (m,1) f = f m`, REWRITE_TAC [ONE,GSUM_def,ADD_CLAUSES]);
23
24val GSUM_ADD = store_thm("GSUM_ADD",
25  `!p m n f. GSUM (p,m + n) f = GSUM (p,m) f + GSUM (p + m,n) f`,
26   Induct_on `n` THEN1 REWRITE_TAC [GSUM_def,ADD_CLAUSES]
27     THEN ASM_SIMP_TAC arith_ss [GSYM ADD_SUC,GSUM_def]);
28
29val GSUM_ZERO = store_thm("GSUM_ZERO",
30  `!p n f. (!m. p <= m /\ m < p + n ==> (f m = 0)) = (GSUM (p,n) f = 0)`,
31  Induct_on `n`
32    THEN ASM_SIMP_TAC arith_ss [GSUM_def] THEN NTAC 2 STRIP_TAC
33    THEN POP_ASSUM (fn th => REWRITE_TAC [GSYM th])
34    THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC arith_ss []
35    THEN PAT_ASSUM `!m. P` (SPEC_THEN `m` IMP_RES_TAC)
36    THEN Cases_on `m < p + n` THEN1 PROVE_TAC []
37    THEN `m = n + p` by DECIDE_TAC
38    THEN ASM_REWRITE_TAC []);
39
40val GSUM_MONO = store_thm("GSUM_MONO",
41  `!p m n f. m <= n /\ ~(f (p + n) = 0) ==> GSUM (p,m) f < GSUM (p,SUC n) f`,
42  RW_TAC arith_ss [GSUM_def]
43    THEN IMP_RES_TAC LESS_EQUAL_ADD
44    THEN FULL_SIMP_TAC arith_ss [GSUM_ADD]);
45
46val GSUM_MONO2 = prove(
47  `!p m n f. GSUM (p,m) f < GSUM (p,n) f ==> m < n`,
48  Induct_on `n` THEN1 REWRITE_TAC [prim_recTheory.NOT_LESS_0,GSUM_def]
49    THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC
50    THEN RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS,GSYM LESS_EQ])
51    THEN IMP_RES_TAC LESS_ADD_1 THEN POP_ASSUM (K ALL_TAC)
52    THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (REWRITE_RULE [GSUM_ADD,
53           REWRITE_RULE [DECIDE (Term `!a b. a + (b + 1) = SUC a + b`)] th]))
54    THEN DECIDE_TAC);
55
56Theorem GSUM_LESS:
57  !p m n f.
58      (?q. m + p <= q /\ q < n + p /\ ~(f q = 0)) <=>
59      GSUM (p,m) f < GSUM (p,n) f
60Proof
61  Induct_on `n` THEN1 SIMP_TAC arith_ss [GSUM_def]
62    THEN REPEAT STRIP_TAC
63    THEN EQ_TAC THEN REPEAT STRIP_TAC
64    THENL [
65      Cases_on `GSUM (p,m) f < GSUM (p,n) f`
66        THEN1 ASM_SIMP_TAC arith_ss [GSUM_def]
67        THEN PAT_ASSUM `!p m f. P` (fn th => FULL_SIMP_TAC arith_ss [GSYM th])
68        THEN Cases_on `q < n + p` THEN1 PROVE_TAC []
69        THEN `m <= n /\ (q = n + p)` by DECIDE_TAC
70        THEN IMP_RES_TAC (ONCE_REWRITE_RULE [ADD_COMM] GSUM_MONO)
71        THEN PROVE_TAC [],
72      Cases_on `GSUM (p,m) f < GSUM (p,n) f`
73        THENL [
74          PAT_ASSUM `!p m f. P` IMP_RES_TAC
75            THEN `q < SUC n + p` by DECIDE_TAC
76            THEN PROVE_TAC [],
77          FULL_SIMP_TAC bool_ss [GSUM_def]
78            THEN `~(f (p + n) = 0)` by DECIDE_TAC
79            THEN EXISTS_TAC `p + n`
80            THEN ASM_SIMP_TAC arith_ss []
81            THEN FULL_SIMP_TAC bool_ss [GSYM GSUM_def]
82            THEN IMP_RES_TAC GSUM_MONO2
83            THEN DECIDE_TAC]]
84QED
85
86val GSUM_EQUAL_LEM = prove(
87  `!p m n f. n < m /\ (!q. p + n <= q /\ q < p + m ==> (f q = 0)) ==>
88            (GSUM (p,m) f = GSUM (p,n) f)`,
89  REPEAT STRIP_TAC THEN IMP_RES_TAC LESS_ADD
90    THEN POP_ASSUM (fn th => FULL_SIMP_TAC arith_ss [GSUM_ADD,GSUM_ZERO,SYM th])
91    THEN Induct_on `p'` THEN RW_TAC arith_ss [GSUM_def]
92    THEN Cases_on `p'` THEN FULL_SIMP_TAC arith_ss [GSUM_def]);
93
94val GSUM_EQUAL_LEM2 = prove(
95  `!p m n f. (GSUM (p,m) f = GSUM (p,n) f) =
96           ((m = n) \/
97            (m < n /\ (!q. p + m <= q /\ q < p + n ==> (f q = 0))) \/
98            (n < m /\ (!q. p + n <= q /\ q < p + m ==> (f q = 0))))`,
99  REPEAT STRIP_TAC THEN Tactical.REVERSE EQ_TAC
100    THEN1 PROVE_TAC [GSUM_EQUAL_LEM]
101    THEN Cases_on `m = n` THEN1 ASM_REWRITE_TAC []
102    THEN IMP_RES_TAC (DECIDE (Term `!(a:num) b. ~(a = b) ==> (a < b) \/ (b < a)`))
103    THEN ASM_SIMP_TAC arith_ss []
104    THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC
105    THEN IMP_RES_TAC GSUM_LESS THEN DECIDE_TAC);
106
107val GSUM_EQUAL = store_thm("GSUM_EQUAL",
108  `!p m n f. (GSUM (p,m) f = GSUM (p,n) f) =
109           ((m <= n /\ (!q. p + m <= q /\ q < p + n ==> (f q = 0))) \/
110            (n < m /\ (!q. p + n <= q /\ q < p + m ==> (f q = 0))))`,
111  RW_TAC arith_ss [GSUM_EQUAL_LEM2]
112    THEN Cases_on `m = n` THEN1 ASM_SIMP_TAC arith_ss []
113    THEN IMP_RES_TAC (DECIDE (Term `!(a:num) b. ~(a = b) ==> (a < b) \/ (b < a)`))
114    THEN ASM_SIMP_TAC arith_ss []);
115
116val GSUM_FUN_EQUAL = store_thm("GSUM_FUN_EQUAL",
117  `!p n f g. (!x. p <= x /\ x < p + n ==> (f x = g x)) ==>
118       (GSUM (p,n) f = GSUM (p,n) g)`,
119  Induct_on `n` THEN RW_TAC arith_ss [GSUM_def]);
120
121(* ------------------------------------------------------------------------- *)
122
123val SUM_def = Define`
124  (SUM 0 f = 0) /\
125  (SUM (SUC m) f = SUM m f + f m)`;
126
127val SUM = store_thm("SUM",
128  `!m f. SUM m f = GSUM (0,m) f`,
129  Induct THEN ASM_SIMP_TAC arith_ss [SUM_def,GSUM_def]);
130
131val SYM_SUM = GSYM SUM;
132
133val SUM_1 = save_thm("SUM_1",
134  (REWRITE_RULE [SYM_SUM] o SPEC `0`) GSUM_1);
135
136val SUM_MONO = save_thm("SUM_MONO",
137  (REWRITE_RULE [SYM_SUM,ADD] o SPEC `0`) GSUM_MONO);
138
139val SUM_LESS = save_thm("SUM_LESS",
140  (REWRITE_RULE [SYM_SUM,ADD_CLAUSES] o SPEC `0`) GSUM_LESS);
141
142val SUM_EQUAL = save_thm("SUM_EQUAL",
143  (SIMP_RULE arith_ss [SYM_SUM] o SPEC `0`) GSUM_EQUAL);
144
145val SUM_FUN_EQUAL = save_thm("SUM_FUN_EQUAL",
146  (SIMP_RULE arith_ss [SYM_SUM] o SPECL [`0`,`n`]) GSUM_FUN_EQUAL);
147
148val SUM_ZERO = save_thm("SUM_ZERO",
149  (SIMP_RULE arith_ss [SYM_SUM] o SPEC `0`) GSUM_ZERO);
150
151val SUM_FOLDL = Q.store_thm("SUM_FOLDL",
152   `!n f. SUM n f = FOLDL (\x n. f n + x) 0 (COUNT_LIST n)`,
153   Induct
154   THEN SRW_TAC [ARITH_ss]
155          [SUM_def, rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC])
156
157(* ------------------------------------------------------------------------- *)
158
159val _ = export_theory();
160