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)"
>
>
pEpkey.asc
Description: application/pgp-keys
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
