author | webertj |
Fri, 19 Oct 2012 15:12:52 +0200 | |
changeset 49962 | a8cc904a6820 |
parent 45933 | ee70da42e08a |
child 51291 | c2b452628afa |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Number_Theory/Binomial.thy |
31719 | 2 |
Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow |
3 |
||
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
4 |
Defines the "choose" function, and establishes basic properties. |
31719 | 5 |
|
6 |
The original theory "Binomial" was by Lawrence C. Paulson, based on |
|
7 |
the work of Andy Gordon and Florian Kammueller. The approach here, |
|
8 |
which derives the definition of binomial coefficients in terms of the |
|
9 |
factorial function, is due to Jeremy Avigad. The binomial theorem was |
|
10 |
formalized by Tobias Nipkow. |
|
11 |
*) |
|
12 |
||
13 |
header {* Binomial *} |
|
14 |
||
15 |
theory Binomial |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
16 |
imports Cong Fact |
31719 | 17 |
begin |
18 |
||
19 |
||
20 |
subsection {* Main definitions *} |
|
21 |
||
22 |
class binomial = |
|
44872 | 23 |
fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65) |
31719 | 24 |
|
25 |
(* definitions for the natural numbers *) |
|
26 |
||
27 |
instantiation nat :: binomial |
|
28 |
begin |
|
29 |
||
44872 | 30 |
fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
31719 | 31 |
where |
32 |
"binomial_nat n k = |
|
33 |
(if k = 0 then 1 else |
|
34 |
if n = 0 then 0 else |
|
35 |
(binomial (n - 1) k) + (binomial (n - 1) (k - 1)))" |
|
36 |
||
44872 | 37 |
instance .. |
31719 | 38 |
|
39 |
end |
|
40 |
||
41 |
(* definitions for the integers *) |
|
42 |
||
43 |
instantiation int :: binomial |
|
44 |
begin |
|
45 |
||
44872 | 46 |
definition binomial_int :: "int => int \<Rightarrow> int" where |
47 |
"binomial_int n k = |
|
48 |
(if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k)) |
|
49 |
else 0)" |
|
50 |
||
51 |
instance .. |
|
31719 | 52 |
|
53 |
end |
|
54 |
||
55 |
||
56 |
subsection {* Set up Transfer *} |
|
57 |
||
58 |
lemma transfer_nat_int_binomial: |
|
59 |
"(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = |
|
60 |
nat (binomial n k)" |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
61 |
unfolding binomial_int_def |
31719 | 62 |
by auto |
63 |
||
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
64 |
lemma transfer_nat_int_binomial_closure: |
31719 | 65 |
"n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
66 |
by (auto simp add: binomial_int_def) |
31719 | 67 |
|
35644 | 68 |
declare transfer_morphism_nat_int[transfer add return: |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
69 |
transfer_nat_int_binomial transfer_nat_int_binomial_closure] |
31719 | 70 |
|
71 |
lemma transfer_int_nat_binomial: |
|
72 |
"binomial (int n) (int k) = int (binomial n k)" |
|
73 |
unfolding fact_int_def binomial_int_def by auto |
|
74 |
||
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
75 |
lemma transfer_int_nat_binomial_closure: |
31719 | 76 |
"is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
77 |
by (auto simp add: binomial_int_def) |
31719 | 78 |
|
35644 | 79 |
declare transfer_morphism_int_nat[transfer add return: |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
80 |
transfer_int_nat_binomial transfer_int_nat_binomial_closure] |
31719 | 81 |
|
82 |
||
83 |
subsection {* Binomial coefficients *} |
|
84 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
85 |
lemma choose_zero_nat [simp]: "(n::nat) choose 0 = 1" |
31719 | 86 |
by simp |
87 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
88 |
lemma choose_zero_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1" |
31719 | 89 |
by (simp add: binomial_int_def) |
90 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
91 |
lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
92 |
by (induct n rule: induct'_nat, auto) |
31719 | 93 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
94 |
lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0" |
44872 | 95 |
unfolding binomial_int_def |
96 |
apply (cases "n < 0") |
|
31719 | 97 |
apply force |
98 |
apply (simp del: binomial_nat.simps) |
|
44872 | 99 |
done |
31719 | 100 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
101 |
lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow> |
31719 | 102 |
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
103 |
by simp |
|
104 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
105 |
lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow> |
31719 | 106 |
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
44872 | 107 |
unfolding binomial_int_def |
108 |
apply (subst choose_reduce_nat) |
|
109 |
apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib) |
|
110 |
done |
|
31719 | 111 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
112 |
lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = |
31719 | 113 |
(n choose (k + 1)) + (n choose k)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
114 |
by (simp add: choose_reduce_nat) |
31719 | 115 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
116 |
lemma choose_Suc_nat: "(Suc n) choose (Suc k) = |
31719 | 117 |
(n choose (Suc k)) + (n choose k)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
118 |
by (simp add: choose_reduce_nat One_nat_def) |
31719 | 119 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
120 |
lemma choose_plus_one_int: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) = |
31719 | 121 |
(n choose (k + 1)) + (n choose k)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
122 |
by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps) |
31719 | 123 |
|
124 |
declare binomial_nat.simps [simp del] |
|
125 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
126 |
lemma choose_self_nat [simp]: "((n::nat) choose n) = 1" |
44872 | 127 |
by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat) |
31719 | 128 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
129 |
lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1" |
31719 | 130 |
by (auto simp add: binomial_int_def) |
131 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
132 |
lemma choose_one_nat [simp]: "(n::nat) choose 1 = n" |
44872 | 133 |
by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat) |
31719 | 134 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
135 |
lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n" |
31719 | 136 |
by (auto simp add: binomial_int_def) |
137 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
138 |
lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
139 |
apply (induct n rule: induct'_nat, force) |
31719 | 140 |
apply (case_tac "n = 0") |
141 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
142 |
apply (subst choose_reduce_nat) |
31719 | 143 |
apply (auto simp add: One_nat_def) |
144 |
(* natdiff_cancel_numerals introduces Suc *) |
|
145 |
done |
|
146 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
147 |
lemma Suc_choose_self_nat [simp]: "(Suc n) choose n = Suc n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
148 |
using plus_one_choose_self_nat by (simp add: One_nat_def) |
31719 | 149 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
150 |
lemma plus_one_choose_self_int [rule_format, simp]: |
31719 | 151 |
"(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1" |
152 |
by (auto simp add: binomial_int_def nat_add_distrib) |
|
153 |
||
154 |
(* bounded quantification doesn't work with the unicode characters? *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
155 |
lemma choose_pos_nat [rule_format]: "ALL k <= (n::nat). |
31719 | 156 |
((n::nat) choose k) > 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
157 |
apply (induct n rule: induct'_nat) |
31719 | 158 |
apply force |
159 |
apply clarify |
|
160 |
apply (case_tac "k = 0") |
|
161 |
apply force |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
162 |
apply (subst choose_reduce_nat) |
31719 | 163 |
apply auto |
44872 | 164 |
done |
31719 | 165 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
166 |
lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow> |
31719 | 167 |
((n::int) choose k) > 0" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
168 |
by (auto simp add: binomial_int_def choose_pos_nat) |
31719 | 169 |
|
170 |
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> |
|
171 |
(ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow> |
|
172 |
P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
173 |
apply (induct n rule: induct'_nat) |
31719 | 174 |
apply auto |
175 |
apply (case_tac "k = 0") |
|
176 |
apply auto |
|
177 |
apply (case_tac "k = n + 1") |
|
178 |
apply auto |
|
179 |
apply (drule_tac x = n in spec) back back |
|
180 |
apply (drule_tac x = "k - 1" in spec) back back back |
|
181 |
apply auto |
|
44872 | 182 |
done |
31719 | 183 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
184 |
lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> |
31719 | 185 |
fact k * fact (n - k) * (n choose k) = fact n" |
186 |
apply (rule binomial_induct [of _ k n]) |
|
187 |
apply auto |
|
188 |
proof - |
|
189 |
fix k :: nat and n |
|
190 |
assume less: "k < n" |
|
191 |
assume ih1: "fact k * fact (n - k) * (n choose k) = fact n" |
|
44872 | 192 |
then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
193 |
by (subst fact_plus_one_nat, auto) |
44872 | 194 |
assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = fact n" |
31719 | 195 |
with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * |
196 |
(n choose (k + 1)) = (n - k) * fact n" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
197 |
by (subst (2) fact_plus_one_nat, auto) |
31719 | 198 |
with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = |
199 |
(n - k) * fact n" by simp |
|
200 |
have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = |
|
201 |
fact (k + 1) * fact (n - k) * (n choose (k + 1)) + |
|
202 |
fact (k + 1) * fact (n - k) * (n choose k)" |
|
36350 | 203 |
by (subst choose_reduce_nat, auto simp add: field_simps) |
31719 | 204 |
also note one |
205 |
also note two |
|
206 |
also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
207 |
apply (subst fact_plus_one_nat) |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
45933
diff
changeset
|
208 |
apply (subst distrib_right [symmetric]) |
31719 | 209 |
apply simp |
210 |
done |
|
211 |
finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = |
|
212 |
fact (n + 1)" . |
|
213 |
qed |
|
214 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
215 |
lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> |
31719 | 216 |
n choose k = fact n div (fact k * fact (n - k))" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
217 |
apply (frule choose_altdef_aux_nat) |
31719 | 218 |
apply (erule subst) |
219 |
apply (simp add: mult_ac) |
|
44872 | 220 |
done |
31719 | 221 |
|
222 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
223 |
lemma choose_altdef_int: |
31719 | 224 |
assumes "(0::int) <= k" and "k <= n" |
225 |
shows "n choose k = fact n div (fact k * fact (n - k))" |
|
41541 | 226 |
apply (subst tsub_eq [symmetric], rule assms) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
227 |
apply (rule choose_altdef_nat [transferred]) |
41541 | 228 |
using assms apply auto |
229 |
done |
|
31719 | 230 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
231 |
lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
232 |
unfolding dvd_def apply (frule choose_altdef_aux_nat) |
31719 | 233 |
(* why don't blast and auto get this??? *) |
234 |
apply (rule exI) |
|
235 |
apply (erule sym) |
|
44872 | 236 |
done |
31719 | 237 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
238 |
lemma choose_dvd_int: |
31719 | 239 |
assumes "(0::int) <= k" and "k <= n" |
240 |
shows "fact k * fact (n - k) dvd fact n" |
|
41541 | 241 |
apply (subst tsub_eq [symmetric], rule assms) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
242 |
apply (rule choose_dvd_nat [transferred]) |
41541 | 243 |
using assms apply auto |
244 |
done |
|
31719 | 245 |
|
246 |
(* generalizes Tobias Nipkow's proof to any commutative semiring *) |
|
247 |
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = |
|
248 |
(SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
249 |
proof (induct n rule: induct'_nat) |
31719 | 250 |
show "?P 0" by simp |
251 |
next |
|
252 |
fix n |
|
253 |
assume ih: "?P n" |
|
254 |
have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}" |
|
255 |
by auto |
|
256 |
have decomp2: "{0..n} = {0} Un {1..n}" |
|
257 |
by auto |
|
258 |
have decomp3: "{1..n+1} = {n+1} Un {1..n}" |
|
259 |
by auto |
|
260 |
have "(a+b)^(n+1) = |
|
261 |
(a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))" |
|
41541 | 262 |
using ih by simp |
31719 | 263 |
also have "... = a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) + |
264 |
b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))" |
|
265 |
by (rule distrib) |
|
266 |
also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + |
|
267 |
(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))" |
|
268 |
by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac) |
|
269 |
also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) + |
|
270 |
(SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))" |
|
41541 | 271 |
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le |
272 |
field_simps One_nat_def del:setsum_cl_ivl_Suc) |
|
31719 | 273 |
also have "... = a^(n+1) + b^(n+1) + |
274 |
(SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) + |
|
275 |
(SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))" |
|
276 |
by (simp add: decomp2 decomp3) |
|
277 |
also have |
|
278 |
"... = a^(n+1) + b^(n+1) + |
|
279 |
(SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))" |
|
36350 | 280 |
by (auto simp add: field_simps setsum_addf [symmetric] |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset
|
281 |
choose_reduce_nat) |
31719 | 282 |
also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))" |
36350 | 283 |
using decomp by (simp add: field_simps) |
31719 | 284 |
finally show "?P (n + 1)" by simp |
285 |
qed |
|
286 |
||
41340 | 287 |
lemma card_subsets_nat: |
31719 | 288 |
fixes S :: "'a set" |
41340 | 289 |
shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k" |
290 |
proof (induct arbitrary: k set: finite) |
|
44872 | 291 |
case empty |
292 |
show ?case by (auto simp add: Collect_conv_if) |
|
41340 | 293 |
next |
294 |
case (insert x F) |
|
295 |
note iassms = insert(1,2) |
|
296 |
note ih = insert(3) |
|
297 |
show ?case |
|
298 |
proof (induct k rule: induct'_nat) |
|
299 |
case zero |
|
300 |
from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}" |
|
301 |
by (auto simp: finite_subset) |
|
44872 | 302 |
then show ?case by auto |
41340 | 303 |
next |
304 |
case (plus1 k) |
|
305 |
from iassms have fin: "finite (insert x F)" by auto |
|
44872 | 306 |
then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} = |
41340 | 307 |
{T. T \<le> F & card T = k + 1} Un |
308 |
{T. T \<le> insert x F & x : T & card T = k + 1}" |
|
41541 | 309 |
by auto |
41340 | 310 |
with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = |
311 |
card ({T. T \<subseteq> F \<and> card T = k + 1}) + |
|
312 |
card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})" |
|
313 |
apply (subst card_Un_disjoint [symmetric]) |
|
314 |
apply auto |
|
315 |
(* note: nice! Didn't have to say anything here *) |
|
316 |
done |
|
317 |
also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = |
|
318 |
card F choose (k+1)" by auto |
|
319 |
also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) = |
|
320 |
card ({T. T <= F & card T = k})" |
|
321 |
proof - |
|
322 |
let ?f = "%T. T Un {x}" |
|
323 |
from iassms have "inj_on ?f {T. T <= F & card T = k}" |
|
41541 | 324 |
unfolding inj_on_def by auto |
44872 | 325 |
then have "card ({T. T <= F & card T = k}) = |
41340 | 326 |
card(?f ` {T. T <= F & card T = k})" |
327 |
by (rule card_image [symmetric]) |
|
328 |
also have "?f ` {T. T <= F & card T = k} = |
|
329 |
{T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R") |
|
330 |
proof- |
|
331 |
{ fix S assume "S \<subseteq> F" |
|
44872 | 332 |
then have "card(insert x S) = card S +1" |
41340 | 333 |
using iassms by (auto simp: finite_subset) } |
334 |
moreover |
|
335 |
{ fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1" |
|
336 |
let ?S = "T - {x}" |
|
337 |
have "?S <= F & card ?S = k \<and> T = insert x ?S" |
|
338 |
using 1 fin by (auto simp: finite_subset) } |
|
339 |
ultimately show ?thesis by(auto simp: image_def) |
|
31719 | 340 |
qed |
41340 | 341 |
finally show ?thesis by (rule sym) |
31719 | 342 |
qed |
41340 | 343 |
also from ih have "card ({T. T <= F & card T = k}) = card F choose k" |
344 |
by auto |
|
345 |
finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = |
|
346 |
card F choose (k + 1) + (card F choose k)". |
|
347 |
with iassms choose_plus_one_nat show ?case |
|
348 |
by (auto simp del: card.insert) |
|
31719 | 349 |
qed |
350 |
qed |
|
351 |
||
45933 | 352 |
lemma choose_le_pow: |
353 |
assumes "r \<le> n" shows "n choose r \<le> n ^ r" |
|
354 |
proof - |
|
355 |
have X: "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" |
|
356 |
by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL) |
|
357 |
have "n choose r \<le> fact n div fact (n - r)" |
|
358 |
using `r \<le> n` by (simp add: choose_altdef_nat div_le_mono2) |
|
359 |
also have "\<dots> \<le> n ^ r" using `r \<le> n` |
|
360 |
by (induct r rule: nat.induct) |
|
361 |
(auto simp add: fact_div_fact Suc_diff_Suc X One_nat_def mult_le_mono) |
|
362 |
finally show ?thesis . |
|
363 |
qed |
|
364 |
||
31719 | 365 |
end |