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] Frag / Poly_Mapping
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 pEpkey.asc Description: application/pgp-keys ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Frag / Poly_Mapping
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 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.
Cheers,
Florian
Am 24.09.2018 um 18:30 schrieb Manuel Eberl:
> 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 seen in a much more general light. On the other hand, the free
> abelian groups have a more narrow focus.
>
> Now, we could implement free abelian groups with poly_mapping. What
> would that entail? We would have to move it to the distribution, but
> then I think we should then also attempt to really clean it up quite a
> bit. Also, we would need to rename it to something catchy and more
> general. "Function with finite support" is what it essentially is, so
> perhaps "fsfun"?
>
> Also, any changes that we make will have repercussions in the AFP and
> possibly other non-AFP applications (I'm concerned about IsaFoR in
> particular, so I cc'ed René).
>
> Manuel
>
>
> On 24/09/2018 16:32, Lawrence Paulson wrote:
>>> 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 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).
>> Thanks for that. Manuel is expressing the opposite point of view, namely
>> that it might be better to keep the two developments 100% separate.
>> Certainly the basic setup of Frag is simple and short (see below) and we
>> don't have to concern ourselves with how Poly_Mapping is used by other
>> developments in the AFP and in other projects outside. So I'm puzzled as to
>> the best course.
>>
>> Larry
>>
>> typedef 'a frag = "{f::'a\int. finite {x. f x \ 0}}"
>> by (rule exI [where x = "\x. 0"]) auto
>>
>> definition support
>> where "support F = {a. Rep_frag F a \ 0}"
>>
>> declare Rep_frag_inverse [simp] Abs_frag_inverse [simp]
>>
>>
>> instantiation frag :: (type)comm_monoid_add
>> begin
>>
>> definition zero_frag_def: "0 \ Abs_frag (\x. 0)"
>>
>> definition add_frag_def: "a+b \ Abs_frag (\x. Rep_frag a x +
>> Rep_frag b x)"
>>
>> lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \
>> 0}"
>> proof -
>> have "finite {x. Rep_frag a x \ 0}" "finite {x. Rep_frag b x
>> \ 0}"
>> using Rep_frag by auto
>> moreover have "{x. Rep_frag a x + Rep_frag b x \ 0} \ {x.
>> Rep_frag a x \ 0} \ {x. Rep_frag b x \ 0}"
>> by auto
>> ultimately show ?thesis
>> using infinite_super by blast
>> qed
>>
>> lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \ 0}"
>> using Rep_frag [of a] by simp
>>
>> instance
>> proof
>> fix a b c :: "'a frag"
>> show "a + b + c = a + (b + c)"
>> by (simp add: add_frag_def finite_add_nonzero add.assoc)
>> next
>> fix a b :: "'a frag"
>> show "a + b = b + a"
>> by (simp add: add_frag_def add.commute)
>> next
>> fix a :: "'a frag"
>> show "0 + a = a"
>> by (simp add: add_frag_def zero_frag_def)
>> qed
>>
>> end
>>
>> instantiation frag :: (type)ab_group_add
>> begin
>>
>> definition minus_frag_def: "-a \ Abs_frag (\x. - Rep_frag a
>> x)"
>>
>> definition diff_frag_def: "a-b \ a + - (b::'a frag)"
>>
>> instance
>> proof
>> fix a :: "'a frag"
>> show "- a + a = 0"
>> using finite_minus_nonzero [of a]
>> by (simp add: minus_frag_def add_frag_def zero_frag_def)
>> qed (simp add: diff_frag_def)
>>
>> end
>>
>>
>> definition frag_of where "frag_of c = Abs_frag (\a. if a = c then 1
>> else 0)"
>>
>> lemma frag_of_nonzero [simp]: "frag_of a \ 0"
>> proof -
>> have "(\x. if x = a then 1 else 0) \ (\x. 0::int)"
>> by (auto simp: fun_eq_iff)
>> then have "Rep_frag (Abs_frag (\aa. if aa = a then 1 else 0))
>> \ Rep_frag (Abs_frag (\x. 0))"
>> by simp
>> then show ?thesis
>> unfolding zero_frag_def frag_of_def Rep_frag_inject .
>> qed
>>
>> definition frag_cmul :: "int \ 'a frag \ 'a frag"
>> where "frag_cmul
Re: [isabelle-dev] Frag / Poly_Mapping
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 seen in a much more general light. On the other hand, the free
abelian groups have a more narrow focus.
Now, we could implement free abelian groups with poly_mapping. What
would that entail? We would have to move it to the distribution, but
then I think we should then also attempt to really clean it up quite a
bit. Also, we would need to rename it to something catchy and more
general. "Function with finite support" is what it essentially is, so
perhaps "fsfun"?
Also, any changes that we make will have repercussions in the AFP and
possibly other non-AFP applications (I'm concerned about IsaFoR in
particular, so I cc'ed René).
Manuel
On 24/09/2018 16:32, Lawrence Paulson wrote:
>> 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 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).
> Thanks for that. Manuel is expressing the opposite point of view, namely that
> it might be better to keep the two developments 100% separate. Certainly the
> basic setup of Frag is simple and short (see below) and we don't have to
> concern ourselves with how Poly_Mapping is used by other developments in the
> AFP and in other projects outside. So I'm puzzled as to the best course.
>
> Larry
>
> typedef 'a frag = "{f::'a\int. finite {x. f x \ 0}}"
> by (rule exI [where x = "\x. 0"]) auto
>
> definition support
> where "support F = {a. Rep_frag F a \ 0}"
>
> declare Rep_frag_inverse [simp] Abs_frag_inverse [simp]
>
>
> instantiation frag :: (type)comm_monoid_add
> begin
>
> definition zero_frag_def: "0 \ Abs_frag (\x. 0)"
>
> definition add_frag_def: "a+b \ Abs_frag (\x. Rep_frag a x +
> Rep_frag b x)"
>
> lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \ 0}"
> proof -
> have "finite {x. Rep_frag a x \ 0}" "finite {x. Rep_frag b x
> \ 0}"
> using Rep_frag by auto
> moreover have "{x. Rep_frag a x + Rep_frag b x \ 0} \ {x.
> Rep_frag a x \ 0} \ {x. Rep_frag b x \ 0}"
> by auto
> ultimately show ?thesis
> using infinite_super by blast
> qed
>
> lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \ 0}"
> using Rep_frag [of a] by simp
>
> instance
> proof
> fix a b c :: "'a frag"
> show "a + b + c = a + (b + c)"
> by (simp add: add_frag_def finite_add_nonzero add.assoc)
> next
> fix a b :: "'a frag"
> show "a + b = b + a"
> by (simp add: add_frag_def add.commute)
> next
> fix a :: "'a frag"
> show "0 + a = a"
> by (simp add: add_frag_def zero_frag_def)
> qed
>
> end
>
> instantiation frag :: (type)ab_group_add
> begin
>
> definition minus_frag_def: "-a \ Abs_frag (\x. - Rep_frag a x)"
>
> definition diff_frag_def: "a-b \ a + - (b::'a frag)"
>
> instance
> proof
> fix a :: "'a frag"
> show "- a + a = 0"
> using finite_minus_nonzero [of a]
> by (simp add: minus_frag_def add_frag_def zero_frag_def)
> qed (simp add: diff_frag_def)
>
> end
>
>
> definition frag_of where "frag_of c = Abs_frag (\a. if a = c then 1
> else 0)"
>
> lemma frag_of_nonzero [simp]: "frag_of a \ 0"
> proof -
> have "(\x. if x = a then 1 else 0) \ (\x. 0::int)"
> by (auto simp: fun_eq_iff)
> then have "Rep_frag (Abs_frag (\aa. if aa = a then 1 else 0))
> \ Rep_frag (Abs_frag (\x. 0))"
> by simp
> then show ?thesis
> unfolding zero_frag_def frag_of_def Rep_frag_inject .
> qed
>
> definition frag_cmul :: "int \ 'a frag \ 'a frag"
> where "frag_cmul c a = Abs_frag (\x. c * Rep_frag a x)"
>
>
pEpkey.asc
Description: application/pgp-keys
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Frag / Poly_Mapping
> 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 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).
Thanks for that. Manuel is expressing the opposite point of view, namely that
it might be better to keep the two developments 100% separate. Certainly the
basic setup of Frag is simple and short (see below) and we don't have to
concern ourselves with how Poly_Mapping is used by other developments in the
AFP and in other projects outside. So I'm puzzled as to the best course.
Larry
typedef 'a frag = "{f::'a\int. finite {x. f x \ 0}}"
by (rule exI [where x = "\x. 0"]) auto
definition support
where "support F = {a. Rep_frag F a \ 0}"
declare Rep_frag_inverse [simp] Abs_frag_inverse [simp]
instantiation frag :: (type)comm_monoid_add
begin
definition zero_frag_def: "0 \ Abs_frag (\x. 0)"
definition add_frag_def: "a+b \ Abs_frag (\x. Rep_frag a x +
Rep_frag b x)"
lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \ 0}"
proof -
have "finite {x. Rep_frag a x \ 0}" "finite {x. Rep_frag b x \
0}"
using Rep_frag by auto
moreover have "{x. Rep_frag a x + Rep_frag b x \ 0} \ {x.
Rep_frag a x \ 0} \ {x. Rep_frag b x \ 0}"
by auto
ultimately show ?thesis
using infinite_super by blast
qed
lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \ 0}"
using Rep_frag [of a] by simp
instance
proof
fix a b c :: "'a frag"
show "a + b + c = a + (b + c)"
by (simp add: add_frag_def finite_add_nonzero add.assoc)
next
fix a b :: "'a frag"
show "a + b = b + a"
by (simp add: add_frag_def add.commute)
next
fix a :: "'a frag"
show "0 + a = a"
by (simp add: add_frag_def zero_frag_def)
qed
end
instantiation frag :: (type)ab_group_add
begin
definition minus_frag_def: "-a \ Abs_frag (\x. - Rep_frag a x)"
definition diff_frag_def: "a-b \ a + - (b::'a frag)"
instance
proof
fix a :: "'a frag"
show "- a + a = 0"
using finite_minus_nonzero [of a]
by (simp add: minus_frag_def add_frag_def zero_frag_def)
qed (simp add: diff_frag_def)
end
definition frag_of where "frag_of c = Abs_frag (\a. if a = c then 1
else 0)"
lemma frag_of_nonzero [simp]: "frag_of a \ 0"
proof -
have "(\x. if x = a then 1 else 0) \ (\x. 0::int)"
by (auto simp: fun_eq_iff)
then have "Rep_frag (Abs_frag (\aa. if aa = a then 1 else 0))
\ Rep_frag (Abs_frag (\x. 0))"
by simp
then show ?thesis
unfolding zero_frag_def frag_of_def Rep_frag_inject .
qed
definition frag_cmul :: "int \ 'a frag \ 'a frag"
where "frag_cmul c a = Abs_frag (\x. c * Rep_frag a x)"
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: discontinued old-style inner comments
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 actually use >> \ CARTOUCHE notation uniformly for inner and outer comments -- >> also note that this needs to be LaTeX-conformant, e.g. by another nested >> cartouche or \<^verbatim>CARTOUCHE. > > The way this works is that I'll have to send them a patch. This should > hopefully be simple enough. OK, thanks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Frag / Poly_Mapping
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 =>_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).
Best regards,
Alexander
On 9/23/18 20:59, Lawrence Paulson wrote:
> 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
>
>
> ___
> 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] NEWS: discontinued old-style inner comments
> 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 uniformly for inner and outer comments -- > also note that this needs to be LaTeX-conformant, e.g. by another nested > cartouche or \<^verbatim>CARTOUCHE. The way this works is that I'll have to send them a patch. This should hopefully be simple enough. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
