Theory Univariate_PM
section ‹Polynomial Mappings and Univariate Polynomials›
theory Univariate_PM
imports "HOL-Computational_Algebra.Polynomial" Polynomials.MPoly_PM
begin
subsection ‹Morphisms ‹pm_of_poly› and ‹poly_of_pm››
text ‹Many things in this section are copied from theory ‹Polynomials.MPoly_Type_Univariate›.›
lemma pm_of_poly_aux:
"{t. (poly.coeff p (lookup t x) when t ∈ .[{x}]) ≠ 0} =
Poly_Mapping.single x ` {d. poly.coeff p d ≠ 0}" (is "?M = _")
proof (intro subset_antisym subsetI)
fix t
assume "t ∈ ?M"
hence "⋀y. y ≠ x ⟹ Poly_Mapping.lookup t y = 0" by (fastforce simp: PPs_def in_keys_iff)
hence "t = Poly_Mapping.single x (lookup t x)"
using poly_mapping_eqI by (metis (full_types) lookup_single_eq lookup_single_not_eq)
then show "t ∈ (Poly_Mapping.single x) ` {d. poly.coeff p d ≠ 0}" using ‹t ∈ ?M› by auto
qed (auto split: if_splits simp: PPs_def)
lift_definition pm_of_poly :: "'x ⇒ 'a poly ⇒ ('x ⇒⇩0 nat) ⇒⇩0 'a::comm_monoid_add"
is "λx p t. (poly.coeff p (lookup t x)) when t ∈ .[{x}]"
proof -
fix x::'x and p::"'a poly"
show "finite {t. (poly.coeff p (lookup t x) when t ∈ .[{x}]) ≠ 0}" unfolding pm_of_poly_aux
using finite_surj[OF MOST_coeff_eq_0[unfolded eventually_cofinite]] by blast
qed
definition poly_of_pm :: "'x ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ 'a::comm_monoid_add poly"
where "poly_of_pm x p = Abs_poly (λd. lookup p (Poly_Mapping.single x d))"
lemma lookup_pm_of_poly_single [simp]:
"lookup (pm_of_poly x p) (Poly_Mapping.single x d) = poly.coeff p d"
by (simp add: pm_of_poly.rep_eq PPs_closed_single)
lemma keys_pm_of_poly: "keys (pm_of_poly x p) = Poly_Mapping.single x ` {d. poly.coeff p d ≠ 0}"
proof -
have "keys (pm_of_poly x p) = {t. (poly.coeff p (lookup t x) when t ∈ .[{x}]) ≠ 0}"
by (rule set_eqI) (simp add: pm_of_poly.rep_eq flip: lookup_not_eq_zero_eq_in_keys)
also have "… = Poly_Mapping.single x ` {d. poly.coeff p d ≠ 0}" by (fact pm_of_poly_aux)
finally show ?thesis .
qed
lemma coeff_poly_of_pm [simp]: "poly.coeff (poly_of_pm x p) k = lookup p (Poly_Mapping.single x k)"
proof -
have 0:"Poly_Mapping.single x ` {d. lookup p (Poly_Mapping.single x d) ≠ 0} ⊆ {d. lookup p d ≠ 0}"
by auto
have "∀⇩∞ k. lookup p (Poly_Mapping.single x 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 by (simp add: poly_of_pm_def Abs_poly_inverse)
qed
lemma pm_of_poly_of_pm:
assumes "p ∈ P[{x}]"
shows "pm_of_poly x (poly_of_pm x p) = p"
proof (rule poly_mapping_eqI)
fix t
from assms have "keys p ⊆ .[{x}]" by (rule PolysD)
show "lookup (pm_of_poly x (poly_of_pm x p)) t = lookup p t"
proof (simp add: pm_of_poly.rep_eq when_def, intro conjI impI)
assume "t ∈ .[{x}]"
hence "Poly_Mapping.single x (lookup t x) = t"
by (simp add: PPsD keys_subset_singleton_imp_monomial)
thus "lookup p (Poly_Mapping.single x (lookup t x)) = lookup p t" by simp
next
assume "t ∉ .[{x}]"
with assms PolysD have "t ∉ keys p" by blast
thus "lookup p t = 0" by (simp add: in_keys_iff)
qed
qed
lemma poly_of_pm_of_poly [simp]: "poly_of_pm x (pm_of_poly x p) = p"
by (simp add: poly_of_pm_def coeff_inverse)
lemma pm_of_poly_in_Polys: "pm_of_poly x p ∈ P[{x}]"
by (auto simp: keys_pm_of_poly PPs_closed_single intro!: PolysI)
lemma pm_of_poly_zero [simp]: "pm_of_poly x 0 = 0"
by (rule poly_mapping_eqI) (simp add: pm_of_poly.rep_eq)
lemma pm_of_poly_eq_zero_iff [iff]: "pm_of_poly x p = 0 ⟷ p = 0"
by (metis poly_of_pm_of_poly pm_of_poly_zero)
lemma pm_of_poly_monom: "pm_of_poly x (Polynomial.monom c d) = monomial c (Poly_Mapping.single x d)"
proof (rule poly_mapping_eqI)
fix t
show "lookup (pm_of_poly x (Polynomial.monom c d)) t = lookup (monomial c (monomial d x)) t"
proof (cases "t ∈ .[{x}]")
case True
thus ?thesis
by (auto simp: pm_of_poly.rep_eq lookup_single PPs_singleton when_def dest: monomial_inj)
next
case False
thus ?thesis by (auto simp add: pm_of_poly.rep_eq lookup_single PPs_singleton)
qed
qed
lemma pm_of_poly_plus: "pm_of_poly x (p + q) = pm_of_poly x p + pm_of_poly x q"
by (rule poly_mapping_eqI) (simp add: pm_of_poly.rep_eq lookup_add when_add_distrib)
lemma pm_of_poly_uminus [simp]: "pm_of_poly x (- p) = - pm_of_poly x p"
by (rule poly_mapping_eqI) (simp add: pm_of_poly.rep_eq when_distrib)
lemma pm_of_poly_minus: "pm_of_poly x (p - q) = pm_of_poly x p - pm_of_poly x q"
by (rule poly_mapping_eqI) (simp add: pm_of_poly.rep_eq lookup_minus when_diff_distrib)
lemma pm_of_poly_one [simp]: "pm_of_poly x 1 = 1"
by (simp add: pm_of_poly_monom flip: single_one monom_eq_1)
lemma pm_of_poly_pCons:
"pm_of_poly x (pCons c p) =
monomial c 0 + punit.monom_mult (1::_::monoid_mult) (Poly_Mapping.single x 1) (pm_of_poly x p)"
(is "?l = ?r")
proof (rule poly_mapping_eqI)
fix t
let ?x = "Poly_Mapping.single x (Suc 0)"
show "lookup ?l t = lookup ?r t"
proof (cases "?x adds t")
case True
have 1: "t - ?x ∈ .[{x}] ⟷ t ∈ .[{x}]"
proof
assume "t - ?x ∈ .[{x}]"
moreover have "?x ∈ .[{x}]" by (rule PPs_closed_single) simp
ultimately have "(t - ?x) + ?x ∈ .[{x}]" by (rule PPs_closed_plus)
with True show "t ∈ .[{x}]" by (simp add: adds_minus)
qed (rule PPs_closed_minus)
from True have "0 < lookup t x"
by (metis adds_minus lookup_add lookup_single_eq n_not_Suc_n neq0_conv plus_eq_zero_2)
moreover from this have "t ≠ 0" by auto
ultimately show ?thesis using True
by (simp add: pm_of_poly.rep_eq lookup_add lookup_single punit.lookup_monom_mult 1 coeff_pCons
lookup_minus split: nat.split)
next
case False
moreover have "t ∈ .[{x}] ⟷ t = 0"
proof
assume "t ∈ .[{x}]"
hence "keys t ⊆ {x}" by (rule PPsD)
show "t = 0"
proof (rule ccontr)
assume "t ≠ 0"
hence "keys t ≠ {}" by simp
then obtain y where "y ∈ keys t" by blast
with ‹keys t ⊆ {x}› have "y ∈ {x}" ..
hence "y = x" by simp
with ‹y ∈ keys t› have "Suc 0 ≤ lookup t x" by (simp add: in_keys_iff)
hence "?x adds t"
by (metis adds_poly_mappingI le0 le_funI lookup_single_eq lookup_single_not_eq)
with False show False ..
qed
qed (simp only: zero_in_PPs)
ultimately show ?thesis
by (simp add: pm_of_poly.rep_eq lookup_add lookup_single punit.lookup_monom_mult when_def)
qed
qed
lemma pm_of_poly_smult [simp]: "pm_of_poly x (Polynomial.smult c p) = c ⋅ pm_of_poly x p"
by (rule poly_mapping_eqI) (simp add: pm_of_poly.rep_eq when_distrib)
lemma pm_of_poly_times: "pm_of_poly x (p * q) = pm_of_poly x p * pm_of_poly x (q::_::ring_1 poly)"
proof (induct p)
case 0
show ?case by simp
next
case (pCons a p)
show ?case
by (simp add: pm_of_poly_plus pm_of_poly_pCons map_scale_eq_times pCons(2) algebra_simps
flip: times_monomial_left)
qed
lemma pm_of_poly_sum: "pm_of_poly x (sum f I) = (∑i∈I. pm_of_poly x (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: pm_of_poly_plus)
lemma pm_of_poly_prod: "pm_of_poly x (prod f I) = (∏i∈I. pm_of_poly x (f i :: _::ring_1 poly))"
by (induct I rule: infinite_finite_induct) (simp_all add: pm_of_poly_times)
lemma pm_of_poly_power [simp]: "pm_of_poly x (p ^ m) = pm_of_poly x (p::_::ring_1 poly) ^ m"
by (induct m) (simp_all add: pm_of_poly_times)
lemma poly_of_pm_zero [simp]: "poly_of_pm x 0 = 0"
by (metis poly_of_pm_of_poly pm_of_poly_zero)
lemma poly_of_pm_eq_zero_iff: "poly_of_pm x p = 0 ⟷ keys p ∩ .[{x}] = {}"
proof
assume eq: "poly_of_pm x p = 0"
{
fix t
assume "t ∈ .[{x}]"
then obtain d where "t = Poly_Mapping.single x d" unfolding PPs_singleton ..
moreover assume "t ∈ keys p"
ultimately have "0 ≠ lookup p (Poly_Mapping.single x d)" by (simp add: in_keys_iff)
also have "lookup p (Poly_Mapping.single x d) = Polynomial.coeff (poly_of_pm x p) d"
by simp
also have "… = 0" by (simp add: eq)
finally have False by blast
}
thus "keys p ∩ .[{x}] = {}" by blast
next
assume *: "keys p ∩ .[{x}] = {}"
{
fix d
have "Poly_Mapping.single x d ∈ .[{x}]" (is "?x ∈ _") by (rule PPs_closed_single) simp
with * have "?x ∉ keys p" by blast
hence "Polynomial.coeff (poly_of_pm x p) d = 0" by (simp add: in_keys_iff)
}
thus "poly_of_pm x p = 0" using leading_coeff_0_iff by blast
qed
lemma poly_of_pm_monomial:
"poly_of_pm x (monomial c t) = (Polynomial.monom c (lookup t x) when t ∈ .[{x}])"
proof (cases "t ∈ .[{x}]")
case True
moreover from this obtain d where "t = Poly_Mapping.single x d"
by (metis PPsD keys_subset_singleton_imp_monomial)
ultimately show ?thesis unfolding Polynomial.monom.abs_eq coeff_poly_of_pm
by (auto simp: poly_of_pm_def lookup_single when_def
dest!: monomial_inj intro!: arg_cong[where f=Abs_poly])
next
case False
moreover from this have "t ≠ monomial d x" for d by (auto simp: PPs_closed_single)
ultimately show ?thesis unfolding Polynomial.monom.abs_eq coeff_poly_of_pm
by (auto simp: poly_of_pm_def lookup_single when_def zero_poly.abs_eq)
qed
lemma poly_of_pm_plus: "poly_of_pm x (p + q) = poly_of_pm x p + poly_of_pm x q"
unfolding Polynomial.plus_poly.abs_eq coeff_poly_of_pm by (simp add: poly_of_pm_def lookup_add)
lemma poly_of_pm_uminus [simp]: "poly_of_pm x (- p) = - poly_of_pm x p"
unfolding Polynomial.uminus_poly.abs_eq coeff_poly_of_pm by (simp add: poly_of_pm_def)
lemma poly_of_pm_minus: "poly_of_pm x (p - q) = poly_of_pm x p - poly_of_pm x q"
unfolding Polynomial.minus_poly.abs_eq coeff_poly_of_pm by (simp add: poly_of_pm_def lookup_minus)
lemma poly_of_pm_one [simp]: "poly_of_pm x 1 = 1"
by (simp add: poly_of_pm_monomial zero_in_PPs flip: single_one monom_eq_1)
lemma poly_of_pm_times:
"poly_of_pm x (p * q) = poly_of_pm x p * poly_of_pm x (q::_ ⇒⇩0 'a::comm_semiring_1)"
proof -
have eq: "poly_of_pm x (monomial c t * q) = poly_of_pm x (monomial c t) * poly_of_pm x q"
if "c ≠ 0" for c t
proof (cases "t ∈ .[{x}]")
case True
then obtain d where t: "t = Poly_Mapping.single x d" unfolding PPs_singleton ..
have "poly_of_pm x (monomial c t) * poly_of_pm x q = Polynomial.monom c (lookup t x) * poly_of_pm x q"
by (simp add: True poly_of_pm_monomial)
also have "… = poly_of_pm x (monomial c t * q)" unfolding t
proof (induct d)
case 0
have "Polynomial.smult c (poly_of_pm x q) = poly_of_pm x (c ⋅ q)"
unfolding Polynomial.smult.abs_eq coeff_poly_of_pm by (simp add: poly_of_pm_def)
with that show ?case by (simp add: Polynomial.times_poly_def flip: map_scale_eq_times)
next
case (Suc d)
have 1: "Poly_Mapping.single x a adds Poly_Mapping.single x b ⟷ a ≤ b" for a b :: nat
by (metis adds_def deg_pm_mono deg_pm_single le_Suc_ex single_add)
have 2: "poly_of_pm x (punit.monom_mult 1 (Poly_Mapping.single x 1) r) = pCons 0 (poly_of_pm x r)"
for r :: "_ ⇒⇩0 'a" unfolding poly.coeff_inject[symmetric]
by (rule ext) (simp add: coeff_pCons punit.lookup_monom_mult adds_zero monomial_0_iff 1
flip: single_diff split: nat.split)
from Suc that have "Polynomial.monom c (lookup (monomial (Suc d) x) x) * poly_of_pm x q =
poly_of_pm x (punit.monom_mult 1 (Poly_Mapping.single x 1)
((monomial c (monomial d x)) * q))"
by (simp add: Polynomial.times_poly_def 2 del: One_nat_def)
also have "… = poly_of_pm x (monomial c (Poly_Mapping.single x (Suc d)) * q)"
by (simp add: ac_simps times_monomial_monomial flip: single_add times_monomial_left)
finally show ?case .
qed
finally show ?thesis by (rule sym)
next
case False
{
fix s
assume "s ∈ keys (monomial c t * q)"
also have "… ⊆ (+) t ` keys q" unfolding times_monomial_left
by (fact punit.keys_monom_mult_subset[simplified])
finally obtain u where s: "s = t + u" ..
assume "s ∈ .[{x}]"
hence "s - u ∈ .[{x}]" by (rule PPs_closed_minus)
hence "t ∈ .[{x}]" by (simp add: s)
with False have False ..
}
hence "poly_of_pm x (monomial c t * q) = 0" by (auto simp: poly_of_pm_eq_zero_iff)
with False show ?thesis by (simp add: poly_of_pm_monomial)
qed
show ?thesis
by (induct p rule: poly_mapping_plus_induct) (simp_all add: poly_of_pm_plus eq distrib_right)
qed
lemma poly_of_pm_sum: "poly_of_pm x (sum f I) = (∑i∈I. poly_of_pm x (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: poly_of_pm_plus)
lemma poly_of_pm_prod: "poly_of_pm x (prod f I) = (∏i∈I. poly_of_pm x (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: poly_of_pm_times)
lemma poly_of_pm_power [simp]: "poly_of_pm x (p ^ m) = poly_of_pm x p ^ m"
by (induct m) (simp_all add: poly_of_pm_times)
subsection ‹Evaluating Polynomials›
lemma poly_eq_poly_eval: "poly (poly_of_pm x p) a = poly_eval (λy. a when y = x) p"
proof (induction p rule: poly_mapping_plus_induct)
case 1
show ?case by simp
next
case (2 p c t)
show ?case
proof (cases "t ∈ .[{x}]")
case True
have "poly_eval (λy. a when y = x) (monomial c t) = c * (∏y∈keys t. (a when y = x) ^ lookup t y)"
by (simp only: poly_eval_monomial)
also from True have "(∏y∈keys t. (a when y = x) ^ lookup t y) = (∏y∈{x}. (a when y = x) ^ lookup t y)"
by (intro prod.mono_neutral_left ballI) (auto simp: in_keys_iff dest: PPsD)
also have "… = a ^ lookup t x" by simp
finally show ?thesis
by (simp add: poly_of_pm_plus poly_of_pm_monomial poly_monom poly_eval_plus True 2(3))
next
case False
have "poly_eval (λy. a when y = x) (monomial c t) = c * (∏y∈keys t. (a when y = x) ^ lookup t y)"
by (simp only: poly_eval_monomial)
also from finite_keys have "(∏y∈keys t. (a when y = x) ^ lookup t y) = 0"
proof (rule prod_zero)
from False obtain y where "y ∈ keys t" and "y ≠ x" by (auto simp: PPs_def)
from this(1) show "∃y∈keys t. (a when y = x) ^ lookup t y = 0"
proof
from ‹y ∈ keys t› have "0 < lookup t y" by (simp add: in_keys_iff)
with ‹y ≠ x› show "(a when y = x) ^ lookup t y = 0" by (simp add: zero_power)
qed
qed
finally show ?thesis
by (simp add: poly_of_pm_plus poly_of_pm_monomial poly_monom poly_eval_plus False 2(3))
qed
qed
corollary poly_eq_poly_eval':
assumes "p ∈ P[{x}]"
shows "poly (poly_of_pm x p) a = poly_eval (λ_. a) p"
unfolding poly_eq_poly_eval using refl
proof (rule poly_eval_cong)
fix y
assume "y ∈ indets p"
also from assms have "… ⊆ {x}" by (rule PolysD)
finally show "(a when y = x) = a" by simp
qed
lemma poly_eval_eq_poly: "poly_eval a (pm_of_poly x p) = poly p (a x)"
by (induct p)
(simp_all add: pm_of_poly_pCons poly_eval_plus poly_eval_times poly_eval_monomial
flip: times_monomial_left)
subsection ‹Morphisms ‹flat_pm_of_poly› and ‹poly_of_focus››
definition flat_pm_of_poly :: "'x ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) poly ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::semiring_1)"
where "flat_pm_of_poly x = flatten ∘ pm_of_poly x"
definition poly_of_focus :: "'x ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::comm_monoid_add) poly"
where "poly_of_focus x = poly_of_pm x ∘ focus {x}"
lemma flat_pm_of_poly_in_Polys:
assumes "range (poly.coeff p) ⊆ P[Y]"
shows "flat_pm_of_poly x p ∈ P[insert x Y]"
proof -
let ?p = "pm_of_poly x p"
from assms have "lookup ?p ` keys ?p ⊆ P[Y]" by (simp add: keys_pm_of_poly image_image) blast
with pm_of_poly_in_Polys have "flatten ?p ∈ P[{x} ∪ Y]" by (rule flatten_in_Polys)
thus ?thesis by (simp add: flat_pm_of_poly_def)
qed
corollary indets_flat_pm_of_poly_subset:
"indets (flat_pm_of_poly x p) ⊆ insert x (⋃ (indets ` range (poly.coeff p)))"
proof -
let ?p = "pm_of_poly x p"
let ?Y = "⋃ (indets ` range (poly.coeff p))"
have "range (poly.coeff p) ⊆ P[?Y]" by (auto intro: PolysI_alt)
hence "flat_pm_of_poly x p ∈ P[insert x ?Y]" by (rule flat_pm_of_poly_in_Polys)
thus ?thesis by (rule PolysD)
qed
lemma
shows flat_pm_of_poly_zero [simp]: "flat_pm_of_poly x 0 = 0"
and flat_pm_of_poly_monom: "flat_pm_of_poly x (Polynomial.monom c d) =
punit.monom_mult 1 (Poly_Mapping.single x d) c"
and flat_pm_of_poly_plus: "flat_pm_of_poly x (p + q) =
flat_pm_of_poly x p + flat_pm_of_poly x q"
and flat_pm_of_poly_one [simp]: "flat_pm_of_poly x 1 = 1"
and flat_pm_of_poly_sum: "flat_pm_of_poly x (sum f I) = (∑i∈I. flat_pm_of_poly x (f i))"
by (simp_all add: flat_pm_of_poly_def pm_of_poly_monom flatten_monomial pm_of_poly_plus
flatten_plus pm_of_poly_sum flatten_sum)
lemma
shows flat_pm_of_poly_uminus [simp]: "flat_pm_of_poly x (- p) = - flat_pm_of_poly x p"
and flat_pm_of_poly_minus: "flat_pm_of_poly x (p - q) =
flat_pm_of_poly x p - flat_pm_of_poly x (q::_::ring poly)"
by (simp_all add: flat_pm_of_poly_def pm_of_poly_minus flatten_minus)
lemma flat_pm_of_poly_pCons:
"flat_pm_of_poly x (pCons c p) =
c + punit.monom_mult 1 (Poly_Mapping.single x 1) (flat_pm_of_poly x (p::_::comm_semiring_1 poly))"
by (simp add: flat_pm_of_poly_def pm_of_poly_pCons flatten_plus flatten_monomial flatten_times
flip: times_monomial_left)
lemma flat_pm_of_poly_smult [simp]:
"flat_pm_of_poly x (Polynomial.smult c p) = c * flat_pm_of_poly x (p::_::comm_semiring_1 poly)"
by (simp add: flat_pm_of_poly_def map_scale_eq_times flatten_times flatten_monomial pm_of_poly_times)
lemma
shows flat_pm_of_poly_times: "flat_pm_of_poly x (p * q) = flat_pm_of_poly x p * flat_pm_of_poly x q"
and flat_pm_of_poly_prod: "flat_pm_of_poly x (prod f I) =
(∏i∈I. flat_pm_of_poly x (f i :: _::comm_ring_1 poly))"
and flat_pm_of_poly_power: "flat_pm_of_poly x (p ^ m) = flat_pm_of_poly x (p::_::comm_ring_1 poly) ^ m"
by (simp_all add: flat_pm_of_poly_def flatten_times pm_of_poly_times flatten_prod pm_of_poly_prod)
lemma coeff_poly_of_focus_subset_Polys:
assumes "p ∈ P[X]"
shows "range (poly.coeff (poly_of_focus x p)) ⊆ P[X - {x}]"
proof -
have "range (poly.coeff (poly_of_focus x p)) ⊆ range (lookup (focus {x} p))"
by (auto simp: poly_of_focus_def)
also from assms have "… ⊆ P[X - {x}]" by (rule focus_coeffs_subset_Polys')
finally show ?thesis .
qed
lemma
shows poly_of_focus_zero [simp]: "poly_of_focus x 0 = 0"
and poly_of_focus_uminus [simp]: "poly_of_focus x (- p) = - poly_of_focus x p"
and poly_of_focus_plus: "poly_of_focus x (p + q) = poly_of_focus x p + poly_of_focus x q"
and poly_of_focus_minus: "poly_of_focus x (p - q) = poly_of_focus x p - poly_of_focus x q"
and poly_of_focus_one [simp]: "poly_of_focus x 1 = 1"
and poly_of_focus_sum: "poly_of_focus x (sum f I) = (∑i∈I. poly_of_focus x (f i))"
by (simp_all add: poly_of_focus_def keys_focus poly_of_pm_plus focus_plus poly_of_pm_minus focus_minus
poly_of_pm_sum focus_sum)
lemma poly_of_focus_eq_zero_iff [iff]: "poly_of_focus x p = 0 ⟷ p = 0"
using focus_in_Polys[of "{x}" p]
by (auto simp: poly_of_focus_def poly_of_pm_eq_zero_iff Int_absorb2 dest: PolysD)
lemma poly_of_focus_monomial:
"poly_of_focus x (monomial c t) = Polynomial.monom (monomial c (except t {x})) (lookup t x)"
by (simp add: poly_of_focus_def focus_monomial poly_of_pm_monomial PPs_def keys_except lookup_except)
lemma
shows poly_of_focus_times: "poly_of_focus x (p * q) = poly_of_focus x p * poly_of_focus x q"
and poly_of_focus_prod: "poly_of_focus x (prod f I) =
(∏i∈I. poly_of_focus x (f i :: _ ⇒⇩0 _::comm_semiring_1))"
and poly_of_focus_power: "poly_of_focus x (p ^ m) = poly_of_focus x (p::_ ⇒⇩0 _::comm_semiring_1) ^ m"
by (simp_all add: poly_of_focus_def poly_of_pm_times focus_times poly_of_pm_prod focus_prod)
lemma flat_pm_of_poly_of_focus [simp]: "flat_pm_of_poly x (poly_of_focus x p) = p"
by (simp add: flat_pm_of_poly_def poly_of_focus_def pm_of_poly_of_pm focus_in_Polys)
lemma poly_of_focus_flat_pm_of_poly:
assumes "range (poly.coeff p) ⊆ P[- {x}]"
shows "poly_of_focus x (flat_pm_of_poly x p) = p"
proof -
from assms have "lookup (pm_of_poly x p) ` keys (pm_of_poly x p) ⊆ P[- {x}]"
by (simp add: keys_pm_of_poly image_image) blast
thus ?thesis by (simp add: flat_pm_of_poly_def poly_of_focus_def focus_flatten pm_of_poly_in_Polys)
qed
lemma flat_pm_of_poly_eq_zeroD:
assumes "flat_pm_of_poly x p = 0" and "range (poly.coeff p) ⊆ P[- {x}]"
shows "p = 0"
proof -
from assms(2) have "p = poly_of_focus x (flat_pm_of_poly x p)"
by (simp only: poly_of_focus_flat_pm_of_poly)
also have "… = 0" by (simp add: assms(1))
finally show ?thesis .
qed
lemma poly_poly_of_focus: "poly (poly_of_focus x p) a = poly_eval (λ_. a) (focus {x} p)"
by (simp add: poly_of_focus_def poly_eq_poly_eval' focus_in_Polys)
corollary poly_poly_of_focus_monomial:
"poly (poly_of_focus x p) (monomial 1 (Poly_Mapping.single x 1)) = (p::_ ⇒⇩0 _::comm_semiring_1)"
unfolding poly_poly_of_focus poly_eval_focus by (rule poly_subst_id) simp
end