author | wenzelm |
Tue, 09 Apr 2013 21:39:55 +0200 | |
changeset 51667 | 354c23ef2784 |
parent 50240 | 019d642d422d |
child 52903 | 6c89225ddeba |
permissions | -rw-r--r-- |
35372 | 1 |
(* Title: HOL/Library/Binomial.thy |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
2 |
Author: Lawrence C Paulson, Amine Chaieb |
21256 | 3 |
Copyright 1997 University of Cambridge |
4 |
*) |
|
5 |
||
21263 | 6 |
header {* Binomial Coefficients *} |
21256 | 7 |
|
8 |
theory Binomial |
|
35372 | 9 |
imports Complex_Main |
21256 | 10 |
begin |
11 |
||
21263 | 12 |
text {* This development is based on the work of Andy Gordon and |
13 |
Florian Kammueller. *} |
|
21256 | 14 |
|
29931 | 15 |
primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) where |
21263 | 16 |
binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" |
48830 | 17 |
| binomial_Suc: "(Suc n choose k) = |
21256 | 18 |
(if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
19 |
||
20 |
lemma binomial_n_0 [simp]: "(n choose 0) = 1" |
|
48830 | 21 |
by (cases n) simp_all |
21256 | 22 |
|
23 |
lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" |
|
48830 | 24 |
by simp |
21256 | 25 |
|
26 |
lemma binomial_Suc_Suc [simp]: |
|
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
27 |
"(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" |
48830 | 28 |
by simp |
21256 | 29 |
|
21263 | 30 |
lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0" |
48830 | 31 |
by (induct n) auto |
21256 | 32 |
|
33 |
declare binomial_0 [simp del] binomial_Suc [simp del] |
|
34 |
||
35 |
lemma binomial_n_n [simp]: "(n choose n) = 1" |
|
48830 | 36 |
by (induct n) (simp_all add: binomial_eq_0) |
21256 | 37 |
|
38 |
lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" |
|
48830 | 39 |
by (induct n) simp_all |
21256 | 40 |
|
41 |
lemma binomial_1 [simp]: "(n choose Suc 0) = n" |
|
48830 | 42 |
by (induct n) simp_all |
21256 | 43 |
|
25162 | 44 |
lemma zero_less_binomial: "k \<le> n ==> (n choose k) > 0" |
48830 | 45 |
by (induct n k rule: diff_induct) simp_all |
21256 | 46 |
|
47 |
lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)" |
|
48830 | 48 |
apply (safe intro!: binomial_eq_0) |
49 |
apply (erule contrapos_pp) |
|
50 |
apply (simp add: zero_less_binomial) |
|
51 |
done |
|
21256 | 52 |
|
25162 | 53 |
lemma zero_less_binomial_iff: "(n choose k > 0) = (k\<le>n)" |
48830 | 54 |
by (simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] del: neq0_conv) |
21256 | 55 |
|
56 |
(*Might be more useful if re-oriented*) |
|
21263 | 57 |
lemma Suc_times_binomial_eq: |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
58 |
"!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" |
48830 | 59 |
apply (induct n) |
60 |
apply (simp add: binomial_0) |
|
61 |
apply (case_tac k) |
|
62 |
apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) |
|
63 |
done |
|
21256 | 64 |
|
65 |
text{*This is the well-known version, but it's harder to use because of the |
|
66 |
need to reason about division.*} |
|
67 |
lemma binomial_Suc_Suc_eq_times: |
|
21263 | 68 |
"k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" |
46507 | 69 |
by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) |
21256 | 70 |
|
71 |
text{*Another version, with -1 instead of Suc.*} |
|
72 |
lemma times_binomial_minus1_eq: |
|
21263 | 73 |
"[|k \<le> n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))" |
74 |
apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) |
|
48830 | 75 |
apply (simp split add: nat_diff_split, auto) |
21263 | 76 |
done |
77 |
||
21256 | 78 |
|
25378 | 79 |
subsection {* Theorems about @{text "choose"} *} |
21256 | 80 |
|
81 |
text {* |
|
82 |
\medskip Basic theorem about @{text "choose"}. By Florian |
|
83 |
Kamm\"uller, tidied by LCP. |
|
84 |
*} |
|
85 |
||
48830 | 86 |
lemma card_s_0_eq_empty: "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1" |
87 |
by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) |
|
21256 | 88 |
|
89 |
lemma choose_deconstruct: "finite M ==> x \<notin> M |
|
90 |
==> {s. s <= insert x M & card(s) = Suc k} |
|
91 |
= {s. s <= M & card(s) = Suc k} Un |
|
92 |
{s. EX t. t <= M & card(t) = k & s = insert x t}" |
|
93 |
apply safe |
|
48830 | 94 |
apply (auto intro: finite_subset [THEN card_insert_disjoint]) |
21256 | 95 |
apply (drule_tac x = "xa - {x}" in spec) |
96 |
apply (subgoal_tac "x \<notin> xa", auto) |
|
97 |
apply (erule rev_mp, subst card_Diff_singleton) |
|
48830 | 98 |
apply (auto intro: finite_subset) |
21256 | 99 |
done |
29918 | 100 |
(* |
101 |
lemma "finite(UN y. {x. P x y})" |
|
102 |
apply simp |
|
103 |
lemma Collect_ex_eq |
|
104 |
||
105 |
lemma "{x. EX y. P x y} = (UN y. {x. P x y})" |
|
106 |
apply blast |
|
107 |
*) |
|
108 |
||
109 |
lemma finite_bex_subset[simp]: |
|
110 |
"finite B \<Longrightarrow> (!!A. A<=B \<Longrightarrow> finite{x. P x A}) \<Longrightarrow> finite{x. EX A<=B. P x A}" |
|
48830 | 111 |
apply (subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})") |
112 |
apply simp |
|
113 |
apply blast |
|
114 |
done |
|
21256 | 115 |
|
116 |
text{*There are as many subsets of @{term A} having cardinality @{term k} |
|
117 |
as there are sets obtained from the former by inserting a fixed element |
|
118 |
@{term x} into each.*} |
|
119 |
lemma constr_bij: |
|
120 |
"[|finite A; x \<notin> A|] ==> |
|
121 |
card {B. EX C. C <= A & card(C) = k & B = insert x C} = |
|
122 |
card {B. B <= A & card(B) = k}" |
|
48830 | 123 |
apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) |
124 |
apply (auto elim!: equalityE simp add: inj_on_def) |
|
125 |
apply (subst Diff_insert0, auto) |
|
126 |
done |
|
21256 | 127 |
|
128 |
text {* |
|
129 |
Main theorem: combinatorial statement about number of subsets of a set. |
|
130 |
*} |
|
131 |
||
132 |
lemma n_sub_lemma: |
|
21263 | 133 |
"!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)" |
21256 | 134 |
apply (induct k) |
135 |
apply (simp add: card_s_0_eq_empty, atomize) |
|
136 |
apply (rotate_tac -1, erule finite_induct) |
|
137 |
apply (simp_all (no_asm_simp) cong add: conj_cong |
|
138 |
add: card_s_0_eq_empty choose_deconstruct) |
|
139 |
apply (subst card_Un_disjoint) |
|
140 |
prefer 4 apply (force simp add: constr_bij) |
|
141 |
prefer 3 apply force |
|
142 |
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] |
|
143 |
finite_subset [of _ "Pow (insert x F)", standard]) |
|
144 |
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) |
|
145 |
done |
|
146 |
||
147 |
theorem n_subsets: |
|
148 |
"finite A ==> card {B. B <= A & card B = k} = (card A choose k)" |
|
149 |
by (simp add: n_sub_lemma) |
|
150 |
||
151 |
||
152 |
text{* The binomial theorem (courtesy of Tobias Nipkow): *} |
|
153 |
||
154 |
theorem binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))" |
|
155 |
proof (induct n) |
|
156 |
case 0 thus ?case by simp |
|
157 |
next |
|
158 |
case (Suc n) |
|
159 |
have decomp: "{0..n+1} = {0} \<union> {n+1} \<union> {1..n}" |
|
160 |
by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) |
|
161 |
have decomp2: "{0..n} = {0} \<union> {1..n}" |
|
162 |
by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) |
|
163 |
have "(a+b::nat)^(n+1) = (a+b) * (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))" |
|
164 |
using Suc by simp |
|
165 |
also have "\<dots> = a*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k)) + |
|
166 |
b*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))" |
|
21263 | 167 |
by (rule nat_distrib) |
21256 | 168 |
also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + |
169 |
(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k+1))" |
|
21263 | 170 |
by (simp add: setsum_right_distrib mult_ac) |
21256 | 171 |
also have "\<dots> = (\<Sum>k=0..n. (n choose k) * a^k * b^(n+1-k)) + |
172 |
(\<Sum>k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" |
|
173 |
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le |
|
174 |
del:setsum_cl_ivl_Suc) |
|
175 |
also have "\<dots> = a^(n+1) + b^(n+1) + |
|
176 |
(\<Sum>k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + |
|
177 |
(\<Sum>k=1..n. (n choose k) * a^k * b^(n+1-k))" |
|
21263 | 178 |
by (simp add: decomp2) |
21256 | 179 |
also have |
21263 | 180 |
"\<dots> = a^(n+1) + b^(n+1) + (\<Sum>k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" |
181 |
by (simp add: nat_distrib setsum_addf binomial.simps) |
|
21256 | 182 |
also have "\<dots> = (\<Sum>k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" |
183 |
using decomp by simp |
|
184 |
finally show ?case by simp |
|
185 |
qed |
|
186 |
||
29906 | 187 |
subsection{* Pochhammer's symbol : generalized raising factorial*} |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
188 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
189 |
definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
190 |
|
48830 | 191 |
lemma pochhammer_0[simp]: "pochhammer a 0 = 1" |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
192 |
by (simp add: pochhammer_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
193 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
194 |
lemma pochhammer_1[simp]: "pochhammer a 1 = a" by (simp add: pochhammer_def) |
48830 | 195 |
lemma pochhammer_Suc0[simp]: "pochhammer a (Suc 0) = a" |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
196 |
by (simp add: pochhammer_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
197 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
198 |
lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
199 |
by (simp add: pochhammer_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
200 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
201 |
lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
202 |
proof- |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
203 |
have eq: "{0..Suc n} = {0..n} \<union> {Suc n}" by auto |
46757 | 204 |
show ?thesis unfolding eq by (simp add: field_simps) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
205 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
206 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
207 |
lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
208 |
proof- |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
209 |
have eq: "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto |
46757 | 210 |
show ?thesis unfolding eq by simp |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
211 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
212 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
213 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
214 |
lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
215 |
proof- |
48830 | 216 |
{ assume "n=0" then have ?thesis by simp } |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
217 |
moreover |
48830 | 218 |
{ fix m assume m: "n = Suc m" |
219 |
have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc .. } |
|
220 |
ultimately show ?thesis by (cases n) auto |
|
221 |
qed |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
222 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
223 |
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
224 |
proof- |
48830 | 225 |
{ assume "n=0" then have ?thesis by (simp add: pochhammer_Suc_setprod) } |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
226 |
moreover |
48830 | 227 |
{ assume n0: "n \<noteq> 0" |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
228 |
have th0: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
229 |
have eq: "insert 0 {1 .. n} = {0..n}" by auto |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
230 |
have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) = |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
231 |
(\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)" |
37388 | 232 |
apply (rule setprod_reindex_cong [where f = Suc]) |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
233 |
using n0 by (auto simp add: fun_eq_iff field_simps) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
234 |
have ?thesis apply (simp add: pochhammer_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
235 |
unfolding setprod_insert[OF th0, unfolded eq] |
48830 | 236 |
using th1 by (simp add: field_simps) } |
237 |
ultimately show ?thesis by blast |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
238 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
239 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
240 |
lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n" |
32042 | 241 |
unfolding fact_altdef_nat |
48830 | 242 |
apply (cases n) |
243 |
apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
244 |
apply (rule setprod_reindex_cong[where f=Suc]) |
48830 | 245 |
apply (auto simp add: fun_eq_iff) |
246 |
done |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
247 |
|
48830 | 248 |
lemma pochhammer_of_nat_eq_0_lemma: |
249 |
assumes kn: "k > n" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
250 |
shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
251 |
proof- |
48830 | 252 |
from kn obtain h where h: "k = Suc h" by (cases k) auto |
253 |
{ assume n0: "n=0" then have ?thesis using kn |
|
254 |
by (cases k) (simp_all add: pochhammer_rec) } |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
255 |
moreover |
48830 | 256 |
{ assume n0: "n \<noteq> 0" |
257 |
then have ?thesis |
|
258 |
apply (simp add: h pochhammer_Suc_setprod) |
|
259 |
apply (rule_tac x="n" in bexI) |
|
260 |
using h kn |
|
261 |
apply auto |
|
262 |
done } |
|
263 |
ultimately show ?thesis by blast |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
264 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
265 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
266 |
lemma pochhammer_of_nat_eq_0_lemma': assumes kn: "k \<le> n" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
267 |
shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k \<noteq> 0" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
268 |
proof- |
48830 | 269 |
{ assume "k=0" then have ?thesis by simp } |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
270 |
moreover |
48830 | 271 |
{ fix h assume h: "k = Suc h" |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
272 |
then have ?thesis apply (simp add: pochhammer_Suc_setprod) |
48830 | 273 |
using h kn by (auto simp add: algebra_simps) } |
274 |
ultimately show ?thesis by (cases k) auto |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
275 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
276 |
|
48830 | 277 |
lemma pochhammer_of_nat_eq_0_iff: |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
278 |
shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k = 0 \<longleftrightarrow> k > n" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
279 |
(is "?l = ?r") |
48830 | 280 |
using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
281 |
pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
282 |
by (auto simp add: not_le[symmetric]) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
283 |
|
32159 | 284 |
|
48830 | 285 |
lemma pochhammer_eq_0_iff: |
32159 | 286 |
"pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (EX k < n . a = - of_nat k) " |
287 |
apply (auto simp add: pochhammer_of_nat_eq_0_iff) |
|
48830 | 288 |
apply (cases n) |
289 |
apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0) |
|
32159 | 290 |
apply (rule_tac x=x in exI) |
291 |
apply auto |
|
292 |
done |
|
293 |
||
294 |
||
48830 | 295 |
lemma pochhammer_eq_0_mono: |
32159 | 296 |
"pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0" |
48830 | 297 |
unfolding pochhammer_eq_0_iff by auto |
32159 | 298 |
|
48830 | 299 |
lemma pochhammer_neq_0_mono: |
32159 | 300 |
"pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0" |
48830 | 301 |
unfolding pochhammer_eq_0_iff by auto |
32159 | 302 |
|
303 |
lemma pochhammer_minus: |
|
48830 | 304 |
assumes kn: "k \<le> n" |
32159 | 305 |
shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k" |
306 |
proof- |
|
48830 | 307 |
{ assume k0: "k = 0" then have ?thesis by simp } |
308 |
moreover |
|
309 |
{ fix h assume h: "k = Suc h" |
|
32159 | 310 |
have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}" |
311 |
using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"] |
|
312 |
by auto |
|
313 |
have ?thesis |
|
46507 | 314 |
unfolding h pochhammer_Suc_setprod eq setprod_timesf[symmetric] |
32159 | 315 |
apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"]) |
316 |
apply (auto simp add: inj_on_def image_def h ) |
|
317 |
apply (rule_tac x="h - x" in bexI) |
|
48830 | 318 |
apply (auto simp add: fun_eq_iff h of_nat_diff) |
319 |
done } |
|
320 |
ultimately show ?thesis by (cases k) auto |
|
32159 | 321 |
qed |
322 |
||
323 |
lemma pochhammer_minus': |
|
48830 | 324 |
assumes kn: "k \<le> n" |
32159 | 325 |
shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" |
326 |
unfolding pochhammer_minus[OF kn, where b=b] |
|
327 |
unfolding mult_assoc[symmetric] |
|
328 |
unfolding power_add[symmetric] |
|
329 |
apply simp |
|
330 |
done |
|
331 |
||
332 |
lemma pochhammer_same: "pochhammer (- of_nat n) n = ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)" |
|
333 |
unfolding pochhammer_minus[OF le_refl[of n]] |
|
334 |
by (simp add: of_nat_diff pochhammer_fact) |
|
335 |
||
29906 | 336 |
subsection{* Generalized binomial coefficients *} |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
337 |
|
31287 | 338 |
definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65) |
48830 | 339 |
where "a gchoose n = |
340 |
(if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
341 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
342 |
lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0" |
48830 | 343 |
apply (simp_all add: gbinomial_def) |
344 |
apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)") |
|
345 |
apply (simp del:setprod_zero_iff) |
|
346 |
apply simp |
|
347 |
done |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
348 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
349 |
lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)" |
48830 | 350 |
proof - |
351 |
{ assume "n=0" then have ?thesis by simp } |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
352 |
moreover |
48830 | 353 |
{ assume n0: "n\<noteq>0" |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
354 |
from n0 setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"] |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
355 |
have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
356 |
by auto |
48830 | 357 |
from n0 have ?thesis |
358 |
by (simp add: pochhammer_def gbinomial_def field_simps |
|
359 |
eq setprod_timesf[symmetric] del: minus_one) (* FIXME: del: minus_one *) } |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
360 |
ultimately show ?thesis by blast |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
361 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
362 |
|
48830 | 363 |
lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n" |
364 |
proof (induct n arbitrary: k rule: nat_less_induct) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
365 |
fix n k assume H: "\<forall>m<n. \<forall>x\<le>m. fact x * fact (m - x) * (m choose x) = |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
366 |
fact m" and kn: "k \<le> n" |
48830 | 367 |
let ?ths = "fact k * fact (n - k) * (n choose k) = fact n" |
368 |
{ assume "n=0" then have ?ths using kn by simp } |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
369 |
moreover |
48830 | 370 |
{ assume "k=0" then have ?ths using kn by simp } |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
371 |
moreover |
48830 | 372 |
{ assume nk: "n=k" then have ?ths by simp } |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
373 |
moreover |
48830 | 374 |
{ fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
375 |
from n have mn: "m < n" by arith |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
376 |
from hm have hm': "h \<le> m" by arith |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
377 |
from hm h n kn have km: "k \<le> m" by arith |
48830 | 378 |
have "m - h = Suc (m - Suc h)" using h km hm by arith |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
379 |
with km h have th0: "fact (m - h) = (m - h) * fact (m - k)" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
380 |
by simp |
48830 | 381 |
from n h th0 |
382 |
have "fact k * fact (n - k) * (n choose k) = |
|
383 |
k * (fact h * fact (m - h) * (m choose h)) + (m - h) * (fact k * fact (m - k) * (m choose k))" |
|
36350 | 384 |
by (simp add: field_simps) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
385 |
also have "\<dots> = (k + (m - h)) * fact m" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
386 |
using H[rule_format, OF mn hm'] H[rule_format, OF mn km] |
36350 | 387 |
by (simp add: field_simps) |
48830 | 388 |
finally have ?ths using h n km by simp } |
389 |
moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (EX m h. n=Suc m \<and> k = Suc h \<and> h < m)" |
|
390 |
using kn by presburger |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
391 |
ultimately show ?ths by blast |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
392 |
qed |
48830 | 393 |
|
394 |
lemma binomial_fact: |
|
395 |
assumes kn: "k \<le> n" |
|
396 |
shows "(of_nat (n choose k) :: 'a::field_char_0) = |
|
397 |
of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
398 |
using binomial_fact_lemma[OF kn] |
36350 | 399 |
by (simp add: field_simps of_nat_mult [symmetric]) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
400 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
401 |
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" |
48830 | 402 |
proof - |
403 |
{ assume kn: "k > n" |
|
404 |
from kn binomial_eq_0[OF kn] have ?thesis |
|
405 |
by (simp add: gbinomial_pochhammer field_simps pochhammer_of_nat_eq_0_iff) } |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
406 |
moreover |
48830 | 407 |
{ assume "k=0" then have ?thesis by simp } |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
408 |
moreover |
48830 | 409 |
{ assume kn: "k \<le> n" and k0: "k\<noteq> 0" |
410 |
from k0 obtain h where h: "k = Suc h" by (cases k) auto |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
411 |
from h |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
412 |
have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
413 |
by (subst setprod_constant, auto) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
414 |
have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
415 |
apply (rule strong_setprod_reindex_cong[where f="op - n"]) |
48830 | 416 |
using h kn |
417 |
apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff) |
|
418 |
apply clarsimp |
|
419 |
apply presburger |
|
420 |
apply presburger |
|
421 |
apply (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add) |
|
422 |
done |
|
423 |
have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" |
|
424 |
"{1..n - Suc h} \<inter> {n - h .. n} = {}" and |
|
425 |
eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" |
|
426 |
using h kn by auto |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
427 |
from eq[symmetric] |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
428 |
have ?thesis using kn |
48830 | 429 |
apply (simp add: binomial_fact[OF kn, where ?'a = 'a] |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset
|
430 |
gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one) |
48830 | 431 |
apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h |
432 |
of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
433 |
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h] |
48830 | 434 |
unfolding mult_assoc[symmetric] |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
435 |
unfolding setprod_timesf[symmetric] |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
436 |
apply simp |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
437 |
apply (rule strong_setprod_reindex_cong[where f= "op - n"]) |
48830 | 438 |
apply (auto simp add: inj_on_def image_iff Bex_def) |
439 |
apply presburger |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
440 |
apply (subgoal_tac "(of_nat (n - x) :: 'a) = of_nat n - of_nat x") |
48830 | 441 |
apply simp |
442 |
apply (rule of_nat_diff) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
443 |
apply simp |
48830 | 444 |
done |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
445 |
} |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
446 |
moreover |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
447 |
have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
448 |
ultimately show ?thesis by blast |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
449 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
450 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
451 |
lemma gbinomial_1[simp]: "a gchoose 1 = a" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
452 |
by (simp add: gbinomial_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
453 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
454 |
lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
455 |
by (simp add: gbinomial_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
456 |
|
48830 | 457 |
lemma gbinomial_mult_1: |
458 |
"a * (a gchoose n) = |
|
459 |
of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") |
|
460 |
proof - |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
461 |
have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
462 |
unfolding gbinomial_pochhammer |
48830 | 463 |
pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc |
36350 | 464 |
by (simp add: field_simps del: of_nat_Suc) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
465 |
also have "\<dots> = ?l" unfolding gbinomial_pochhammer |
36350 | 466 |
by (simp add: field_simps) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
467 |
finally show ?thesis .. |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
468 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
469 |
|
48830 | 470 |
lemma gbinomial_mult_1': |
471 |
"(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
472 |
by (simp add: mult_commute gbinomial_mult_1) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
473 |
|
48830 | 474 |
lemma gbinomial_Suc: |
475 |
"a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
476 |
by (simp add: gbinomial_def) |
48830 | 477 |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
478 |
lemma gbinomial_mult_fact: |
48830 | 479 |
"(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = |
480 |
(setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
|
481 |
by (simp_all add: gbinomial_Suc field_simps del: fact_Suc) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
482 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
483 |
lemma gbinomial_mult_fact': |
48830 | 484 |
"((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = |
485 |
(setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
486 |
using gbinomial_mult_fact[of k a] |
48830 | 487 |
apply (subst mult_commute) |
488 |
apply assumption |
|
489 |
done |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
490 |
|
48830 | 491 |
|
492 |
lemma gbinomial_Suc_Suc: |
|
493 |
"((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" |
|
494 |
proof - |
|
495 |
{ assume "k = 0" then have ?thesis by simp } |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
496 |
moreover |
48830 | 497 |
{ fix h assume h: "k = Suc h" |
498 |
have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)" |
|
499 |
apply (rule strong_setprod_reindex_cong[where f = Suc]) |
|
500 |
using h |
|
501 |
apply auto |
|
502 |
done |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
503 |
|
48830 | 504 |
have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = |
505 |
((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)" |
|
506 |
apply (simp add: h field_simps del: fact_Suc) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
507 |
unfolding gbinomial_mult_fact' |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
508 |
apply (subst fact_Suc) |
48830 | 509 |
unfolding of_nat_mult |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
510 |
apply (subst mult_commute) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
511 |
unfolding mult_assoc |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
512 |
unfolding gbinomial_mult_fact |
48830 | 513 |
apply (simp add: field_simps) |
514 |
done |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
515 |
also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
516 |
unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc |
36350 | 517 |
by (simp add: field_simps h) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
518 |
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
519 |
using eq0 |
48830 | 520 |
by (simp add: h setprod_nat_ivl_1_Suc) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
521 |
also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
522 |
unfolding gbinomial_mult_fact .. |
48830 | 523 |
finally have ?thesis by (simp del: fact_Suc) |
524 |
} |
|
525 |
ultimately show ?thesis by (cases k) auto |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
526 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
527 |
|
32158
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
528 |
|
48830 | 529 |
lemma binomial_symmetric: |
530 |
assumes kn: "k \<le> n" |
|
32158
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
531 |
shows "n choose k = n choose (n - k)" |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
532 |
proof- |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
533 |
from kn have kn': "n - k \<le> n" by arith |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
534 |
from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] |
48830 | 535 |
have "fact k * fact (n - k) * (n choose k) = |
536 |
fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp |
|
32158
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
537 |
then show ?thesis using kn by simp |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
538 |
qed |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
539 |
|
50224 | 540 |
(* Contributed by Manuel Eberl *) |
541 |
(* Alternative definition of the binomial coefficient as \<Prod>i<k. (n - i) / (k - i) *) |
|
542 |
lemma binomial_altdef_of_nat: |
|
543 |
fixes n k :: nat and x :: "'a :: {field_char_0, field_inverse_zero}" |
|
544 |
assumes "k \<le> n" shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)" |
|
545 |
proof cases |
|
546 |
assume "0 < k" |
|
547 |
then have "(of_nat (n choose k) :: 'a) = (\<Prod>i<k. of_nat n - of_nat i) / of_nat (fact k)" |
|
548 |
unfolding binomial_gbinomial gbinomial_def |
|
549 |
by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost) |
|
550 |
also have "\<dots> = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)" |
|
551 |
using `k \<le> n` unfolding fact_eq_rev_setprod_nat of_nat_setprod |
|
552 |
by (auto simp add: setprod_dividef intro!: setprod_cong of_nat_diff[symmetric]) |
|
553 |
finally show ?thesis . |
|
554 |
qed simp |
|
555 |
||
556 |
lemma binomial_ge_n_over_k_pow_k: |
|
557 |
fixes k n :: nat and x :: "'a :: linordered_field_inverse_zero" |
|
558 |
assumes "0 < k" and "k \<le> n" shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)" |
|
559 |
proof - |
|
560 |
have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)" |
|
561 |
by (simp add: setprod_constant) |
|
562 |
also have "\<dots> \<le> of_nat (n choose k)" |
|
563 |
unfolding binomial_altdef_of_nat[OF `k\<le>n`] |
|
564 |
proof (safe intro!: setprod_mono) |
|
565 |
fix i::nat assume "i < k" |
|
566 |
from assms have "n * i \<ge> i * k" by simp |
|
567 |
hence "n * k - n * i \<le> n * k - i * k" by arith |
|
568 |
hence "n * (k - i) \<le> (n - i) * k" |
|
569 |
by (simp add: diff_mult_distrib2 nat_mult_commute) |
|
570 |
hence "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)" |
|
571 |
unfolding of_nat_mult[symmetric] of_nat_le_iff . |
|
572 |
with assms show "of_nat n / of_nat k \<le> of_nat (n - i) / (of_nat (k - i) :: 'a)" |
|
573 |
using `i < k` by (simp add: field_simps) |
|
574 |
qed (simp add: zero_le_divide_iff) |
|
575 |
finally show ?thesis . |
|
576 |
qed |
|
577 |
||
50240
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
578 |
lemma binomial_le_pow: |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
579 |
assumes "r \<le> n" shows "n choose r \<le> n ^ r" |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
580 |
proof - |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
581 |
have "n choose r \<le> fact n div fact (n - r)" |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
582 |
using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
583 |
with fact_div_fact_le_pow[OF assms] show ?thesis by auto |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
584 |
qed |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
585 |
|
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
586 |
lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
587 |
n choose k = fact n div (fact k * fact (n - k))" |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
588 |
by (subst binomial_fact_lemma[symmetric]) auto |
019d642d422d
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
hoelzl
parents:
50224
diff
changeset
|
589 |
|
21256 | 590 |
end |