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
  also have "lead_monom (p * r) = lead_monom p + lead_monom r"
    by (intro lead_monom_mult) auto
  finally have "lead_monom p = 0"
    by simp
  hence "vars p = {}"
    by (simp add: lead_monom_eq_0_iff)
  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
  also have "lead_coeff (p * r) = lead_coeff p * lead_coeff r"
    by (intro lead_coeff_mult) auto
  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'"
  by (metis lead_coeff_Const)

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)))"
    by (simp add: MPoly_Type.degree_def)
  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"
    by (simp add: in_keys_iff)
  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"
  by (simp add: More_MPoly_Type.coeff_monom coeff_all_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"
  by (metis lead_coeff_Const mpoly_Const_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) = {}" 
  by (simp add: sign_def)

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: *)
  hence "lead_monom a = 0 ∧ lead_monom b = 0"
    by (subst (asm) lead_monom_mult) (use assms * in auto)
  hence "vars a = {}" "vars b = {}"
    by (auto simp: lead_monom_eq_0_iff)
  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"
      by (simp add: mpoly_Const_mult)
    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"
    by (simp add: mpoly_coeff_Const)
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))" 

lemma mpoly_to_mpoly_poly_add [simp]:
  "mpoly_to_mpoly_poly x (p + q) = mpoly_to_mpoly_poly x p + mpoly_to_mpoly_poly x q" 
  unfolding mpoly_to_mpoly_poly_def  More_MPoly_Type.coeff_add[symmetric]  MPoly_Type.monom_add add_monom[symmetric]
  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)"
    by (simp add: Polynomial.coeff_sum)
  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:]"
  by (simp_all add: mpoly_to_mpoly_poly_Var)

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"
  by (subst diff_conv_add_uminus, subst mpoly_to_mpoly_poly_add) auto

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)
     (simp_all add: mpoly_to_mpoly_poly_monom mpoly_to_mpoly_poly_mult_monom ring_distribs)

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)
  then show ?case by (simp add: mpoly_to_mpoly_poly_add)
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)
  then show ?case by (simp add: mpoly_to_mpoly_poly_add insertion_add map_poly_add) 
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"
    by (simp add: poly_mpoly_to_mpoly_poly)
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]
    by transfer (simp add: degree_mult_eq)
  thus ?thesis
    by (simp add: deg_def)
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)
  then show ?case by (simp add: partial_insertion_add insertion_add map_poly_add) 
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