18 |
18 |
19 |
19 |
20 subsection {* Main definitions *} |
20 subsection {* Main definitions *} |
21 |
21 |
22 class binomial = |
22 class binomial = |
23 |
23 fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65) |
24 fixes |
|
25 binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65) |
|
26 |
24 |
27 (* definitions for the natural numbers *) |
25 (* definitions for the natural numbers *) |
28 |
26 |
29 instantiation nat :: binomial |
27 instantiation nat :: binomial |
30 |
|
31 begin |
28 begin |
32 |
29 |
33 fun |
30 fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
34 binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
35 where |
31 where |
36 "binomial_nat n k = |
32 "binomial_nat n k = |
37 (if k = 0 then 1 else |
33 (if k = 0 then 1 else |
38 if n = 0 then 0 else |
34 if n = 0 then 0 else |
39 (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))" |
35 (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))" |
40 |
36 |
41 instance proof qed |
37 instance .. |
42 |
38 |
43 end |
39 end |
44 |
40 |
45 (* definitions for the integers *) |
41 (* definitions for the integers *) |
46 |
42 |
47 instantiation int :: binomial |
43 instantiation int :: binomial |
48 |
|
49 begin |
44 begin |
50 |
45 |
51 definition |
46 definition binomial_int :: "int => int \<Rightarrow> int" where |
52 binomial_int :: "int => int \<Rightarrow> int" |
47 "binomial_int n k = |
53 where |
48 (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k)) |
54 "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k)) |
49 else 0)" |
55 else 0)" |
50 |
56 instance proof qed |
51 instance .. |
57 |
52 |
58 end |
53 end |
59 |
54 |
60 |
55 |
61 subsection {* Set up Transfer *} |
56 subsection {* Set up Transfer *} |
95 |
90 |
96 lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0" |
91 lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0" |
97 by (induct n rule: induct'_nat, auto) |
92 by (induct n rule: induct'_nat, auto) |
98 |
93 |
99 lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0" |
94 lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0" |
100 unfolding binomial_int_def apply (case_tac "n < 0") |
95 unfolding binomial_int_def |
|
96 apply (cases "n < 0") |
101 apply force |
97 apply force |
102 apply (simp del: binomial_nat.simps) |
98 apply (simp del: binomial_nat.simps) |
103 done |
99 done |
104 |
100 |
105 lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow> |
101 lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow> |
106 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
102 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
107 by simp |
103 by simp |
108 |
104 |
109 lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow> |
105 lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow> |
110 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
106 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
111 unfolding binomial_int_def apply (subst choose_reduce_nat) |
107 unfolding binomial_int_def |
112 apply (auto simp del: binomial_nat.simps |
108 apply (subst choose_reduce_nat) |
113 simp add: nat_diff_distrib) |
109 apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib) |
114 done |
110 done |
115 |
111 |
116 lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = |
112 lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = |
117 (n choose (k + 1)) + (n choose k)" |
113 (n choose (k + 1)) + (n choose k)" |
118 by (simp add: choose_reduce_nat) |
114 by (simp add: choose_reduce_nat) |
119 |
115 |
126 by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps) |
122 by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps) |
127 |
123 |
128 declare binomial_nat.simps [simp del] |
124 declare binomial_nat.simps [simp del] |
129 |
125 |
130 lemma choose_self_nat [simp]: "((n::nat) choose n) = 1" |
126 lemma choose_self_nat [simp]: "((n::nat) choose n) = 1" |
131 by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat) |
127 by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat) |
132 |
128 |
133 lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1" |
129 lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1" |
134 by (auto simp add: binomial_int_def) |
130 by (auto simp add: binomial_int_def) |
135 |
131 |
136 lemma choose_one_nat [simp]: "(n::nat) choose 1 = n" |
132 lemma choose_one_nat [simp]: "(n::nat) choose 1 = n" |
137 by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat) |
133 by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat) |
138 |
134 |
139 lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n" |
135 lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n" |
140 by (auto simp add: binomial_int_def) |
136 by (auto simp add: binomial_int_def) |
141 |
137 |
142 lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1" |
138 lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1" |
163 apply clarify |
159 apply clarify |
164 apply (case_tac "k = 0") |
160 apply (case_tac "k = 0") |
165 apply force |
161 apply force |
166 apply (subst choose_reduce_nat) |
162 apply (subst choose_reduce_nat) |
167 apply auto |
163 apply auto |
168 done |
164 done |
169 |
165 |
170 lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow> |
166 lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow> |
171 ((n::int) choose k) > 0" |
167 ((n::int) choose k) > 0" |
172 by (auto simp add: binomial_int_def choose_pos_nat) |
168 by (auto simp add: binomial_int_def choose_pos_nat) |
173 |
169 |
181 apply (case_tac "k = n + 1") |
177 apply (case_tac "k = n + 1") |
182 apply auto |
178 apply auto |
183 apply (drule_tac x = n in spec) back back |
179 apply (drule_tac x = n in spec) back back |
184 apply (drule_tac x = "k - 1" in spec) back back back |
180 apply (drule_tac x = "k - 1" in spec) back back back |
185 apply auto |
181 apply auto |
186 done |
182 done |
187 |
183 |
188 lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> |
184 lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> |
189 fact k * fact (n - k) * (n choose k) = fact n" |
185 fact k * fact (n - k) * (n choose k) = fact n" |
190 apply (rule binomial_induct [of _ k n]) |
186 apply (rule binomial_induct [of _ k n]) |
191 apply auto |
187 apply auto |
192 proof - |
188 proof - |
193 fix k :: nat and n |
189 fix k :: nat and n |
194 assume less: "k < n" |
190 assume less: "k < n" |
195 assume ih1: "fact k * fact (n - k) * (n choose k) = fact n" |
191 assume ih1: "fact k * fact (n - k) * (n choose k) = fact n" |
196 hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n" |
192 then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n" |
197 by (subst fact_plus_one_nat, auto) |
193 by (subst fact_plus_one_nat, auto) |
198 assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = |
194 assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = fact n" |
199 fact n" |
|
200 with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * |
195 with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * |
201 (n choose (k + 1)) = (n - k) * fact n" |
196 (n choose (k + 1)) = (n - k) * fact n" |
202 by (subst (2) fact_plus_one_nat, auto) |
197 by (subst (2) fact_plus_one_nat, auto) |
203 with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = |
198 with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = |
204 (n - k) * fact n" by simp |
199 (n - k) * fact n" by simp |
220 lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> |
215 lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> |
221 n choose k = fact n div (fact k * fact (n - k))" |
216 n choose k = fact n div (fact k * fact (n - k))" |
222 apply (frule choose_altdef_aux_nat) |
217 apply (frule choose_altdef_aux_nat) |
223 apply (erule subst) |
218 apply (erule subst) |
224 apply (simp add: mult_ac) |
219 apply (simp add: mult_ac) |
225 done |
220 done |
226 |
221 |
227 |
222 |
228 lemma choose_altdef_int: |
223 lemma choose_altdef_int: |
229 assumes "(0::int) <= k" and "k <= n" |
224 assumes "(0::int) <= k" and "k <= n" |
230 shows "n choose k = fact n div (fact k * fact (n - k))" |
225 shows "n choose k = fact n div (fact k * fact (n - k))" |
236 lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n" |
231 lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n" |
237 unfolding dvd_def apply (frule choose_altdef_aux_nat) |
232 unfolding dvd_def apply (frule choose_altdef_aux_nat) |
238 (* why don't blast and auto get this??? *) |
233 (* why don't blast and auto get this??? *) |
239 apply (rule exI) |
234 apply (rule exI) |
240 apply (erule sym) |
235 apply (erule sym) |
241 done |
236 done |
242 |
237 |
243 lemma choose_dvd_int: |
238 lemma choose_dvd_int: |
244 assumes "(0::int) <= k" and "k <= n" |
239 assumes "(0::int) <= k" and "k <= n" |
245 shows "fact k * fact (n - k) dvd fact n" |
240 shows "fact k * fact (n - k) dvd fact n" |
246 apply (subst tsub_eq [symmetric], rule assms) |
241 apply (subst tsub_eq [symmetric], rule assms) |
291 |
286 |
292 lemma card_subsets_nat: |
287 lemma card_subsets_nat: |
293 fixes S :: "'a set" |
288 fixes S :: "'a set" |
294 shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k" |
289 shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k" |
295 proof (induct arbitrary: k set: finite) |
290 proof (induct arbitrary: k set: finite) |
296 case empty show ?case by (auto simp add: Collect_conv_if) |
291 case empty |
|
292 show ?case by (auto simp add: Collect_conv_if) |
297 next |
293 next |
298 case (insert x F) |
294 case (insert x F) |
299 note iassms = insert(1,2) |
295 note iassms = insert(1,2) |
300 note ih = insert(3) |
296 note ih = insert(3) |
301 show ?case |
297 show ?case |
302 proof (induct k rule: induct'_nat) |
298 proof (induct k rule: induct'_nat) |
303 case zero |
299 case zero |
304 from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}" |
300 from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}" |
305 by (auto simp: finite_subset) |
301 by (auto simp: finite_subset) |
306 thus ?case by auto |
302 then show ?case by auto |
307 next |
303 next |
308 case (plus1 k) |
304 case (plus1 k) |
309 from iassms have fin: "finite (insert x F)" by auto |
305 from iassms have fin: "finite (insert x F)" by auto |
310 hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} = |
306 then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} = |
311 {T. T \<le> F & card T = k + 1} Un |
307 {T. T \<le> F & card T = k + 1} Un |
312 {T. T \<le> insert x F & x : T & card T = k + 1}" |
308 {T. T \<le> insert x F & x : T & card T = k + 1}" |
313 by auto |
309 by auto |
314 with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = |
310 with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = |
315 card ({T. T \<subseteq> F \<and> card T = k + 1}) + |
311 card ({T. T \<subseteq> F \<and> card T = k + 1}) + |
324 card ({T. T <= F & card T = k})" |
320 card ({T. T <= F & card T = k})" |
325 proof - |
321 proof - |
326 let ?f = "%T. T Un {x}" |
322 let ?f = "%T. T Un {x}" |
327 from iassms have "inj_on ?f {T. T <= F & card T = k}" |
323 from iassms have "inj_on ?f {T. T <= F & card T = k}" |
328 unfolding inj_on_def by auto |
324 unfolding inj_on_def by auto |
329 hence "card ({T. T <= F & card T = k}) = |
325 then have "card ({T. T <= F & card T = k}) = |
330 card(?f ` {T. T <= F & card T = k})" |
326 card(?f ` {T. T <= F & card T = k})" |
331 by (rule card_image [symmetric]) |
327 by (rule card_image [symmetric]) |
332 also have "?f ` {T. T <= F & card T = k} = |
328 also have "?f ` {T. T <= F & card T = k} = |
333 {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R") |
329 {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R") |
334 proof- |
330 proof- |
335 { fix S assume "S \<subseteq> F" |
331 { fix S assume "S \<subseteq> F" |
336 hence "card(insert x S) = card S +1" |
332 then have "card(insert x S) = card S +1" |
337 using iassms by (auto simp: finite_subset) } |
333 using iassms by (auto simp: finite_subset) } |
338 moreover |
334 moreover |
339 { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1" |
335 { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1" |
340 let ?S = "T - {x}" |
336 let ?S = "T - {x}" |
341 have "?S <= F & card ?S = k \<and> T = insert x ?S" |
337 have "?S <= F & card ?S = k \<and> T = insert x ?S" |