# Theory Factor_Algebraic_Polynomial.Poly_Connection

```section ‹Resultants and Multivariate Polynomials›

subsection ‹Connecting Univariate and Multivariate Polynomials›

text ‹We define a conversion of multivariate polynomials into univariate polynomials
w.r.t.\ a fixed variable \$x\$ and multivariate polynomials as coefficients.›

theory Poly_Connection
imports
Polynomials.MPoly_Type_Univariate
Jordan_Normal_Form.Missing_Misc
Polynomial_Interpolation.Ring_Hom_Poly
Hermite_Lindemann.More_Multivariate_Polynomial_HLW
Polynomials.MPoly_Type_Class
begin

lemma mpoly_is_unitE:
fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} mpoly"
assumes "p dvd 1"
obtains c where "p = Const c" "c dvd 1"
proof -
obtain r where r: "p * r = 1"
using assms by auto
from r have [simp]: "p ≠ 0" "r ≠ 0"
by auto
have "0 = lead_monom (1 :: 'a mpoly)"
by simp
also have "1 = p * r"
using r by simp
finally have "lead_monom p = 0"
by simp
hence "vars p = {}"
hence *: "p = Const (lead_coeff p)"
by (auto simp: vars_empty_iff)

have "1 = lead_coeff (1 :: 'a mpoly)"
by simp
also have "1 = p * r"
using r by simp
finally have "lead_coeff p dvd 1"
using dvdI by blast
with * show ?thesis using that
by blast
qed

lemma Const_eq_Const_iff [simp]:
"Const c = Const c' ⟷ c = c'"

lemma is_unit_ConstI [intro]: "c dvd 1 ⟹ Const c dvd 1"
by (metis dvd_def mpoly_Const_1 mpoly_Const_mult)

lemma is_unit_Const_iff:
fixes c :: "'a :: {comm_semiring_1, semiring_no_zero_divisors}"
shows "Const c dvd 1 ⟷ c dvd 1"
proof
assume "Const c dvd 1"
thus "c dvd 1"
by (auto elim!: mpoly_is_unitE)
qed auto

lemma vars_emptyE: "vars p = {} ⟹ (⋀c. p = Const c ⟹ P) ⟹ P"
by (auto simp: vars_empty_iff)

lemma degree_geI:
assumes "MPoly_Type.coeff p m ≠ 0"
shows   "MPoly_Type.degree p i ≥ Poly_Mapping.lookup m i"
proof -
have "lookup m i ≤ Max (insert 0 ((λm. lookup m i) ` keys (mapping_of p)))"
proof (rule Max.coboundedI)
show "lookup m i ∈ insert 0 ((λm. lookup m i) ` keys (mapping_of p))"
using assms by (auto simp: coeff_keys)
qed auto
thus ?thesis unfolding MPoly_Type.degree_def by auto
qed

lemma monom_of_degree_exists:
assumes "p ≠ 0"
obtains m where "MPoly_Type.coeff p m ≠ 0" "Poly_Mapping.lookup m i = MPoly_Type.degree p i"
proof (cases "MPoly_Type.degree p i = 0")
case False
have "MPoly_Type.degree p i = Max (insert 0 ((λm. lookup m i) ` keys (mapping_of p)))"
also have "… ∈ insert 0 ((λm. lookup m i) ` keys (mapping_of p))"
by (rule Max_in) auto
finally show ?thesis
using False that by (auto simp: coeff_keys)
next
case [simp]: True
from assms obtain m where m: "MPoly_Type.coeff p m ≠ 0"
using coeff_all_0 by blast
show ?thesis using degree_geI[of p m i] m
by (intro that[of m]) auto
qed

lemma degree_leI:
assumes "⋀m. Poly_Mapping.lookup m i > n ⟹ MPoly_Type.coeff p m = 0"
shows   "MPoly_Type.degree p i ≤ n"
proof (cases "p = 0")
case False
obtain m where m: "MPoly_Type.coeff p m ≠ 0" "Poly_Mapping.lookup m i = MPoly_Type.degree p i"
using monom_of_degree_exists False by blast
with assms show ?thesis
by force
qed auto

lemma coeff_gt_degree_eq_0:
assumes "Poly_Mapping.lookup m i > MPoly_Type.degree p i"
shows   "MPoly_Type.coeff p m = 0"
using assms degree_geI leD by blast

lemma vars_altdef: "vars p = (⋃m∈{m. MPoly_Type.coeff p m ≠ 0}. keys m)"
unfolding vars_def
by (intro arg_cong[where f = "⋃"] image_cong refl) (simp flip: coeff_keys)

