generalize class constraints on some lemmas

--- a/src/HOL/Finite_Set.thy	Wed Jun 06 17:00:09 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jun 06 17:01:33 2007 +0200
@@ -1405,7 +1405,7 @@
   by (induct set: finite) auto
 
 lemma setprod_zero:
-     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
+     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
   apply (induct set: finite, force, clarsimp)
   apply (erule disjE, auto)
   done
@@ -1429,24 +1429,24 @@
   done
 
 lemma setprod_nonzero [rule_format]:
-    "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
+    "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
   apply (erule finite_induct, auto)
   done
 
 lemma setprod_zero_eq:
-    "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
+    "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
   done
 
 lemma setprod_nonzero_field:
-    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
+    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
   apply (rule setprod_nonzero, auto)
   done
 
 lemma setprod_zero_eq_field:
-    "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
+    "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
   apply (rule setprod_zero_eq, auto)
   done
 
@@ -1657,7 +1657,7 @@
   done
 
 lemma setsum_bounded:
-  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
   shows "setsum f A \<le> of_nat(card A) * K"
 proof (cases "finite A")
   case True

--- a/src/HOL/NatBin.thy	Wed Jun 06 17:00:09 2007 +0200
+++ b/src/HOL/NatBin.thy	Wed Jun 06 17:01:33 2007 +0200
@@ -274,13 +274,13 @@
 We cannot prove general results about the numeral @{term "-1"}, so we have to
 use @{term "- 1"} instead.*}
 
-lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
+lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
   by (simp add: numeral_2_eq_2 Power.power_Suc)
 
-lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
+lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
   by (simp add: power2_eq_square)
 
-lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
+lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
   by (simp add: power2_eq_square)
 
 lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"

--- a/src/HOL/SetInterval.thy	Wed Jun 06 17:00:09 2007 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jun 06 17:01:33 2007 +0200
@@ -750,7 +750,7 @@
 subsection {* The formula for arithmetic sums *}
 
 lemma gauss_sum:
-  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
+  "((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    of_nat n*((of_nat n)+1)"
 proof (induct n)
   case 0
@@ -761,7 +761,7 @@
 qed
 
 theorem arith_series_general:
-  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
+  "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   of_nat n * (a + (a + of_nat(n - 1)*d))"
 proof cases
   assume ngt1: "n > 1"