src/HOL/Finite_Set.thy
changeset 16775 c1b87ef4a1c3
parent 16760 5c5f051aaaaa
child 17022 b257300c3a9c
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 12 12:49:46 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 12 17:56:03 2005 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Finite_Set.thy
     1.5      ID:         $Id$
     1.6      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     1.7 -                Additions by Jeremy Avigad in Feb 2004
     1.8 +                with contributions by Jeremy Avigad
     1.9  *)
    1.10  
    1.11  header {* Finite sets *}
    1.12 @@ -1137,6 +1137,26 @@
    1.13    finally show ?thesis .
    1.14  qed
    1.15  
    1.16 +lemma setsum_mono3: "finite B ==> A <= B ==> 
    1.17 +    ALL x: B - A. 
    1.18 +      0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
    1.19 +        setsum f A <= setsum f B"
    1.20 +  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
    1.21 +  apply (erule ssubst)
    1.22 +  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
    1.23 +  apply simp
    1.24 +  apply (rule add_left_mono)
    1.25 +  apply (erule setsum_nonneg)
    1.26 +  apply (subst setsum_Un_disjoint [THEN sym])
    1.27 +  apply (erule finite_subset, assumption)
    1.28 +  apply (rule finite_subset)
    1.29 +  prefer 2
    1.30 +  apply assumption
    1.31 +  apply auto
    1.32 +  apply (rule setsum_cong)
    1.33 +  apply auto
    1.34 +done
    1.35 +
    1.36  (* FIXME: this is distributitivty, name as such! *)
    1.37  
    1.38  lemma setsum_mult: 
    1.39 @@ -1197,7 +1217,8 @@
    1.40      case (insert a A)
    1.41      hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
    1.42      also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
    1.43 -    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
    1.44 +    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
    1.45 +      by (simp del: abs_of_nonneg)
    1.46      also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
    1.47      finally show ?case .
    1.48    qed