[isabelle-dev] Frag / Poly_Mapping

[Lawrence Paulson]

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