31719
|
1 |
(* Title: Binomial.thy
|
|
2 |
Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
|
|
3 |
|
|
4 |
|
|
5 |
Defines factorial and the "choose" function, and establishes basic properties.
|
|
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
|
|
19 |
imports Cong
|
|
20 |
begin
|
|
21 |
|
|
22 |
|
|
23 |
subsection {* Main definitions *}
|
|
24 |
|
|
25 |
class binomial =
|
|
26 |
|
|
27 |
fixes
|
|
28 |
fact :: "'a \<Rightarrow> 'a" and
|
|
29 |
binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
|
|
30 |
|
|
31 |
(* definitions for the natural numbers *)
|
|
32 |
|
|
33 |
instantiation nat :: binomial
|
|
34 |
|
|
35 |
begin
|
|
36 |
|
|
37 |
fun
|
|
38 |
fact_nat :: "nat \<Rightarrow> nat"
|
|
39 |
where
|
|
40 |
"fact_nat x =
|
|
41 |
(if x = 0 then 1 else
|
|
42 |
x * fact(x - 1))"
|
|
43 |
|
|
44 |
fun
|
|
45 |
binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
|
46 |
where
|
|
47 |
"binomial_nat n k =
|
|
48 |
(if k = 0 then 1 else
|
|
49 |
if n = 0 then 0 else
|
|
50 |
(binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
|
|
51 |
|
|
52 |
instance proof qed
|
|
53 |
|
|
54 |
end
|
|
55 |
|
|
56 |
(* definitions for the integers *)
|
|
57 |
|
|
58 |
instantiation int :: binomial
|
|
59 |
|
|
60 |
begin
|
|
61 |
|
|
62 |
definition
|
|
63 |
fact_int :: "int \<Rightarrow> int"
|
|
64 |
where
|
|
65 |
"fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
|
|
66 |
|
|
67 |
definition
|
|
68 |
binomial_int :: "int => int \<Rightarrow> int"
|
|
69 |
where
|
|
70 |
"binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
|
|
71 |
else 0)"
|
|
72 |
instance proof qed
|
|
73 |
|
|
74 |
end
|
|
75 |
|
|
76 |
|
|
77 |
subsection {* Set up Transfer *}
|
|
78 |
|
|
79 |
|
|
80 |
lemma transfer_nat_int_binomial:
|
|
81 |
"(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
|
|
82 |
"(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) =
|
|
83 |
nat (binomial n k)"
|
|
84 |
unfolding fact_int_def binomial_int_def
|
|
85 |
by auto
|
|
86 |
|
|
87 |
|
|
88 |
lemma transfer_nat_int_binomial_closures:
|
|
89 |
"x >= (0::int) \<Longrightarrow> fact x >= 0"
|
|
90 |
"n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
|
|
91 |
by (auto simp add: fact_int_def binomial_int_def)
|
|
92 |
|
|
93 |
declare TransferMorphism_nat_int[transfer add return:
|
|
94 |
transfer_nat_int_binomial transfer_nat_int_binomial_closures]
|
|
95 |
|
|
96 |
lemma transfer_int_nat_binomial:
|
|
97 |
"fact (int x) = int (fact x)"
|
|
98 |
"binomial (int n) (int k) = int (binomial n k)"
|
|
99 |
unfolding fact_int_def binomial_int_def by auto
|
|
100 |
|
|
101 |
lemma transfer_int_nat_binomial_closures:
|
|
102 |
"is_nat x \<Longrightarrow> fact x >= 0"
|
|
103 |
"is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
|
|
104 |
by (auto simp add: fact_int_def binomial_int_def)
|
|
105 |
|
|
106 |
declare TransferMorphism_int_nat[transfer add return:
|
|
107 |
transfer_int_nat_binomial transfer_int_nat_binomial_closures]
|
|
108 |
|
|
109 |
|
|
110 |
subsection {* Factorial *}
|
|
111 |
|
|
112 |
lemma nat_fact_zero [simp]: "fact (0::nat) = 1"
|
|
113 |
by simp
|
|
114 |
|
|
115 |
lemma int_fact_zero [simp]: "fact (0::int) = 1"
|
|
116 |
by (simp add: fact_int_def)
|
|
117 |
|
|
118 |
lemma nat_fact_one [simp]: "fact (1::nat) = 1"
|
|
119 |
by simp
|
|
120 |
|
|
121 |
lemma nat_fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
|
|
122 |
by (simp add: One_nat_def)
|
|
123 |
|
|
124 |
lemma int_fact_one [simp]: "fact (1::int) = 1"
|
|
125 |
by (simp add: fact_int_def)
|
|
126 |
|
|
127 |
lemma nat_fact_plus_one: "fact ((n::nat) + 1) = (n + 1) * fact n"
|
|
128 |
by simp
|
|
129 |
|
|
130 |
lemma nat_fact_Suc: "fact (Suc n) = (Suc n) * fact n"
|
|
131 |
by (simp add: One_nat_def)
|
|
132 |
|
|
133 |
lemma int_fact_plus_one:
|
|
134 |
assumes "n >= 0"
|
|
135 |
shows "fact ((n::int) + 1) = (n + 1) * fact n"
|
|
136 |
|
|
137 |
using prems by (rule nat_fact_plus_one [transferred])
|
|
138 |
|
|
139 |
lemma nat_fact_reduce: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
|
|
140 |
by simp
|
|
141 |
|
|
142 |
lemma int_fact_reduce:
|
|
143 |
assumes "(n::int) > 0"
|
|
144 |
shows "fact n = n * fact (n - 1)"
|
|
145 |
|
|
146 |
using prems apply (subst tsub_eq [symmetric], auto)
|
|
147 |
apply (rule nat_fact_reduce [transferred])
|
|
148 |
using prems apply auto
|
|
149 |
done
|
|
150 |
|
|
151 |
declare fact_nat.simps [simp del]
|
|
152 |
|
|
153 |
lemma nat_fact_nonzero [simp]: "fact (n::nat) \<noteq> 0"
|
|
154 |
apply (induct n rule: nat_induct')
|
|
155 |
apply (auto simp add: nat_fact_plus_one)
|
|
156 |
done
|
|
157 |
|
|
158 |
lemma int_fact_nonzero [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
|
|
159 |
by (simp add: fact_int_def)
|
|
160 |
|
|
161 |
lemma nat_fact_gt_zero [simp]: "fact (n :: nat) > 0"
|
|
162 |
by (insert nat_fact_nonzero [of n], arith)
|
|
163 |
|
|
164 |
lemma int_fact_gt_zero [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
|
|
165 |
by (auto simp add: fact_int_def)
|
|
166 |
|
|
167 |
lemma nat_fact_ge_one [simp]: "fact (n :: nat) >= 1"
|
|
168 |
by (insert nat_fact_nonzero [of n], arith)
|
|
169 |
|
|
170 |
lemma nat_fact_ge_Suc_0 [simp]: "fact (n :: nat) >= Suc 0"
|
|
171 |
by (insert nat_fact_nonzero [of n], arith)
|
|
172 |
|
|
173 |
lemma int_fact_ge_one [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
|
|
174 |
apply (auto simp add: fact_int_def)
|
|
175 |
apply (subgoal_tac "1 = int 1")
|
|
176 |
apply (erule ssubst)
|
|
177 |
apply (subst zle_int)
|
|
178 |
apply auto
|
|
179 |
done
|
|
180 |
|
|
181 |
lemma nat_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
|
|
182 |
apply (induct n rule: nat_induct')
|
|
183 |
apply (auto simp add: nat_fact_plus_one)
|
|
184 |
apply (subgoal_tac "m = n + 1")
|
|
185 |
apply auto
|
|
186 |
done
|
|
187 |
|
|
188 |
lemma int_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
|
|
189 |
apply (case_tac "1 <= n")
|
|
190 |
apply (induct n rule: int_ge_induct)
|
|
191 |
apply (auto simp add: int_fact_plus_one)
|
|
192 |
apply (subgoal_tac "m = i + 1")
|
|
193 |
apply auto
|
|
194 |
done
|
|
195 |
|
|
196 |
lemma nat_interval_plus_one: "(i::nat) <= j + 1 \<Longrightarrow>
|
|
197 |
{i..j+1} = {i..j} Un {j+1}"
|
|
198 |
by auto
|
|
199 |
|
|
200 |
lemma int_interval_plus_one: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
|
|
201 |
by auto
|
|
202 |
|
|
203 |
lemma nat_fact_altdef: "fact (n::nat) = (PROD i:{1..n}. i)"
|
|
204 |
apply (induct n rule: nat_induct')
|
|
205 |
apply force
|
|
206 |
apply (subst nat_fact_plus_one)
|
|
207 |
apply (subst nat_interval_plus_one)
|
|
208 |
apply auto
|
|
209 |
done
|
|
210 |
|
|
211 |
lemma int_fact_altdef: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
|
|
212 |
apply (induct n rule: int_ge_induct)
|
|
213 |
apply force
|
|
214 |
apply (subst int_fact_plus_one, assumption)
|
|
215 |
apply (subst int_interval_plus_one)
|
|
216 |
apply auto
|
|
217 |
done
|
|
218 |
|
|
219 |
subsection {* Infinitely many primes *}
|
|
220 |
|
|
221 |
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
|
|
222 |
proof-
|
|
223 |
have f1: "fact n + 1 \<noteq> 1" using nat_fact_ge_one [of n] by arith
|
|
224 |
from nat_prime_factor [OF f1]
|
|
225 |
obtain p where "prime p" and "p dvd fact n + 1" by auto
|
|
226 |
hence "p \<le> fact n + 1"
|
|
227 |
by (intro dvd_imp_le, auto)
|
|
228 |
{assume "p \<le> n"
|
|
229 |
from `prime p` have "p \<ge> 1"
|
|
230 |
by (cases p, simp_all)
|
|
231 |
with `p <= n` have "p dvd fact n"
|
|
232 |
by (intro nat_dvd_fact)
|
|
233 |
with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
|
|
234 |
by (rule nat_dvd_diff)
|
|
235 |
hence "p dvd 1" by simp
|
|
236 |
hence "p <= 1" by auto
|
|
237 |
moreover from `prime p` have "p > 1" by auto
|
|
238 |
ultimately have False by auto}
|
|
239 |
hence "n < p" by arith
|
|
240 |
with `prime p` and `p <= fact n + 1` show ?thesis by auto
|
|
241 |
qed
|
|
242 |
|
|
243 |
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
|
|
244 |
using next_prime_bound by auto
|
|
245 |
|
|
246 |
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
|
|
247 |
proof
|
|
248 |
assume "finite {(p::nat). prime p}"
|
|
249 |
with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
|
|
250 |
by auto
|
|
251 |
then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
|
|
252 |
by auto
|
|
253 |
with bigger_prime [of b] show False by auto
|
|
254 |
qed
|
|
255 |
|
|
256 |
|
|
257 |
subsection {* Binomial coefficients *}
|
|
258 |
|
|
259 |
lemma nat_choose_zero [simp]: "(n::nat) choose 0 = 1"
|
|
260 |
by simp
|
|
261 |
|
|
262 |
lemma int_choose_zero [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
|
|
263 |
by (simp add: binomial_int_def)
|
|
264 |
|
|
265 |
lemma nat_zero_choose [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
|
|
266 |
by (induct n rule: nat_induct', auto)
|
|
267 |
|
|
268 |
lemma int_zero_choose [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
|
|
269 |
unfolding binomial_int_def apply (case_tac "n < 0")
|
|
270 |
apply force
|
|
271 |
apply (simp del: binomial_nat.simps)
|
|
272 |
done
|
|
273 |
|
|
274 |
lemma nat_choose_reduce: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
|
|
275 |
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
|
|
276 |
by simp
|
|
277 |
|
|
278 |
lemma int_choose_reduce: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
|
|
279 |
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
|
|
280 |
unfolding binomial_int_def apply (subst nat_choose_reduce)
|
|
281 |
apply (auto simp del: binomial_nat.simps
|
|
282 |
simp add: nat_diff_distrib)
|
|
283 |
done
|
|
284 |
|
|
285 |
lemma nat_choose_plus_one: "((n::nat) + 1) choose (k + 1) =
|
|
286 |
(n choose (k + 1)) + (n choose k)"
|
|
287 |
by (simp add: nat_choose_reduce)
|
|
288 |
|
|
289 |
lemma nat_choose_Suc: "(Suc n) choose (Suc k) =
|
|
290 |
(n choose (Suc k)) + (n choose k)"
|
|
291 |
by (simp add: nat_choose_reduce One_nat_def)
|
|
292 |
|
|
293 |
lemma int_choose_plus_one: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) =
|
|
294 |
(n choose (k + 1)) + (n choose k)"
|
|
295 |
by (simp add: binomial_int_def nat_choose_plus_one nat_add_distrib
|
|
296 |
del: binomial_nat.simps)
|
|
297 |
|
|
298 |
declare binomial_nat.simps [simp del]
|
|
299 |
|
|
300 |
lemma nat_choose_self [simp]: "((n::nat) choose n) = 1"
|
|
301 |
by (induct n rule: nat_induct', auto simp add: nat_choose_plus_one)
|
|
302 |
|
|
303 |
lemma int_choose_self [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
|
|
304 |
by (auto simp add: binomial_int_def)
|
|
305 |
|
|
306 |
lemma nat_choose_one [simp]: "(n::nat) choose 1 = n"
|
|
307 |
by (induct n rule: nat_induct', auto simp add: nat_choose_reduce)
|
|
308 |
|
|
309 |
lemma int_choose_one [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
|
|
310 |
by (auto simp add: binomial_int_def)
|
|
311 |
|
|
312 |
lemma nat_plus_one_choose_self [simp]: "(n::nat) + 1 choose n = n + 1"
|
|
313 |
apply (induct n rule: nat_induct', force)
|
|
314 |
apply (case_tac "n = 0")
|
|
315 |
apply auto
|
|
316 |
apply (subst nat_choose_reduce)
|
|
317 |
apply (auto simp add: One_nat_def)
|
|
318 |
(* natdiff_cancel_numerals introduces Suc *)
|
|
319 |
done
|
|
320 |
|
|
321 |
lemma nat_Suc_choose_self [simp]: "(Suc n) choose n = Suc n"
|
|
322 |
using nat_plus_one_choose_self by (simp add: One_nat_def)
|
|
323 |
|
|
324 |
lemma int_plus_one_choose_self [rule_format, simp]:
|
|
325 |
"(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
|
|
326 |
by (auto simp add: binomial_int_def nat_add_distrib)
|
|
327 |
|
|
328 |
(* bounded quantification doesn't work with the unicode characters? *)
|
|
329 |
lemma nat_choose_pos [rule_format]: "ALL k <= (n::nat).
|
|
330 |
((n::nat) choose k) > 0"
|
|
331 |
apply (induct n rule: nat_induct')
|
|
332 |
apply force
|
|
333 |
apply clarify
|
|
334 |
apply (case_tac "k = 0")
|
|
335 |
apply force
|
|
336 |
apply (subst nat_choose_reduce)
|
|
337 |
apply auto
|
|
338 |
done
|
|
339 |
|
|
340 |
lemma int_choose_pos: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
|
|
341 |
((n::int) choose k) > 0"
|
|
342 |
by (auto simp add: binomial_int_def nat_choose_pos)
|
|
343 |
|
|
344 |
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
|
|
345 |
(ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
|
|
346 |
P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
|
|
347 |
apply (induct n rule: nat_induct')
|
|
348 |
apply auto
|
|
349 |
apply (case_tac "k = 0")
|
|
350 |
apply auto
|
|
351 |
apply (case_tac "k = n + 1")
|
|
352 |
apply auto
|
|
353 |
apply (drule_tac x = n in spec) back back
|
|
354 |
apply (drule_tac x = "k - 1" in spec) back back back
|
|
355 |
apply auto
|
|
356 |
done
|
|
357 |
|
|
358 |
lemma nat_choose_altdef_aux: "(k::nat) \<le> n \<Longrightarrow>
|
|
359 |
fact k * fact (n - k) * (n choose k) = fact n"
|
|
360 |
apply (rule binomial_induct [of _ k n])
|
|
361 |
apply auto
|
|
362 |
proof -
|
|
363 |
fix k :: nat and n
|
|
364 |
assume less: "k < n"
|
|
365 |
assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
|
|
366 |
hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
|
|
367 |
by (subst nat_fact_plus_one, auto)
|
|
368 |
assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =
|
|
369 |
fact n"
|
|
370 |
with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) *
|
|
371 |
(n choose (k + 1)) = (n - k) * fact n"
|
|
372 |
by (subst (2) nat_fact_plus_one, auto)
|
|
373 |
with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) =
|
|
374 |
(n - k) * fact n" by simp
|
|
375 |
have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
|
|
376 |
fact (k + 1) * fact (n - k) * (n choose (k + 1)) +
|
|
377 |
fact (k + 1) * fact (n - k) * (n choose k)"
|
|
378 |
by (subst nat_choose_reduce, auto simp add: ring_simps)
|
|
379 |
also note one
|
|
380 |
also note two
|
|
381 |
also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
|
|
382 |
apply (subst nat_fact_plus_one)
|
|
383 |
apply (subst left_distrib [symmetric])
|
|
384 |
apply simp
|
|
385 |
done
|
|
386 |
finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
|
|
387 |
fact (n + 1)" .
|
|
388 |
qed
|
|
389 |
|
|
390 |
lemma nat_choose_altdef: "(k::nat) \<le> n \<Longrightarrow>
|
|
391 |
n choose k = fact n div (fact k * fact (n - k))"
|
|
392 |
apply (frule nat_choose_altdef_aux)
|
|
393 |
apply (erule subst)
|
|
394 |
apply (simp add: mult_ac)
|
|
395 |
done
|
|
396 |
|
|
397 |
|
|
398 |
lemma int_choose_altdef:
|
|
399 |
assumes "(0::int) <= k" and "k <= n"
|
|
400 |
shows "n choose k = fact n div (fact k * fact (n - k))"
|
|
401 |
|
|
402 |
apply (subst tsub_eq [symmetric], rule prems)
|
|
403 |
apply (rule nat_choose_altdef [transferred])
|
|
404 |
using prems apply auto
|
|
405 |
done
|
|
406 |
|
|
407 |
lemma nat_choose_dvd: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
|
|
408 |
unfolding dvd_def apply (frule nat_choose_altdef_aux)
|
|
409 |
(* why don't blast and auto get this??? *)
|
|
410 |
apply (rule exI)
|
|
411 |
apply (erule sym)
|
|
412 |
done
|
|
413 |
|
|
414 |
lemma int_choose_dvd:
|
|
415 |
assumes "(0::int) <= k" and "k <= n"
|
|
416 |
shows "fact k * fact (n - k) dvd fact n"
|
|
417 |
|
|
418 |
apply (subst tsub_eq [symmetric], rule prems)
|
|
419 |
apply (rule nat_choose_dvd [transferred])
|
|
420 |
using prems apply auto
|
|
421 |
done
|
|
422 |
|
|
423 |
(* generalizes Tobias Nipkow's proof to any commutative semiring *)
|
|
424 |
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n =
|
|
425 |
(SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
|
|
426 |
proof (induct n rule: nat_induct')
|
|
427 |
show "?P 0" by simp
|
|
428 |
next
|
|
429 |
fix n
|
|
430 |
assume ih: "?P n"
|
|
431 |
have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
|
|
432 |
by auto
|
|
433 |
have decomp2: "{0..n} = {0} Un {1..n}"
|
|
434 |
by auto
|
|
435 |
have decomp3: "{1..n+1} = {n+1} Un {1..n}"
|
|
436 |
by auto
|
|
437 |
have "(a+b)^(n+1) =
|
|
438 |
(a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
|
|
439 |
using ih by (simp add: power_plus_one)
|
|
440 |
also have "... = a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
|
|
441 |
b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
|
|
442 |
by (rule distrib)
|
|
443 |
also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
|
|
444 |
(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
|
|
445 |
by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
|
|
446 |
also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
|
|
447 |
(SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
|
|
448 |
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
|
|
449 |
power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc)
|
|
450 |
also have "... = a^(n+1) + b^(n+1) +
|
|
451 |
(SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
|
|
452 |
(SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
|
|
453 |
by (simp add: decomp2 decomp3)
|
|
454 |
also have
|
|
455 |
"... = a^(n+1) + b^(n+1) +
|
|
456 |
(SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
|
|
457 |
by (auto simp add: ring_simps setsum_addf [symmetric]
|
|
458 |
nat_choose_reduce)
|
|
459 |
also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
|
|
460 |
using decomp by (simp add: ring_simps)
|
|
461 |
finally show "?P (n + 1)" by simp
|
|
462 |
qed
|
|
463 |
|
|
464 |
lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
|
|
465 |
by auto
|
|
466 |
|
|
467 |
lemma nat_card_subsets [rule_format]:
|
|
468 |
fixes S :: "'a set"
|
|
469 |
assumes "finite S"
|
|
470 |
shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k"
|
|
471 |
(is "?P S")
|
|
472 |
using `finite S`
|
|
473 |
proof (induct set: finite)
|
|
474 |
show "?P {}" by (auto simp add: set_explicit)
|
|
475 |
next fix x :: "'a" and F
|
|
476 |
assume iassms: "finite F" "x ~: F"
|
|
477 |
assume ih: "?P F"
|
|
478 |
show "?P (insert x F)" (is "ALL k. ?Q k")
|
|
479 |
proof
|
|
480 |
fix k
|
|
481 |
show "card {T. T \<subseteq> (insert x F) \<and> card T = k} =
|
|
482 |
card (insert x F) choose k" (is "?Q k")
|
|
483 |
proof (induct k rule: nat_induct')
|
|
484 |
from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
|
|
485 |
apply auto
|
|
486 |
apply (subst (asm) card_0_eq)
|
|
487 |
apply (auto elim: finite_subset)
|
|
488 |
done
|
|
489 |
thus "?Q 0"
|
|
490 |
by auto
|
|
491 |
next fix k
|
|
492 |
show "?Q (k + 1)"
|
|
493 |
proof -
|
|
494 |
from iassms have fin: "finite (insert x F)" by auto
|
|
495 |
hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
|
|
496 |
{T. T \<le> F & card T = k + 1} Un
|
|
497 |
{T. T \<le> insert x F & x : T & card T = k + 1}"
|
|
498 |
by (auto intro!: subsetI)
|
|
499 |
with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
|
|
500 |
card ({T. T \<subseteq> F \<and> card T = k + 1}) +
|
|
501 |
card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
|
|
502 |
apply (subst card_Un_disjoint [symmetric])
|
|
503 |
apply auto
|
|
504 |
(* note: nice! Didn't have to say anything here *)
|
|
505 |
done
|
|
506 |
also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) =
|
|
507 |
card F choose (k+1)" by auto
|
|
508 |
also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
|
|
509 |
card ({T. T <= F & card T = k})"
|
|
510 |
proof -
|
|
511 |
let ?f = "%T. T Un {x}"
|
|
512 |
from iassms have "inj_on ?f {T. T <= F & card T = k}"
|
|
513 |
unfolding inj_on_def by (auto intro!: subsetI)
|
|
514 |
hence "card ({T. T <= F & card T = k}) =
|
|
515 |
card(?f ` {T. T <= F & card T = k})"
|
|
516 |
by (rule card_image [symmetric])
|
|
517 |
also from iassms fin have "?f ` {T. T <= F & card T = k} =
|
|
518 |
{T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}"
|
|
519 |
unfolding image_def
|
|
520 |
(* I can't figure out why this next line takes so long *)
|
|
521 |
apply auto
|
|
522 |
apply (frule (1) finite_subset, force)
|
|
523 |
apply (rule_tac x = "xa - {x}" in exI)
|
|
524 |
apply (subst card_Diff_singleton)
|
|
525 |
apply (auto elim: finite_subset)
|
|
526 |
done
|
|
527 |
finally show ?thesis by (rule sym)
|
|
528 |
qed
|
|
529 |
also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
|
|
530 |
by auto
|
|
531 |
finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
|
|
532 |
card F choose (k + 1) + (card F choose k)".
|
|
533 |
with iassms nat_choose_plus_one show ?thesis
|
|
534 |
by auto
|
|
535 |
qed
|
|
536 |
qed
|
|
537 |
qed
|
|
538 |
qed
|
|
539 |
|
|
540 |
end
|