lemma degree_pos_iff: "MPoly_Type.degree p x > 0 ⟷ x ∈ vars p"
proof
assume "MPoly_Type.degree p x > 0"
hence "p ≠ 0" by auto
then obtain m where m: "lookup m x = MPoly_Type.degree p x" "MPoly_Type.coeff p m ≠ 0"
using monom_of_degree_exists[of p x] by metis
from m and ‹MPoly_Type.degree p x > 0› have "x ∈ keys m"
with m show "x ∈ vars p"
by (auto simp: vars_altdef)
next
assume "x ∈ vars p"
then obtain m where m: "x ∈ keys m" "MPoly_Type.coeff p m ≠ 0"
by (auto simp: vars_altdef)
have "0 < lookup m x"
using m by (auto simp: in_keys_iff)
also from m have "… ≤ MPoly_Type.degree p x"
by (intro degree_geI) auto
finally show "MPoly_Type.degree p x > 0" .
qed

lemma degree_eq_0_iff: "MPoly_Type.degree p x = 0 ⟷ x ∉ vars p"
using degree_pos_iff[of p x] by auto

lemma MPoly_Type_monom_zero[simp]: "MPoly_Type.monom m 0 = 0"

lemma vars_monom_keys': "vars (MPoly_Type.monom m c) = (if c = 0 then {} else keys m)"
by (cases "c = 0") (auto simp: vars_monom_keys)

lemma Const_eq_0_iff [simp]: "Const c = 0 ⟷ c = 0"

lemma monom_remove_key: "MPoly_Type.monom m (a :: 'a :: semiring_1) =
MPoly_Type.monom (remove_key x m) a * MPoly_Type.monom (Poly_Mapping.single x (lookup m x)) 1"
unfolding MPoly_Type.mult_monom
by (rule arg_cong2[of _ _ _ _ MPoly_Type.monom], auto simp: remove_key_sum)

lemma MPoly_Type_monom_0_iff[simp]: "MPoly_Type.monom m x = 0 ⟷ x = 0"
by (metis (full_types) MPoly_Type_monom_zero More_MPoly_Type.coeff_monom when_def)

lemma vars_signof[simp]: "vars (signof x) = {}"

lemma prod_mset_Const: "prod_mset (image_mset Const A) = Const (prod_mset A)"
by (induction A) (auto simp: mpoly_Const_mult)

lemma Const_eq_product_iff:
fixes c :: "'a :: idom"
assumes "c ≠ 0"
shows   "Const c = a * b ⟷ (∃a' b'. a = Const a' ∧ b = Const b' ∧ c = a' * b')"
proof
assume *: "Const c = a * b"
have "lead_monom (a * b) = 0"
by (auto simp flip: *)
by (subst (asm) lead_monom_mult) (use assms * in auto)
hence "vars a = {}" "vars b = {}"
then obtain a' b' where "a = Const a'" "b = Const b'"
by (auto simp: vars_empty_iff)
with * show "(∃a' b'. a = Const a' ∧ b = Const b' ∧ c = a' * b')"
by (auto simp flip: mpoly_Const_mult)
qed (auto simp: mpoly_Const_mult)

lemma irreducible_Const_iff [simp]:
"irreducible (Const (c :: 'a :: idom)) ⟷ irreducible c"
proof
assume *: "irreducible (Const c)"
show "irreducible c"
proof (rule irreducibleI)
fix a b assume "c = a * b"
hence "Const c = Const a * Const b"
with * have "Const a dvd 1 ∨ Const b dvd 1"
by blast
thus "a dvd 1 ∨ b dvd 1"
by (meson is_unit_Const_iff)
qed (use * in ‹auto simp: irreducible_def›)
next
assume *: "irreducible c"
have [simp]: "c ≠ 0"
using * by auto
show "irreducible (Const c)"
proof (rule irreducibleI)
fix a b assume "Const c = a * b"
then obtain a' b' where [simp]: "a = Const a'" "b = Const b'" and "c = a' * b'"
by (auto simp: Const_eq_product_iff)
hence "a' dvd 1 ∨ b' dvd 1"
using * by blast
thus "a dvd 1 ∨ b dvd 1"
by auto
qed (use * in ‹auto simp: irreducible_def is_unit_Const_iff›)
qed

