[isabelle-dev] Frag / Poly_Mapping

[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.maletzky at 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)"
>
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 1757 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180924/c86e7a06/attachment-0002.key>