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
On 24/09/18 08:19, Lars Hupel wrote:
>> There were a few remaining uses in AFP. Notable changes are
>> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
>> generated by LEM (!). I don't know how LEM is maintained: it needs to
>> produce different inner comments next time, and can
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
> There were a few remaining uses in AFP. Notable changes are
> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
> generated by LEM (!). I don't know how LEM is maintained: it needs to
> produce different inner comments next time, and can actually use
> \ CARTOUCHE notation
