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 >>> <alexander.malet...@risc.jku.at> 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\<Rightarrow>int. finite {x. f x \<noteq> 0}}" >> by (rule exI [where x = "\<lambda>x. 0"]) auto >> >> definition support >> where "support F = {a. Rep_frag F a \<noteq> 0}" >> >> declare Rep_frag_inverse [simp] Abs_frag_inverse [simp] >> >> >> instantiation frag :: (type)comm_monoid_add >> begin >> >> definition zero_frag_def: "0 \<equiv> Abs_frag (\<lambda>x. 0)" >> >> definition add_frag_def: "a+b \<equiv> Abs_frag (\<lambda>x. Rep_frag a x + >> Rep_frag b x)" >> >> lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \<noteq> >> 0}" >> proof - >> have "finite {x. Rep_frag a x \<noteq> 0}" "finite {x. Rep_frag b x >> \<noteq> 0}" >> using Rep_frag by auto >> moreover have "{x. Rep_frag a x + Rep_frag b x \<noteq> 0} \<subseteq> {x. >> Rep_frag a x \<noteq> 0} \<union> {x. Rep_frag b x \<noteq> 0}" >> by auto >> ultimately show ?thesis >> using infinite_super by blast >> qed >> >> lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \<noteq> 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 \<equiv> Abs_frag (\<lambda>x. - Rep_frag a >> x)" >> >> definition diff_frag_def: "a-b \<equiv> 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 (\<lambda>a. if a = c then 1 >> else 0)" >> >> lemma frag_of_nonzero [simp]: "frag_of a \<noteq> 0" >> proof - >> have "(\<lambda>x. if x = a then 1 else 0) \<noteq> (\<lambda>x. 0::int)" >> by (auto simp: fun_eq_iff) >> then have "Rep_frag (Abs_frag (\<lambda>aa. if aa = a then 1 else 0)) >> \<noteq> Rep_frag (Abs_frag (\<lambda>x. 0))" >> by simp >> then show ?thesis >> unfolding zero_frag_def frag_of_def Rep_frag_inject . >> qed >> >> definition frag_cmul :: "int \<Rightarrow> 'a frag \<Rightarrow> 'a frag" >> where "frag_cmul c a = Abs_frag (\<lambda>x. c * Rep_frag a x)" >> >> >> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev