--- a/src/HOL/Binomial.thy Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Binomial.thy Fri Feb 19 13:40:50 2016 +0100
@@ -28,7 +28,7 @@
lemma of_nat_fact [simp]:
"of_nat (fact n) = fact n"
by (induct n) (auto simp add: algebra_simps of_nat_mult)
-
+
lemma of_int_fact [simp]:
"of_int (fact n) = fact n"
proof -
@@ -56,22 +56,22 @@
context
assumes "SORT_CONSTRAINT('a::linordered_semidom)"
begin
-
+
lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
-
+
lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
by (metis le0 fact.simps(1) fact_mono)
-
+
lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
using fact_ge_1 less_le_trans zero_less_one by blast
-
+
lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
by (simp add: less_imp_le)
lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))"
by (simp add: not_less_iff_gr_or_eq)
-
+
lemma fact_le_power:
"fact n \<le> (of_nat (n^n) ::'a)"
proof (induct n)
@@ -86,7 +86,7 @@
by (metis of_nat_mult order_refl power_Suc)
finally show ?case .
qed simp
-
+
end
text\<open>Note that @{term "fact 0 = fact 1"}\<close>
@@ -100,7 +100,7 @@
lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
by (metis One_nat_def fact_ge_1)
-lemma dvd_fact:
+lemma dvd_fact:
shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
by (induct n) (auto simp: dvdI le_Suc_eq)
@@ -112,7 +112,7 @@
lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
by (induct n) (auto simp: atLeastAtMostSuc_conv)
-
+
lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
by (subst fact_altdef_nat [symmetric]) simp
@@ -145,7 +145,7 @@
from this \<open>m = n + d\<close> show ?thesis by simp
qed
-lemma fact_num_eq_if:
+lemma fact_num_eq_if:
"fact m = (if m=0 then 1 else of_nat m * fact (m - 1))"
by (cases m) auto
@@ -402,20 +402,20 @@
lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
by (induct n) auto
-lemma choose_alternating_sum:
+lemma choose_alternating_sum:
"n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)"
using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)
lemma choose_even_sum:
assumes "n > 0"
shows "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
-proof -
+proof -
have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
using choose_row_sum[of n]
by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"
by (simp add: setsum.distrib)
- also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)"
+ also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)"
by (subst setsum_right_distrib, intro setsum.cong) simp_all
finally show ?thesis ..
qed
@@ -423,13 +423,13 @@
lemma choose_odd_sum:
assumes "n > 0"
shows "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
-proof -
+proof -
have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
using choose_row_sum[of n]
by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"
by (simp add: setsum_subtractf)
- also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)"
+ also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)"
by (subst setsum_right_distrib, intro setsum.cong) simp_all
finally show ?thesis ..
qed
@@ -473,7 +473,7 @@
lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
by (simp add: pochhammer_def)
-
+
lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
by (simp add: pochhammer_def of_nat_setprod)
@@ -525,10 +525,10 @@
lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
proof (induction n arbitrary: z)
case (Suc n z)
- have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)"
+ have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)"
by (simp add: pochhammer_rec)
also note Suc
- also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) =
+ also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) =
(z + of_nat (Suc n)) * pochhammer z (Suc n)"
by (simp_all add: pochhammer_rec algebra_simps)
finally show ?case .
@@ -621,11 +621,11 @@
unfolding pochhammer_minus
by (simp add: of_nat_diff pochhammer_fact)
-lemma pochhammer_product':
+lemma pochhammer_product':
"pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
proof (induction n arbitrary: z)
case (Suc n z)
- have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
+ have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
by (simp add: pochhammer_rec ac_simps)
also note Suc[symmetric]
@@ -634,7 +634,7 @@
finally show ?case by simp
qed simp
-lemma pochhammer_product:
+lemma pochhammer_product:
"m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
using pochhammer_product'[of z m "n - m"] by simp
@@ -645,7 +645,7 @@
case (Suc n)
def n' \<equiv> "Suc n"
have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
- (pochhammer z n' * pochhammer (z + 1 / 2) n') *
+ (pochhammer z n' * pochhammer (z + 1 / 2) n') *
((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")
by (simp_all add: pochhammer_rec' mult_ac)
also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
@@ -661,7 +661,7 @@
shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
proof (induction n)
case (Suc n)
- have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
+ have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
(2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
by (simp add: pochhammer_rec' ac_simps of_nat_mult)
also note Suc
@@ -673,7 +673,7 @@
qed simp
lemma pochhammer_absorb_comp:
- "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
+ "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
(is "?lhs = ?rhs")
proof -
have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps)
@@ -714,7 +714,7 @@
finally show ?thesis by simp
qed
-lemma binomial_gbinomial:
+lemma binomial_gbinomial:
"of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
proof -
{ assume kn: "k > n"
@@ -741,7 +741,7 @@
have ?thesis using kn
apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
- apply (simp add: pochhammer_Suc_setprod fact_altdef h
+ apply (simp add: pochhammer_Suc_setprod fact_altdef h
of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
unfolding mult.assoc
@@ -817,19 +817,19 @@
(a gchoose Suc h) * (fact (Suc (Suc h))) +
(a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
by (simp add: Suc field_simps del: fact.simps)
- also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
+ also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
(\<Prod>i = 0..Suc h. a - of_nat i)"
by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)
- also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
+ also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
(\<Prod>i = 0..Suc h. a - of_nat i)"
by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
- also have "... = of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) +
+ also have "... = of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) +
(\<Prod>i = 0..Suc h. a - of_nat i)"
by (metis gbinomial_mult_fact mult.commute)
also have "... = (\<Prod>i = 0..Suc h. a - of_nat i) +
(of_nat h * (\<Prod>i = 0..h. a - of_nat i) + 2 * (\<Prod>i = 0..h. a - of_nat i))"
by (simp add: field_simps)
- also have "... =
+ also have "... =
((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0::nat..Suc h}. a - of_nat i)"
unfolding gbinomial_mult_fact'
by (simp add: comm_semiring_class.distrib field_simps Suc)
@@ -842,7 +842,7 @@
also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
unfolding gbinomial_mult_fact ..
finally show ?thesis
- by (metis fact_nonzero mult_cancel_left)
+ by (metis fact_nonzero mult_cancel_left)
qed
lemma gbinomial_reduce_nat:
@@ -887,7 +887,7 @@
case (Suc m)
have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" by (simp add: Suc)
also have "... = Suc m * 2 ^ m"
- by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric])
+ by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric])
(simp add: choose_row_sum')
finally show ?thesis using Suc by simp
qed simp_all
@@ -898,7 +898,7 @@
proof (cases n)
case (Suc m)
with assms have "m > 0" by simp
- have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =
+ have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) =
(\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)
also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp
@@ -940,7 +940,7 @@
also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
a * pochhammer ((a + 1) + b) n"
by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac)
- also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) =
+ also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) =
(\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
@@ -1010,7 +1010,7 @@
"of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
proof (cases b)
case (Suc b)
- hence "((a + 1) gchoose (Suc (Suc b))) =
+ hence "((a + 1) gchoose (Suc (Suc b))) =
(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
by (simp add: field_simps gbinomial_def)
also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
@@ -1024,7 +1024,7 @@
"((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
proof (cases b)
case (Suc b)
- hence "((a + 1) gchoose (Suc (Suc b))) =
+ hence "((a + 1) gchoose (Suc (Suc b))) =
(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
by (simp add: field_simps gbinomial_def)
also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
@@ -1045,9 +1045,9 @@
text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[
{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
\]\<close>
-lemma gbinomial_absorption':
+lemma gbinomial_absorption':
"k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))"
- using gbinomial_rec[of "r - 1" "k - 1"]
+ using gbinomial_rec[of "r - 1" "k - 1"]
by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)
text \<open>The absorption identity is written in the following form to avoid
@@ -1096,7 +1096,7 @@
summation formula, operating on both indices:\[
\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
\quad \textnormal{integer } n.
- \]
+ \]
\<close>
lemma gbinomial_parallel_sum:
"(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
@@ -1108,7 +1108,7 @@
subsection \<open>Summation on the upper index\<close>
text \<open>
Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
- aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
+ aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
{n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
\<close>
lemma gbinomial_sum_up_index:
@@ -1121,7 +1121,7 @@
thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac)
qed
-lemma gbinomial_index_swap:
+lemma gbinomial_index_swap:
"((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
(is "?lhs = ?rhs")
proof -
@@ -1132,7 +1132,7 @@
finally show ?thesis .
qed
-lemma gbinomial_sum_lower_neg:
+lemma gbinomial_sum_lower_neg:
"(\<Sum>k\<le>m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs")
proof -
have "?lhs = (\<Sum>k\<le>m. -(r + 1) + of_nat k gchoose k)"
@@ -1146,7 +1146,7 @@
"(\<Sum>k\<le>m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
proof (induction m)
case (Suc mm)
- hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =
+ hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) =
(r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps)
also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)
also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
@@ -1175,10 +1175,10 @@
also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))
+ (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
by (subst setsum.distrib [symmetric]) (simp add: algebra_simps)
- also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
+ also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) =
(\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
by (simp only: atLeast0AtMost lessThan_Suc_atMost)
- also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k))
+ also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k))
+ (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" (is "_ = ?A + ?B")
by (subst setsum_lessThan_Suc) simp
also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
@@ -1188,17 +1188,17 @@
thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:)
qed
- also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+ also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps)
also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps)
also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def)
- finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k)))
+ finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k)))
+ (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
by (simp add: ring_distribs)
- also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm"
+ also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm"
by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost)
- finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
+ finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)"
by (simp add: algebra_simps)
also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))"
by (subst gbinomial_negated_upper) simp
@@ -1208,13 +1208,13 @@
unfolding S_def by (subst Suc.IH) simp
also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le)
- also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm =
+ also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm =
(\<Sum>n\<le>Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp
finally show ?case unfolding S_def .
qed simp_all
lemma gbinomial_partial_sum_poly_xpos:
- "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
+ "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
(\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
apply (subst gbinomial_partial_sum_poly)
apply (subst gbinomial_negated_upper)
@@ -1222,7 +1222,7 @@
apply (simp add: power_mult_distrib [symmetric])
done
-lemma setsum_nat_symmetry:
+lemma setsum_nat_symmetry:
"(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m - k))"
by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m - i" and j="\<lambda>i. m - i"]) auto
@@ -1247,7 +1247,7 @@
lemma gbinomial_r_part_sum:
"(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")
proof -
- have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)"
+ have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)"
by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)
also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)
finally show ?thesis by (simp add: of_nat_power)
@@ -1270,7 +1270,7 @@
assumes "k \<le> m"
shows "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
proof -
- have "(r gchoose m) * (of_nat m gchoose k) =
+ have "(r gchoose m) * (of_nat m gchoose k) =
(r gchoose m) * fact m / (fact k * fact (m - k))"
using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
also have "\<dots> = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms
@@ -1315,7 +1315,7 @@
apply (auto simp: of_nat_mult)
done
-lemma fact_fact_dvd_fact:
+lemma fact_fact_dvd_fact:
"fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"
by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
@@ -1568,12 +1568,12 @@
qed
lemma pochhammer_code [code]:
- "pochhammer a n = (if n = 0 then 1 else
+ "pochhammer a n = (if n = 0 then 1 else
fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
by (simp add: setprod_atLeastAtMost_code pochhammer_def)
lemma gbinomial_code [code]:
- "a gchoose n = (if n = 0 then 1 else
+ "a gchoose n = (if n = 0 then 1 else
fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
by (simp add: setprod_atLeastAtMost_code gbinomial_def)
@@ -1593,7 +1593,7 @@
by (simp add: setprod.union_disjoint fact_altdef_nat)
}
thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
-qed
+qed
*)
end