author | kuncar |
Fri, 27 Sep 2013 14:43:26 +0200 | |
changeset 53952 | b2781a3ce958 |
parent 53374 | a14d2a854c02 |
child 55130 | 70db8d380d62 |
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 |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
51292
diff
changeset
|
206 |
also from 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 |
||
51291 | 365 |
lemma card_UNION: |
51292 | 366 |
assumes "finite A" and "\<forall>k \<in> A. finite k" |
51291 | 367 |
shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))" |
368 |
(is "?lhs = ?rhs") |
|
369 |
proof - |
|
370 |
have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp |
|
371 |
also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs") |
|
51292 | 372 |
by(subst setsum_right_distrib) simp |
51291 | 373 |
also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))" |
374 |
using assms by(subst setsum_Sigma)(auto) |
|
375 |
also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))" |
|
376 |
by(rule setsum_reindex_cong[where f="\<lambda>(x, y). (y, x)"])(auto intro: inj_onI simp add: split_beta) |
|
377 |
also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))" |
|
378 |
using assms by(auto intro!: setsum_mono_zero_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"]) |
|
379 |
also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. -1 ^ (card I + 1)))" |
|
380 |
using assms by(subst setsum_Sigma) auto |
|
381 |
also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _") |
|
382 |
proof(rule setsum_cong[OF refl]) |
|
383 |
fix x |
|
384 |
assume x: "x \<in> \<Union>A" |
|
385 |
def K \<equiv> "{X \<in> A. x \<in> X}" |
|
386 |
with `finite A` have K: "finite K" by auto |
|
387 |
||
388 |
let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}" |
|
389 |
have "inj_on snd (SIGMA i:{1..card A}. ?I i)" |
|
390 |
using assms by(auto intro!: inj_onI) |
|
391 |
moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}" |
|
392 |
using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq] One_nat_def dest: finite_subset intro: card_mono) |
|
393 |
ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))" |
|
394 |
by(rule setsum_reindex_cong[where f=snd]) fastforce |
|
395 |
also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))" |
|
396 |
using assms by(subst setsum_Sigma) auto |
|
397 |
also have "\<dots> = (\<Sum>i=1..card A. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))" |
|
51292 | 398 |
by(subst setsum_right_distrib) simp |
51291 | 399 |
also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs") |
400 |
proof(rule setsum_mono_zero_cong_right[rule_format]) |
|
401 |
show "{1..card K} \<subseteq> {1..card A}" using `finite A` |
|
402 |
by(auto simp add: K_def intro: card_mono) |
|
403 |
next |
|
404 |
fix i |
|
405 |
assume "i \<in> {1..card A} - {1..card K}" |
|
406 |
hence i: "i \<le> card A" "card K < i" by auto |
|
407 |
have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}" |
|
408 |
by(auto simp add: K_def) |
|
409 |
also have "\<dots> = {}" using `finite A` i |
|
410 |
by(auto simp add: K_def dest: card_mono[rotated 1]) |
|
411 |
finally show "-1 ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0" |
|
412 |
by(simp only:) simp |
|
413 |
next |
|
414 |
fix i |
|
415 |
have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)" |
|
416 |
(is "?lhs = ?rhs") |
|
417 |
by(rule setsum_cong)(auto simp add: K_def) |
|
418 |
thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp |
|
419 |
qed simp |
|
420 |
also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms |
|
421 |
by(auto simp add: card_eq_0_iff K_def dest: finite_subset) |
|
422 |
hence "?rhs = (\<Sum>i = 0..card K. -1 ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1" |
|
423 |
by(subst (2) setsum_head_Suc)(simp_all add: One_nat_def) |
|
424 |
also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1" |
|
425 |
using K by(subst card_subsets_nat[symmetric]) simp_all |
|
426 |
also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1" |
|
51292 | 427 |
by(subst setsum_right_distrib[symmetric]) simp |
51291 | 428 |
also have "\<dots> = - ((-1 + 1) ^ card K) + 1" |
429 |
by(subst binomial)(simp add: mult_ac) |
|
430 |
also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff) |
|
431 |
finally show "?lhs x = 1" . |
|
432 |
qed |
|
433 |
also have "nat \<dots> = card (\<Union>A)" by simp |
|
434 |
finally show ?thesis .. |
|
435 |
qed |
|
436 |
||
31719 | 437 |
end |