> 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