--- a/src/HOL/Groups_Big.thy Fri Oct 05 23:49:12 2018 +0200
+++ b/src/HOL/Groups_Big.thy Sat Oct 06 08:59:05 2018 +0200
@@ -1427,7 +1427,7 @@
qed
lemma sum_image_le:
- fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
+ fixes g :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
shows "sum g (f ` I) \<le> sum (g \<circ> f) I"
using assms
@@ -1435,12 +1435,14 @@
case empty
then show ?case by auto
next
- case (insert x F) then
+ case (insert x F)
+ from insertI1 have "0 \<le> g (f x)" by (rule insert)
+ hence 1: "sum g (f ` F) \<le> g (f x) + sum g (f ` F)" using add_increasing by blast
+ have 2: "sum g (f ` F) \<le> sum (g \<circ> f) F" using insert by blast
have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
- also have "\<dots> \<le> g (f x) + sum g (f ` F)"
- by (simp add: insert sum.insert_if)
- also have "\<dots> \<le> sum (g \<circ> f) (insert x F)"
- using insert by auto
+ also have "\<dots> \<le> g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if)
+ also from 2 have "\<dots> \<le> g (f x) + sum (g \<circ> f) F" by (rule add_left_mono)
+ also from insert(1, 2) have "\<dots> = sum (g \<circ> f) (insert x F)" by (simp add: sum.insert_if)
finally show ?case .
qed