--- a/src/HOL/Library/Binomial.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Wed Apr 29 14:20:26 2009 +0200
@@ -292,7 +292,7 @@
subsection{* Generalized binomial coefficients *}
-definition gbinomial :: "'a::{field, recpower,ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a::{field, ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
where "a gchoose n = (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
@@ -420,16 +420,16 @@
by (simp add: gbinomial_def)
lemma gbinomial_mult_fact:
- "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0,recpower}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+ "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
unfolding gbinomial_Suc
by (simp_all add: field_simps del: fact_Suc)
lemma gbinomial_mult_fact':
- "((a::'a::{field, ring_char_0,recpower}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+ "((a::'a::{field, ring_char_0}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
using gbinomial_mult_fact[of k a]
apply (subst mult_commute) .
-lemma gbinomial_Suc_Suc: "((a::'a::{field,recpower, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+lemma gbinomial_Suc_Suc: "((a::'a::{field, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
proof-
{assume "k = 0" then have ?thesis by simp}
moreover