lemma Const_dvd_Const_iff [simp]: "Const a dvd Const b ⟷ a dvd b"
proof
assume "a dvd b"
then obtain c where "b = a * c"
by auto
hence "Const b = Const a * Const c"
by (auto simp: mpoly_Const_mult)
thus "Const a dvd Const b"
by simp
next
assume "Const a dvd Const b"
then obtain p where p: "Const b = Const a * p"
by auto
have "MPoly_Type.coeff (Const b) 0 = MPoly_Type.coeff (Const a * p) 0"
using p by simp
also have "… = MPoly_Type.coeff (Const a) 0 * MPoly_Type.coeff p 0"
using mpoly_coeff_times_0 by blast
finally show "a dvd b"
qed

text ‹The lemmas above should be moved into the right theories. The part below is on the new
connection between multivariate polynomials and univariate polynomials.›

text ‹The imported theories only allow a conversion from one-variable mpoly's to poly and vice-versa.
However, we require a conversion from arbitrary mpoly's into poly's with mpolys as coefficients.›

(* converts a multi-variate polynomial into a univariate polynomial with multivariate coefficients *)
definition mpoly_to_mpoly_poly :: "nat ⇒ 'a :: comm_ring_1 mpoly ⇒ 'a mpoly poly" where
"mpoly_to_mpoly_poly x p = (∑m .
Polynomial.monom (MPoly_Type.monom (remove_key x m) (MPoly_Type.coeff p m)) (lookup m x))"

"mpoly_to_mpoly_poly x (p + q) = mpoly_to_mpoly_poly x p + mpoly_to_mpoly_poly x q"
by (rule Sum_any.distrib) auto

lemma mpoly_to_mpoly_poly_monom: "mpoly_to_mpoly_poly x (MPoly_Type.monom m a) = Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x)"
proof -
have "mpoly_to_mpoly_poly x (MPoly_Type.monom m a) =
(∑ m'. Polynomial.monom (MPoly_Type.monom (remove_key x m') a) (lookup m' x) when m' = m)"
unfolding mpoly_to_mpoly_poly_def
by (intro Sum_any.cong, auto simp: when_def More_MPoly_Type.coeff_monom)
also have "… = Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x)"
unfolding Sum_any_when_equal ..
finally show ?thesis .
qed

lemma remove_key_transfer [transfer_rule]:
"rel_fun (=) (rel_fun (pcr_poly_mapping (=) (=)) (pcr_poly_mapping (=) (=)))
(λk0 f k. f k when k ≠ k0) remove_key"
unfolding pcr_poly_mapping_def cr_poly_mapping_def OO_def
by (auto simp: rel_fun_def remove_key_lookup)

lemma remove_key_0 [simp]: "remove_key x 0 = 0"
by transfer auto

lemma remove_key_single' [simp]:
"x ≠ y ⟹ remove_key x (Poly_Mapping.single y n) = Poly_Mapping.single y n"
by transfer (auto simp: when_def fun_eq_iff)

lemma poly_coeff_Sum_any:
assumes "finite {x. f x ≠ 0}"
shows   "poly.coeff (Sum_any f) n = Sum_any (λx. poly.coeff (f x) n)"
proof -
have "Sum_any f = (∑x | f x ≠ 0. f x)"
by (rule Sum_any.expand_set)
also have "poly.coeff … n = (∑x | f x ≠ 0. poly.coeff (f x) n)"
also have "… = Sum_any (λx. poly.coeff (f x) n)"
by (rule Sum_any.expand_superset [symmetric]) (use assms in auto)
finally show ?thesis .
qed

lemma coeff_coeff_mpoly_to_mpoly_poly:
"MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) n) m =
(MPoly_Type.coeff p (m + Poly_Mapping.single x n) when lookup m x = 0)"
proof -
have "MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) n) m =
MPoly_Type.coeff (∑a. MPoly_Type.monom (remove_key x a) (MPoly_Type.coeff p a) when lookup a x = n) m"
unfolding mpoly_to_mpoly_poly_def by (subst poly_coeff_Sum_any) (auto simp: when_def)
also have "… = (∑xa. MPoly_Type.coeff (MPoly_Type.monom (remove_key x xa) (MPoly_Type.coeff p xa)) m when lookup xa x = n)"
by (subst coeff_Sum_any, force) (auto simp: when_def intro!: Sum_any.cong)
also have "… = (∑a. MPoly_Type.coeff p a when lookup a x = n ∧ m = remove_key x a)"
by (intro Sum_any.cong) (simp add: More_MPoly_Type.coeff_monom when_def)
also have "(λa. lookup a x = n ∧ m = remove_key x a) =
(λa. lookup m x = 0 ∧ a = m + Poly_Mapping.single x n)"
by (rule ext, transfer) (auto simp: fun_eq_iff when_def)
also have "(∑a. MPoly_Type.coeff p a when … a) =
(∑a. MPoly_Type.coeff p a when lookup m x = 0 when a = m + Poly_Mapping.single x n)"
by (intro Sum_any.cong) (auto simp: when_def)
also have "… = (MPoly_Type.coeff p (m + Poly_Mapping.single x n) when lookup m x = 0)"
by (rule Sum_any_when_equal)
finally show ?thesis .
qed

