# HG changeset patch
# User nipkow
# Date 1330339988 -3600
# Node ID 1fef02b93723b65720146d4303246994979beea0
# Parent  b07ae33cc4598cf8a9c00309989372e45061b736# Parent  ae3f30a5063aac5abf7f45c66a1b7972c511fbc5
merged

diff -r b07ae33cc459 -r 1fef02b93723 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Mon Feb 27 10:56:36 2012 +0100
+++ b/src/HOL/Big_Operators.thy	Mon Feb 27 11:53:08 2012 +0100
@@ -523,6 +523,25 @@
   case insert thus ?case by (auto simp: add_strict_mono)
 qed
 
+lemma setsum_strict_mono_ex1:
+fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
+assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
+shows "setsum f A < setsum g A"
+proof-
+  from assms(3) obtain a where a: "a:A" "f a < g a" by blast
+  have "setsum f A = setsum f ((A-{a}) \<union> {a})"
+    by(simp add:insert_absorb[OF `a:A`])
+  also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
+    using `finite A` by(subst setsum_Un_disjoint) auto
+  also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
+    by(rule setsum_mono)(simp add: assms(2))
+  also have "setsum f {a} < setsum g {a}" using a by simp
+  also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
+    using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
+  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
+  finally show ?thesis by (metis add_right_mono add_strict_left_mono)
+qed
+
 lemma setsum_negf:
   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
 proof (cases "finite A")
diff -r b07ae33cc459 -r 1fef02b93723 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Feb 27 10:56:36 2012 +0100
+++ b/src/HOL/List.thy	Mon Feb 27 11:53:08 2012 +0100
@@ -960,6 +960,8 @@
 
 subsubsection {* @{text set} *}
 
+declare set.simps [code_post]  --"pretty output"
+
 lemma finite_set [iff]: "finite (set xs)"
 by (induct xs) auto