Dear list, lemma "sum_image_le" in theory "Groups_Big", which is stated for type-class "ordered_ab_group_add", holds more generally for "ordered_comm_monoid_add" (proof below). May I propose to change it accordingly?
Best regards, Alexander lemma sum_image_le: fixes g :: "'a ⇒ 'b::ordered_comm_monoid_add" assumes "finite I" and "⋀i. i ∈ I ⟹ 0 ≤ g(f i)" shows "sum g (f ` I) ≤ sum (g ∘ f) I" using assms proof induction case empty then show ?case by auto next case (insert x F) from insertI1 have "0 ≤ g (f x)" by (rule insert) hence 1: "sum g (f ` F) ≤ g (f x) + sum g (f ` F)" using add_increasing by blast from insert have 2: "sum g (f ` F) ≤ sum (g ∘ f) F" by blast have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp also have "… ≤ g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if) also from 2 have "… ≤ g (f x) + sum (g ∘ f) F" by (rule add_left_mono) also from insert(1, 2) have "… = sum (g ∘ f) (insert x F)" by (simp add: sum.insert_if) finally show ?case . qed _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