lemma mpoly_to_mpoly_poly_Const [simp]:
"mpoly_to_mpoly_poly x (Const c) = [:Const c:]"
proof -
have "mpoly_to_mpoly_poly x (Const c) =
(∑m. Polynomial.monom (MPoly_Type.monom (remove_key x m)
(MPoly_Type.coeff (Const c) m)) (lookup m x) when m = 0)"
unfolding mpoly_to_mpoly_poly_def
by (intro Sum_any.cong) (auto simp: when_def mpoly_coeff_Const)
also have "… = [:Const c:]"
by (subst Sum_any_when_equal)
(auto simp: mpoly_coeff_Const monom_altdef simp flip: Const_conv_monom)
finally show ?thesis .
qed

lemma mpoly_to_mpoly_poly_Var:
"mpoly_to_mpoly_poly x (Var y) = (if x = y then [:0, 1:] else [:Var y:])"
proof -
have "mpoly_to_mpoly_poly x (Var y) =
(∑a. Polynomial.monom (MPoly_Type.monom (remove_key x a) 1) (lookup a x)
when a = Poly_Mapping.single y 1)"
unfolding mpoly_to_mpoly_poly_def by (intro Sum_any.cong) (auto simp: when_def coeff_Var)
also have "… = (if x = y then [:0, 1:] else [:Var y:])"
by (auto simp: Polynomial.monom_altdef lookup_single Var_altdef)
finally show ?thesis .
qed

lemma mpoly_to_mpoly_poly_Var_this [simp]:
"mpoly_to_mpoly_poly x (Var x) = [:0, 1:]"
"x ≠ y ⟹ mpoly_to_mpoly_poly x (Var y) = [:Var y:]"

lemma mpoly_to_mpoly_poly_uminus [simp]:
"mpoly_to_mpoly_poly x (-p) = -mpoly_to_mpoly_poly x p"
unfolding mpoly_to_mpoly_poly_def
by (auto simp: monom_uminus Sum_any_uminus simp flip: minus_monom)

lemma mpoly_to_mpoly_poly_diff [simp]:
"mpoly_to_mpoly_poly x (p - q) = mpoly_to_mpoly_poly x p - mpoly_to_mpoly_poly x q"

lemma mpoly_to_mpoly_poly_0 [simp]:
"mpoly_to_mpoly_poly x 0 = 0"
unfolding mpoly_Const_0 [symmetric] mpoly_to_mpoly_poly_Const by simp

lemma mpoly_to_mpoly_poly_1 [simp]:
"mpoly_to_mpoly_poly x 1 = 1"
unfolding mpoly_Const_1 [symmetric] mpoly_to_mpoly_poly_Const by simp

lemma mpoly_to_mpoly_poly_of_nat [simp]:
"mpoly_to_mpoly_poly x (of_nat n) = of_nat n"
unfolding of_nat_mpoly_eq mpoly_to_mpoly_poly_Const of_nat_poly ..

lemma mpoly_to_mpoly_poly_of_int [simp]:
"mpoly_to_mpoly_poly x (of_int n) = of_int n"
unfolding of_nat_mpoly_eq mpoly_to_mpoly_poly_Const of_nat_poly by (cases n) auto

lemma mpoly_to_mpoly_poly_numeral [simp]:
"mpoly_to_mpoly_poly x (numeral n) = numeral n"
using mpoly_to_mpoly_poly_of_nat[of x "numeral n"] by (simp del: mpoly_to_mpoly_poly_of_nat)

