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