Re: [isabelle-dev] Frag / Poly_Mapping
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 I sent out yesterday and make independent of Poly_Mapping, but would that meet everyone's needs? Larry > On 25 Sep 2018, at 06:18, Akihisa Yamada > wrote: > > 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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] 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