lemma coeff_monom_mult':
"MPoly_Type.coeff (MPoly_Type.monom m a * q) m' =
(a * MPoly_Type.coeff q (m' - m) when lookup m' ≥ lookup m)"
proof (cases "lookup m' ≥ lookup m")
case True
have "a * MPoly_Type.coeff q (m' - m) = MPoly_Type.coeff (MPoly_Type.monom m a * q) (m + (m' - m))"
by (rule More_MPoly_Type.coeff_monom_mult [symmetric])
also have "m + (m' - m) = m'"
using True by transfer (auto simp: le_fun_def)
finally show ?thesis
using True by (simp add: when_def)
next
case False
have "MPoly_Type.coeff (MPoly_Type.monom m a * q) m' =
(∑m1. a * (∑m2. MPoly_Type.coeff q m2 when m' = m1 + m2) when m1 = m)"
unfolding coeff_mpoly_times prod_fun_def
by (intro Sum_any.cong) (auto simp: More_MPoly_Type.coeff_monom when_def)
also have "… = a * (∑m2. MPoly_Type.coeff q m2 when m' = m + m2)"
by (subst Sum_any_when_equal) auto
also have "(λm2. m' = m + m2) = (λm2. False)"
by (rule ext) (use False in ‹transfer, auto simp: le_fun_def›)
finally show ?thesis
using False by simp
qed

lemma mpoly_to_mpoly_poly_mult_monom:
"mpoly_to_mpoly_poly x (MPoly_Type.monom m a * q) =
Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x) * mpoly_to_mpoly_poly x q"
(is "?lhs = ?rhs")
proof (rule poly_eqI, rule mpoly_eqI)
fix n :: nat and mon :: "nat ⇒⇩0 nat"
have "MPoly_Type.coeff (poly.coeff ?lhs n) mon =
(a * MPoly_Type.coeff q (mon + Poly_Mapping.single x n - m)
when lookup m ≤ lookup (mon + Poly_Mapping.single x n) ∧ lookup mon x = 0)"
by (simp add: coeff_coeff_mpoly_to_mpoly_poly coeff_monom_mult' when_def)
have "MPoly_Type.coeff (poly.coeff ?rhs n) mon =
(a * MPoly_Type.coeff q (mon - remove_key x m + Poly_Mapping.single x (n - lookup m x))
when lookup (remove_key x m) ≤ lookup mon ∧ lookup m x ≤ n ∧ lookup mon x = 0)"
by (simp add: coeff_coeff_mpoly_to_mpoly_poly coeff_monom_mult' lookup_minus_fun
remove_key_lookup Missing_Polynomial.coeff_monom_mult when_def)
also have "lookup (remove_key x m) ≤ lookup mon ∧ lookup m x ≤ n ∧ lookup mon x = 0 ⟷
lookup m ≤ lookup (mon + Poly_Mapping.single x n) ∧ lookup mon x = 0" (is "_ = ?P")
by transfer (auto simp: when_def le_fun_def)
also have "mon - remove_key x m + Poly_Mapping.single x (n - lookup m x) = mon + Poly_Mapping.single x n - m" if ?P
using that by transfer (auto simp: fun_eq_iff when_def)
hence "(a * MPoly_Type.coeff q (mon - remove_key x m + Poly_Mapping.single x (n - lookup m x)) when ?P) =
(a * MPoly_Type.coeff q … when ?P)"
by (intro when_cong) auto
also have "… = MPoly_Type.coeff (poly.coeff ?lhs n) mon"
by (simp add: coeff_coeff_mpoly_to_mpoly_poly coeff_monom_mult' when_def)
finally show "MPoly_Type.coeff (poly.coeff ?lhs n) mon = MPoly_Type.coeff (poly.coeff ?rhs n) mon" ..
qed

lemma mpoly_to_mpoly_poly_mult [simp]:
"mpoly_to_mpoly_poly x (p * q) = mpoly_to_mpoly_poly x p * mpoly_to_mpoly_poly x q"
by (induction p arbitrary: q rule: mpoly_induct)

lemma coeff_mpoly_to_mpoly_poly:
"Polynomial.coeff (mpoly_to_mpoly_poly x p) n =
Sum_any (λm. MPoly_Type.monom (remove_key x m) (MPoly_Type.coeff p m) when Poly_Mapping.lookup m x = n)"
unfolding mpoly_to_mpoly_poly_def by (subst poly_coeff_Sum_any) (auto simp: when_def)

lemma mpoly_coeff_to_mpoly_poly_coeff:
"MPoly_Type.coeff p m = MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) (lookup m x)) (remove_key x m)"
proof -
have "MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) (lookup m x)) (remove_key x m) =
(∑xa. MPoly_Type.coeff (MPoly_Type.monom (remove_key x xa) (MPoly_Type.coeff p xa) when
lookup xa x = lookup m x) (remove_key x m))"
by (subst coeff_mpoly_to_mpoly_poly, subst coeff_Sum_any) auto
also have "… = (∑xa. MPoly_Type.coeff (MPoly_Type.monom (remove_key x xa) (MPoly_Type.coeff p xa)) (remove_key x m)
when lookup xa x = lookup m x)"
by (intro Sum_any.cong) (auto simp: when_def)
also have "… = (∑xa. MPoly_Type.coeff p xa when remove_key x m = remove_key x xa ∧ lookup xa x = lookup m x)"
by (intro Sum_any.cong) (auto simp: More_MPoly_Type.coeff_monom when_def)
also have "(λxa. remove_key x m = remove_key x xa ∧ lookup xa x = lookup m x) = (λxa. xa = m)"
using remove_key_sum by metis
also have "(∑xa. MPoly_Type.coeff p xa when xa = m) = MPoly_Type.coeff p m"
by simp
finally show ?thesis ..
qed

lemma degree_mpoly_to_mpoly_poly [simp]:
"Polynomial.degree (mpoly_to_mpoly_poly x p) = MPoly_Type.degree p x"
proof (rule antisym)
show "Polynomial.degree (mpoly_to_mpoly_poly x p) ≤ MPoly_Type.degree p x"
proof (intro Polynomial.degree_le allI impI)
fix i assume i: "i > MPoly_Type.degree p x"
have "poly.coeff (mpoly_to_mpoly_poly x p) i =
(∑m. 0 when lookup m x = i)"
unfolding coeff_mpoly_to_mpoly_poly using i
by (intro Sum_any.cong when_cong refl) (auto simp: coeff_gt_degree_eq_0)
also have "… = 0"
by simp
finally show "poly.coeff (mpoly_to_mpoly_poly x p) i = 0" .
qed
next
show "Polynomial.degree (mpoly_to_mpoly_poly x p) ≥ MPoly_Type.degree p x"
proof (cases "p = 0")
case False
then obtain m where m: "MPoly_Type.coeff p m ≠ 0" "lookup m x = MPoly_Type.degree p x"
using monom_of_degree_exists by blast
show "Polynomial.degree (mpoly_to_mpoly_poly x p) ≥ MPoly_Type.degree p x"
proof (rule Polynomial.le_degree)
have "0 ≠ MPoly_Type.coeff p m"
using m by auto
also have "MPoly_Type.coeff p m = MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) (lookup m x)) (remove_key x m)"
by (rule mpoly_coeff_to_mpoly_poly_coeff)
finally show "poly.coeff (mpoly_to_mpoly_poly x p) (MPoly_Type.degree p x) ≠ 0"
using m by auto
qed
qed auto
qed

text ‹The upcoming lemma is similar to @{thm reduce_nested_mpoly_extract_var}.›
lemma poly_mpoly_to_mpoly_poly:
"poly (mpoly_to_mpoly_poly x p) (Var x) = p"
proof (induct p rule: mpoly_induct)
case (monom m a)
show ?case unfolding mpoly_to_mpoly_poly_monom poly_monom
by (transfer, simp add: Var⇩0_power mult_single remove_key_sum)
next
case (sum p1 p2 m a)
qed

lemma mpoly_to_mpoly_poly_eq_iff [simp]:
"mpoly_to_mpoly_poly x p = mpoly_to_mpoly_poly x q ⟷ p = q"
proof
assume "mpoly_to_mpoly_poly x p = mpoly_to_mpoly_poly x q"
hence "poly (mpoly_to_mpoly_poly x p) (Var x) =
poly (mpoly_to_mpoly_poly x q) (Var x)"
by simp
thus "p = q"
by (auto simp: poly_mpoly_to_mpoly_poly)
qed auto

text ‹Evaluation, i.e., insertion of concrete values is identical›
lemma insertion_mpoly_to_mpoly_poly: assumes "⋀ y. y ≠ x ⟹ β y = α y"
shows "poly (map_poly (insertion β) (mpoly_to_mpoly_poly x p)) (α x) = insertion α p"
proof (induct p rule: mpoly_induct)
case (monom m a)
let ?rkm = "remove_key x m"
have to_alpha: "insertion β (MPoly_Type.monom ?rkm a) = insertion α (MPoly_Type.monom ?rkm a)"
by (rule insertion_irrelevant_vars, rule assms, insert vars_monom_subset[of ?rkm a], auto simp: remove_key_keys[symmetric])
have main: "insertion α (MPoly_Type.monom ?rkm a) * α x ^ lookup m x = insertion α (MPoly_Type.monom m a)"
unfolding monom_remove_key[of m a x] insertion_mult
by (metis insertion_single mult.left_neutral)
show ?case using main to_alpha
by (simp add: mpoly_to_mpoly_poly_monom map_poly_monom poly_monom)
next
case (sum p1 p2 m a)
qed

lemma mpoly_to_mpoly_poly_dvd_iff [simp]:
"mpoly_to_mpoly_poly x p dvd mpoly_to_mpoly_poly x q ⟷ p dvd q"
proof
assume "mpoly_to_mpoly_poly x p dvd mpoly_to_mpoly_poly x q"
hence "poly (mpoly_to_mpoly_poly x p) (Var x) dvd poly (mpoly_to_mpoly_poly x q) (Var x)"
by (intro poly_hom.hom_dvd)
thus "p dvd q"
qed auto

lemma vars_coeff_mpoly_to_mpoly_poly: "vars (poly.coeff (mpoly_to_mpoly_poly x p) i) ⊆ vars p - {x}"
unfolding mpoly_to_mpoly_poly_def Sum_any.expand_set Polynomial.coeff_sum More_MPoly_Type.coeff_monom
apply (rule order.trans[OF vars_setsum], force)
apply (rule UN_least, simp)
apply (intro impI order.trans[OF vars_monom_subset])
by (simp add: remove_key_keys[symmetric] Diff_mono SUP_upper2 coeff_keys vars_def)

locale transfer_mpoly_to_mpoly_poly =
fixes x :: nat
begin

definition R :: "'a :: comm_ring_1 mpoly poly ⇒ 'a mpoly ⇒ bool" where
"R p p' ⟷ p = mpoly_to_mpoly_poly x p'"

context
includes lifting_syntax
begin

lemma transfer_0 [transfer_rule]: "R 0 0"
and transfer_1 [transfer_rule]: "R 1 1"
and transfer_Const [transfer_rule]: "R [:Const c:] (Const c)"
and transfer_uminus [transfer_rule]: "(R ===> R) uminus uminus"
and transfer_of_nat [transfer_rule]: "((=) ===> R) of_nat of_nat"
and transfer_of_int [transfer_rule]: "((=) ===> R) of_nat of_nat"
and transfer_numeral [transfer_rule]: "((=) ===> R) of_nat of_nat"
and transfer_add [transfer_rule]: "(R ===> R ===> R) (+) (+)"
and transfer_diff [transfer_rule]: "(R ===> R ===> R) (+) (+)"
and transfer_mult [transfer_rule]: "(R ===> R ===> R) (*) (*)"
and transfer_dvd [transfer_rule]: "(R ===> R ===> (=)) (dvd) (dvd)"
and transfer_monom [transfer_rule]:
"((=) ===> (=) ===> R)
(λm a. Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x))
MPoly_Type.monom"
and transfer_coeff [transfer_rule]:
"(R ===> (=) ===> (=))
(λp m. MPoly_Type.coeff (poly.coeff p (lookup m x)) (remove_key x m))
MPoly_Type.coeff"
and transfer_degree [transfer_rule]:
"(R ===> (=)) Polynomial.degree (λp. MPoly_Type.degree p x)"
unfolding R_def
by (auto simp: rel_fun_def mpoly_to_mpoly_poly_monom
simp flip: mpoly_coeff_to_mpoly_poly_coeff)

lemma transfer_vars [transfer_rule]:
assumes [transfer_rule]: "R p p'"
shows   "(⋃i. vars (poly.coeff p i)) ∪ (if Polynomial.degree p = 0 then {} else {x}) = vars p'"
(is "?A ∪ ?B = _")
proof (intro equalityI)
have "vars p' = vars (poly p (Var x))"
using assms by (simp add: R_def poly_mpoly_to_mpoly_poly)
also have "poly p (Var x) = (∑i≤Polynomial.degree p. poly.coeff p i * Var x ^ i)"
unfolding poly_altdef ..
also have "vars … ⊆ (⋃i. vars (poly.coeff p i) ∪ (if Polynomial.degree p = 0 then {} else {x}))"
proof (intro order.trans[OF vars_sum] UN_mono order.trans[OF vars_mult] Un_mono)
fix i :: nat
assume i: "i ∈ {..Polynomial.degree p}"
show "vars (Var x ^ i) ⊆ (if Polynomial.degree p = 0 then {} else {x})"
proof (cases "Polynomial.degree p = 0")
case False
thus ?thesis
by (intro order.trans[OF vars_power]) (auto simp: vars_Var)
qed (use i in auto)
qed auto
finally show "vars p' ⊆ ?A ∪ ?B" by blast
next
have "?A ⊆ vars p'"
using assms vars_coeff_mpoly_to_mpoly_poly by (auto simp: R_def)
moreover have "?B ⊆ vars p'"
using assms by (auto simp: R_def degree_pos_iff)
ultimately show "?A ∪ ?B ⊆ vars p'"
by blast
qed

lemma right_total [transfer_rule]: "right_total R"
unfolding right_total_def
proof safe
fix p' :: "'a mpoly"
show "∃p. R p p'"
by (rule exI[of _ "mpoly_to_mpoly_poly x p'"]) (auto simp: R_def)
qed

lemma bi_unique [transfer_rule]: "bi_unique R"
unfolding bi_unique_def by (auto simp: R_def)

end

end

lemma mpoly_degree_mult_eq:
fixes p q :: "'a :: idom mpoly"
assumes "p ≠ 0" "q ≠ 0"
shows   "MPoly_Type.degree (p * q) x = MPoly_Type.degree p x + MPoly_Type.degree q x"
proof -
interpret transfer_mpoly_to_mpoly_poly x .
define deg :: "'a mpoly ⇒ nat" where "deg = (λp. MPoly_Type.degree p x)"
have [transfer_rule]: "rel_fun R (=) Polynomial.degree deg"
using transfer_degree unfolding deg_def .

have "deg (p * q) = deg p + deg q"
using assms unfolding deg_def [symmetric]
thus ?thesis
qed

text ‹Converts a multi-variate polynomial into a univariate polynomial via inserting values for all but one variable›
definition partial_insertion :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a :: comm_ring_1 mpoly ⇒ 'a poly" where
"partial_insertion α x p = map_poly (insertion α) (mpoly_to_mpoly_poly x p)"

lemma comm_ring_hom_insertion: "comm_ring_hom (insertion α)"
by (unfold_locales, auto simp: insertion_add insertion_mult)

lemma partial_insertion_add: "partial_insertion α x (p + q) = partial_insertion α x p + partial_insertion α x q"
proof -
interpret i: comm_ring_hom "insertion α" by (rule comm_ring_hom_insertion)
show ?thesis unfolding partial_insertion_def mpoly_to_mpoly_poly_add hom_distribs ..
qed

lemma partial_insertion_monom: "partial_insertion α x (MPoly_Type.monom m a) = Polynomial.monom (insertion α (MPoly_Type.monom (remove_key x m) a)) (lookup m x)"
unfolding partial_insertion_def mpoly_to_mpoly_poly_monom
by (subst map_poly_monom, auto)

text ‹Partial insertion + insertion of last value is identical to (full) insertion›
lemma insertion_partial_insertion: assumes "⋀ y. y ≠ x ⟹ β y = α y"
shows "poly (partial_insertion β x p) (α x) = insertion α p"
proof (induct p rule: mpoly_induct)
case (monom m a)
let ?rkm = "remove_key x m"
have to_alpha: "insertion β (MPoly_Type.monom ?rkm a) = insertion α (MPoly_Type.monom ?rkm a)"
by (rule insertion_irrelevant_vars, rule assms, insert vars_monom_subset[of ?rkm a], auto simp: remove_key_keys[symmetric])
have main: "insertion α (MPoly_Type.monom ?rkm a) * α x ^ lookup m x = insertion α (MPoly_Type.monom m a)"
unfolding monom_remove_key[of m a x] insertion_mult
by (metis insertion_single mult.left_neutral)
show ?case using main to_alpha by (simp add: partial_insertion_monom poly_monom)
next
case (sum p1 p2 m a)
qed

lemma insertion_coeff_mpoly_to_mpoly_poly[simp]:
"insertion α (coeff (mpoly_to_mpoly_poly x p) k) = coeff (partial_insertion α x p) k"
unfolding partial_insertion_def
by (subst coeff_map_poly, auto)

lemma degree_map_poly_Const: "degree (map_poly (Const :: 'a :: semiring_0 ⇒ _) f) = degree f"
by (rule degree_map_poly, auto)

lemma degree_partial_insertion_le_mpoly: "degree (partial_insertion α x p) ≤ degree (mpoly_to_mpoly_poly x p)"
unfolding partial_insertion_def by (rule degree_map_poly_le)

end```