relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
authorobua
Tue Nov 23 15:50:27 2004 +0100 (2004-11-23)
changeset 1531455eec5c6d401
parent 15313 24aee76539df
child 15315 a358e31572d9
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 23 15:36:39 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 23 15:50:27 2004 +0100
     1.3 @@ -958,7 +958,7 @@
     1.4    by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
     1.5  
     1.6  lemma setsum_Un_ring: "finite A ==> finite B ==>
     1.7 -    (setsum f (A Un B) :: 'a :: comm_ring_1) =
     1.8 +    (setsum f (A Un B) :: 'a :: ab_group_add) =
     1.9        setsum f A + setsum f B - setsum f (A Int B)"
    1.10    by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps)
    1.11  
    1.12 @@ -1043,24 +1043,24 @@
    1.13      qed
    1.14    qed
    1.15  
    1.16 -lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A =
    1.17 +lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A =
    1.18    - setsum f A"
    1.19    by (induct set: Finites, auto)
    1.20  
    1.21 -lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::comm_ring_1) - g x) A =
    1.22 +lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
    1.23    setsum f A - setsum g A"
    1.24    by (simp add: diff_minus setsum_addf setsum_negf)
    1.25  
    1.26  lemma setsum_nonneg: "[| finite A;
    1.27 -    \<forall>x \<in> A. (0::'a::ordered_semidom) \<le> f x |] ==>
    1.28 -    0 \<le>  setsum f A";
    1.29 +    \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==>
    1.30 +    0 \<le> setsum f A";
    1.31    apply (induct set: Finites, auto)
    1.32    apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
    1.33    apply (blast intro: add_mono)
    1.34    done
    1.35  
    1.36  lemma setsum_nonpos: "[| finite A;
    1.37 -    \<forall>x \<in> A. f x \<le> (0::'a::ordered_semidom) |] ==>
    1.38 +    \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==>
    1.39      setsum f A \<le> 0";
    1.40    apply (induct set: Finites, auto)
    1.41    apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp)