Re: [isabelle-dev] Frag / Poly_Mapping
Dear Alexander, Florian, Larry, Manuel, recently I also made the same typedef, so that derivatives can be defined, which wants real norm in current Isabelle/HOL. Unfortunately I didn't notice it is called "poly_mapping". I propose calling them finsupp or finite_supp. Support is often written "supp", and the term in this meaning is clearly about functions so I don't think "_fun" is needed. Best regards, Akihisa On 2018/09/25 1:49, Manuel Eberl wrote: On 24/09/2018 18:41, Florian Haftmann wrote: First-letter abbreviations are not very self-explanatory though. So I'd go with something more explicit like »finite_support_fun« – note that this type constructor does not show up in concrete type syntax, only in type class instantiations, so its length should be fine. It does show up in the name of the operations you define on it and the theorems you prove about it though. Manuel ___ 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
Re: [isabelle-dev] reflect_poly
Dear Manuel, There are definitely books out there that call it the "reflected polynomial", and that's what my undergraduate discrete maths course called it, so that's what I called it. oh I'm fine with the naming if it's textbook-level standard. I wouldn't have raised this if there were a reference in the thy file, though. BTW, Google-books search will find "reciprocal polynomial": 152 "reverse polynomial": 118 "reflected polynomial": 18 (try to access the last hit, otherwise reciprocal looks dominant). So "rev_poly" seems to be a good option (in connection with rev, obviously). Best, Akihisa ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] reflect_poly
Dear HOL-Computational_Algebra developers, how about renaming "reflect_poly" in Polynomial.thy to "reciprocal_poly"? It seems to be standard to call them "reciprocal polynomials", cf. https://en.wikipedia.org/wiki/Reciprocal_polynomial, and the current naming wants an extra sentence to relate the notions in paper writing. Best regards, Akihisa ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
