author | paulson |
Mon, 25 Nov 2013 16:47:28 +0000 | |
changeset 54585 | bfbfecb3102e |
parent 54568 | 08b642269a0d |
child 54679 | 88adcd3b34e8 |
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 |
|
52903 | 15 |
primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) |
16 |
where |
|
17 |
"0 choose k = (if k = 0 then 1 else 0)" |
|
18 |
| "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
|
21256 | 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 |
|
52903 | 26 |
lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" |
48830 | 27 |
by simp |
21256 | 28 |
|
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
29 |
lemma choose_reduce_nat: |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
30 |
"0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow> |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
31 |
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
32 |
by (metis Suc_diff_1 binomial.simps(2) nat_add_commute neq0_conv) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
33 |
|
52903 | 34 |
lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0" |
35 |
by (induct n arbitrary: k) auto |
|
21256 | 36 |
|
52903 | 37 |
declare binomial.simps [simp del] |
21256 | 38 |
|
52903 | 39 |
lemma binomial_n_n [simp]: "n choose n = 1" |
48830 | 40 |
by (induct n) (simp_all add: binomial_eq_0) |
21256 | 41 |
|
52903 | 42 |
lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n" |
48830 | 43 |
by (induct n) simp_all |
21256 | 44 |
|
52903 | 45 |
lemma binomial_1 [simp]: "n choose Suc 0 = n" |
48830 | 46 |
by (induct n) simp_all |
21256 | 47 |
|
52903 | 48 |
lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0" |
48830 | 49 |
by (induct n k rule: diff_induct) simp_all |
21256 | 50 |
|
52903 | 51 |
lemma binomial_eq_0_iff: "n choose k = 0 \<longleftrightarrow> n < k" |
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
52 |
by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial) |
21256 | 53 |
|
52903 | 54 |
lemma zero_less_binomial_iff: "n choose k > 0 \<longleftrightarrow> k \<le> n" |
48830 | 55 |
by (simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] del: neq0_conv) |
21256 | 56 |
|
57 |
(*Might be more useful if re-oriented*) |
|
21263 | 58 |
lemma Suc_times_binomial_eq: |
52903 | 59 |
"k \<le> n \<Longrightarrow> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" |
60 |
apply (induct n arbitrary: k) |
|
61 |
apply (simp add: binomial.simps) |
|
48830 | 62 |
apply (case_tac k) |
63 |
apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) |
|
64 |
done |
|
21256 | 65 |
|
66 |
text{*This is the well-known version, but it's harder to use because of the |
|
67 |
need to reason about division.*} |
|
68 |
lemma binomial_Suc_Suc_eq_times: |
|
52903 | 69 |
"k \<le> n \<Longrightarrow> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k" |
46507 | 70 |
by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) |
21256 | 71 |
|
72 |
text{*Another version, with -1 instead of Suc.*} |
|
73 |
lemma times_binomial_minus1_eq: |
|
52903 | 74 |
"k \<le> n \<Longrightarrow> 0 < k \<Longrightarrow> (n choose k) * k = n * ((n - 1) choose (k - 1))" |
75 |
using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"] |
|
76 |
by (auto split add: nat_diff_split) |
|
21263 | 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 |
||
52903 | 86 |
lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1" |
48830 | 87 |
by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) |
21256 | 88 |
|
52903 | 89 |
lemma choose_deconstruct: "finite M \<Longrightarrow> x \<notin> M \<Longrightarrow> |
90 |
{s. s \<subseteq> insert x M \<and> card s = Suc k} = |
|
91 |
{s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}" |
|
21256 | 92 |
apply safe |
48830 | 93 |
apply (auto intro: finite_subset [THEN card_insert_disjoint]) |
54585 | 94 |
by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if |
95 |
card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff) |
|
29918 | 96 |
|
52903 | 97 |
lemma finite_bex_subset [simp]: |
98 |
assumes "finite B" |
|
99 |
and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}" |
|
100 |
shows "finite {x. \<exists>A \<subseteq> B. P x A}" |
|
54585 | 101 |
by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets) |
21256 | 102 |
|
103 |
text{*There are as many subsets of @{term A} having cardinality @{term k} |
|
104 |
as there are sets obtained from the former by inserting a fixed element |
|
105 |
@{term x} into each.*} |
|
106 |
lemma constr_bij: |
|
52903 | 107 |
"finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> |
108 |
card {B. \<exists>C. C \<subseteq> A \<and> card C = k \<and> B = insert x C} = |
|
109 |
card {B. B \<subseteq> A & card(B) = k}" |
|
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
110 |
apply (rule card_bij_eq [where f = "\<lambda>s. s - {x}" and g = "insert x"]) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
111 |
apply (auto elim!: equalityE simp add: inj_on_def) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
112 |
apply (metis card_Diff_singleton_if finite_subset in_mono) |
48830 | 113 |
done |
21256 | 114 |
|
115 |
text {* |
|
116 |
Main theorem: combinatorial statement about number of subsets of a set. |
|
117 |
*} |
|
118 |
||
52903 | 119 |
theorem n_subsets: "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)" |
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
120 |
proof (induct k arbitrary: A) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
121 |
case 0 then show ?case by (simp add: card_s_0_eq_empty) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
122 |
next |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
123 |
case (Suc k) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
124 |
show ?case using `finite A` |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
125 |
proof (induct A) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
126 |
case empty show ?case by (simp add: card_s_0_eq_empty) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
127 |
next |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
128 |
case (insert x A) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
129 |
then show ?case using Suc.hyps |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
130 |
apply (simp add: card_s_0_eq_empty choose_deconstruct) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
131 |
apply (subst card_Un_disjoint) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
132 |
prefer 4 apply (force simp add: constr_bij) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
133 |
prefer 3 apply force |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
134 |
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
135 |
finite_subset [of _ "Pow (insert x F)", standard]) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
136 |
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
137 |
done |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
138 |
qed |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
139 |
qed |
21256 | 140 |
|
141 |
||
142 |
text{* The binomial theorem (courtesy of Tobias Nipkow): *} |
|
143 |
||
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
144 |
(* Avigad's version, generalized to any commutative semiring *) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
145 |
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
146 |
(\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n") |
21256 | 147 |
proof (induct n) |
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
148 |
case 0 then show "?P 0" by simp |
21256 | 149 |
next |
150 |
case (Suc n) |
|
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
151 |
have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
152 |
by auto |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
153 |
have decomp2: "{0..n} = {0} Un {1..n}" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
154 |
by auto |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
155 |
have "(a+b)^(n+1) = |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
156 |
(a+b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
157 |
using Suc.hyps by simp |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
158 |
also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) + |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
159 |
b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
160 |
by (rule distrib) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
161 |
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
162 |
(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
163 |
by (auto simp add: setsum_right_distrib mult_ac) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
164 |
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) + |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
165 |
(\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
166 |
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
167 |
del:setsum_cl_ivl_Suc) |
21256 | 168 |
also have "\<dots> = a^(n+1) + b^(n+1) + |
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
169 |
(\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) + |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
170 |
(\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))" |
21263 | 171 |
by (simp add: decomp2) |
21256 | 172 |
also have |
54568
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
173 |
"\<dots> = a^(n+1) + b^(n+1) + |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
174 |
(\<Sum>k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
175 |
by (auto simp add: field_simps setsum_addf [symmetric] choose_reduce_nat) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
176 |
also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))" |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
177 |
using decomp by (simp add: field_simps) |
08b642269a0d
Simplified, tidied and generalised proofs esp of Binomial Theorem.
paulson
parents:
54489
diff
changeset
|
178 |
finally show "?P (Suc n)" by simp |
21256 | 179 |
qed |
180 |
||
29906 | 181 |
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
|
182 |
|
52903 | 183 |
definition "pochhammer (a::'a::comm_semiring_1) n = |
184 |
(if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})" |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
185 |
|
52903 | 186 |
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
|
187 |
by (simp add: pochhammer_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
188 |
|
52903 | 189 |
lemma pochhammer_1 [simp]: "pochhammer a 1 = a" |
190 |
by (simp add: pochhammer_def) |
|
191 |
||
192 |
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
|
193 |
by (simp add: pochhammer_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
194 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
195 |
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
|
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 setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)" |
52903 | 199 |
proof - |
200 |
have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto |
|
201 |
then show ?thesis 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
|
202 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
203 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
204 |
lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}" |
52903 | 205 |
proof - |
206 |
have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto |
|
207 |
then show ?thesis by simp |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
208 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
209 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
210 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
211 |
lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" |
52903 | 212 |
proof (cases n) |
213 |
case 0 |
|
214 |
then show ?thesis by simp |
|
215 |
next |
|
216 |
case (Suc n) |
|
217 |
show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc .. |
|
48830 | 218 |
qed |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
219 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
220 |
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n" |
52903 | 221 |
proof (cases "n = 0") |
222 |
case True |
|
223 |
then show ?thesis by (simp add: pochhammer_Suc_setprod) |
|
224 |
next |
|
225 |
case False |
|
226 |
have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto |
|
227 |
have eq: "insert 0 {1 .. n} = {0..n}" by auto |
|
228 |
have **: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) = (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)" |
|
229 |
apply (rule setprod_reindex_cong [where f = Suc]) |
|
230 |
using False |
|
231 |
apply (auto simp add: fun_eq_iff field_simps) |
|
232 |
done |
|
233 |
show ?thesis |
|
234 |
apply (simp add: pochhammer_def) |
|
235 |
unfolding setprod_insert [OF *, unfolded eq] |
|
236 |
using ** apply (simp add: field_simps) |
|
237 |
done |
|
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: |
52903 | 249 |
assumes "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" |
52903 | 251 |
proof (cases "n = 0") |
252 |
case True |
|
253 |
then show ?thesis |
|
254 |
using assms by (cases k) (simp_all add: pochhammer_rec) |
|
255 |
next |
|
256 |
case False |
|
257 |
from assms obtain h where "k = Suc h" by (cases k) auto |
|
258 |
then show ?thesis |
|
54585 | 259 |
by (simp add: pochhammer_Suc_setprod) |
260 |
(metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1)) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
261 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
262 |
|
52903 | 263 |
lemma pochhammer_of_nat_eq_0_lemma': |
264 |
assumes kn: "k \<le> n" |
|
265 |
shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0" |
|
266 |
proof (cases k) |
|
267 |
case 0 |
|
268 |
then show ?thesis by simp |
|
269 |
next |
|
270 |
case (Suc h) |
|
271 |
then show ?thesis |
|
272 |
apply (simp add: pochhammer_Suc_setprod) |
|
273 |
using Suc kn apply (auto simp add: algebra_simps) |
|
274 |
done |
|
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: |
52903 | 278 |
shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n" |
29694
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 |
|
52903 | 285 |
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)" |
32159 | 286 |
apply (auto simp add: pochhammer_of_nat_eq_0_iff) |
48830 | 287 |
apply (cases n) |
288 |
apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0) |
|
54585 | 289 |
apply (metis leD not_less_eq) |
32159 | 290 |
done |
291 |
||
292 |
||
48830 | 293 |
lemma pochhammer_eq_0_mono: |
32159 | 294 |
"pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0" |
48830 | 295 |
unfolding pochhammer_eq_0_iff by auto |
32159 | 296 |
|
48830 | 297 |
lemma pochhammer_neq_0_mono: |
32159 | 298 |
"pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0" |
48830 | 299 |
unfolding pochhammer_eq_0_iff by auto |
32159 | 300 |
|
301 |
lemma pochhammer_minus: |
|
48830 | 302 |
assumes kn: "k \<le> n" |
32159 | 303 |
shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k" |
52903 | 304 |
proof (cases k) |
305 |
case 0 |
|
306 |
then show ?thesis by simp |
|
307 |
next |
|
308 |
case (Suc h) |
|
309 |
have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}" |
|
310 |
using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"] |
|
311 |
by auto |
|
312 |
show ?thesis |
|
313 |
unfolding Suc pochhammer_Suc_setprod eq setprod_timesf[symmetric] |
|
314 |
apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"]) |
|
315 |
using Suc |
|
316 |
apply (auto simp add: inj_on_def image_def) |
|
317 |
apply (rule_tac x="h - x" in bexI) |
|
318 |
apply (auto simp add: fun_eq_iff of_nat_diff) |
|
319 |
done |
|
32159 | 320 |
qed |
321 |
||
322 |
lemma pochhammer_minus': |
|
48830 | 323 |
assumes kn: "k \<le> n" |
32159 | 324 |
shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" |
325 |
unfolding pochhammer_minus[OF kn, where b=b] |
|
326 |
unfolding mult_assoc[symmetric] |
|
327 |
unfolding power_add[symmetric] |
|
52903 | 328 |
by simp |
32159 | 329 |
|
52903 | 330 |
lemma pochhammer_same: "pochhammer (- of_nat n) n = |
331 |
((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)" |
|
32159 | 332 |
unfolding pochhammer_minus[OF le_refl[of n]] |
333 |
by (simp add: of_nat_diff pochhammer_fact) |
|
334 |
||
52903 | 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 |
|
52903 | 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)" |
52903 | 350 |
proof (cases "n = 0") |
351 |
case True |
|
352 |
then show ?thesis by simp |
|
353 |
next |
|
354 |
case False |
|
355 |
from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"] |
|
356 |
have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}" |
|
357 |
by auto |
|
358 |
from False show ?thesis |
|
359 |
by (simp add: pochhammer_def gbinomial_def field_simps |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52903
diff
changeset
|
360 |
eq setprod_timesf[symmetric]) |
29694
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) = |
|
52903 | 383 |
k * (fact h * fact (m - h) * (m choose h)) + |
384 |
(m - h) * (fact k * fact (m - k) * (m choose k))" |
|
36350 | 385 |
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
|
386 |
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
|
387 |
using H[rule_format, OF mn hm'] H[rule_format, OF mn km] |
36350 | 388 |
by (simp add: field_simps) |
48830 | 389 |
finally have ?ths using h n km by simp } |
52903 | 390 |
moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (\<exists>m h. n = Suc m \<and> k = Suc h \<and> h < m)" |
48830 | 391 |
using kn by presburger |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
392 |
ultimately show ?ths by blast |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
393 |
qed |
48830 | 394 |
|
395 |
lemma binomial_fact: |
|
396 |
assumes kn: "k \<le> n" |
|
397 |
shows "(of_nat (n choose k) :: 'a::field_char_0) = |
|
398 |
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
|
399 |
using binomial_fact_lemma[OF kn] |
36350 | 400 |
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
|
401 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
402 |
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" |
48830 | 403 |
proof - |
404 |
{ assume kn: "k > n" |
|
405 |
from kn binomial_eq_0[OF kn] have ?thesis |
|
406 |
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
|
407 |
moreover |
48830 | 408 |
{ 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
|
409 |
moreover |
48830 | 410 |
{ assume kn: "k \<le> n" and k0: "k\<noteq> 0" |
411 |
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
|
412 |
from h |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
413 |
have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}" |
52903 | 414 |
by (subst setprod_constant) auto |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
415 |
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
|
416 |
apply (rule strong_setprod_reindex_cong[where f="op - n"]) |
48830 | 417 |
using h kn |
418 |
apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff) |
|
419 |
apply clarsimp |
|
420 |
apply presburger |
|
421 |
apply presburger |
|
422 |
apply (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add) |
|
423 |
done |
|
424 |
have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" |
|
425 |
"{1..n - Suc h} \<inter> {n - h .. n} = {}" and |
|
426 |
eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" |
|
427 |
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
|
428 |
from eq[symmetric] |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
429 |
have ?thesis using kn |
48830 | 430 |
apply (simp add: binomial_fact[OF kn, where ?'a = 'a] |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52903
diff
changeset
|
431 |
gbinomial_pochhammer field_simps pochhammer_Suc_setprod) |
48830 | 432 |
apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52903
diff
changeset
|
433 |
of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
434 |
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h] |
48830 | 435 |
unfolding mult_assoc[symmetric] |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
436 |
unfolding setprod_timesf[symmetric] |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
437 |
apply simp |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
438 |
apply (rule strong_setprod_reindex_cong[where f= "op - n"]) |
48830 | 439 |
apply (auto simp add: inj_on_def image_iff Bex_def) |
440 |
apply presburger |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
441 |
apply (subgoal_tac "(of_nat (n - x) :: 'a) = of_nat n - of_nat x") |
48830 | 442 |
apply simp |
443 |
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
|
444 |
apply simp |
48830 | 445 |
done |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
446 |
} |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
447 |
moreover |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
448 |
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
|
449 |
ultimately show ?thesis by blast |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
450 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
451 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
452 |
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
|
453 |
by (simp add: gbinomial_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
454 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
455 |
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
|
456 |
by (simp add: gbinomial_def) |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
457 |
|
48830 | 458 |
lemma gbinomial_mult_1: |
459 |
"a * (a gchoose n) = |
|
460 |
of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") |
|
461 |
proof - |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
462 |
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
|
463 |
unfolding gbinomial_pochhammer |
48830 | 464 |
pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc |
36350 | 465 |
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
|
466 |
also have "\<dots> = ?l" unfolding gbinomial_pochhammer |
36350 | 467 |
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
|
468 |
finally show ?thesis .. |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
469 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
470 |
|
48830 | 471 |
lemma gbinomial_mult_1': |
472 |
"(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
|
473 |
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
|
474 |
|
48830 | 475 |
lemma gbinomial_Suc: |
476 |
"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
|
477 |
by (simp add: gbinomial_def) |
48830 | 478 |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
479 |
lemma gbinomial_mult_fact: |
48830 | 480 |
"(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = |
481 |
(setprod (\<lambda>i. a - of_nat i) {0 .. k})" |
|
482 |
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
|
483 |
|
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
484 |
lemma gbinomial_mult_fact': |
48830 | 485 |
"((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = |
486 |
(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
|
487 |
using gbinomial_mult_fact[of k a] |
52903 | 488 |
by (subst mult_commute) |
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
489 |
|
48830 | 490 |
|
491 |
lemma gbinomial_Suc_Suc: |
|
492 |
"((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" |
|
52903 | 493 |
proof (cases k) |
494 |
case 0 |
|
495 |
then show ?thesis by simp |
|
496 |
next |
|
497 |
case (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 Suc |
|
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 |
|
52903 | 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: Suc field_simps del: fact_Suc) |
|
507 |
unfolding gbinomial_mult_fact' |
|
508 |
apply (subst fact_Suc) |
|
509 |
unfolding of_nat_mult |
|
510 |
apply (subst mult_commute) |
|
511 |
unfolding mult_assoc |
|
512 |
unfolding gbinomial_mult_fact |
|
513 |
apply (simp add: field_simps) |
|
514 |
done |
|
515 |
also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)" |
|
516 |
unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc |
|
517 |
by (simp add: field_simps Suc) |
|
518 |
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)" |
|
519 |
using eq0 |
|
520 |
by (simp add: Suc setprod_nat_ivl_1_Suc) |
|
521 |
also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" |
|
522 |
unfolding gbinomial_mult_fact .. |
|
523 |
finally show ?thesis by (simp del: fact_Suc) |
|
29694
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
524 |
qed |
2f2558d7bc3e
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
chaieb
parents:
27487
diff
changeset
|
525 |
|
32158
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
526 |
|
48830 | 527 |
lemma binomial_symmetric: |
528 |
assumes kn: "k \<le> n" |
|
32158
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
529 |
shows "n choose k = n choose (n - k)" |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
530 |
proof- |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
531 |
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
|
532 |
from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] |
48830 | 533 |
have "fact k * fact (n - k) * (n choose k) = |
534 |
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
|
535 |
then show ?thesis using kn by simp |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
536 |
qed |
4dc119d4fc8b
Moved theorem binomial_symmetric from Formal_Power_Series to here
chaieb
parents:
31287
diff
changeset
|
537 |
|
50224 | 538 |
(* Contributed by Manuel Eberl *) |
539 |
(* Alternative definition of the binomial coefficient as \<Prod>i<k. (n - i) / (k - i) *) |
|
540 |
lemma binomial_altdef_of_nat: |
|
52903 | 541 |
fixes n k :: nat |
542 |
and x :: "'a :: {field_char_0,field_inverse_zero}" |
|
543 |
assumes "k \<le> n" |
|
544 |
shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)" |
|
545 |
proof (cases "0 < k") |
|
546 |
case True |
|
50224 | 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 . |
|
52903 | 554 |
next |
555 |
case False |
|
556 |
then show ?thesis by simp |
|
557 |
qed |
|
50224 | 558 |
|
559 |
lemma binomial_ge_n_over_k_pow_k: |
|
52903 | 560 |
fixes k n :: nat |
561 |
and x :: "'a :: linordered_field_inverse_zero" |
|
562 |
assumes "0 < k" |
|
563 |
and "k \<le> n" |
|
564 |
shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)" |
|
50224 | 565 |
proof - |
566 |
have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)" |
|
567 |
by (simp add: setprod_constant) |
|
568 |
also have "\<dots> \<le> of_nat (n choose k)" |
|
569 |
unfolding binomial_altdef_of_nat[OF `k\<le>n`] |
|
570 |
proof (safe intro!: setprod_mono) |
|
52903 | 571 |
fix i :: nat |
572 |
assume "i < k" |
|
50224 | 573 |
from assms have "n * i \<ge> i * k" by simp |
52903 | 574 |
then have "n * k - n * i \<le> n * k - i * k" by arith |
575 |
then have "n * (k - i) \<le> (n - i) * k" |
|
50224 | 576 |
by (simp add: diff_mult_distrib2 nat_mult_commute) |
52903 | 577 |
then have "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)" |
50224 | 578 |
unfolding of_nat_mult[symmetric] of_nat_le_iff . |
579 |
with assms show "of_nat n / of_nat k \<le> of_nat (n - i) / (of_nat (k - i) :: 'a)" |
|
580 |
using `i < k` by (simp add: field_simps) |
|
581 |
qed (simp add: zero_le_divide_iff) |
|
582 |
finally show ?thesis . |
|
583 |
qed |
|
584 |
||
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
|
585 |
lemma binomial_le_pow: |
52903 | 586 |
assumes "r \<le> n" |
587 |
shows "n choose r \<le> n ^ r" |
|
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
|
588 |
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
|
589 |
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
|
590 |
using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto |
52903 | 591 |
with fact_div_fact_le_pow [OF assms] show ?thesis by auto |
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
|
592 |
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
|
593 |
|
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
|
594 |
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
|
595 |
n choose k = fact n div (fact k * fact (n - k))" |
52903 | 596 |
by (subst binomial_fact_lemma [symmetric]) auto |
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
|
597 |
|
21256 | 598 |
end |