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