It seems there is clearly a need for something of the sort to go into
HOL/Library. Maybe it could be completely independent of Poly_Mapping, and the
latter perhaps could be rewritten in terms of it.
Now who is volunteering to do this? I could certainly rewrite my "Frag.thy" to
use the material
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
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
Just my five cent: instead of thinking about *integrating* the
developments, I'd suggest to distill their *common essence* into a
generic base theory, which would indeed be dedicated to functions with
finite support.
First-letter abbreviations are not very self-explanatory though. So I'd
go with
Indeed, I am not sure whether avoiding duplication at all cost is what
we should do here. poly_mapping is quite a big thing (and much essential
material is still missing). It was introduced very specifically for the
purpose of building monomials and polynomials. In principle, it can of
course be
> On 24 Sep 2018, at 10:30, Alexander Maletzky
> wrote:
>
> 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
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
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 /
