[isabelle-dev] Frag / Poly_Mapping

[Alexander Maletzky]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180924/8c896426/attachment-0002.html>