1(* interactive mode 2app load ["bossLib","summationTheory","powerTheory"]; 3quietdec := true; 4*) 5 6open HolKernel Parse boolLib 7open bossLib arithmeticTheory powerTheory summationTheory ; 8 9(* 10quietdec := false; 11*) 12 13infix THEN THENC THENL; 14infix 8 by; 15 16val ARW = RW_TAC arith_ss; 17 18val _ = new_theory "binomial"; 19 20val FACT_def = ONCE_REWRITE_RULE [MULT_COMM] FACT; 21 22val BINOMIAL = 23 Define 24 `(binomial a 0 = 1) 25 /\ (binomial 0 (SUC b) = 0) 26 /\ (binomial (SUC a) (SUC b) = binomial a (SUC b) + binomial a b)`; 27 28 29val BINOMIAL_DEF1 = store_thm("BINOMIAL_DEF1", 30 Term `!a. binomial a 0 = 1`, 31 Cases_on `a` THEN REWRITE_TAC[BINOMIAL]); 32 33val BINOMIAL_DEF2 = store_thm("BINOMIAL_DEF2", 34 Term `!a b. a < b ==> (binomial a b = 0)`, 35 Induct_on `a` THEN Cases_on `b` 36 THEN REWRITE_TAC[BINOMIAL] THEN ARW[]); 37 38val BINOMIAL_DEF3 = store_thm("BINOMIAL_DEF3", 39 Term `!a. binomial a a = 1`, 40 Induct_on `a` THEN REWRITE_TAC[BINOMIAL] 41 THEN ARW[BINOMIAL_DEF2]); 42 43val BINOMIAL_DEF4 = store_thm("BINOMIAL_DEF4", 44 Term `!a b. binomial (SUC a) (SUC b) 45 = 46 binomial a (SUC b) + binomial a b`, 47 REWRITE_TAC[BINOMIAL]); 48 49val BINOMIAL_FACT = store_thm("BINOMIAL_FACT", 50Term `!a b. binomial (a+b) b * (FACT a * FACT b) 51 = 52 FACT (a+b)`, 53Induct_on `b` 54 THENL [ 55 REWRITE_TAC[BINOMIAL_DEF1,FACT,ADD_CLAUSES,MULT_CLAUSES], 56 Induct_on `a` 57 THENL [ 58 REWRITE_TAC[BINOMIAL_DEF3,FACT,ADD_CLAUSES,MULT_CLAUSES], 59 `SUC a + SUC b = SUC (SUC a + b)` by ARW[ADD_CLAUSES] 60 THEN ASM_REWRITE_TAC[BINOMIAL_DEF4,RIGHT_ADD_DISTRIB] 61 THEN `binomial (SUC a + b) (SUC b) * (FACT (SUC a) * FACT (SUC b)) 62 = 63 (binomial (a + SUC b) (SUC b) * (FACT a * FACT (SUC b))) 64 * SUC a` 65 by (REWRITE_TAC[FACT_def,ADD_CLAUSES] 66 THEN PROVE_TAC[MULT_ASSOC,MULT_SYM]) 67 THEN ASM_REWRITE_TAC[] 68 THEN `binomial (SUC a + b) b * (FACT (SUC a) * FACT (SUC b)) 69 = 70 (binomial (SUC a + b) b * (FACT (SUC a) * FACT b)) * SUC b` 71 by (REWRITE_TAC[FACT_def,ADD_CLAUSES] 72 THEN PROVE_TAC[MULT_ASSOC,MULT_SYM]) 73 THEN ASM_REWRITE_TAC 74 [ADD_CLAUSES,SYM(SPEC_ALL LEFT_ADD_DISTRIB),FACT_def] 75 ] 76 ] 77); 78 79 80val EXP_PASCAL = store_thm("EXP_PASCAL", 81Term `!a b n. 82 (a + b) EXP n 83 = 84 summation 0 (n + 1) 85 (\k. binomial n k * (a EXP (n-k) * b EXP k))`, 86Induct_on `n` 87 THENL [ 88 RW_TAC bool_ss [power_def,summation_def,BINOMIAL_DEF1, GSYM ADD1] 89 THEN ARW[], 90 ONCE_REWRITE_TAC[power_def] 91 THEN ASM_REWRITE_TAC[RIGHT_ADD_DISTRIB,SUMMATION_TIMES,GSYM ADD1] 92 THEN REPEAT STRIP_TAC 93 THEN POP_ASSUM (K ALL_TAC) 94 THEN `summation 0 (SUC n) 95 (\k. a * (binomial n k * (a EXP (n - k) * b EXP k))) 96 = 97 a * a EXP n + 98 summation 1 n 99 (\k. a * (binomial n k * (a EXP (n - k) * b EXP k)))` 100 by (RW_TAC bool_ss 101 [SUMMATION_1,BINOMIAL_DEF1,power_def,MULT_CLAUSES,ONE] 102 THEN ARW []) 103 THEN `summation 0 (SUC n) 104 (\k. b * (binomial n k * (a EXP (n - k) * b EXP k))) 105 = 106 summation 0 n 107 (\k. b * (binomial n k * (a EXP (n - k) * b EXP k))) 108 + b * b EXP n` 109 by (RW_TAC bool_ss [SUMMATION_2,BINOMIAL_DEF1, 110 power_def,MULT_CLAUSES,ONE] 111 THEN ARW [BINOMIAL_DEF3]) 112 THEN BETA_TAC THEN ASM_REWRITE_TAC[] 113 THEN POP_ASSUM_LIST (K ALL_TAC) 114 THEN MP_TAC (Q.SPECL[`n`,`0`] SUMMATION_SHIFT) 115 THEN DISCH_THEN (fn th => REWRITE_TAC [th]) 116 THEN BETA_TAC 117 THEN sg `(a * a EXP n 118 + (summation 1 n 119 (\k. a * (binomial n k * (a EXP (n - k) * b EXP k))) 120 + (summation (SUC 0) n 121 (\n'. b * (binomial n (n'-1) * 122 (a EXP (n-(n'-1)) * b EXP (n' - 1)))) 123 + b * b EXP n))) 124 = 125 (a * a EXP n 126 + (summation 1 n 127 (\k. binomial (SUC n) k * (a EXP (SUC n - k) * b EXP k)) 128 + b * b EXP n))` 129 THENL [ 130 ARW[] 131 THEN RW_TAC bool_ss [ONE, SUMMATION_ADD] 132 THEN MATCH_MP_TAC SUMMATION_EXT 133 THEN ARW[ADD_CLAUSES,Q.SPEC`n` BINOMIAL_DEF4,RIGHT_ADD_DISTRIB] 134 THEN `n - k = SUC (n - SUC k)` by ARW[] 135 THEN ASM_REWRITE_TAC[power_def] 136 THEN `!x y p q : num. (x = q) /\ (y = p) ==> (x + y = p + q)` 137 by DECIDE_TAC 138 THEN POP_ASSUM MATCH_MP_TAC 139 THEN PROVE_TAC [MULT_SYM,MULT_ASSOC], 140 POP_ASSUM (fn th => REWRITE_TAC [th, GSYM ADD_ASSOC]) 141 THEN ARW[Q.SPEC`SUC n` SUMMATION_1, Q.SPEC`n` SUMMATION_2] 142 THEN ARW[power_def,BINOMIAL_DEF1,MULT_CLAUSES,ADD_CLAUSES] 143 THEN ARW[GSYM ADD1,BINOMIAL_DEF3,power_def] 144 ] 145 ] 146 ); 147 148val _ = export_theory(); 149