diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy Tue Jul 12 12:49:46 2005 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jul 12 17:56:03 2005 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Finite_Set.thy
ID: $Id$
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
- Additions by Jeremy Avigad in Feb 2004
+ with contributions by Jeremy Avigad
*)
header {* Finite sets *}
@@ -1137,6 +1137,26 @@
finally show ?thesis .
qed
+lemma setsum_mono3: "finite B ==> A <= B ==>
+ ALL x: B - A.
+ 0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
+ setsum f A <= setsum f B"
+ apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
+ apply (erule ssubst)
+ apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
+ apply simp
+ apply (rule add_left_mono)
+ apply (erule setsum_nonneg)
+ apply (subst setsum_Un_disjoint [THEN sym])
+ apply (erule finite_subset, assumption)
+ apply (rule finite_subset)
+ prefer 2
+ apply assumption
+ apply auto
+ apply (rule setsum_cong)
+ apply auto
+done
+
(* FIXME: this is distributitivty, name as such! *)
lemma setsum_mult:
@@ -1197,7 +1217,8 @@
case (insert a A)
hence "\\a\insert a A. \f a\\ = \\f a\ + (\a\A. \f a\)\" by simp
also have "\ = \\f a\ + \\a\A. \f a\\\" using insert by simp
- also have "\ = \f a\ + \\a\A. \f a\\" by simp
+ also have "\ = \f a\ + \\a\A. \f a\\"
+ by (simp del: abs_of_nonneg)
also have "\ = (\a\insert a A. \f a\)" using insert by simp
finally show ?case .
qed