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