58 |
58 |
59 Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"; |
59 Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"; |
60 by (Simp_tac 1); |
60 by (Simp_tac 1); |
61 qed "binomial_Suc_Suc"; |
61 qed "binomial_Suc_Suc"; |
62 |
62 |
|
63 Goal "ALL k. n < k --> (n choose k) = 0"; |
|
64 by (induct_tac "n" 1); |
|
65 by Auto_tac; |
|
66 by (etac allE 1); |
|
67 by (etac mp 1); |
|
68 by (arith_tac 1); |
|
69 qed_spec_mp "binomial_eq_0"; |
|
70 |
63 Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc]; |
71 Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc]; |
64 Delsimps [binomial_0, binomial_Suc]; |
72 Delsimps [binomial_0, binomial_Suc]; |
65 |
73 |
66 |
74 |
67 Goal "!k. n<k --> (n choose k) = 0"; |
75 Goal "!k. n<k --> (n choose k) = 0"; |
85 Goal "(n choose 1) = n"; |
93 Goal "(n choose 1) = n"; |
86 by (induct_tac "n" 1); |
94 by (induct_tac "n" 1); |
87 by (ALLGOALS Asm_simp_tac); |
95 by (ALLGOALS Asm_simp_tac); |
88 qed "binomial_1"; |
96 qed "binomial_1"; |
89 Addsimps [binomial_1]; |
97 Addsimps [binomial_1]; |
|
98 |
|
99 Goal "k <= n --> 0 < (n choose k)"; |
|
100 by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); |
|
101 by (ALLGOALS Asm_simp_tac); |
|
102 qed_spec_mp "zero_less_binomial"; |
|
103 |
|
104 (*Might be more useful if re-oriented*) |
|
105 Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"; |
|
106 by (induct_tac "n" 1); |
|
107 by (simp_tac (simpset() addsimps [binomial_0]) 1); |
|
108 by (Clarify_tac 1); |
|
109 by (exhaust_tac "k" 1); |
|
110 by (auto_tac (claset(), |
|
111 simpset() addsimps [add_mult_distrib, add_mult_distrib2, |
|
112 le_Suc_eq, binomial_eq_0])); |
|
113 qed_spec_mp "Suc_times_binomial_eq"; |
|
114 |
|
115 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
|
116 by (asm_simp_tac |
|
117 (simpset_of Nat.thy addsimps [Suc_times_binomial_eq, |
|
118 div_mult_self_is_m]) 1); |
|
119 qed "binomial_Suc_Suc_eq_times"; |
|
120 |