Re: [isabelle-dev] Lemma "sum_image_le"
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 >>> >> <mailto:alexander.malet...@risc.jku.at>> 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
[isabelle-dev] Lemma "sum_image_le"
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
Re: [isabelle-dev] Frag / Poly_Mapping
Some notions defined in "Frag.thy" already exist in "Poly_Mapping.thy":
"support" is called "keys" there, and I think "frag_cmul" could easily
be defined in terms of "map".
"frag_extend" looks like a special case of a more general subsitution
homomorphism "subst" of type "('a => 'b => 'c) => ('a =>_0 'b) => 'c",
defined as "subst f x = (\Sum i\in keys x. f i (lookup x i))", which
could indeed be added to "Poly_Mapping.thy". The insertion morphism in
"MPoly_Type.thy" could then perhaps be defined in terms of "subst" (at
least partially; for power-products, the above sum would have to be
replaced by a product).
Best regards,
Alexander
On 9/23/18 20:59, Lawrence Paulson wrote:
> Attached is a port of the HOL Light “frag” library (free Abelian groups)
> built upon Poly_Mapping. It’s a mess, especially with the combination of frag
> and Poly_Mapping names. Some of it clearly could be added to Poly_Mapping,
> maybe all of it. But it needs to be rationalised.
>
> Comments / advice?
>
> Larry
>
>
> ___
> 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
