author  haftmann 
Mon, 08 Mar 2010 09:38:58 +0100  
changeset 35644  d20cf282342e 
parent 32479  521cc9bf2958 
child 35731  1bdaa24fb56d 
permissions  rwrr 
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)" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31719
diff
changeset

211 
by (subst choose_reduce_nat, auto simp add: ring_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^(nk))" (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^(nk))" 

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^(nk)) + 

274 
b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(nk))" 

275 
by (rule distrib) 

276 
also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(nk)) + 

277 
(SUM k=0..n. of_nat (n choose k) * a^k * b^(nk+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+1k)) + 

280 
(SUM k=1..n+1. of_nat (n choose (k  1)) * a^k * b^(n+1k))" 

281 
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le 

282 
power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc) 

283 
also have "... = a^(n+1) + b^(n+1) + 

284 
(SUM k=1..n. of_nat (n choose (k  1)) * a^k * b^(n+1k)) + 

285 
(SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1k))" 

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+1k))" 

290 
by (auto simp add: ring_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+1k))" 
293 
using decomp by (simp add: ring_simps) 

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 
31719  367 
by auto 
368 
qed 

369 
qed 

370 
qed 

371 
qed 

372 

373 
end 