<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><tt>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".</tt></p>
<p><tt>"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).</tt></p>
<tt>Best regards,</tt><br>
<tt>Alexander</tt>
<p><tt></tt><br>
</p>
<div class="moz-cite-prefix">On 9/23/18 20:59, Lawrence Paulson
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:09F10F3E-E1CE-4F2C-AD54-F766FB4D7DFE@cam.ac.uk">
<pre class="moz-quote-pre" wrap="">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
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>