# HG changeset patch
# User huffman
# Date 1243543933 25200
# Node ID 6c593b431f04318dcc82832167b6eb4a9d925381
# Parent  4248748138405d9d7b5cf5d00df81053a449c0e5
use class field_char_0

diff -r 424874813840 -r 6c593b431f04 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Thu May 28 13:43:45 2009 -0700
+++ b/src/HOL/Library/Binomial.thy	Thu May 28 13:52:13 2009 -0700
@@ -6,7 +6,7 @@
 header {* Binomial Coefficients *}
 
 theory Binomial
-imports Fact SetInterval Presburger Main
+imports Fact SetInterval Presburger Main Rational
 begin
 
 text {* This development is based on the work of Andy Gordon and
@@ -290,7 +290,7 @@
 
 subsection{* Generalized binomial coefficients *}
 
-definition gbinomial :: "'a::{field, ring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
+definition gbinomial :: "'a::field_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"
@@ -345,7 +345,7 @@
   
 lemma binomial_fact: 
   assumes kn: "k \<le> n" 
-  shows "(of_nat (n choose k) :: 'a::{field, ring_char_0}) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
+  shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
   using binomial_fact_lemma[OF kn]
   by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric])
 
@@ -418,16 +418,16 @@
   by (simp add: gbinomial_def)
  
 lemma gbinomial_mult_fact:
-  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::{field, ring_char_0}) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_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}) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+  "((a::'a::field_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, ring_char_0}) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
+lemma gbinomial_Suc_Suc: "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
 proof-
   {assume "k = 0" then have ?thesis by simp}
   moreover
diff -r 424874813840 -r 6c593b431f04 src/HOL/ex/Formal_Power_Series_Examples.thy
--- a/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu May 28 13:43:45 2009 -0700
+++ b/src/HOL/ex/Formal_Power_Series_Examples.thy	Thu May 28 13:52:13 2009 -0700
@@ -11,7 +11,7 @@
 
 section{* The generalized binomial theorem *}
 lemma gbinomial_theorem: 
-  "((a::'a::{ring_char_0, field, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+  "((a::'a::{field_char_0, division_by_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
 proof-
   from E_add_mult[of a b] 
   have "(E (a + b)) $ n = (E a * E b)$n" by simp
@@ -38,7 +38,7 @@
   by (simp add: fps_binomial_def)
 
 lemma fps_binomial_ODE_unique:
-  fixes c :: "'a::{field, ring_char_0}"
+  fixes c :: "'a::field_char_0"
   shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
@@ -302,4 +302,4 @@
   finally show ?thesis .
 qed
 
-end
\ No newline at end of file
+end