Theory MPoly_Type_Univariate
theory MPoly_Type_Univariate
imports
More_MPoly_Type
"HOL-Computational_Algebra.Polynomial"
begin
text ‹This file connects univariate MPolys to the theory of univariate polynomials from
@{theory "HOL-Computational_Algebra.Polynomial"}.›
definition poly_to_mpoly::"nat ⇒ 'a::comm_monoid_add poly ⇒ 'a mpoly"
where "poly_to_mpoly v p = MPoly (Abs_poly_mapping (λm. (coeff p (Poly_Mapping.lookup m v)) when Poly_Mapping.keys m ⊆ {v}))"
lemma poly_to_mpoly_finite: "finite {m::nat ⇒⇩0 nat. (coeff p (Poly_Mapping.lookup m v) when Poly_Mapping.keys m ⊆ {v}) ≠ 0}" (is "finite ?M")
proof -
have "?M ⊆ Poly_Mapping.single v ` {x. Polynomial.coeff p x ≠ 0}"
proof
fix m assume "m ∈ ?M"
then have "⋀v'. v'≠v ⟹ Poly_Mapping.lookup m v' = 0" by (fastforce simp add: in_keys_iff)
then have "m = Poly_Mapping.single v (Poly_Mapping.lookup m v)"
using Poly_Mapping.poly_mapping_eqI by (metis (full_types) lookup_single_eq lookup_single_not_eq)
then show "m ∈ (Poly_Mapping.single v) ` {x. Polynomial.coeff p x ≠ 0}" using ‹m ∈ ?M› by auto
qed
then show ?thesis using finite_surj[OF MOST_coeff_eq_0[unfolded eventually_cofinite]] by blast
qed
lemma coeff_poly_to_mpoly: "MPoly_Type.coeff (poly_to_mpoly v p) (Poly_Mapping.single v k) = Polynomial.coeff p k"
unfolding poly_to_mpoly_def coeff_def MPoly_inverse[OF Set.UNIV_I] lookup_Abs_poly_mapping[OF poly_to_mpoly_finite]
using empty_subsetI keys_single lookup_single order_refl when_simps(1) by simp
definition mpoly_to_poly::"nat ⇒ 'a::comm_monoid_add mpoly ⇒ 'a poly"
where "mpoly_to_poly v p = Abs_poly (λk. MPoly_Type.coeff p (Poly_Mapping.single v k))"
lemma coeff_mpoly_to_poly[simp]: "Polynomial.coeff (mpoly_to_poly v p) k = MPoly_Type.coeff p (Poly_Mapping.single v k)"
proof -
have 0:"Poly_Mapping.single v ` {x. Poly_Mapping.lookup (mapping_of p) (Poly_Mapping.single v x) ≠ 0}
⊆ {k. Poly_Mapping.lookup (mapping_of p) k ≠ 0}"
by auto
have "∀⇩∞ k. MPoly_Type.coeff p (Poly_Mapping.single v k) = 0" unfolding coeff_def eventually_cofinite
using finite_imageD[OF finite_subset[OF 0 Poly_Mapping.finite_lookup]] inj_single by (metis inj_eq inj_onI)
then show ?thesis
unfolding mpoly_to_poly_def by (simp add: Abs_poly_inverse)
qed
lemma mpoly_to_poly_inverse:
assumes "vars p ⊆ {v}"
shows "poly_to_mpoly v (mpoly_to_poly v p) = p"
proof -
define f where "f = (λm. Polynomial.coeff (mpoly_to_poly v p) (Poly_Mapping.lookup m v) when Poly_Mapping.keys m ⊆ {v})"
have "finite {m. f m ≠ 0}" unfolding f_def using poly_to_mpoly_finite by blast
have "Abs_poly_mapping f = mapping_of p"
proof (rule "Poly_Mapping.poly_mapping_eqI")
fix m
show "Poly_Mapping.lookup (Abs_poly_mapping f) m = Poly_Mapping.lookup (mapping_of p) m"
proof (cases "Poly_Mapping.keys m ⊆ {v}")
assume "Poly_Mapping.keys m ⊆ {v}"
then show ?thesis unfolding "Poly_Mapping.lookup_Abs_poly_mapping"[OF ‹finite {m. f m ≠ 0}›] unfolding f_def
unfolding coeff_mpoly_to_poly coeff_def using when_simps(1) apply simp
using keys_single lookup_not_eq_zero_eq_in_keys lookup_single_eq
lookup_single_not_eq poly_mapping_eqI subset_singletonD
by (metis (no_types, lifting) aux lookup_eq_zero_in_keys_contradict)
next
assume "¬Poly_Mapping.keys m ⊆ {v}"
then show ?thesis unfolding "Poly_Mapping.lookup_Abs_poly_mapping"[OF ‹finite {m. f m ≠ 0}›] unfolding f_def
using ‹vars p ⊆ {v}› unfolding vars_def by (metis (no_types, lifting) UN_I lookup_not_eq_zero_eq_in_keys subsetCE subsetI when_def)
qed
qed
then show ?thesis
unfolding poly_to_mpoly_def f_def by (simp add: mapping_of_inverse)
qed
lemma poly_to_mpoly_inverse: "mpoly_to_poly v (poly_to_mpoly v p) = p"
unfolding mpoly_to_poly_def coeff_poly_to_mpoly by (simp add: coeff_inverse)
lemma poly_to_mpoly0: "poly_to_mpoly v 0 = 0"
proof -
have "⋀m. (Polynomial.coeff 0 (Poly_Mapping.lookup m v) when Poly_Mapping.keys m ⊆ {v}) = 0" by simp
have "Abs_poly_mapping (λm. Polynomial.coeff 0 (Poly_Mapping.lookup m v) when Poly_Mapping.keys m ⊆ {v}) = 0"
apply (rule Poly_Mapping.poly_mapping_eqI) unfolding lookup_Abs_poly_mapping[OF poly_to_mpoly_finite] by auto
then show ?thesis using poly_to_mpoly_def zero_mpoly.abs_eq by (metis (no_types))
qed
lemma mpoly_to_poly_add: "mpoly_to_poly v (p1 + p2) = mpoly_to_poly v p1 + mpoly_to_poly v p2"
unfolding Polynomial.plus_poly.abs_eq More_MPoly_Type.coeff_add coeff_mpoly_to_poly
using mpoly_to_poly_def by auto
lemma poly_eq_insertion:
assumes "vars p ⊆ {v}"
shows "poly (mpoly_to_poly v p) x = insertion (λv. x) p"
using assms proof (induction p rule:mpoly_induct)
case (monom m a)
then show ?case
proof (cases "a=0")
case True
then show ?thesis
by (metis MPoly_Type.monom.abs_eq insertion_zero monom_zero poly_0 poly_to_mpoly0 poly_to_mpoly_inverse single_zero)
next
case False
then have "Poly_Mapping.keys m ⊆ {v}" using monom unfolding vars_def MPoly_Type.mapping_of_monom keys_single by simp
then have "⋀v'. v'≠v ⟹ Poly_Mapping.lookup m v' = 0" unfolding vars_def by (auto simp: in_keys_iff)
then have "m = Poly_Mapping.single v (Poly_Mapping.lookup m v)"
by (metis lookup_single_eq lookup_single_not_eq poly_mapping_eqI)
then have 0:"insertion (λv. x) (MPoly_Type.monom m a) = a * x ^ (Poly_Mapping.lookup m v)"
using insertion_single by metis
have "⋀k. Poly_Mapping.single v k = m ⟷ Poly_Mapping.lookup m v = k"
using ‹m = Poly_Mapping.single v (Poly_Mapping.lookup m v)› by auto
then have "monom a (Poly_Mapping.lookup m v) = (Abs_poly (λk. if Poly_Mapping.single v k = m then a else 0))"
by (simp add: Polynomial.monom.abs_eq)
then show ?thesis unfolding mpoly_to_poly_def More_MPoly_Type.coeff_monom 0 when_def by (metis poly_monom)
qed
next
case (sum p1 p2 m a)
then have "poly (mpoly_to_poly v p1) x = insertion (λv. x) p1"
"poly (mpoly_to_poly v p2) x = insertion (λv. x) p2"
by (simp_all add: vars_add_monom)
then show ?case unfolding insertion_add mpoly_to_poly_add by simp
qed
text ‹Using the new connection between MPoly and univariate polynomials, we can transfer:›
lemma univariate_mpoly_roots_finite:
fixes p::"'a::idom mpoly"
assumes "vars p ⊆ {v}" "p ≠ 0"
shows "finite {x. insertion (λv. x) p = 0}"
using poly_roots_finite[of "mpoly_to_poly v p", unfolded poly_eq_insertion[OF ‹vars p ⊆ {v}›]]
using assms(1) assms(2) mpoly_to_poly_inverse poly_to_mpoly0 by fastforce
end