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