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