[isabelle-dev] Poly_Mapping

[Manuel Eberl]

I'm sure this is very useful, but I have to say once again that
"Poly_Mapping" is probably not a good name for this now that it is
disconnected from its original application of multivariate polynomials.
I vaguely recall that we had this discussion already a while ago and
didn't really resolve it.

I currently don't have any input beyond that (I'm feeling a bit poorly);
I just wanted to point this out.

Manuel


On 03/04/2019 12:57, Lawrence Paulson wrote:
> I have adopted the theory Poly_Mapping, which is part of the AFP entry Polynomials, as the basis for a theory of finite abelian groups, which plays a huge role in the homology development. (It concerns "almost everywhere zero functions”.) I am gradually installing the components of this development in various places, and think that Poly_Mapping could go into Library, as it depends only on other Library entries. I hope nobody objects to this. Then I guess the duplicate in the AFP should be deleted.
>
> I also managed to accomplish the following:
>
> instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
>
> But I never found a use for it and I’m not sure what to do with it.
>
> Larry
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev