Re: [isabelle-dev] Lemma "sum_image_le"

[Alexander Maletzky]

Great, thanks!

Alexander


Am 06.10.2018 um 13:06 schrieb Tobias Nipkow:
> Since Alexander cannot push changes, I have done so now.
>
> Tobias
>
> On 28/09/2018 18:44, Lawrence Paulson wrote:
>> Sounds good to me!
>> Larry
>>
>>> On 28 Sep 2018, at 14:00, Alexander Maletzky
>>> >> > wrote:
>>>
>>>
>>> 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
>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Lemma "sum_image_le"

[Tobias Nipkow]

Since Alexander cannot push changes, I have done so now.

Tobias

On 28/09/2018 18:44, Lawrence Paulson wrote:

Sounds good to me!
Larry

On 28 Sep 2018, at 14:00, Alexander Maletzky > wrote:



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




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Lemma "sum_image_le"

[Lawrence Paulson]

Sounds good to me!
Larry

> On 28 Sep 2018, at 14:00, Alexander Maletzky  
> wrote:
> 
> 
> 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Lemma "sum_image_le"

[Alexander Maletzky]

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