[isabelle-dev] Lemma "sum_image_le"
Alexander Maletzky
alexander.maletzky at risc.jku.at
Fri Sep 28 15:00:18 CEST 2018
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
More information about the isabelle-dev
mailing list