[isabelle-dev] Frag / Poly_Mapping

[Florian Haftmann]

Just my five cent: instead of thinking about *integrating* the
developments, I'd suggest to distill their *common essence* into a
generic base theory, which would indeed be dedicated to functions with
finite support.

First-letter abbreviations are not very self-explanatory though.  So I'd
go with something more explicit like »finite_support_fun« – note that
this type constructor does not show up in concrete type syntax, only in
type class instantiations, so its length should be fine.

Cheers,
	Florian

Am 24.09.2018 um 18:30 schrieb 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)"
>>
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de