--- a/src/HOL/Binomial.thy Mon May 06 14:39:33 2024 +0100
+++ b/src/HOL/Binomial.thy Sun May 12 23:23:39 2024 +0100
@@ -362,7 +362,7 @@
subsection \<open>Generalized binomial coefficients\<close>
-definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infix "gchoose" 64)
where gbinomial_prod_rev: "a gchoose k = prod (\<lambda>i. a - of_nat i) {0..<k} div fact k"
lemma gbinomial_0 [simp]:
@@ -379,6 +379,9 @@
lemma gbinomial_Suc0 [simp]: "a gchoose Suc 0 = a"
by (simp add: gbinomial_prod_rev lessThan_Suc)
+lemma gbinomial_0_left: "0 gchoose k = (if k = 0 then 1 else 0)"
+ by (cases k) simp_all
+
lemma gbinomial_mult_fact: "fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - of_nat i)"
for a :: "'a::field_char_0"
by (simp_all add: gbinomial_prod_rev field_simps)
@@ -479,7 +482,7 @@
for a :: "'a::field_char_0"
by (simp add: mult.commute gbinomial_mult_1)
-lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+lemma gbinomial_Suc_Suc: "(a + 1) gchoose (Suc k) = (a gchoose k) + (a gchoose (Suc k))"
for a :: "'a::field_char_0"
proof (cases k)
case 0
@@ -491,16 +494,13 @@
show "{1..k} = Suc ` {0..h}"
using Suc by (auto simp add: image_Suc_atMost)
qed auto
- have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
+ have "fact (Suc k) * ((a gchoose k) + (a gchoose (Suc k))) =
(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_Suc)
also have "\<dots> =
(a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)"
- apply (simp only: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
- apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact
- mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
- done
+ by (metis atLeastLessThanSuc_atLeastAtMost fact_Suc gbinomial_mult_fact mult.commute of_nat_fact of_nat_mult)
also have "\<dots> =
(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_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
@@ -526,7 +526,7 @@
using fact_nonzero [of "Suc k"] by auto
qed
-lemma gbinomial_reduce_nat: "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
+lemma gbinomial_reduce_nat: "0 < k \<Longrightarrow> a gchoose k = (a-1 gchoose k-1) + (a-1 gchoose k)"
for a :: "'a::field_char_0"
by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)