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