# HG changeset patch
# User obua
# Date 1101221427 -3600
# Node ID 55eec5c6d40119fa3ca6c6b0e10d3e8fd01788c6
# Parent  24aee76539df5963b790df7004529f741c7ae2a8
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring

diff -r 24aee76539df -r 55eec5c6d401 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Nov 23 15:36:39 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 23 15:50:27 2004 +0100
@@ -958,7 +958,7 @@
   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
 
 lemma setsum_Un_ring: "finite A ==> finite B ==>
-    (setsum f (A Un B) :: 'a :: comm_ring_1) =
+    (setsum f (A Un B) :: 'a :: ab_group_add) =
       setsum f A + setsum f B - setsum f (A Int B)"
   by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
 
@@ -1043,24 +1043,24 @@
     qed
   qed
 
-lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A =
+lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
   - setsum f A"
   by (induct set: Finites, auto)
 
-lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::comm_ring_1) - g x) A =
+lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   setsum f A - setsum g A"
   by (simp add: diff_minus setsum_addf setsum_negf)
 
 lemma setsum_nonneg: "[| finite A;
-    \<forall>x \<in> A. (0::'a::ordered_semidom) \<le> f x |] ==>
-    0 \<le>  setsum f A";
+    \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
+    0 \<le> setsum f A";
   apply (induct set: Finites, auto)
   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
   apply (blast intro: add_mono)
   done
 
 lemma setsum_nonpos: "[| finite A;
-    \<forall>x \<in> A. f x \<le> (0::'a::ordered_semidom) |] ==>
+    \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
     setsum f A \<le> 0";
   apply (induct set: Finites, auto)
   apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)