# [isabelle-dev] Frag / Poly_Mapping

Lawrence Paulson lp15 at cam.ac.uk
Mon Sep 24 16:32:52 CEST 2018

> 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]

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)"
next
fix a b :: "'a frag"
show "a + b = b + a"
next
fix a :: "'a frag"
show "0 + a = a"
qed

end

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]

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)"