Session Algebraic_Numbers

Theory Algebraic_Numbers_Prelim

(*
    Author:      René Thiemann
                 Sebastiaan Joosten
                 Akihisa Yamada
    License:     BSD
*)
section ‹Algebraic Numbers -- Excluding Addition and Multiplication›

text ‹This theory contains basic definition and results on algebraic numbers, namely that
  algebraic numbers are closed under negation, inversion, $n$-th roots, and
  that every rational number is algebraic. For all of these closure properties, corresponding
  polynomial witnesses are available.

  Moreover, this theory contains the uniqueness result,
  that for every algebraic number there is exactly one content-free irreducible polynomial with
  positive leading coefficient for it.
  This result is stronger than similar ones which you find in many textbooks.
  The reason is that here we do not require a least degree construction.

  This is essential, since given some content-free irreducible polynomial for x,
  how should we check whether the degree is optimal. In the formalized result, this is
  not required. The result is proven via GCDs, and that the GCD does not change
  when executed on the rational numbers or on the reals or complex numbers, and that
  the GCD of a rational polynomial can be expressed via the GCD of integer polynomials.›

text ‹Many results are taken from the textbook \cite[pages 317ff]{AlgNumbers}.›

theory Algebraic_Numbers_Prelim
imports
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
  Polynomial_Interpolation.Newton_Interpolation (* for lemma smult_1 *)
  Polynomial_Factorization.Gauss_Lemma
  Berlekamp_Zassenhaus.Unique_Factorization_Poly
  Polynomial_Factorization.Square_Free_Factorization
begin

lemma primitive_imp_unit_iff:
  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
  assumes pr: "primitive p"
  shows "p dvd 1  degree p = 0"
proof
  assume "degree p = 0"
  from degree0_coeffs[OF this] obtain p0 where p: "p = [:p0:]" by auto
  then have "c  set (coeffs p). p0 dvd c" by (simp add: cCons_def)
  with pr have "p0 dvd 1" by (auto dest: primitiveD)
  with p show "p dvd 1" by auto
next
  assume "p dvd 1"
  then show "degree p = 0" by (auto simp: poly_dvd_1)
qed

lemma dvd_all_coeffs_imp_dvd:
  assumes "a  set (coeffs p). c dvd a" shows "[:c:] dvd p"
proof (insert assms, induct p)
  case 0
  then show ?case by simp
next
  case (pCons a p)
  have "pCons a p = [:a:] + pCons 0 p" by simp
  also have "[:c:] dvd ..."
  proof (rule dvd_add)
    from pCons show "[:c:] dvd [:a:]" by (auto simp: cCons_def)
    from pCons have "[:c:] dvd p" by auto
    from Rings.dvd_mult[OF this]
    show "[:c:] dvd pCons 0 p" by (subst pCons_0_as_mult)
  qed
  finally show ?case.
qed

lemma irreducible_content:
  fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  assumes "irreducible p" shows "degree p = 0  primitive p"
proof(rule ccontr)
  assume not: "¬?thesis"
  then obtain c where c1: "¬c dvd 1" and "a  set (coeffs p). c dvd a" by (auto elim: not_primitiveE)
  from dvd_all_coeffs_imp_dvd[OF this(2)]
  obtain r where p: "p = r * [:c:]" by (elim dvdE, auto)
  from irreducibleD[OF assms this] have "r dvd 1  [:c:] dvd 1" by auto
  with c1 have "r dvd 1" unfolding const_poly_dvd_1 by auto
  then have "degree r = 0" unfolding poly_dvd_1 by auto
  with p have "degree p = 0" by auto
  with not show False by auto
qed

(* TODO: move *)
lemma linear_irreducible_field:
  fixes p :: "'a :: field poly"
  assumes deg: "degree p = 1" shows "irreducible p"
proof (intro irreducibleI)
  from deg show p0: "p  0" by auto
  from deg show "¬ p dvd 1" by (auto simp: poly_dvd_1)
  fix a b assume p: "p = a * b"
  with p0 have a0: "a  0" and b0: "b  0" by auto
  from degree_mult_eq[OF this, folded p] assms
  consider "degree a = 1" "degree b = 0" | "degree a = 0" "degree b = 1" by force
  then show "a dvd 1  b dvd 1"
    by (cases; insert a0 b0, auto simp: primitive_imp_unit_iff)
qed

(* TODO: move *)
lemma linear_irreducible_int:
  fixes p :: "int poly"
  assumes deg: "degree p = 1" and cp: "content p dvd 1"
  shows "irreducible p"
proof (intro irreducibleI)
  from deg show p0: "p  0" by auto
  from deg show "¬ p dvd 1" by (auto simp: poly_dvd_1)
  fix a b assume p: "p = a * b"
  note * = cp[unfolded p is_unit_content_iff, unfolded content_mult]
  have a1: "content a dvd 1" and b1: "content b dvd 1"
    using content_ge_0_int[of a] pos_zmult_eq_1_iff_lemma[OF *] * by (auto simp: abs_mult)
  with p0 have a0: "a  0" and b0: "b  0" by auto
  from degree_mult_eq[OF this, folded p] assms
  consider "degree a = 1" "degree b = 0" | "degree a = 0" "degree b = 1" by force
  then show "a dvd 1  b dvd 1"
    by (cases; insert a1 b1, auto simp: primitive_imp_unit_iff)
qed

lemma irreducible_connect_rev:
  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
  assumes irr: "irreducible p" and deg: "degree p > 0"
  shows "irreducibled p"
proof(intro irreducibledI deg)
  fix q r
  assume degq: "degree q > 0" and diff: "degree q < degree p" and p: "p = q * r"
  from degq have nu: "¬ q dvd 1" by (auto simp: poly_dvd_1)
  from irreducibleD[OF irr p] nu have "r dvd 1" by auto
  then have "degree r = 0" by (auto simp: poly_dvd_1)
  with degq diff show False unfolding p using degree_mult_le[of q r] by auto
qed

subsection ‹Polynomial Evaluation of Integer and Rational Polynomials in Fields.›

abbreviation ipoly where "ipoly f x  poly (of_int_poly f) x"

lemma poly_map_poly_code[code_unfold]: "poly (map_poly h p) x = fold_coeffs (λ a b. h a + x * b) p 0"
  by (induct p, auto)

abbreviation real_of_int_poly :: "int poly  real poly" where
  "real_of_int_poly  of_int_poly"

abbreviation real_of_rat_poly :: "rat poly  real poly" where
  "real_of_rat_poly  map_poly of_rat"

lemma of_rat_of_int[simp]: "of_rat  of_int = of_int" by auto

lemma ipoly_of_rat[simp]: "ipoly p (of_rat y) = of_rat (ipoly p y)"
proof-
  have id: "of_int = of_rat o of_int" unfolding comp_def by auto
  show ?thesis by (subst id, subst map_poly_map_poly[symmetric], auto)
qed

lemma ipoly_of_real[simp]:
  "ipoly p (of_real x :: 'a :: {field,real_algebra_1}) = of_real (ipoly p x)"
proof -
  have id: "of_int = of_real o of_int" unfolding comp_def by auto
  show ?thesis by (subst id, subst map_poly_map_poly[symmetric], auto)
qed

lemma finite_ipoly_roots: assumes "p  0"
  shows "finite {x :: real. ipoly p x = 0}"
proof -
  let ?p = "real_of_int_poly p"
  from assms have "?p  0" by auto
  thus ?thesis by (rule poly_roots_finite)
qed

subsection ‹Algebraic Numbers -- Definition, Inverse, and Roots›

text ‹A number @{term "x :: 'a :: field"} is algebraic iff it is the root of an integer polynomial.
  Whereas the Isabelle distribution this is defined via the embedding
  of integers in an field via @{const Ints}, we work with integer polynomials
  of type @{type int} and then use @{const ipoly} for evaluating the polynomial at
  a real or complex point.›

lemma algebraic_altdef_ipoly:
  shows "algebraic x  (p. ipoly p x = 0  p  0)"
unfolding algebraic_def
proof (safe, goal_cases)
  case (1 p)
  define the_int where "the_int = (λx::'a. THE r. x = of_int r)"
  define p' where "p' = map_poly the_int p"
  have of_int_the_int: "of_int (the_int x) = x" if "x  " for x
    unfolding the_int_def by (rule sym, rule theI') (insert that, auto simp: Ints_def)
  have the_int_0_iff: "the_int x = 0  x = 0" if "x  "
    using of_int_the_int[OF that] by auto
  have "map_poly of_int p' = map_poly (of_int  the_int) p"
      by (simp add: p'_def map_poly_map_poly)
  also from 1 of_int_the_int have " = p"
    by (subst poly_eq_iff) (auto simp: coeff_map_poly)
  finally have p_p': "map_poly of_int p' = p" .
  show ?case
  proof (intro exI conjI notI)
    from 1 show "ipoly p' x = 0" by (simp add: p_p')
  next
    assume "p' = 0"
    hence "p = 0" by (simp add: p_p' [symmetric])
    with p  0 show False by contradiction
  qed
next
  case (2 p)
  thus ?case by (intro exI[of _ "map_poly of_int p"], auto)
qed

text ‹Definition of being algebraic with explicit witness polynomial.›

definition represents :: "int poly  'a :: field_char_0  bool" (infix "represents" 51)
  where "p represents x = (ipoly p x = 0  p  0)"

lemma representsI[intro]: "ipoly p x = 0  p  0  p represents x"
  unfolding represents_def by auto

lemma representsD:
  assumes "p represents x" shows "p  0" and "ipoly p x = 0" using assms unfolding represents_def by auto

lemma representsE:
  assumes "p represents x" and "p  0  ipoly p x = 0  thesis"
  shows thesis using assms unfolding represents_def by auto

lemma represents_imp_degree:
  fixes x :: "'a :: field_char_0"
  assumes "p represents x" shows "degree p  0"
proof-
  from assms have "p  0" and px: "ipoly p x = 0" by (auto dest:representsD)
  then have "(of_int_poly p :: 'a poly)  0" by auto
  then have "degree (of_int_poly p :: 'a poly)  0" by (fold poly_zero[OF px])
  then show ?thesis by auto
qed

lemma representsE_full[elim]:
  assumes rep: "p represents x"
    and main: "p  0  ipoly p x = 0  degree p  0  thesis"
  shows thesis
  by (rule main, insert represents_imp_degree[OF rep] rep, auto elim: representsE)

lemma represents_of_rat[simp]: "p represents (of_rat x) = p represents x" by (auto elim!:representsE)
lemma represents_of_real[simp]: "p represents (of_real x) = p represents x" by (auto elim!:representsE)

lemma algebraic_iff_represents: "algebraic x  ( p. p represents x)"
  unfolding algebraic_altdef_ipoly represents_def ..

lemma represents_irr_non_0:
  assumes irr: "irreducible p" and ap: "p represents x" and x0: "x  0"
  shows "poly p 0  0"
proof
  have nu: "¬ [:0,1::int:] dvd 1" by (auto simp: poly_dvd_1)
  assume "poly p 0 = 0"
  hence dvd: "[: 0, 1 :] dvd p" by (unfold dvd_iff_poly_eq_0, simp)
  then obtain q where pq: "p = [:0,1:] * q" by (elim dvdE)
  from irreducibleD[OF irr this] nu have "q dvd 1" by auto
  from this obtain r where "q = [:r:]" "r dvd 1" by (auto simp add: poly_dvd_1 dest: degree0_coeffs)
  with pq have "p = [:0,r:]" by auto
  with ap have "x = 0" by (auto simp: of_int_hom.map_poly_pCons_hom)
  with x0 show False by auto
qed

text ‹The polynomial encoding a rational number.›

definition poly_rat :: "rat  int poly" where
  "poly_rat x = (case quotient_of x of (n,d)  [:-n,d:])"

definition abs_int_poly:: "int poly  int poly" where
  "abs_int_poly p  if lead_coeff p < 0 then -p else p"

lemma pos_poly_abs_poly[simp]:
  shows "lead_coeff (abs_int_poly p) > 0  p  0"
proof-
  have "p  0  lead_coeff p * sgn (lead_coeff p) > 0" by (fold abs_sgn, auto)
  then show ?thesis by (auto simp: abs_int_poly_def mult.commute)
qed

lemma abs_int_poly_0[simp]: "abs_int_poly 0 = 0"
  by (auto simp: abs_int_poly_def)

lemma abs_int_poly_eq_0_iff[simp]: "abs_int_poly p = 0  p = 0"
  by (auto simp: abs_int_poly_def sgn_eq_0_iff)

lemma degree_abs_int_poly[simp]: "degree (abs_int_poly p) = degree p"
  by (auto simp: abs_int_poly_def sgn_eq_0_iff)

lemma abs_int_poly_dvd[simp]: "abs_int_poly p dvd q  p dvd q"
  by (unfold abs_int_poly_def, auto)

(*TODO: move & generalize *)
lemma (in idom) irreducible_uminus[simp]: "irreducible (-x)  irreducible x"
proof-
  have "-x = -1 * x" by simp
  also have "irreducible ...  irreducible x" by (rule irreducible_mult_unit_left, auto)
  finally show ?thesis.
qed

lemma irreducible_abs_int_poly[simp]:
  "irreducible (abs_int_poly p)  irreducible p"
  by (unfold abs_int_poly_def, auto)

lemma coeff_abs_int_poly[simp]:
  "coeff (abs_int_poly p) n = (if lead_coeff p < 0 then - coeff p n else coeff p n)"
  by (simp add: abs_int_poly_def)

lemma lead_coeff_abs_int_poly[simp]:
  "lead_coeff (abs_int_poly p) = abs (lead_coeff p)"
  by auto

lemma ipoly_abs_int_poly_eq_zero_iff[simp]:
  "ipoly (abs_int_poly p) (x :: 'a :: comm_ring_1) = 0  ipoly p x = 0"
  by (auto simp: abs_int_poly_def sgn_eq_0_iff of_int_poly_hom.hom_uminus)

lemma abs_int_poly_represents[simp]:
  "abs_int_poly p represents x  p represents x" by (auto elim!:representsE)


(* TODO: Move *)
lemma content_pCons[simp]: "content (pCons a p) = gcd a (content p)"
  by (unfold content_def coeffs_pCons_eq_cCons cCons_def, auto)

lemma content_uminus[simp]:
  fixes p :: "'a :: ring_gcd poly" shows "content (-p) = content p"
  by (induct p, auto)

lemma primitive_abs_int_poly[simp]:
  "primitive (abs_int_poly p)  primitive p"
  by (auto simp: abs_int_poly_def)

lemma abs_int_poly_inv[simp]: "smult (sgn (lead_coeff p)) (abs_int_poly p) = p"
  by (cases "lead_coeff p > 0", auto simp: abs_int_poly_def)



definition cf_pos :: "int poly  bool" where
  "cf_pos p = (content p = 1  lead_coeff p > 0)"

definition cf_pos_poly :: "int poly  int poly" where
  "cf_pos_poly f = (let
      c = content f;
      d = (sgn (lead_coeff f) * c)
    in sdiv_poly f d)"

lemma sgn_is_unit[intro!]:
  fixes x :: "'a :: linordered_idom" (* find/make better class *)
  assumes "x  0"
  shows "sgn x dvd 1" using assms by(cases x "0::'a" rule:linorder_cases, auto)

lemma cf_pos_poly_0[simp]: "cf_pos_poly 0 = 0" by (unfold cf_pos_poly_def sdiv_poly_def, auto)

lemma cf_pos_poly_eq_0[simp]: "cf_pos_poly f = 0  f = 0"
proof(cases "f = 0")
  case True
  thus ?thesis unfolding cf_pos_poly_def Let_def by (simp add: sdiv_poly_def)
next
  case False
  then have lc0: "lead_coeff f  0" by auto
  then have s0: "sgn (lead_coeff f)  0" (is "?s  0") and "content f  0" (is "?c  0") by (auto simp: sgn_0_0)
  then have sc0: "?s * ?c  0" by auto
  { fix i
    from content_dvd_coeff sgn_is_unit[OF lc0]
    have "?s * ?c dvd coeff f i" by (auto simp: unit_dvd_iff)
    then have "coeff f i div (?s * ?c) = 0  coeff f i = 0" by (auto simp:dvd_div_eq_0_iff)
  } note * = this
  show ?thesis unfolding cf_pos_poly_def Let_def sdiv_poly_def poly_eq_iff by (auto simp: coeff_map_poly *)
qed

lemma
  shows cf_pos_poly_main: "smult (sgn (lead_coeff f) * content f) (cf_pos_poly f) = f" (is ?g1)
    and content_cf_pos_poly[simp]: "content (cf_pos_poly f) = (if f = 0 then 0 else 1)" (is ?g2)
    and lead_coeff_cf_pos_poly[simp]: "lead_coeff (cf_pos_poly f) > 0  f  0" (is ?g3)
    and cf_pos_poly_dvd[simp]: "cf_pos_poly f dvd f" (is ?g4)
proof(atomize(full), (cases "f = 0"; intro conjI))
  case True
  then show ?g1 ?g2 ?g3 ?g4 by simp_all
next
  case f0: False
  let ?s = "sgn (lead_coeff f)"
  have s: "?s  {-1,1}" using f0 unfolding sgn_if by auto
  define g where "g  smult ?s f"
  define d where "d  ?s * content f"
  have "content g = content ([:?s:] * f)" unfolding g_def by simp
  also have " = content [:?s:] * content f" unfolding content_mult by simp
  also have "content [:?s:] = 1" using s by (auto simp: content_def)
  finally have cg: "content g = content f" by simp
  from f0
  have d: "cf_pos_poly f = sdiv_poly f d"  by (auto simp: cf_pos_poly_def Let_def d_def)
  let ?g = "primitive_part g"
  define ng where "ng = primitive_part g"
  note d
  also have "sdiv_poly f d = sdiv_poly g (content g)" unfolding cg unfolding g_def d_def
    by (rule poly_eqI, unfold coeff_sdiv_poly coeff_smult, insert s, auto simp: div_minus_right)
  finally have fg: "cf_pos_poly f = primitive_part g" unfolding primitive_part_alt_def .
  have "lead_coeff f  0" using f0 by auto
  hence lg: "lead_coeff g > 0" unfolding g_def lead_coeff_smult
    by (meson linorder_neqE_linordered_idom sgn_greater sgn_less zero_less_mult_iff)
  hence g0: "g  0" by auto
  from f0 content_primitive_part[OF this]
  show ?g2 unfolding fg by auto
  from g0 have "content g  0" by simp
  with arg_cong[OF content_times_primitive_part[of g], of lead_coeff, unfolded lead_coeff_smult]
    lg content_ge_0_int[of g] have lg': "lead_coeff ng > 0" unfolding ng_def
    by (metis dual_order.antisym dual_order.strict_implies_order zero_less_mult_iff)
  with f0 show ?g3 unfolding fg ng_def by auto

  have d0: "d  0" using s f0 by (force simp add: d_def)
  have "smult d (cf_pos_poly f) = smult ?s (smult (content f) (sdiv_poly (smult ?s f) (content f)))"
    unfolding fg primitive_part_alt_def cg by (simp add: g_def d_def)
  also have "sdiv_poly (smult ?s f) (content f) = smult ?s (sdiv_poly f (content f))"
    using s by (metis cg g_def primitive_part_alt_def primitive_part_smult_int sgn_sgn)
  finally have "smult d (cf_pos_poly f) = smult (content f) (primitive_part f)"
    unfolding primitive_part_alt_def using s by auto
  also have " = f" by (rule content_times_primitive_part)
  finally have df: "smult d (cf_pos_poly f) = f" .
  with d0 show ?g1 by (auto simp: d_def)
  from df have *: "f = cf_pos_poly f * [:d:]" by simp
  from dvdI[OF this] show ?g4.
qed

(* TODO: remove *)
lemma irreducible_connect_int:
  fixes p :: "int poly"
  assumes ir: "irreducibled p" and c: "content p = 1"
  shows "irreducible p"
  using c primitive_iff_content_eq_1 ir irreducible_primitive_connect by blast

lemma
  fixes x :: "'a :: {idom,ring_char_0}"
  shows ipoly_cf_pos_poly_eq_0[simp]: "ipoly (cf_pos_poly p) x = 0  ipoly p x = 0"
    and degree_cf_pos_poly[simp]: "degree (cf_pos_poly p) = degree p"
    and cf_pos_cf_pos_poly[intro]: "p  0  cf_pos (cf_pos_poly p)"
proof-
  show "degree (cf_pos_poly p) = degree p"
    by (subst(3) cf_pos_poly_main[symmetric], auto simp:sgn_eq_0_iff)
  {
    assume p: "p  0"
    show "cf_pos (cf_pos_poly p)" using cf_pos_poly_main p by (auto simp: cf_pos_def)
    have "(ipoly (cf_pos_poly p) x = 0) = (ipoly p x = 0)"
      apply (subst(3) cf_pos_poly_main[symmetric]) by (auto simp: sgn_eq_0_iff hom_distribs)
  }
  then show "(ipoly (cf_pos_poly p) x = 0) = (ipoly p x = 0)" by (cases "p = 0", auto)
qed


lemma cf_pos_poly_eq_1: "cf_pos_poly f = 1  degree f = 0  f  0" (is "?l  ?r")
proof(intro iffI conjI)
  assume ?r
  then have df0: "degree f = 0" and f0: "f  0" by auto
  from  degree0_coeffs[OF df0] obtain f0 where f: "f = [:f0:]" by auto
  show "cf_pos_poly f = 1" using f0 unfolding f cf_pos_poly_def Let_def sdiv_poly_def
    by (auto simp: content_def mult_sgn_abs)
next
  assume l: ?l
  then have "degree (cf_pos_poly f) = 0" by auto
  then show "degree f = 0" by simp
  from l have "cf_pos_poly f  0" by auto
  then show "f  0" by simp
qed



lemma irr_cf_poly_rat[simp]: "irreducible (poly_rat x)"
  "lead_coeff (poly_rat x) > 0" "primitive (poly_rat x)"
proof -
  obtain n d where x: "quotient_of x = (n,d)" by force
  hence id: "poly_rat x = [:-n,d:]" by (auto simp: poly_rat_def)
  from quotient_of_denom_pos[OF x] have d: "d > 0" by auto
  show "lead_coeff (poly_rat x) > 0" "primitive (poly_rat x)"
    unfolding id cf_pos_def using d quotient_of_coprime[OF x] by (auto simp: content_def)
  from this[unfolded cf_pos_def]
  show irr: "irreducible (poly_rat x)" unfolding id using d by (auto intro!: linear_irreducible_int)
qed

lemma poly_rat[simp]: "ipoly (poly_rat x) (of_rat x :: 'a :: field_char_0) = 0" "ipoly (poly_rat x) x = 0"
  "poly_rat x  0" "ipoly (poly_rat x) y = 0  y = (of_rat x :: 'a)"
proof -
  from irr_cf_poly_rat(1)[of x] show "poly_rat x  0"
    unfolding Factorial_Ring.irreducible_def by auto
  obtain n d where x: "quotient_of x = (n,d)" by force
  hence id: "poly_rat x = [:-n,d:]" by (auto simp: poly_rat_def)
  from quotient_of_denom_pos[OF x] have d: "d  0" by auto
  have "y * of_int d = of_int n  y = of_int n / of_int d" using d
    by (simp add: eq_divide_imp)
  with d id show "ipoly (poly_rat x) (of_rat x) = 0" "ipoly (poly_rat x) x = 0"
    "ipoly (poly_rat x) y = 0  y = (of_rat x :: 'a)"
    by (auto simp: of_rat_minus of_rat_divide simp: quotient_of_div[OF x])
qed

lemma poly_rat_represents_of_rat: "(poly_rat x) represents (of_rat x)" by auto

lemma ipoly_smult_0_iff: assumes c: "c  0"
  shows "(ipoly (smult c p) x = (0 :: real)) = (ipoly p x = 0)"
  using c by (simp add: hom_distribs)


(* TODO *)
lemma not_irreducibleD:
  assumes "¬ irreducible x" and "x  0" and "¬ x dvd 1"
  shows "y z. x = y * z  ¬ y dvd 1  ¬ z dvd 1" using assms
  apply (unfold Factorial_Ring.irreducible_def) by auto


lemma cf_pos_poly_represents[simp]: "(cf_pos_poly p) represents x  p represents x"
  unfolding represents_def by auto

lemma coprime_prod: (* TODO: move *)
  "a  0  c  0  coprime (a * b) (c * d)  coprime b (d::'a::{semiring_gcd})"
  by auto

lemma smult_prod: (* TODO: move or find corresponding lemma *)
  "smult a b = monom a 0 * b"
  by (simp add: monom_0)

lemma degree_map_poly_2:
  assumes "f (lead_coeff p)  0"
  shows   "degree (map_poly f p) = degree p"
proof (cases "p=0")
  case False thus ?thesis
    unfolding degree_eq_length_coeffs Polynomial.coeffs_map_poly
    using assms by (simp add:coeffs_def)
qed auto

lemma irreducible_cf_pos_poly:
  assumes irr: "irreducible p" and deg: "degree p  0"
  shows "irreducible (cf_pos_poly p)" (is "irreducible ?p")
proof (unfold irreducible_altdef, intro conjI allI impI)
  from irr show "?p  0" by auto
  from deg have "degree ?p  0" by simp
  then show "¬ ?p dvd 1" unfolding poly_dvd_1 by auto
  fix b assume "b dvd cf_pos_poly p"
  also note cf_pos_poly_dvd
  finally have "b dvd p".
  with irr[unfolded irreducible_altdef] have "p dvd b  b dvd 1" by auto
  then show "?p dvd b  b dvd 1" by (auto dest: dvd_trans[OF cf_pos_poly_dvd])
qed

locale dvd_preserving_hom = comm_semiring_1_hom +
  assumes hom_eq_mult_hom_imp: "hom x = hom y * hz  z. hz = hom z  x = y * z"
begin

  lemma hom_dvd_hom_iff[simp]: "hom x dvd hom y  x dvd y"
  proof
    assume "hom x dvd hom y"
    then obtain hz where "hom y = hom x * hz" by (elim dvdE)
    from hom_eq_mult_hom_imp[OF this] obtain z
    where "hz = hom z" and mult: "y = x * z" by auto
    then show "x dvd y" by auto
  qed auto

  sublocale unit_preserving_hom
  proof unfold_locales
    fix x assume "hom x dvd 1" then have "hom x dvd hom 1" by simp
    then show "x dvd 1" by (unfold hom_dvd_hom_iff)
  qed

  sublocale zero_hom_0
  proof (unfold_locales)
    fix a :: 'a
    assume "hom a = 0"
    then have "hom 0 dvd hom a" by auto
    then have "0 dvd a" by (unfold hom_dvd_hom_iff)
    then show "a = 0" by auto
  qed

end

lemma smult_inverse_monom:"p  0  smult (inverse c) (p::rat poly) = 1  p = [: c :]"
  proof (cases "c=0")
    case True thus "p  0  ?thesis" by auto
  next
    case False thus ?thesis by (metis left_inverse right_inverse smult_1 smult_1_left smult_smult)
  qed

lemma of_int_monom:"of_int_poly p = [:rat_of_int c:]  p = [: c :]" by (induct p, auto)

lemma degree_0_content:
  fixes p :: "int poly"
  assumes deg: "degree p = 0" shows "content p = abs (coeff p 0)"
proof-
  from deg obtain a where p: "p = [:a:]" by (auto dest: degree0_coeffs)
  show ?thesis by (auto simp: p)
qed

lemma prime_elem_imp_gcd_eq:
  fixes x::"'a:: ring_gcd"
  shows "prime_elem x  gcd x y = normalize x  gcd x y = 1"
  using prime_elem_imp_coprime [of x y]
  by (auto simp add: gcd_proj1_iff intro: coprime_imp_gcd_eq_1) 

lemma irreducible_pos_gcd:
  fixes p :: "int poly"
  assumes ir: "irreducible p" and pos: "lead_coeff p > 0" shows "gcd p q  {1,p}"
proof-
  from pos have "[:sgn (lead_coeff p):] = 1" by auto
  with prime_elem_imp_gcd_eq[of p, unfolded prime_elem_iff_irreducible, OF ir, of q]
  show ?thesis by (auto simp: normalize_poly_def)
qed

lemma irreducible_pos_gcd_twice:
  fixes p q :: "int poly"
  assumes p: "irreducible p" "lead_coeff p > 0"
  and q: "irreducible q" "lead_coeff q > 0"
  shows "gcd p q = 1  p = q"
proof (cases "gcd p q = 1")
  case False note pq = this
  have "p = gcd p q" using irreducible_pos_gcd [OF p, of q] pq
    by auto
  also have " = q" using irreducible_pos_gcd [OF q, of p] pq
    by (auto simp add: ac_simps)
  finally show ?thesis by auto
qed simp

interpretation of_rat_hom: field_hom_0' of_rat..

lemma poly_zero_imp_not_unit:
  assumes "poly p x = 0" shows "¬ p dvd 1"
proof (rule notI)
  assume "p dvd 1"
  from poly_hom.hom_dvd_1[OF this] have "poly p x dvd 1" by auto
  with assms show False by auto
qed

lemma poly_prod_mset_zero_iff:
  fixes x :: "'a :: idom"
  shows "poly (prod_mset F) x = 0  (f ∈# F. poly f x = 0)"
  by (induct F, auto simp: poly_mult_zero_iff)

lemma algebraic_imp_represents_irreducible:
  fixes x :: "'a :: field_char_0"
  assumes "algebraic x"
  shows "p. p represents x  irreducible p"
proof -
  from assms obtain p
  where px0: "ipoly p x = 0" and p0: "p  0" unfolding algebraic_altdef_ipoly by auto
  from poly_zero_imp_not_unit[OF px0]
  have "¬ p dvd 1" by (auto dest: of_int_poly_hom.hom_dvd_1[where 'a = 'a])
  from mset_factors_exist[OF p0 this]
  obtain F where F: "mset_factors F p" by auto
  then have "p = prod_mset F" by auto
  also have "(of_int_poly ... :: 'a poly) = prod_mset (image_mset of_int_poly F)" by simp
  finally have "poly ... x = 0" using px0 by auto
  from this[unfolded poly_prod_mset_zero_iff]
  obtain f where "f ∈# F" and fx0: "ipoly f x = 0" by auto
  with F have "irreducible f" by auto
  with fx0 show ?thesis by auto
qed

lemma algebraic_imp_represents_irreducible_cf_pos:
  assumes "algebraic (x::'a::field_char_0)"
  shows "p. p represents x  irreducible p  lead_coeff p > 0  primitive p"
proof -
  from algebraic_imp_represents_irreducible[OF assms(1)]
  obtain p where px: "p represents x" and irr: "irreducible p" by auto
  let ?p = "cf_pos_poly p"
  from px irr represents_imp_degree
  have 1: "?p represents x" and 2: "irreducible ?p" and 3: "cf_pos ?p"
    by (auto intro: irreducible_cf_pos_poly)
  then show ?thesis by (auto intro: exI[of _ ?p] simp: cf_pos_def)
qed

lemma gcd_of_int_poly: "gcd (of_int_poly f) (of_int_poly g :: 'a :: {field_char_0,field_gcd} poly) =
  smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))"
proof -
  let ?ia = "of_int_poly :: _  'a poly"
  let ?ir = "of_int_poly :: _  rat poly"
  let ?ra = "map_poly of_rat :: _  'a poly"
  have id: "?ia x = ?ra (?ir x)" for x by (subst map_poly_map_poly, auto)
  show ?thesis
    unfolding id
    unfolding of_rat_hom.map_poly_gcd[symmetric]
    unfolding gcd_rat_to_gcd_int by (auto simp: hom_distribs)
qed

lemma algebraic_imp_represents_unique:
  fixes x :: "'a :: {field_char_0,field_gcd}"
  assumes "algebraic x"
  shows "∃! p. p represents x  irreducible p  lead_coeff p > 0" (is "Ex1 ?p")
proof -
  from assms obtain p
  where p: "?p p" and cfp: "cf_pos p"
    by (auto simp: cf_pos_def dest: algebraic_imp_represents_irreducible_cf_pos)
  show ?thesis
  proof (rule ex1I)
    show "?p p" by fact
    fix q
    assume q: "?p q"
    then have "q represents x" by auto
    from represents_imp_degree[OF this] q irreducible_content[of q]
    have cfq: "cf_pos q" by (auto simp: cf_pos_def)
    show "q = p"
    proof (rule ccontr)
      let ?ia = "map_poly of_int :: int poly  'a poly"
      assume "q  p"
      with irreducible_pos_gcd_twice[of p q] p q cfp cfq have gcd: "gcd p q = 1" by auto
      from p q have rt: "ipoly p x = 0" "ipoly q x = 0" unfolding represents_def by auto
      define c :: 'a where "c = inverse (of_int (lead_coeff (gcd p q)))"
      have rt: "poly (?ia p) x = 0" "poly (?ia q) x = 0" using rt by auto
      hence "[:-x,1:] dvd ?ia p" "[:-x,1:] dvd ?ia q"
        unfolding poly_eq_0_iff_dvd by auto
      hence "[:-x,1:] dvd gcd (?ia p) (?ia q)" by (rule gcd_greatest)
      also have " = smult c (?ia (gcd p q))" unfolding gcd_of_int_poly c_def ..
      also have "?ia (gcd p q) = 1" by (simp add: gcd)
      also have "smult c 1 = [: c :]" by simp
      finally show False using c_def gcd by (simp add: dvd_iff_poly_eq_0)
    qed
  qed
qed

lemma ipoly_poly_compose:
  fixes x :: "'a :: idom"
  shows "ipoly (p p q) x = ipoly p (ipoly q x)"
proof (induct p)
  case (pCons a p)
  have "ipoly ((pCons a p) p q) x = of_int a + ipoly (q * p p q) x" by (simp add: hom_distribs)
  also have "ipoly (q * p p q) x = ipoly q x * ipoly (p p q) x" by (simp add: hom_distribs)
  also have "ipoly (p p q) x = ipoly p (ipoly q x)" unfolding pCons(2) ..
  also have "of_int a + ipoly q x *  = ipoly (pCons a p) (ipoly q x)"
    unfolding map_poly_pCons[OF pCons(1)] by simp
  finally show ?case .
qed simp

text ‹Polynomial for unary minus.›

definition poly_uminus :: "'a :: ring_1 poly  'a poly" where [code del]:
  "poly_uminus p  idegree p. monom ((-1)^i * coeff p i) i"

lemma poly_uminus_pCons_pCons[simp]:
  "poly_uminus (pCons a (pCons b p)) = pCons a (pCons (-b) (poly_uminus p))" (is "?l = ?r")
proof(cases "p = 0")
  case False
  then have deg: "degree (pCons a (pCons b p)) = Suc (Suc (degree p))" by simp
  show ?thesis
  by (unfold poly_uminus_def deg sum.atMost_Suc_shift monom_Suc monom_0 sum_pCons_0_commute, simp)
next
  case True
  then show ?thesis by (auto simp add: poly_uminus_def monom_0 monom_Suc)
qed

fun poly_uminus_inner :: "'a :: ring_1 list  'a poly"
where "poly_uminus_inner [] = 0"
  |   "poly_uminus_inner [a] = [:a:]"
  |   "poly_uminus_inner (a#b#cs) = pCons a (pCons (-b) (poly_uminus_inner cs))"

lemma poly_uminus_code[code,simp]: "poly_uminus p = poly_uminus_inner (coeffs p)"
proof-
  have "poly_uminus (Poly as) = poly_uminus_inner as" for as :: "'a list"
  proof (induct "length as" arbitrary:as rule: less_induct)
    case less
    show ?case
    proof(cases as)
      case Nil
      then show ?thesis by (simp add: poly_uminus_def)
    next
      case [simp]: (Cons a bs)
      show ?thesis
      proof (cases bs)
        case Nil
        then show ?thesis by (simp add: poly_uminus_def monom_0)
      next
        case [simp]: (Cons b cs)
        show ?thesis by (simp add: less)
      qed
    qed
  qed
  from this[of "coeffs p"]
  show ?thesis by simp
qed

lemma poly_uminus_inner_0[simp]: "poly_uminus_inner as = 0  Poly as = 0"
  by (induct as rule: poly_uminus_inner.induct, auto)

lemma degree_poly_uminus_inner[simp]: "degree (poly_uminus_inner as) = degree (Poly as)"
  by (induct as rule: poly_uminus_inner.induct, auto)

lemma ipoly_uminus_inner[simp]:
  "ipoly (poly_uminus_inner as) (x::'a::comm_ring_1) = ipoly (Poly as) (-x)"
  by (induct as rule: poly_uminus_inner.induct, auto simp: hom_distribs ring_distribs)

lemma represents_uminus: assumes alg: "p represents x"
  shows "(poly_uminus p) represents (-x)"
proof -
  from representsD[OF alg] have "p  0" and rp: "ipoly p x = 0" by auto
  hence 0: "poly_uminus p  0" by simp
  show ?thesis
    by (rule representsI[OF _ 0], insert rp, auto)
qed


lemma content_poly_uminus_inner[simp]:
  fixes as :: "'a :: ring_gcd list"
  shows "content (poly_uminus_inner as) = content (Poly as)"
  by (induct as rule: poly_uminus_inner.induct, auto)


text ‹Multiplicative inverse is represented by @{const reflect_poly}.›

lemma inverse_pow_minus: assumes "x  (0 :: 'a :: field)"
  and "i  n"
  shows "inverse x ^ n * x ^ i = inverse x ^ (n - i)"
  using assms by (simp add: field_class.field_divide_inverse power_diff power_inverse)

lemma (in inj_idom_hom) reflect_poly_hom:
  "reflect_poly (map_poly hom p) = map_poly hom (reflect_poly p)"
proof -
  obtain xs where xs: "rev (coeffs p) = xs" by auto
  show ?thesis unfolding reflect_poly_def coeffs_map_poly_hom rev_map
    xs by (induct xs, auto simp: hom_distribs)
qed

lemma ipoly_reflect_poly: assumes x: "(x :: 'a :: field_char_0)  0"
  shows "ipoly (reflect_poly p) x = x ^ (degree p) * ipoly p (inverse x)" (is "?l = ?r")
proof -
  let ?or = "of_int :: int  'a"
  have hom: "inj_idom_hom ?or" ..
  show ?thesis
    using poly_reflect_poly_nz[OF x, of "map_poly ?or p"] by (simp add: inj_idom_hom.reflect_poly_hom[OF hom])
qed

lemma represents_inverse: assumes x: "x  0"
  and alg: "p represents x"
  shows "(reflect_poly p) represents (inverse x)"
proof (intro representsI)
  from representsD[OF alg] have "p  0" and rp: "ipoly p x = 0" by auto
  then show "reflect_poly p  0" by (metis reflect_poly_0 reflect_poly_at_0_eq_0_iff)
  show "ipoly (reflect_poly p) (inverse x) = 0" by (subst ipoly_reflect_poly, insert x, auto simp:rp)
qed

lemma inverse_roots: assumes x: "(x :: 'a :: field_char_0)  0"
  shows "ipoly (reflect_poly p) x = 0  ipoly p (inverse x) = 0"
  using x by (auto simp: ipoly_reflect_poly)

context
  fixes n :: nat
begin
text ‹Polynomial for n-th root.›

definition poly_nth_root :: "'a :: idom poly  'a poly" where
  "poly_nth_root p = p p monom 1 n"

lemma ipoly_nth_root:
  fixes x :: "'a :: idom"
  shows "ipoly (poly_nth_root p) x = ipoly p (x ^ n)"
  unfolding poly_nth_root_def ipoly_poly_compose by (simp add: map_poly_monom poly_monom)

context
  assumes n: "n  0"
begin
lemma poly_nth_root_0[simp]: "poly_nth_root p = 0  p = 0"
  unfolding poly_nth_root_def
  by (rule pcompose_eq_0, insert n, auto simp: degree_monom_eq)

lemma represents_nth_root:
  assumes y: "y^n = x" and alg: "p represents x"
  shows "(poly_nth_root p) represents y"
proof -
  from representsD[OF alg] have "p  0" and rp: "ipoly p x = 0" by auto
  hence 0: "poly_nth_root p  0" by simp
  show ?thesis
    by (rule representsI[OF _ 0], unfold ipoly_nth_root y rp, simp)
qed

lemma represents_nth_root_odd_real:
  assumes alg: "p represents x" and odd: "odd n"
  shows "(poly_nth_root p) represents (root n x)"
  by (rule represents_nth_root[OF odd_real_root_pow[OF odd] alg])

lemma represents_nth_root_pos_real:
  assumes alg: "p represents x" and pos: "x > 0"
  shows "(poly_nth_root p) represents (root n x)"
proof -
  from n have id: "Suc (n - 1) = n" by auto
  show ?thesis
  proof (rule represents_nth_root[OF _ alg])
    show "root n x ^ n = x" using id pos by auto
  qed
qed

lemma represents_nth_root_neg_real:
  assumes alg: "p represents x" and neg: "x < 0"
  shows "(poly_uminus (poly_nth_root (poly_uminus p))) represents (root n x)"
proof -
  have rt: "root n x = - root n (-x)" unfolding real_root_minus by simp
  show ?thesis unfolding rt
    by (rule represents_uminus[OF represents_nth_root_pos_real[OF represents_uminus[OF alg]]], insert neg, auto)
qed
end
end

lemma represents_csqrt:
  assumes alg: "p represents x" shows "(poly_nth_root 2 p) represents (csqrt x)"
  by (rule represents_nth_root[OF _ _ alg], auto)

lemma represents_sqrt:
  assumes alg: "p represents x" and pos: "x  0"
  shows "(poly_nth_root 2 p) represents (sqrt x)"
  by (rule represents_nth_root[OF _ _ alg], insert pos, auto)

lemma represents_degree:
  assumes "p represents x" shows "degree p  0"
proof
  assume "degree p = 0"
  from degree0_coeffs[OF this] obtain c where p: "p = [:c:]" by auto
  from assms[unfolded represents_def p]
  show False by auto
qed


text ‹Polynomial for multiplying a rational number with an algebraic number.›

definition poly_mult_rat_main where
  "poly_mult_rat_main n d (f :: 'a :: idom poly) = (let fs = coeffs f; k = length fs in
    poly_of_list (map (λ (fi, i). fi * d ^ i * n ^ (k - Suc i)) (zip fs [0 ..< k])))"

definition poly_mult_rat :: "rat  int poly  int poly" where
  "poly_mult_rat r p  case quotient_of r of (n,d)  poly_mult_rat_main n d p"

lemma coeff_poly_mult_rat_main: "coeff (poly_mult_rat_main n d f) i = coeff f i * n ^ (degree f - i) * d ^ i"
proof -
  have id: "coeff (poly_mult_rat_main n d f) i = (coeff f i * d ^ i) * n ^ (length (coeffs f) - Suc i)"
    unfolding poly_mult_rat_main_def Let_def poly_of_list_def coeff_Poly
    unfolding nth_default_coeffs_eq[symmetric]
    unfolding nth_default_def by auto
  show ?thesis unfolding id by (simp add: degree_eq_length_coeffs)
qed

lemma degree_poly_mult_rat_main: "n  0  degree (poly_mult_rat_main n d f) = (if d = 0 then 0 else degree f)"
proof (cases "d = 0")
  case True
  thus ?thesis unfolding degree_def unfolding coeff_poly_mult_rat_main by simp
next
  case False
  hence id: "(d = 0) = False" by simp
  show "n  0  ?thesis" unfolding degree_def coeff_poly_mult_rat_main id
    by (simp add: id)
qed

lemma ipoly_mult_rat_main:
  fixes x :: "'a :: {field,ring_char_0}"
  assumes "d  0" and "n  0"
  shows "ipoly (poly_mult_rat_main n d p) x = of_int n ^ degree p * ipoly p (x * of_int d / of_int n)"
proof -
  from assms have d: "(if d = 0 then t else f) = f" for t f :: 'b by simp
  show ?thesis
    unfolding poly_altdef of_int_hom.coeff_map_poly_hom mult.assoc[symmetric] of_int_mult[symmetric]
      sum_distrib_left
    unfolding of_int_hom.degree_map_poly_hom degree_poly_mult_rat_main[OF assms(2)] d
  proof (rule sum.cong[OF refl])
    fix i
    assume "i  {..degree p}"
    hence i: "i  degree p" by auto
    hence id: "of_int n ^ (degree p - i) = (of_int n ^ degree p / of_int n ^ i :: 'a)"
      by (simp add: assms(2) power_diff)
    thus "of_int (coeff (poly_mult_rat_main n d p) i) * x ^ i = of_int n ^ degree p * of_int (coeff p i) * (x * of_int d / of_int n) ^ i"
      unfolding coeff_poly_mult_rat_main
      by (simp add: field_simps)
  qed
qed

lemma degree_poly_mult_rat[simp]: assumes "r  0" shows "degree (poly_mult_rat r p) = degree p"
proof -
  obtain n d where quot: "quotient_of r = (n,d)" by force
  from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto
  from quotient_of_denom_pos[OF quot] have d: "d  0" by auto
  with assms r have n0: "n  0" by simp
  from quot have id: "poly_mult_rat r p = poly_mult_rat_main n d p"  unfolding poly_mult_rat_def by simp
  show ?thesis unfolding id degree_poly_mult_rat_main[OF n0] using d by simp
qed

lemma ipoly_mult_rat:
  assumes r0: "r  0"
  shows "ipoly (poly_mult_rat r p) x = of_int (fst (quotient_of r)) ^ degree p * ipoly p (x * inverse (of_rat r))"
proof -
  obtain n d where quot: "quotient_of r = (n,d)" by force
  from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto
  from quotient_of_denom_pos[OF quot] have d: "d  0" by auto
  from r r0 have n: "n  0" by simp
  from r d n have inv: "of_int d / of_int n = inverse r" by simp
  from quot have id: "poly_mult_rat r p = poly_mult_rat_main n d p"  unfolding poly_mult_rat_def by simp
  show ?thesis unfolding id ipoly_mult_rat_main[OF d n] quot fst_conv of_rat_inverse[symmetric] inv[symmetric]
    by (simp add: of_rat_divide)
qed

lemma poly_mult_rat_main_0[simp]:
  assumes "n  0" "d  0" shows "poly_mult_rat_main n d p = 0  p = 0"
proof
  assume "p = 0" thus "poly_mult_rat_main n d p = 0"
    by (simp add: poly_mult_rat_main_def)
next
  assume 0: "poly_mult_rat_main n d p = 0"
  {
    fix i
    from 0 have "coeff (poly_mult_rat_main n d p) i = 0" by simp
    hence "coeff p i = 0" unfolding coeff_poly_mult_rat_main using assms by simp
  }
  thus "p = 0" by (intro poly_eqI, auto)
qed


lemma poly_mult_rat_0[simp]: assumes r0: "r  0" shows "poly_mult_rat r p = 0  p = 0"
proof -
  obtain n d where quot: "quotient_of r = (n,d)" by force
  from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto
  from quotient_of_denom_pos[OF quot] have d: "d  0" by auto
  from r r0 have n: "n  0" by simp
  from quot have id: "poly_mult_rat r p = poly_mult_rat_main n d p"  unfolding poly_mult_rat_def by simp
  show ?thesis unfolding id using n d by simp
qed

lemma represents_mult_rat:
  assumes r: "r  0" and "p represents x" shows "(poly_mult_rat r p) represents (of_rat r * x)"
  using assms
  unfolding represents_def ipoly_mult_rat[OF r] by (simp add: field_simps)

text ‹Polynomial for adding a rational number on an algebraic number.
  Again, we do not have to factor afterwards.›

definition poly_add_rat :: "rat  int poly  int poly" where
  "poly_add_rat r p  case quotient_of r of (n,d) 
     (poly_mult_rat_main d 1 p p [:-n,d:])"

lemma poly_add_rat_code[code]: "poly_add_rat r p  case quotient_of r of (n,d) 
     let p' = (let fs = coeffs p; k = length fs in poly_of_list (map (λ(fi, i). fi * d ^ (k - Suc i)) (zip fs [0..<k])));
         p'' = p' p [:-n,d:]
      in p''"
  unfolding poly_add_rat_def poly_mult_rat_main_def Let_def by simp

lemma degree_poly_add_rat[simp]: "degree (poly_add_rat r p) = degree p"
proof -
  obtain n d where quot: "quotient_of r = (n,d)" by force
  from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto
  from quotient_of_denom_pos[OF quot] have d: "d  0" "d > 0" by auto
  show ?thesis unfolding poly_add_rat_def quot split
    by (simp add: degree_poly_mult_rat_main d)
qed

lemma ipoly_add_rat: "ipoly (poly_add_rat r p) x = (of_int (snd (quotient_of r)) ^ degree p) * ipoly p (x - of_rat r)"
proof -
  obtain n d where quot: "quotient_of r = (n,d)" by force
  from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto
  from quotient_of_denom_pos[OF quot] have d: "d  0" "d > 0" by auto
  have id: "ipoly [:- n, 1:] (x / of_int d :: 'a) = - of_int n + x / of_int d" by simp
  show ?thesis unfolding poly_add_rat_def quot split
    by (simp add: ipoly_mult_rat_main ipoly_poly_compose d r degree_poly_mult_rat_main field_simps id of_rat_divide)
qed

lemma poly_add_rat_0[simp]: "poly_add_rat r p = 0  p = 0"
proof -
  obtain n d where quot: "quotient_of r = (n,d)" by force
  from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto
  from quotient_of_denom_pos[OF quot] have d: "d  0" "d > 0" by auto
  show ?thesis unfolding poly_add_rat_def quot split
    by (simp add: d pcompose_eq_0)
qed

lemma add_rat_roots: "ipoly (poly_add_rat r p) x = 0  ipoly p (x - of_rat r) = 0"
  unfolding ipoly_add_rat using quotient_of_nonzero by auto

lemma represents_add_rat:
  assumes "p represents x" shows "(poly_add_rat r p) represents (of_rat r + x)"
  using assms unfolding represents_def ipoly_add_rat by simp

(* TODO: move? *)
lemmas pos_mult[simplified,simp] = mult_less_cancel_left_pos[of _ 0] mult_less_cancel_left_pos[of _ _ 0]

lemma ipoly_add_rat_pos_neg:
  "ipoly (poly_add_rat r p) (x::'a::linordered_field) < 0  ipoly p (x - of_rat r) < 0"
  "ipoly (poly_add_rat r p) (x::'a::linordered_field) > 0  ipoly p (x - of_rat r) > 0"
  using quotient_of_nonzero unfolding ipoly_add_rat by auto

lemma sgn_ipoly_add_rat[simp]:
  "sgn (ipoly (poly_add_rat r p) (x::'a::linordered_field)) = sgn (ipoly p (x - of_rat r))" (is "sgn ?l = sgn ?r")
  using ipoly_add_rat_pos_neg[of r p x]
  by (cases ?r "0::'a" rule: linorder_cases,auto simp:  sgn_1_pos sgn_1_neg sgn_eq_0_iff)

lemma deg_nonzero_represents:
  assumes deg: "degree p  0" shows " x :: complex. p represents x"
proof -
  let ?p = "of_int_poly p :: complex poly"
  from fundamental_theorem_algebra_factorized[of ?p]
  obtain as c where id: "smult c (aas. [:- a, 1:]) = ?p"
    and len: "length as = degree ?p" by blast
  have "degree ?p = degree p" by simp
  with deg len obtain b bs where as: "as = b # bs" by (cases as, auto)
  have "p represents b" unfolding represents_def id[symmetric] as using deg by auto
  thus ?thesis by blast
qed

end

Theory Bivariate_Polynomials

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Resultants›

text ‹We need some results on resultants to show that 
  a suitable prime for Berlekamp's algorithm always exists
  if the input is square free. Most of this theory has
  been developed for algebraic numbers, though. We moved this
  theory here, so that algebraic numbers can already use the
  factorization algorithm of this entry.›

subsection ‹Bivariate Polynomials›

theory Bivariate_Polynomials
imports 
  Polynomial_Interpolation.Ring_Hom_Poly
  Subresultants.More_Homomorphisms 
  Berlekamp_Zassenhaus.Unique_Factorization_Poly (* Only for preserving sublocaling *)
begin

subsubsection ‹Evaluation of Bivariate Polynomials›

definition poly2 :: "'a::comm_semiring_1 poly poly  'a  'a  'a"
  where "poly2 p x y = poly (poly p [: y :]) x"

lemma poly2_by_map: "poly2 p x = poly (map_poly (λc. poly c x) p)"
  apply (rule ext) unfolding poly2_def by (induct p; simp)

lemma poly2_const[simp]: "poly2 [:[:a:]:] x y = a" by (simp add: poly2_def)
lemma poly2_smult[simp,hom_distribs]: "poly2 (smult a p) x y = poly a x * poly2 p x y" by (simp add: poly2_def)

interpretation poly2_hom: comm_semiring_hom "λp. poly2 p x y" by (unfold_locales; simp add: poly2_def)
interpretation poly2_hom: comm_ring_hom "λp. poly2 p x y"..
interpretation poly2_hom: idom_hom "λp. poly2 p x y"..

lemma poly2_pCons[simp,hom_distribs]: "poly2 (pCons a p) x y = poly a x + y * poly2 p x y" by (simp add: poly2_def)
lemma poly2_monom: "poly2 (monom a n) x y = poly a x * y ^ n" by (auto simp: poly_monom poly2_def)

lemma poly_poly_as_poly2: "poly2 p x (poly q x) = poly (poly p q) x" by (induct p; simp add:poly2_def)

text ‹The following lemma is an extension rule for bivariate polynomials.›

lemma poly2_ext:
  fixes p q :: "'a :: {ring_char_0,idom} poly poly"
  assumes "x y. poly2 p x y = poly2 q x y" shows "p = q"
proof(intro poly_ext)
  fix r x
  show "poly (poly p r) x = poly (poly q r) x"
    unfolding poly_poly_as_poly2[symmetric] using assms by auto
qed

abbreviation (input) "coeff_lift2 == λa. [:[: a :]:]"


lemma coeff_lift2_lift: "coeff_lift2 = coeff_lift  coeff_lift" by auto

definition "poly_lift = map_poly coeff_lift"
definition "poly_lift2 = map_poly coeff_lift2"

lemma degree_poly_lift[simp]: "degree (poly_lift p) = degree p"
  unfolding poly_lift_def by(rule degree_map_poly; auto)

lemma poly_lift_0[simp]: "poly_lift 0 = 0" unfolding poly_lift_def by simp

lemma poly_lift_0_iff[simp]: "poly_lift p = 0  p = 0"
  unfolding poly_lift_def by(induct p;simp)

lemma poly_lift_pCons[simp]:
  "poly_lift (pCons a p) = pCons [:a:] (poly_lift p)"
  unfolding poly_lift_def map_poly_simps by simp

lemma coeff_poly_lift[simp]:
  fixes p:: "'a :: comm_monoid_add poly"
  shows "coeff (poly_lift p) i = coeff_lift (coeff p i)"
  unfolding poly_lift_def by simp

lemma pcompose_conv_poly: "pcompose p q = poly (poly_lift p) q"
  by (induction p) auto

interpretation poly_lift_hom: inj_comm_monoid_add_hom poly_lift
proof-
  interpret map_poly_inj_comm_monoid_add_hom coeff_lift..
  show "inj_comm_monoid_add_hom poly_lift" by (unfold_locales, auto simp: poly_lift_def hom_distribs)
qed
interpretation poly_lift_hom: inj_comm_semiring_hom poly_lift
proof-
  interpret map_poly_inj_comm_semiring_hom coeff_lift..
  show "inj_comm_semiring_hom poly_lift" by (unfold_locales, auto simp add: poly_lift_def hom_distribs)
qed
interpretation poly_lift_hom: inj_comm_ring_hom poly_lift..
interpretation poly_lift_hom: inj_idom_hom poly_lift..

lemma (in comm_monoid_add_hom) map_poly_hom_coeff_lift[simp, hom_distribs]:
  "map_poly hom (coeff_lift a) = coeff_lift (hom a)" by (cases "a=0";simp)

lemma (in comm_ring_hom) map_poly_coeff_lift_hom:
  "map_poly (coeff_lift  hom) p = map_poly (map_poly hom) (map_poly coeff_lift p)"
proof (induct p)
  case (pCons a p) show ?case
    proof(cases "a = 0")
      case True
        hence "poly_lift p  0" using pCons(1) by simp
        thus ?thesis
          unfolding map_poly_pCons[OF pCons(1)]
          unfolding pCons(2) True by simp
      next case False
        hence "coeff_lift a  0" by simp
        thus ?thesis
        unfolding map_poly_pCons[OF pCons(1)]
        unfolding pCons(2) by simp
    qed
qed auto

lemma poly_poly_lift[simp]:
  fixes p :: "'a :: comm_semiring_0 poly"
  shows "poly (poly_lift p) [:x:] = [: poly p x :]"
proof (induct p)
  case 0 show ?case by simp
  next case (pCons a p) show ?case
    unfolding poly_lift_pCons
    unfolding poly_pCons
    unfolding pCons apply (subst mult.commute) by auto
qed

lemma degree_poly_lift2[simp]:
  "degree (poly_lift2 p) = degree p" unfolding poly_lift2_def by (induct p; auto)

lemma poly_lift2_0[simp]: "poly_lift2 0 = 0" unfolding poly_lift2_def by simp

lemma poly_lift2_0_iff[simp]: "poly_lift2 p = 0  p = 0"
  unfolding poly_lift2_def by(induct p;simp)

lemma poly_lift2_pCons[simp]:
  "poly_lift2 (pCons a p) = pCons [:[:a:]:] (poly_lift2 p)"
  unfolding poly_lift2_def map_poly_simps by simp

lemma poly_lift2_lift: "poly_lift2 = poly_lift  poly_lift" (is "?l = ?r")
proof
  fix p show "?l p = ?r p"
    unfolding poly_lift2_def coeff_lift2_lift poly_lift_def by (induct p; auto)
qed

lemma poly2_poly_lift[simp]: "poly2 (poly_lift p) x y = poly p y" by (induct p;simp)

lemma poly_lift2_nonzero:
  assumes "p  0" shows "poly_lift2 p  0"
  unfolding poly_lift2_def
  apply (subst map_poly_zero)
  using assms by auto

subsubsection ‹Swapping the Order of Variables›

definition
  "poly_y_x p  idegree p. jdegree (coeff p i). monom (monom (coeff (coeff p i) j) i) j"

lemma poly_y_x_fix_y_deg:
  assumes ydeg: "idegree p. degree (coeff p i)  d"
  shows "poly_y_x p = (idegree p. jd. monom (monom (coeff (coeff p i) j) i) j)"
    (is "_ = sum (λi. sum (?f i) _) _")
  unfolding poly_y_x_def
  apply (rule sum.cong,simp)
  unfolding atMost_iff
proof -
  fix i assume i: "i  degree p"
  let ?d = "degree (coeff p i)"
  have "{..d} = {..?d}  {Suc ?d .. d}" using ydeg[rule_format, OF i] by auto
  also have "sum (?f i) ... = sum (?f i) {..?d} + sum (?f i) {Suc ?d .. d}"
    by(rule sum.union_disjoint,auto)
  also { fix j
    assume j: "j  { Suc ?d .. d }"
    have "coeff (coeff p i) j = 0" apply (rule coeff_eq_0) using j by auto
    hence "?f i j = 0" by auto
  } hence "sum (?f i) {Suc ?d .. d} = 0" by auto
  finally show "sum (?f i) {..?d} = sum (?f i) {..d}" by auto
qed

lemma poly_y_x_fixed_deg:
  fixes p :: "'a :: comm_monoid_add poly poly"
  defines "d  Max { degree (coeff p i) | i. i  degree p }" 
  shows "poly_y_x p = (idegree p. jd. monom (monom (coeff (coeff p i) j) i) j)"
  apply (rule poly_y_x_fix_y_deg, intro allI impI)
  unfolding d_def
  by (subst Max_ge,auto)

lemma poly_y_x_swapped:
  fixes p :: "'a :: comm_monoid_add poly poly"
  defines "d  Max { degree (coeff p i) | i. i  degree p }" 
  shows "poly_y_x p = (jd. idegree p. monom (monom (coeff (coeff p i) j) i) j)"
  using poly_y_x_fixed_deg[of p, folded d_def] sum.swap by auto

lemma poly2_poly_y_x[simp]: "poly2 (poly_y_x p) x y = poly2 p y x"
  using [[unfold_abs_def = false]]
  apply(subst(3) poly_as_sum_of_monoms[symmetric])
  apply(subst poly_as_sum_of_monoms[symmetric,of "coeff p _"])
  unfolding poly_y_x_def
  unfolding coeff_sum monom_sum
  unfolding poly2_hom.hom_sum
  apply(rule sum.cong, simp)
  apply(rule sum.cong, simp)
  unfolding poly2_monom poly_monom
  unfolding mult.assoc
  unfolding mult.commute..

context begin
private lemma poly_monom_mult:
  fixes p :: "'a :: comm_semiring_1"
  shows "poly (monom p i * q ^ j) y = poly (monom p j * [:y:] ^ i) (poly q y)"
  unfolding poly_hom.hom_mult
  unfolding poly_monom
  apply(subst mult.assoc)
  apply(subst(2) mult.commute)
  by (auto simp: mult.assoc)

lemma poly_poly_y_x:
  fixes p :: "'a :: comm_semiring_1 poly poly"
  shows "poly (poly (poly_y_x p) q) y = poly (poly p [:y:]) (poly q y)"
  apply(subst(5) poly_as_sum_of_monoms[symmetric])
  apply(subst poly_as_sum_of_monoms[symmetric,of "coeff p _"])
  unfolding poly_y_x_def
  unfolding coeff_sum monom_sum
  unfolding poly_hom.hom_sum
  apply(rule sum.cong, simp)
  apply(rule sum.cong, simp)
  unfolding atMost_iff
  unfolding poly2_monom poly_monom
  apply(subst poly_monom_mult)..

end

interpretation poly_y_x_hom: zero_hom poly_y_x by (unfold_locales, auto simp: poly_y_x_def)
interpretation poly_y_x_hom: one_hom poly_y_x by (unfold_locales, auto simp: poly_y_x_def monom_0)


lemma map_poly_sum_commute:
  assumes "h 0 = 0" "p q. h (p + q) = h p + h q"
  shows "sum (λi. map_poly h (f i)) S = map_poly h (sum f S)"
  apply(induct S rule: infinite_finite_induct)
  using map_poly_add[OF assms] by auto

lemma poly_y_x_const: "poly_y_x [:p:] = poly_lift p" (is "?l = ?r")
proof -
  have "?l = (jdegree p. monom [:coeff p j:] j)"
    unfolding poly_y_x_def by (simp add: monom_0)
  also have "... = poly_lift (xdegree p. monom (coeff p x) x)"
    unfolding poly_lift_hom.hom_sum unfolding poly_lift_def by simp
  also have "... = poly_lift p" unfolding poly_as_sum_of_monoms..
  finally show ?thesis.
qed

lemma poly_y_x_pCons:
  shows "poly_y_x (pCons a p) = poly_lift a + map_poly (pCons 0) (poly_y_x p)"
proof(cases "p = 0")
  interpret ml: map_poly_comm_monoid_add_hom "coeff_lift"..
  interpret mc: map_poly_comm_monoid_add_hom "pCons 0"..
  interpret mm: map_poly_comm_monoid_add_hom "λx. monom x i" for i..
  { case False show ?thesis (* I know this is a worst kind of a proof... *)
      apply(subst(1) poly_y_x_fixed_deg)
      apply(unfold degree_pCons_eq[OF False])
      apply(subst(2) atLeast0AtMost[symmetric])
      apply(subst atLeastAtMost_insertL[OF le0,symmetric])
      apply(subst sum.insert,simp,simp)
      apply(unfold coeff_pCons_0)
      apply(unfold monom_0)
      apply(fold coeff_lift_hom.map_poly_hom_monom poly_lift_def)
      apply(fold poly_lift_hom.hom_sum)
      apply(subst poly_as_sum_of_monoms', subst Max_ge,simp,simp,force,simp)
      apply(rule cong[of "λx. poly_lift a + x", OF refl])
      apply(simp only: image_Suc_atLeastAtMost [symmetric])
      apply(unfold atLeast0AtMost)
      apply(subst sum.reindex,simp)
      apply(unfold o_def)
      apply(unfold coeff_pCons_Suc)
      apply(unfold monom_Suc)
      apply (subst poly_y_x_fix_y_deg[of _ "Max {degree (coeff (pCons a p) i) | i. i  Suc (degree p)}"])
       apply (intro allI impI)
       apply (rule Max.coboundedI)
      by (auto simp: hom_distribs intro: exI[of _ "Suc _"])
  }
  case True show ?thesis by (simp add: True poly_y_x_const)
qed

lemma poly_y_x_pCons_0: "poly_y_x (pCons 0 p) = map_poly (pCons 0) (poly_y_x p)"
proof(cases "p=0")
  case False
  interpret mc: map_poly_comm_monoid_add_hom "pCons 0"..
  interpret mm: map_poly_comm_monoid_add_hom "λx. monom x i" for i..
  from False show ?thesis
    apply (unfold poly_y_x_def degree_pCons_eq)
    apply (unfold sum.atMost_Suc_shift)
    by (simp add: hom_distribs monom_Suc)
qed simp

lemma poly_y_x_map_poly_pCons_0: "poly_y_x (map_poly (pCons 0) p) = pCons 0 (poly_y_x p)"
proof-
  let ?l = "λi j. monom (monom (coeff (pCons 0 (coeff p i)) j) i) j"
  let ?r = "λi j. pCons 0 (monom (monom (coeff (coeff p i) j) i) j)"
  have *: "(jdegree (pCons 0 (coeff p i)). ?l i j) = (jdegree (coeff p i). ?r i j)" for i
  proof(cases "coeff p i = 0")
    case True then show ?thesis by simp
  next
    case False
    show ?thesis
      apply (unfold degree_pCons_eq[OF False])
      apply (unfold sum.atMost_Suc_shift,simp)
      apply (fold monom_Suc)..
  qed
  show ?thesis
    apply (unfold poly_y_x_def)
    apply (unfold hom_distribs pCons_0_hom.degree_map_poly_hom pCons_0_hom.coeff_map_poly_hom)
    unfolding *..
qed

interpretation poly_y_x_hom: comm_monoid_add_hom "poly_y_x :: 'a :: comm_monoid_add poly poly  _"
proof (unfold_locales)
  fix p q :: "'a poly poly"
  show "poly_y_x (p + q) = poly_y_x p + poly_y_x q"
  proof (induct p arbitrary:q)
    case 0 show ?case by simp
  next
    case p: (pCons a p)
    show ?case
    proof (induct q)
      case q: (pCons b q)
      show ?case
      apply (unfold add_pCons)
      apply (unfold poly_y_x_pCons)
      apply (unfold p)
      by (simp add: poly_y_x_const ac_simps hom_distribs)
    qed auto
  qed
qed

text @{const poly_y_x} is bijective.›
lemma poly_y_x_poly_lift:
  fixes p :: "'a :: comm_monoid_add poly"
  shows "poly_y_x (poly_lift p) = [:p:]"
  apply(subst poly_y_x_fix_y_deg[of _ 0],force)
  apply(subst(10) poly_as_sum_of_monoms[symmetric])
  by (auto simp add: monom_sum monom_0 hom_distribs)

lemma poly_y_x_id[simp]:
  fixes p:: "'a :: comm_monoid_add poly poly"
  shows "poly_y_x (poly_y_x p) = p"
proof (induct p)
  case 0
  then show ?case by simp
next
  case (pCons a p)
  interpret mm: map_poly_comm_monoid_add_hom "λx. monom x i" for i..
  interpret mc: map_poly_comm_monoid_add_hom "pCons 0" ..
  have pCons_as_add: "pCons a p = [:a:] + pCons 0 p" by simp
  from pCons show ?case
    apply (unfold pCons_as_add)
    by (simp add: poly_y_x_pCons poly_y_x_poly_lift poly_y_x_map_poly_pCons_0 hom_distribs)
qed

interpretation poly_y_x_hom:
  bijective "poly_y_x :: 'a :: comm_monoid_add poly poly  _"
  by(unfold bijective_eq_bij, auto intro!:o_bij[of poly_y_x])

lemma inv_poly_y_x[simp]: "Hilbert_Choice.inv poly_y_x = poly_y_x" by auto

interpretation poly_y_x_hom: comm_monoid_add_isom poly_y_x
  by (unfold_locales, auto)

lemma pCons_as_add:
  fixes p :: "'a :: comm_semiring_1 poly"
  shows "pCons a p = [:a:] + monom 1 1 * p" by (auto simp: monom_Suc)

lemma mult_pCons_0: "(*) (pCons 0 1) = pCons 0" by auto

lemma pCons_0_as_mult:(*TODO: Move *)
  shows "pCons (0 :: 'a :: comm_semiring_1)  = (λp. pCons 0 1 * p)" by auto

lemma map_poly_pCons_0_as_mult:
  fixes p :: "'a :: comm_semiring_1 poly poly"
  shows "map_poly (pCons 0) p = [:pCons 0 1:] * p"
  apply (subst(1) pCons_0_as_mult)
  apply (fold smult_as_map_poly) by simp

lemma poly_y_x_monom:
  fixes a :: "'a :: comm_semiring_1 poly"
  shows "poly_y_x (monom a n) = smult (monom 1 n) (poly_lift a)"
proof (cases "a = 0")
  case True then show ?thesis by simp
next
  case False
  interpret map_poly_comm_monoid_add_hom "λx. c * x" for c :: "'a poly"..
  from False show ?thesis
    apply (unfold poly_y_x_def)
    apply (unfold degree_monom_eq)
    apply (subst(2) lessThan_Suc_atMost[symmetric])
    apply (unfold sum.lessThan_Suc)
    apply (subst sum.neutral,force)
    apply (subst(14) poly_as_sum_of_monoms[symmetric])
    apply (unfold smult_as_map_poly)
    by (auto simp: monom_altdef[unfolded x_as_monom x_pow_n,symmetric] hom_distribs)
qed

lemma poly_y_x_smult:
  fixes c :: "'a :: comm_semiring_1 poly"
  shows "poly_y_x (smult c p) = poly_lift c * poly_y_x p" (is "?l = ?r")
proof-
  have "smult c p = (idegree p. monom (coeff (smult c p) i) i)"
    by (metis (no_types, lifting) degree_smult_le poly_as_sum_of_monoms' sum.cong)
  also have "... = (idegree p. monom (c * coeff p i) i)"
    by auto
  also have "poly_y_x ... = poly_lift c * (idegree p. smult (monom 1 i) (poly_lift (coeff p i)))"
    by (simp add: poly_y_x_monom hom_distribs)
  also have "... = poly_lift c * poly_y_x (idegree p. monom (coeff p i) i)"
    by (simp add: poly_y_x_monom hom_distribs)
  finally show ?thesis by (simp add: poly_as_sum_of_monoms)
qed

interpretation poly_y_x_hom:
  comm_semiring_isom "poly_y_x :: 'a :: comm_semiring_1 poly poly  _"
proof
  fix p q :: "'a poly poly"
  show "poly_y_x (p * q) = poly_y_x p * poly_y_x q"
  proof (induct p)
    case (pCons a p)
    show ?case
      apply (unfold mult_pCons_left)
      apply (unfold hom_distribs)
      apply (unfold poly_y_x_smult)
      apply (unfold poly_y_x_pCons_0)
      apply (unfold pCons)
      by (simp add: poly_y_x_pCons map_poly_pCons_0_as_mult field_simps)
  qed simp
qed

interpretation poly_y_x_hom: comm_ring_isom "poly_y_x"..
interpretation poly_y_x_hom: idom_isom "poly_y_x"..

lemma Max_degree_coeff_pCons:
  "Max { degree (coeff (pCons a p) i) | i. i  degree (pCons a p)} =
   max (degree a) (Max {degree (coeff p x) |x. x  degree p})"
proof (cases "p = 0")
  case False show ?thesis
    unfolding degree_pCons_eq[OF False]
    unfolding image_Collect[symmetric]
    unfolding atMost_def[symmetric]
    apply(subst(1) atLeast0AtMost[symmetric])
    unfolding atLeastAtMost_insertL[OF le0,symmetric]
    unfolding image_insert
    apply(subst Max_insert,simp,simp)
    unfolding image_Suc_atLeastAtMost [symmetric]
    unfolding image_image
    unfolding atLeast0AtMost by simp
qed simp


lemma degree_poly_y_x:
  fixes p :: "'a :: comm_ring_1 poly poly"
  assumes "p  0"
  shows "degree (poly_y_x p) = Max { degree (coeff p i) | i. i  degree p }"
    (is "_ = ?d p")
  using assms
proof(induct p)
  interpret rhm: map_poly_comm_ring_hom coeff_lift ..
  let ?f = "λp i j. monom (monom (coeff (coeff p i) j) i) j"
  case (pCons a p)
    show ?case
    proof(cases "p=0")
      case True show ?thesis unfolding True unfolding poly_y_x_pCons by auto
      next case False
        note IH = pCons(2)[OF False]
        let ?a = "poly_lift a"
        let ?p = "map_poly (pCons 0) (poly_y_x p)"
        show ?thesis
        proof(cases rule:linorder_cases[of "degree ?a" "degree ?p"])
          case less
            have dle: "degree a  degree (poly_y_x p)"
              apply(rule le_trans[OF less_imp_le[OF less[simplified]]])
              using degree_map_poly_le by auto
            show ?thesis
              unfolding poly_y_x_pCons
              unfolding degree_add_eq_right[OF less]
              unfolding Max_degree_coeff_pCons
              unfolding IH[symmetric]
              unfolding max_absorb2[OF dle]
              apply (rule degree_map_poly) by auto
          next case equal
            have dega: "degree ?a = degree a" by auto
            have degp: "degree (poly_y_x p) = degree a"
              using equal[unfolded dega]
              using degree_map_poly[of "pCons 0" "poly_y_x p"] by auto
            have *: "degree (?a + ?p) = degree a"
            proof(cases "a = 0")
              case True show ?thesis using equal unfolding True by auto
              next case False show ?thesis
                apply(rule antisym)
                  apply(rule degree_add_le, simp, fold equal, simp)
                apply(rule le_degree)
                unfolding coeff_add
                using False
                by auto
            qed
            show ?thesis unfolding poly_y_x_pCons
              unfolding *
              unfolding Max_degree_coeff_pCons
              unfolding IH[symmetric]
              unfolding degp by auto
          next case greater
            have dge: "degree a  degree (poly_y_x p)"
              apply(rule le_trans[OF _ less_imp_le[OF greater[simplified]]])
              by auto
            show ?thesis
              unfolding poly_y_x_pCons
              unfolding degree_add_eq_left[OF greater]
              unfolding Max_degree_coeff_pCons
              unfolding IH[symmetric]
              unfolding max_absorb1[OF dge] by simp
       qed
   qed
qed auto

end

Theory Resultant

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
subsection ‹Resultant›

text ‹This theory contains 
  facts about resultants which are required for addition and multiplication
  of algebraic numbers.

  The results are taken from the textbook \cite[pages 227ff and 235ff]{AlgNumbers}.
› 

theory Resultant
imports
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" (* for lmpoly_base_conv *)
  Subresultants.Resultant_Prelim
  Berlekamp_Zassenhaus.Unique_Factorization_Poly
  Bivariate_Polynomials
begin

subsubsection ‹Sylvester matrices and vector representation of polynomials›

definition vec_of_poly_rev_shifted where
  "vec_of_poly_rev_shifted p n j 
   vec n (λi. if i  j  j  degree p + i then coeff p (degree p + i - j) else 0)"

lemma vec_of_poly_rev_shifted_dim[simp]: "dim_vec (vec_of_poly_rev_shifted p n j) = n"
  unfolding vec_of_poly_rev_shifted_def by auto

lemma col_sylvester:
  fixes p q
  defines "m  degree p" and "n  degree q"
  assumes j: "j < m+n"
  shows "col (sylvester_mat p q) j =
    vec_of_poly_rev_shifted p n j @v vec_of_poly_rev_shifted q m j" (is "?l = ?r")
proof
  note [simp] = m_def[symmetric] n_def[symmetric]
  show "dim_vec ?l = dim_vec ?r" by simp
  fix i assume "i < dim_vec ?r" hence i: "i < m+n" by auto
  show "?l $ i = ?r $ i"
    unfolding vec_of_poly_rev_shifted_def
    apply (subst index_col) using i apply simp using j apply simp
    apply (subst sylvester_index_mat) using i apply simp using j apply simp
    apply (cases "i < n") apply force using i by simp
qed

lemma inj_on_diff_nat2: "inj_on (λi. (n::nat) - i) {..n}" by (rule inj_onI, auto)

lemma image_diff_atMost: "(λi. (n::nat) - i) ` {..n} = {..n}" (is "?l = ?r")
  unfolding set_eq_iff
proof (intro allI iffI)
  fix x assume x: "x  ?r"
    thus "x  ?l" unfolding image_def mem_Collect_eq
    by(intro bexI[of _ "n-x"],auto)
qed auto

lemma sylvester_sum_mat_upper:
  fixes p q :: "'a :: comm_semiring_1 poly"
  defines "m  degree p" and "n  degree q"
  assumes i: "i < n"
  shows "(j<m+n. monom (sylvester_mat p q $$ (i,j)) (m + n - Suc j)) =
    monom 1 (n - Suc i) * p" (is "sum ?f _ = ?r")
proof -
  have n1: "n  1" using i by auto
  define ni1 where "ni1 = n-Suc i"
  hence ni1: "n-i = Suc ni1" using i by auto
  define l where "l = m+n-1"
  hence l: "Suc l = m+n" using n1 by auto
  let ?g = "λj. monom (coeff (monom 1 (n-Suc i) * p) j) j"
  let ?p = "λj. l-j"
  have "sum ?f {..<m+n} = sum ?f {..l}"
    unfolding l[symmetric] unfolding lessThan_Suc_atMost..
  also {
    fix j assume j: "jl"
    have "?f j = ((λj. monom (coeff (monom 1 (n-i) * p) (Suc j)) j)  ?p) j"
      apply(subst sylvester_index_mat2)
      using i j unfolding l_def m_def[symmetric] n_def[symmetric]
      by (auto simp add: Suc_diff_Suc)
    also have "... = (?g  ?p) j"
      unfolding ni1
      unfolding coeff_monom_Suc
      unfolding ni1_def
      using i by auto
    finally have "?f j = (?g  ?p) j".
  }
  hence "(jl. ?f j) = (jl. (?g?p) j)" using l by auto
  also have "... = (jl. ?g j)"
    unfolding l_def
    using sum.reindex[OF inj_on_diff_nat2,symmetric,unfolded image_diff_atMost].
  also have "degree ?r  l"
      using degree_mult_le[of "monom 1 (n-Suc i)" p]
      unfolding l_def m_def
      unfolding degree_monom_eq[OF one_neq_zero] using i by auto
    from poly_as_sum_of_monoms'[OF this]
    have "(jl. ?g j) = ?r".
  finally show ?thesis.
qed

lemma sylvester_sum_mat_lower:
  fixes p q :: "'a :: comm_semiring_1 poly"
  defines "m  degree p" and "n  degree q"
  assumes ni: "n  i" and imn: "i < m+n"
  shows "(j<m+n. monom (sylvester_mat p q $$ (i,j)) (m + n - Suc j)) =
    monom 1 (m + n - Suc i) * q" (is "sum ?f _ = ?r")
proof -
  define l where "l = m+n-1"
  hence l: "Suc l = m+n" using imn by auto
  define mni1 where "mni1 = m + n - Suc i"
  hence mni1: "m+n-i = Suc mni1" using imn by auto
  let ?g = "λj. monom (coeff (monom 1 (m + n - Suc i) * q) j) j"
  let ?p = "λj. l-j"
  have "sum ?f {..<m+n} = sum ?f {..l}"
    unfolding l[symmetric] unfolding lessThan_Suc_atMost..
  also {
    fix j assume j: "jl"
    have "?f j = ((λj. monom (coeff (monom 1 (m+n-i) * q) (Suc j)) j)  ?p) j"
      apply(subst sylvester_index_mat2)
      using ni imn j unfolding l_def m_def[symmetric] n_def[symmetric]
      by (auto simp add: Suc_diff_Suc)
    also have "... = (?g  ?p) j"
      unfolding mni1
      unfolding coeff_monom_Suc
      unfolding mni1_def..
    finally have "?f j = ...".
  }
  hence "(jl. ?f j) = (jl. (?g?p) j)" by auto
  also have "... = (jl. ?g j)"
    using sum.reindex[OF inj_on_diff_nat2,symmetric,unfolded image_diff_atMost].
  also have "degree ?r  l"
      using degree_mult_le[of "monom 1 (m+n-1-i)" q]
      unfolding l_def n_def[symmetric]
      unfolding degree_monom_eq[OF one_neq_zero] using ni imn by auto
    from poly_as_sum_of_monoms'[OF this]
    have "(jl. ?g j) = ?r".
  finally show ?thesis.
qed

definition "vec_of_poly p  let m = degree p in vec (Suc m) (λi. coeff p (m-i))"

definition "poly_of_vec v  let d = dim_vec v in i<d. monom (v $ (d - Suc i)) i"

lemma poly_of_vec_of_poly[simp]:
  fixes p :: "'a :: comm_monoid_add poly"
  shows "poly_of_vec (vec_of_poly p) = p"
  unfolding poly_of_vec_def vec_of_poly_def Let_def
  unfolding dim_vec
  unfolding lessThan_Suc_atMost
  using poly_as_sum_of_monoms[of p] by auto

lemma poly_of_vec_0[simp]: "poly_of_vec (0v n) = 0" unfolding poly_of_vec_def Let_def by auto

lemma poly_of_vec_0_iff[simp]:
  fixes v  :: "'a :: comm_monoid_add vec"
  shows "poly_of_vec v = 0  v = 0v (dim_vec v)" (is "?v = _  _ = ?z")
proof
  assume "?v = 0"
  hence "i{..<dim_vec v}. v $ (dim_vec v - Suc i) = 0"
    unfolding poly_of_vec_def Let_def
    by (subst sum_monom_0_iff[symmetric],auto)
  hence a: "i. i < dim_vec v  v $ (dim_vec v - Suc i) = 0" by auto
  { fix i assume "i < dim_vec v"
    hence "v $ i = 0" using a[of "dim_vec v - Suc i"] by auto
  }
  thus "v = ?z" by auto
  next assume r: "v = ?z"
  show "?v = 0" apply (subst r) by auto
qed

(* TODO: move, copied from no longer existing Cayley-Hamilton/Polynomial_extension *)
lemma degree_sum_smaller:
  assumes "n > 0" "finite A"
  shows "( x. x A  degree (f x) < n)  degree (xA. f x) < n"
  using ‹finite A
  by(induct rule: finite_induct)
    (simp_all add: degree_add_less assms)

lemma degree_poly_of_vec_less:
  fixes v :: "'a :: comm_monoid_add vec"
  assumes dim: "dim_vec v > 0"
  shows "degree (poly_of_vec v) < dim_vec v"
  unfolding poly_of_vec_def Let_def
  apply(rule degree_sum_smaller)
    using dim apply force
    apply force
  unfolding lessThan_iff
  by (metis degree_0 degree_monom_eq dim monom_eq_0_iff)

lemma coeff_poly_of_vec:
  "coeff (poly_of_vec v) i = (if i < dim_vec v then v $ (dim_vec v - Suc i) else 0)"
  (is "?l = ?r")
proof -
  have "?l = (x<dim_vec v. if x = i then v $ (dim_vec v - Suc x) else 0)" (is "_ = ?m")
    unfolding poly_of_vec_def Let_def coeff_sum coeff_monom ..
  also have " = ?r"
  proof (cases "i < dim_vec v")
    case False
    show ?thesis
      by (subst sum.neutral, insert False, auto)
  next
    case True
    show ?thesis
      by (subst sum.remove[of _ i], force, force simp: True, subst sum.neutral, insert True, auto)
  qed
  finally show ?thesis .
qed

lemma vec_of_poly_rev_shifted_scalar_prod:
  fixes p v
  defines "q  poly_of_vec v"
  assumes m[simp]: "degree p = m" and n: "dim_vec v = n"
  assumes j: "j < m+n"
  shows "vec_of_poly_rev_shifted p n (n+m-Suc j)  v = coeff (p * q) j" (is "?l = ?r")
proof -
  have id1: " i. m + i - (n + m - Suc j) = i + Suc j - n"
    using j by auto
  let ?g = "λ i. if i  n + m - Suc j  n - Suc j  i then coeff p (i + Suc j - n) *  v $ i else 0"
  have "?thesis = ((i = 0..<n. ?g i) =          
        (ij. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else 0)))" (is "_ = (?l = ?r)")
    unfolding vec_of_poly_rev_shifted_def coeff_mult m scalar_prod_def n q_def
      coeff_poly_of_vec 
    by (subst sum.cong, insert id1, auto)
  also have "..." 
  proof -
    have "?r = (ij. (if j - i < n then coeff p i * v $ (n - Suc (j - i)) else 0))" (is "_ = sum ?f _")
      by (rule sum.cong, auto)
    also have "sum ?f {..j} = sum ?f ({i. i  j  j - i < n}  {i. i  j  ¬ j - i < n})" 
      (is "_ = sum _ (?R1  ?R2)")
      by (rule sum.cong, auto)
    also have " = sum ?f ?R1 + sum ?f ?R2"
      by (subst sum.union_disjoint, auto)
    also have "sum ?f ?R2 = 0"
      by (rule sum.neutral, auto)
    also have "sum ?f ?R1 + 0 = sum (λ i. coeff p i * v $ (i + n - Suc j)) ?R1"
      (is "_ = sum ?F _")
      by (subst sum.cong, auto simp: ac_simps)
    also have " = sum ?F ((?R1  {..m})  (?R1 - {..m}))"
      (is "_ = sum _ (?R  ?R')")
      by (rule sum.cong, auto)
    also have " = sum ?F ?R + sum ?F ?R'"
      by (subst sum.union_disjoint, auto)
    also have "sum ?F ?R' = 0"
    proof -
      { 
        fix x
        assume "x > m" 
        from coeff_eq_0[OF this[folded m]]
        have "?F x = 0" by simp
      }
      thus ?thesis
        by (subst sum.neutral, auto)
    qed
    finally have r: "?r = sum ?F ?R" by simp

    have "?l = sum ?g ({i. i < n  i  n + m - Suc j  n - Suc j  i} 
       {i. i < n  ¬ (i  n + m - Suc j  n - Suc j  i)})" 
      (is "_ = sum _ (?L1  ?L2)")
      by (rule sum.cong, auto)
    also have " = sum ?g ?L1 + sum ?g ?L2"
      by (subst sum.union_disjoint, auto)
    also have "sum ?g ?L2 = 0"
      by (rule sum.neutral, auto)
    also have "sum ?g ?L1 + 0 = sum (λ i. coeff p (i + Suc j - n) * v $ i) ?L1"
      (is "_ = sum ?G _")
      by (subst sum.cong, auto)
    also have " = sum ?G (?L1  {i. i + Suc j - n  m}  (?L1 - {i. i + Suc j - n  m}))"
      (is "_ = sum _ (?L  ?L')")
      by (subst sum.cong, auto)
    also have " = sum ?G ?L + sum ?G ?L'"      
      by (subst sum.union_disjoint, auto)
    also have "sum ?G ?L' = 0"
    proof -
      {
        fix x
        assume "x + Suc j - n > m" 
        from coeff_eq_0[OF this[folded m]]
        have "?G x = 0" by simp
      }
      thus ?thesis
        by (subst sum.neutral, auto)
    qed
    finally have l: "?l = sum ?G ?L" by simp

    let ?bij = "λ i. i + n - Suc j"
    {
      fix x
      assume x: "j < m + n" "Suc (x + j) - n  m" "x < n" "n - Suc j  x" 
      define y where "y = x + Suc j - n"
      from x have "x + Suc j  n" by auto
      with x have xy: "x = ?bij y" unfolding y_def by auto
      from x have y: "y  ?R" unfolding y_def by auto
      have "x  ?bij ` ?R" unfolding xy using y by blast
    } note tedious = this
    show ?thesis unfolding l r
      by (rule sum.reindex_cong[of ?bij], insert j, auto simp: inj_on_def tedious)
  qed
  finally show ?thesis by simp
qed

lemma sylvester_vec_poly:
  fixes p q :: "'a :: comm_semiring_0 poly"
  defines "m  degree p"
      and "n  degree q"
  assumes v: "v  carrier_vec (m+n)"
  shows "poly_of_vec (transpose_mat (sylvester_mat p q) *v v) =
    poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q" (is "?l = ?r")
proof (rule poly_eqI)
  fix i
  note mn[simp] = m_def[symmetric] n_def[symmetric]
  let ?Tv = "transpose_mat (sylvester_mat p q) *v v"
  have dim: "dim_vec (vec_first v n) = n" "dim_vec (vec_last v m) = m" "dim_vec ?Tv = n + m" 
    using v by auto
  have if_distrib: " x y z. (if x then y else (0 :: 'a)) * z = (if x then y * z else 0)" 
    by auto
  show "coeff ?l i = coeff ?r i"
  proof (cases "i < m+n")
    case False
      hence i_mn: "i  m+n"
        and i_n: "x. x  i  x < n  x < n"
        and i_m: "x. x  i  x < m  x < m" by auto
      have "coeff ?r i =
            ( x < n. vec_first v n $ (n - Suc x) * coeff p (i - x)) +
            ( x < m. vec_last v m $ (m - Suc x) * coeff q (i - x))"
        (is "_ = sum ?f _ + sum ?g _")
        unfolding coeff_add coeff_mult Let_def 
        unfolding coeff_poly_of_vec dim if_distrib
        unfolding atMost_def
        apply(subst sum.inter_filter[symmetric],simp)
        apply(subst sum.inter_filter[symmetric],simp)
        unfolding mem_Collect_eq
        unfolding i_n i_m
        unfolding lessThan_def by simp
      also { fix x assume x: "x < n"
        have "coeff p (i-x) = 0"
          apply(rule coeff_eq_0) using i_mn x unfolding m_def by auto
        hence "?f x = 0" by auto
      } hence "sum ?f {..<n} = 0" by auto
      also { fix x assume x: "x < m"
        have "coeff q (i-x) = 0"
          apply(rule coeff_eq_0) using i_mn x unfolding n_def by auto
        hence "?g x = 0" by auto
      } hence "sum ?g {..<m} = 0" by auto
      finally have "coeff ?r i = 0" by auto
      also from False have "0 = coeff ?l i"
        unfolding coeff_poly_of_vec dim sum.distrib[symmetric] by auto
      finally show ?thesis by auto
    next case True
      hence "coeff ?l i = (transpose_mat (sylvester_mat p q) *v v) $ (n + m - Suc i)"
        unfolding coeff_poly_of_vec dim sum.distrib[symmetric] by auto
      also have "... = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i"
        apply(subst index_mult_mat_vec) using True apply simp
        apply(subst row_transpose) using True apply simp
        apply(subst col_sylvester)
        unfolding mn using True apply simp
        apply(subst vec_first_last_append[of v n m,symmetric]) using v apply(simp add: add.commute)
        apply(subst scalar_prod_append)
        apply (rule carrier_vecI,simp)+
        apply (subst vec_of_poly_rev_shifted_scalar_prod,simp,simp) using True apply simp
        apply (subst add.commute[of n m])
        apply (subst vec_of_poly_rev_shifted_scalar_prod,simp,simp) using True apply simp
        by simp
      also have "... =
        (xi. (if x < n then vec_first v n $ (n - Suc x) else 0) * coeff p (i - x)) +
        (xi. (if x < m then vec_last v m $ (m - Suc x) else 0) * coeff q (i - x))"
        unfolding coeff_poly_of_vec[of "vec_first v n",unfolded dim_vec_first,symmetric]
        unfolding coeff_poly_of_vec[of "vec_last v m",unfolded dim_vec_last,symmetric]
        unfolding coeff_mult[symmetric] by (simp add: mult.commute)
      also have "... = coeff ?r i"
        unfolding coeff_add coeff_mult Let_def
        unfolding coeff_poly_of_vec dim..
      finally show ?thesis.
  qed
qed
  
subsubsection ‹Homomorphism and Resultant›

text ‹Here we prove Lemma~7.3.1 of the textbook.›

lemma(in comm_ring_hom) resultant_sub_map_poly:
  fixes p q :: "'a poly"
  shows "hom (resultant_sub m n p q) = resultant_sub m n (map_poly hom p) (map_poly hom q)"
    (is "?l = ?r'")
proof -
  let ?mh = "map_poly hom"
  have "?l = det (sylvester_mat_sub m n (?mh p) (?mh q))"
    unfolding resultant_sub_def
    apply(subst sylvester_mat_sub_map[symmetric]) by auto
  thus ?thesis unfolding resultant_sub_def.
qed

(*
lemma (in comm_ring_hom) resultant_map_poly:
  fixes p q :: "'a poly"
    defines "p' ≡ map_poly hom p"
    defines "q' ≡ map_poly hom q"
    defines "m ≡ degree p"
    defines "n ≡ degree q"
    defines "m' ≡ degree p'"
    defines "n' ≡ degree q'"
    defines "r ≡ resultant p q"
    defines "r' ≡ resultant p' q'"
  shows "m' = m ⟹ n' = n ⟹ hom r = r'"
    and "m' = m ⟹ hom r = hom (coeff p m')^(n-n') * r'"
    and "m' ≠ m ⟹ n' = n ⟹
      hom r = (if even n then 1 else (-1)^(m-m')) * hom (coeff q n)^(m-m') * r'"
      (is "_ ⟹ _ ⟹ ?goal")
    and "m' ≠ m ⟹ n' ≠ n ⟹ hom r = 0"
proof -
  have m'm: "m' ≤ m" unfolding m_def m'_def p'_def using degree_map_poly_le by auto
  have n'n: "n' ≤ n" unfolding n_def n'_def q'_def using degree_map_poly_le by auto

  have coeffp'[simp]: "⋀i. coeff p' i = hom (coeff p i)" unfolding p'_def by auto
  have coeffq'[simp]: "⋀i. coeff q' i = hom (coeff q i)" unfolding q'_def by auto

  let ?f = "λi. (if even n then 1 else (-1)^i) * hom (coeff q n)^i"

  have "hom r = resultant_sub m n p' q'"
    unfolding r_def resultant_sub
    unfolding m_def n_def p'_def q'_def
    by(rule resultant_sub_map_poly)
  also have "... = ?f (m-m') * resultant_sub m' n p' q'"
    using resultant_sub_trim_upper[of p' "m-m'" n q',folded m'_def] m'm
    by (auto simp: power_minus[symmetric])
  also have "... = ?f (m-m') * hom (coeff p m')^(n-n') * r'"
    using resultant_sub_trim_lower[of m' q' "n-n'" p'] n'n
    unfolding r'_def resultant_sub m'_def n'_def by auto
  finally have main: "hom r = ?f (m-m') * hom (coeff p m')^(n-n') * r'" by auto

  { assume "m' = m"
    thus "hom r = hom (coeff p m')^(n-n') * r'" using main by auto
    thus "n' = n ⟹ hom r = r'" by auto
  }
  assume "m' ≠ m"
  hence m'm: "m' < m" using m'm by auto
  thus "n' = n ⟹ ?goal" using main by simp
  assume "n' ≠ n"
  hence "n' < n" using n'n by auto
  hence "hom (coeff q n) = 0"
    unfolding coeffq'[symmetric] unfolding n'_def by(rule coeff_eq_0)
  hence "hom (coeff q n) ^ (m-m') = 0" using m'm by (simp add: power_0_left)
  from main[unfolded this]
  show "hom r = 0" using power_0_Suc by auto
qed
*)
  
subsubsection‹Resultant as Polynomial Expression›
context begin
text ‹This context provides notions for proving Lemma 7.2.1 of the textbook.›

private fun mk_poly_sub where
  "mk_poly_sub A l 0 = A"
| "mk_poly_sub A l (Suc j) = mat_addcol (monom 1 (Suc j)) l (l-Suc j) (mk_poly_sub A l j)"

definition  "mk_poly A = mk_poly_sub (map_mat coeff_lift A) (dim_col A - 1) (dim_col A - 1)"

private lemma mk_poly_sub_dim[simp]:
  "dim_row (mk_poly_sub A l j) = dim_row A"
  "dim_col (mk_poly_sub A l j) = dim_col A"
  by (induct j,auto)

private lemma mk_poly_sub_carrier:
  assumes "A  carrier_mat nr nc" shows "mk_poly_sub A l j  carrier_mat nr nc"
  apply (rule carrier_matI) using assms by auto

private lemma mk_poly_dim[simp]:
  "dim_col (mk_poly A) = dim_col A"
  "dim_row (mk_poly A) = dim_row A"
  unfolding mk_poly_def by auto

private lemma mk_poly_sub_others[simp]:
  assumes "l  j'" and "i < dim_row A" and "j' < dim_col A"
  shows "mk_poly_sub A l j $$ (i,j') = A $$ (i,j')"
  using assms by (induct j; simp)

private lemma mk_poly_others[simp]:
  assumes i: "i < dim_row A" and j: "j < dim_col A - 1"
  shows "mk_poly A $$ (i,j) = [: A $$ (i,j) :]"
  unfolding mk_poly_def
  apply(subst mk_poly_sub_others)
  using i j by auto

private lemma mk_poly_delete[simp]:
  assumes i: "i < dim_row A"
  shows "mat_delete (mk_poly A) i (dim_col A - 1) = map_mat coeff_lift (mat_delete A i (dim_col A - 1))"
  apply(rule eq_matI) unfolding mat_delete_def by auto

private lemma col_mk_poly_sub[simp]:
  assumes "l  j'" and "j' < dim_col A"
  shows "col (mk_poly_sub A l j) j' = col A j'"
  by(rule eq_vecI; insert assms; simp)

private lemma det_mk_poly_sub:
  assumes A: "(A :: 'a :: comm_ring_1 poly mat)  carrier_mat n n" and i: "i < n"
  shows "det (mk_poly_sub A (n-1) i) = det A"
  using i
proof (induct i)
  case (Suc i)
    show ?case unfolding mk_poly_sub.simps
    apply(subst det_addcol[of _ n])
      using Suc apply simp
      using Suc apply simp
      apply (rule mk_poly_sub_carrier[OF A])
      using Suc by auto
qed simp

private lemma det_mk_poly:
  fixes A :: "'a :: comm_ring_1 mat"
  shows "det (mk_poly A) = [: det A :]"
proof (cases "dim_row A = dim_col A")
  case True
    define n where "n = dim_col A"
    have "map_mat coeff_lift A  carrier_mat (dim_row A) (dim_col A)" by simp
    hence sq: "map_mat coeff_lift A  carrier_mat (dim_col A) (dim_col A)" unfolding True.
    show ?thesis
    proof(cases "dim_col A = 0")
      case True thus ?thesis unfolding det_def by simp
      next case False thus ?thesis
      unfolding mk_poly_def
      by (subst det_mk_poly_sub[OF sq]; simp)
    qed
  next case False
    hence f2: "dim_row A = dim_col A  False" by simp
    hence f3: "dim_row (mk_poly A) = dim_col (mk_poly A)  False"
      unfolding mk_poly_dim by auto
    show ?thesis unfolding det_def unfolding f2 f3 if_False by simp
qed

private fun mk_poly2_row where
  "mk_poly2_row A d j pv 0 = pv"
| "mk_poly2_row A d j pv (Suc n) =
   mk_poly2_row A d j pv n |v n  pv $ n + monom (A$$(n,j)) d"

private fun mk_poly2_col where
  "mk_poly2_col A pv 0 = pv"
| "mk_poly2_col A pv (Suc m) =
   mk_poly2_row A m (dim_col A - Suc m) (mk_poly2_col A pv m) (dim_row A)"

private definition "mk_poly2 A  mk_poly2_col A (0v (dim_row A)) (dim_col A)"

private lemma mk_poly2_row_dim[simp]: "dim_vec (mk_poly2_row A d j pv i) = dim_vec pv"
  by(induct i arbitrary: pv, auto)

private lemma mk_poly2_col_dim[simp]: "dim_vec (mk_poly2_col A pv j) = dim_vec pv"
  by (induct j arbitrary: pv, auto)

private lemma mk_poly2_row:
  assumes n: "n  dim_vec pv"
  shows "mk_poly2_row A d j pv n $ i =
    (if i < n then pv $ i + monom (A $$ (i,j)) d else pv $ i)"
  using n
proof (induct n arbitrary: pv)
  case (Suc n) thus ?case
    unfolding mk_poly2_row.simps by (cases rule: linorder_cases[of "i" "n"],auto)
qed simp

private lemma mk_poly2_row_col:
  assumes dim[simp]: "dim_vec pv = n" "dim_row A = n" and j: "j < dim_col A"
  shows "mk_poly2_row A d j pv n = pv + map_vec (λa. monom a d) (col A j)"
  apply rule using mk_poly2_row[of _ pv] j by auto

private lemma mk_poly2_col:
  fixes pv :: "'a :: comm_semiring_1 poly vec" and A :: "'a mat"
  assumes i: "i < dim_row A" and dim: "dim_row A = dim_vec pv"
  shows "mk_poly2_col A pv j $ i = pv $ i + (j'<j. monom (A $$ (i, dim_col A - Suc j')) j')"
  using dim
proof (induct j arbitrary: pv)
  case (Suc j) show ?case
    unfolding mk_poly2_col.simps
    apply (subst mk_poly2_row)
      using Suc apply simp
    unfolding Suc(1)[OF Suc(2)]
    using i by (simp add: add.assoc)
qed simp

private lemma mk_poly2_pre:
  fixes A :: "'a :: comm_semiring_1 mat"
  assumes i: "i < dim_row A"
  shows "mk_poly2 A $ i = (j'<dim_col A. monom (A $$ (i, dim_col A - Suc j')) j')"
  unfolding mk_poly2_def
  apply(subst mk_poly2_col) using i by auto

private lemma mk_poly2:
  fixes A :: "'a :: comm_semiring_1 mat"
  assumes i: "i < dim_row A"
      and c: "dim_col A > 0"
  shows "mk_poly2 A $ i = (j'<dim_col A. monom (A $$ (i,j')) (dim_col A - Suc  j'))"
    (is "?l = sum ?f ?S")
proof -
  define l where "l = dim_col A - 1"
  have dim: "dim_col A = Suc l" unfolding l_def using i c by auto
  let ?g = "λj. l - j"
  have "?l = sum (?f  ?g) ?S" unfolding l_def mk_poly2_pre[OF i] by auto
  also have "... = sum ?f ?S"
    unfolding dim
    unfolding lessThan_Suc_atMost
    using sum.reindex[OF inj_on_diff_nat2,symmetric,unfolded image_diff_atMost].
  finally show ?thesis.
qed

private lemma mk_poly2_sylvester_upper:
  fixes p q :: "'a :: comm_semiring_1 poly"
  assumes i: "i < degree q"
  shows "mk_poly2 (sylvester_mat p q) $ i = monom 1 (degree q - Suc i) * p"
  apply (subst mk_poly2)
    using i apply simp using i apply simp
  apply (subst sylvester_sum_mat_upper[OF i,symmetric])
  apply (rule sum.cong)
    unfolding sylvester_mat_dim lessThan_Suc_atMost apply simp
  by auto

private lemma mk_poly2_sylvester_lower:
  fixes p q :: "'a :: comm_semiring_1 poly"
  assumes mi: "i  degree q" and imn: "i < degree p + degree q"
  shows "mk_poly2 (sylvester_mat p q) $ i = monom 1 (degree p + degree q - Suc i) * q"
  apply (subst mk_poly2)
    using imn apply simp using mi imn apply simp
  unfolding sylvester_mat_dim
  using sylvester_sum_mat_lower[OF mi imn]
  apply (subst sylvester_sum_mat_lower) using mi imn by auto

private lemma foo:
  fixes v :: "'a :: comm_semiring_1 vec"
  shows "monom 1 d v map_vec coeff_lift v = map_vec (λa. monom a d) v"
  apply (rule eq_vecI)
  unfolding index_map_vec index_col
  by (auto simp add: Polynomial.smult_monom)

private lemma mk_poly_sub_corresp:
  assumes dimA[simp]: "dim_col A = Suc l" and dimpv[simp]: "dim_vec pv = dim_row A"
      and j: "j < dim_col A"
  shows "pv + col (mk_poly_sub (map_mat coeff_lift A) l j) l =
    mk_poly2_col A pv (Suc j)"
proof(insert j, induct j)
  have le: "dim_row A  dim_vec pv" using dimpv by simp
  have l: "l < dim_col A" using dimA by simp
  { case 0 show ?case
      apply (rule eq_vecI)
      using mk_poly2_row[OF le]
      by (auto simp add: monom_0)
  }
  { case (Suc j)
      hence j: "j < dim_col A" by simp
      show ?case
        unfolding mk_poly_sub.simps
        apply(subst col_addcol)
          apply simp
         apply simp
        apply(subst(2) comm_add_vec)
          apply(rule carrier_vecI, simp)
         apply(rule carrier_vecI, simp)
        apply(subst assoc_add_vec[symmetric])
           apply(rule carrier_vecI, rule refl)
          apply(rule carrier_vecI, simp)
         apply(rule carrier_vecI, simp)
        unfolding Suc(1)[OF j]
        apply(subst(2) mk_poly2_col.simps)
        apply(subst mk_poly2_row_col)
           apply simp
          apply simp
        using Suc apply simp
        apply(subst col_mk_poly_sub)
        using Suc apply simp
        using Suc apply simp
        apply(subst col_map_mat)
        using dimA apply simp
        unfolding foo dimA by simp
  }
qed

private lemma col_mk_poly_mk_poly2:
  fixes A :: "'a :: comm_semiring_1 mat"
  assumes dim: "dim_col A > 0"
  shows "col (mk_poly A) (dim_col A - 1) = mk_poly2 A"
proof -
  define l where "l = dim_col A - 1"
  have dim: "dim_col A = Suc l" unfolding l_def using dim by auto
  show ?thesis
    unfolding mk_poly_def mk_poly2_def dim
    apply(subst mk_poly_sub_corresp[symmetric])
      apply(rule dim)
      apply simp
      using dim apply simp
    apply(subst left_zero_vec)
      apply(rule carrier_vecI) using dim apply simp
    apply simp
    done
qed

private lemma mk_poly_mk_poly2:
  fixes A :: "'a :: comm_semiring_1 mat"
  assumes dim: "dim_col A > 0" and i: "i < dim_row A"
  shows "mk_poly A $$ (i,dim_col A - 1) = mk_poly2 A $ i"
proof -
  have "mk_poly A $$ (i,dim_col A - 1) = col (mk_poly A) (dim_col A - 1) $ i"
    apply (subst index_col(1)) using dim i by auto
  also note col_mk_poly_mk_poly2[OF dim] 
  finally show ?thesis.
qed

lemma mk_poly_sylvester_upper:
  fixes p q :: "'a :: comm_ring_1 poly"
  defines "m  degree p" and "n  degree q"
  assumes i: "i < n"
  shows "mk_poly (sylvester_mat p q) $$ (i, m + n - 1) = monom 1 (n - Suc i) * p" (is "?l = ?r")
proof -
  let ?S = "sylvester_mat p q"
  have c: "m+n = dim_col ?S" and r: "m+n = dim_row ?S" unfolding m_def n_def by auto
  hence "dim_col ?S > 0" "i < dim_row ?S" using i by auto
  from mk_poly_mk_poly2[OF this]
  have "?l = mk_poly2 (sylvester_mat p q) $ i" unfolding m_def n_def by auto
  also have "... = ?r"
    apply(subst mk_poly2_sylvester_upper)
      using i unfolding n_def m_def by auto
  finally show ?thesis.
qed

lemma mk_poly_sylvester_lower:
  fixes p q :: "'a :: comm_ring_1 poly"
  defines "m  degree p" and "n  degree q"
  assumes ni: "n  i" and imn: "i < m+n"
  shows "mk_poly (sylvester_mat p q) $$ (i, m + n - 1) = monom 1 (m + n - Suc i) * q" (is "?l = ?r")
proof -
  let ?S = "sylvester_mat p q"
  have c: "m+n = dim_col ?S" and r: "m+n = dim_row ?S" unfolding m_def n_def by auto
  hence "dim_col ?S > 0" "i < dim_row ?S" using imn by auto
  from mk_poly_mk_poly2[OF this]
  have "?l = mk_poly2 (sylvester_mat p q) $ i" unfolding m_def n_def by auto
  also have "... = ?r"
    apply(subst mk_poly2_sylvester_lower)
      using ni imn unfolding n_def m_def by auto
  finally show ?thesis.
qed

text ‹The next lemma corresponds to Lemma 7.2.1.›
lemma resultant_as_poly:
  fixes p q :: "'a :: comm_ring_1 poly"
  assumes degp: "degree p > 0" and degq: "degree q > 0"
  shows "p' q'. degree p' < degree q  degree q' < degree p 
         [: resultant p q :] = p' * p + q' * q"
proof (intro exI conjI)
  define m where "m = degree p"
  define n where "n = degree q"
  define d where "d = dim_row (mk_poly (sylvester_mat p q))"
  define c where "c = (λi. coeff_lift (cofactor (sylvester_mat p q) i (m+n-1)))"
  define p' where "p' = (i<n. monom 1 (n - Suc i) * c i)"
  define q' where "q' = (i<m. monom 1 (m - Suc i) * c (n+i))"

  have degc: "i. degree (c i) = 0" unfolding c_def by auto

  have dmn: "d = m+n" and mnd: "m + n = d" unfolding d_def m_def n_def by auto
  have "[: resultant p q :] =
    (i<d. mk_poly (sylvester_mat p q) $$ (i,m+n-1) *
        cofactor (mk_poly (sylvester_mat p q)) i (m+n-1))"
    unfolding resultant_def
    unfolding det_mk_poly[symmetric]
    unfolding m_def n_def d_def
    apply(rule laplace_expansion_column[of _ _ "degree p + degree q - 1"])
     apply(rule carrier_matI) using degp by auto
  also { fix i assume i: "i<d"
    have d2: "d = dim_row (sylvester_mat p q)" unfolding d_def by auto
    have "cofactor (mk_poly (sylvester_mat p q)) i (m+n-1) =
      (- 1) ^ (i + (m+n-1)) * det (mat_delete (mk_poly (sylvester_mat p q)) i (m+n-1))"
      using cofactor_def.
    also have "... =
      (- 1) ^ (i+m+n-1) * coeff_lift (det (mat_delete (sylvester_mat p q) i (m+n-1)))"
      using mk_poly_delete[OF i[unfolded d2]] degp degq
      unfolding m_def n_def by (auto simp add: add.assoc)
    also have "i+m+n-1 = i+(m+n-1)" using i[folded mnd] by auto
    finally have "cofactor (mk_poly (sylvester_mat p q)) i (m+n-1) = c i"
      unfolding c_def cofactor_def hom_distribs by simp
  }
  hence "... = (i<d. mk_poly (sylvester_mat p q) $$ (i, m+n-1) * c i)"
    (is "_ = sum ?f _") by auto
  also have "... = sum ?f ({..<n}  {n ..<d})" unfolding dmn apply(subst ivl_disj_un(8)) by auto
  also have "... = sum ?f {..<n} + sum ?f {n..<d}" apply(subst sum.union_disjoint) by auto
  also { fix i assume i: "i < n"
    have "?f i = monom 1 (n - Suc i) * c i * p"
      unfolding m_def n_def
      apply(subst mk_poly_sylvester_upper)
      using i unfolding n_def by auto
  }
  hence "sum ?f {..<n} = p' * p" unfolding p'_def sum_distrib_right by auto 
  also { fix i assume i: "i  {n..<d}"
    have "?f i = monom 1 (m + n - Suc i) * c i * q"
      unfolding m_def n_def
      apply(subst mk_poly_sylvester_lower)
      using i unfolding dmn n_def m_def by auto
  }
  hence "sum ?f {n..<d} = (i=n..<d. monom 1 (m + n - Suc i) * c i) * q"
    (is "_ = sum ?h _ * _") unfolding sum_distrib_right by auto
  also have "{n..<d} = (λi. i+n) ` {0..<m}"
    by (simp add: dmn)
  also have "sum ?h ... = sum (?h  (λi. i+n)) {0..<m}"
    apply(subst sum.reindex[symmetric])
     apply (rule inj_onI) by auto
  also have "... = q'" unfolding q'_def apply(rule sum.cong) by (auto simp add: add.commute)
  finally show main: "[:resultant p q:] = p' * p + q' * q".
  show "degree p' < n"
    unfolding p'_def
    apply(rule degree_sum_smaller)
    using degq[folded n_def] apply force+
  proof -
    fix i assume i: "i  {..<n}"
    show "degree (monom 1 (n - Suc i) * c i) < n"
      apply (rule order.strict_trans1)
       apply (rule degree_mult_le)
      unfolding add.right_neutral degc
      apply (rule order.strict_trans1)
       apply (rule degree_monom_le) using i by auto
  qed
  show "degree q' < m"
    unfolding q'_def
    apply (rule degree_sum_smaller)
    using degp[folded m_def] apply force+
  proof -
    fix i assume i: "i  {..<m}"
    show "degree (monom 1 (m-Suc i) * c (n+i)) < m"
      apply (rule order.strict_trans1)
       apply (rule degree_mult_le)
      unfolding add.right_neutral degc
      apply (rule order.strict_trans1)
       apply (rule degree_monom_le) using i by auto
  qed
qed

end

subsubsection ‹Resultant as Nonzero Polynomial Expression›

lemma resultant_zero:
  fixes p q :: "'a :: comm_ring_1 poly"
  assumes deg: "degree p > 0  degree q > 0"
      and xp: "poly p x = 0" and xq: "poly q x = 0"
  shows "resultant p q = 0"
proof -
  { assume degp: "degree p > 0" and degq: "degree q > 0"
    obtain p' q' where "[: resultant p q :] = p' * p + q' * q"
      using resultant_as_poly[OF degp degq] by force
    hence "resultant p q = poly (p' * p + q' * q) x"
      using mpoly_base_conv(2)[of "resultant p q"] by auto
    also have "... = poly p x * poly p' x + poly q x * poly q' x"
      unfolding poly2_def by simp
    finally have ?thesis using xp xq by simp
  } moreover
  { assume degp: "degree p = 0"
    have p: "p = [:0:]" using xp degree_0_id[OF degp,symmetric] by (metis mpoly_base_conv(2))
    have ?thesis unfolding p using degp deg by simp
  } moreover
  { assume degq: "degree q = 0"
    have q: "q = [:0:]" using xq degree_0_id[OF degq,symmetric] by (metis mpoly_base_conv(2))
    have ?thesis unfolding q using degq deg by simp
  }
  ultimately show ?thesis by auto
qed

lemma poly_resultant_zero:
  fixes p q :: "'a :: comm_ring_1 poly poly"
  assumes deg: "degree p > 0  degree q > 0"
  assumes p0: "poly2 p x y = 0" and q0: "poly2 q x y = 0"
  shows "poly (resultant p q) x = 0"
proof -
  { assume "degree p > 0" "degree q > 0"
    from resultant_as_poly[OF this]
    obtain p' q' where "[: resultant p q :] = p' * p + q' * q" by force
    hence "resultant p q = poly (p' * p + q' * q) [:y:]"
      using mpoly_base_conv(2)[of "resultant p q"] by auto
    also have "poly ... x = poly2 p x y * poly2 p' x y + poly2 q x y * poly2 q' x y"
      unfolding poly2_def by simp
    finally have ?thesis unfolding p0 q0 by simp
  } moreover {
    assume degp: "degree p = 0"
    hence p: "p = [: coeff p 0 :]" by(subst degree_0_id[OF degp,symmetric],simp)
    hence "resultant p q = coeff p 0 ^ degree q" using resultant_const(1) by metis
    also have "poly ... x = poly (coeff p 0) x ^ degree q" by auto
    also have "... = poly2 p x y ^ degree q" unfolding poly2_def by(subst p, auto)
    finally have ?thesis unfolding p0 using deg degp zero_power by auto
  } moreover {
    assume degq: "degree q = 0"
    hence q: "q = [: coeff q 0 :]" by(subst degree_0_id[OF degq,symmetric],simp)
    hence "resultant p q = coeff q 0 ^ degree p" using resultant_const(2) by metis
    also have "poly ... x = poly (coeff q 0) x ^ degree p" by auto
    also have "... = poly2 q x y ^ degree p" unfolding poly2_def by(subst q, auto)
    finally have ?thesis unfolding q0 using deg degq zero_power by auto
  }
  ultimately show ?thesis by auto
qed

lemma resultant_as_nonzero_poly_weak:
  fixes p q :: "'a :: idom poly"
  assumes degp: "degree p > 0" and degq: "degree q > 0"
      and r0: "resultant p q  0"
  shows "p' q'. degree p' < degree q  degree q' < degree p 
         [: resultant p q :] = p' * p + q' * q  p'  0  q'  0"
proof -
  obtain p' q'
    where deg: "degree p' < degree q" "degree q' < degree p"
      and main: "[: resultant p q :] = p' * p + q' * q"
      using resultant_as_poly[OF degp degq] by auto
  have p0: "p  0" using degp by auto
  have q0: "q  0" using degq by auto
  show ?thesis
  proof (intro exI conjI notI)
    assume "p' = 0"
    hence "[: resultant p q :] = q' * q" using main by auto
    also hence d0: "0 = degree (q' * q)" by (metis degree_pCons_0)
      { assume "q'  0"
        hence "degree (q' * q) = degree q' + degree q"
          apply(rule degree_mult_eq) using q0 by auto
        hence False using d0 degq by auto
      } hence "q' = 0" by auto
    finally show False using r0 by auto
  next
    assume "q' = 0"
    hence "[: resultant p q :] = p' * p" using main by auto
    also
      hence d0: "0 = degree (p' * p)" by (metis degree_pCons_0)
      { assume "p'  0"
        hence "degree (p' * p) = degree p' + degree p"
          apply(rule degree_mult_eq) using p0 by auto
        hence False using d0 degp by auto
      } hence "p' = 0" by auto
    finally show False using r0 by auto
  qed fact+
qed

text ‹ Next lemma corresponds to Lemma 7.2.2 of the textbook ›

lemma resultant_as_nonzero_poly:
  fixes p q :: "'a :: idom poly"
  defines "m  degree p" and "n  degree q"
  assumes degp: "m > 0" and degq: "n > 0"
  shows "p' q'. degree p' < n  degree q' < m 
         [: resultant p q :] = p' * p + q' * q  p'  0  q'  0"
proof (cases "resultant p q = 0")
  case False
  thus ?thesis
    using resultant_as_nonzero_poly_weak degp degq
    unfolding m_def n_def by auto
next case True
  define S where "S = transpose_mat (sylvester_mat p q)"
  have S: "S  carrier_mat (m+n) (m+n)" unfolding S_def m_def n_def by auto
  have "det S = 0" using True
    unfolding resultant_def S_def apply (subst det_transpose) by auto
  then obtain v
    where v: "v  carrier_vec (m+n)" and v0: "v  0v (m+n)" and "S *v v = 0v (m+n)"
    using det_0_iff_vec_prod_zero[OF S] by auto
  hence "poly_of_vec (S *v v) = 0" by auto
  hence main: "poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q = 0"
    (is "?p * _ + ?q * _ = _")
    using sylvester_vec_poly[OF v[unfolded m_def n_def], folded m_def n_def S_def]
    by auto
  have split: "vec_first v n @v vec_last v m = v"
    using vec_first_last_append[simplified add.commute] v by auto
  show ?thesis
  proof(intro exI conjI)
    show "[: resultant p q :] = ?p * p + ?q * q" unfolding True using main by auto
    show "?p  0"
    proof
      assume p'0: "?p = 0"
      hence "?q * q = 0" using main by auto
      hence "?q = 0" using degq n_def by auto
      hence "vec_last v m = 0v m" unfolding poly_of_vec_0_iff by auto
      also have "vec_first v n @v ... = 0v (m+n)" using p'0 unfolding poly_of_vec_0_iff by auto
      finally have "v = 0v (m+n)" using split by auto
      thus False using v0 by auto
    qed
    show "?q  0"
    proof
      assume q'0: "?q = 0"
      hence "?p * p = 0" using main by auto
      hence "?p = 0" using degp m_def by auto
      hence "vec_first v n = 0v n" unfolding poly_of_vec_0_iff by auto
      also have "... @v vec_last v m = 0v (m+n)" using q'0 unfolding poly_of_vec_0_iff by auto
      finally have "v = 0v (m+n)" using split by auto
      thus False using v0 by auto
    qed
    show "degree ?p < n" using degree_poly_of_vec_less[of "vec_first v n"] using degq by auto
    show "degree ?q < m" using degree_poly_of_vec_less[of "vec_last v m"] using degp by auto
  qed
qed

text‹Corresponds to Lemma 7.2.3 of the textbook›

lemma resultant_zero_imp_common_factor:
  fixes p q :: "'a :: ufd poly"
  assumes deg: "degree p > 0  degree q > 0" and r0: "resultant p q = 0"
  shows "¬ coprime p q"
  unfolding neq0_conv[symmetric]
proof -
  { assume degp: "degree p > 0" and degq: "degree q > 0"
    assume cop: "coprime p q"
    obtain p' q' where "p' * p + q' * q = 0"
      and p': "degree p' < degree q" and q': "degree q' < degree p"
      and p'0: "p'  0" and q'0: "q'  0"
      using resultant_as_nonzero_poly[OF degp degq] r0 by auto
    hence "p' * p = - q' * q" by (simp add: eq_neg_iff_add_eq_0)
    
    from some_gcd.coprime_mult_cross_dvd[OF cop this]
    have "p dvd q'" by auto
    from dvd_imp_degree_le[OF this q'0]
    have "degree p  degree q'" by auto
    hence False using q' by auto
  }
  moreover
  { assume degp: "degree p = 0"
    then obtain x where "p = [:x:]" by (elim degree_eq_zeroE)
    moreover hence "resultant p q = x ^ degree q" using resultant_const by auto
      hence "x = 0" using r0 by auto
    ultimately have "p = 0" by auto
    hence ?thesis unfolding not_coprime_iff_common_factor
      by (metis deg degp dvd_0_right dvd_refl less_numeral_extra(3) poly_dvd_1)
  }
  moreover
  { assume degq: "degree q = 0"
    then obtain x where "q = [:x:]" by (elim degree_eq_zeroE)
    moreover hence "resultant p q = x ^ degree p" using resultant_const by auto
      hence "x = 0" using r0 by auto
    ultimately have "q = 0" by auto
    hence ?thesis unfolding not_coprime_iff_common_factor
      by (metis deg degq dvd_0_right dvd_refl less_numeral_extra(3) poly_dvd_1)
  }
  ultimately show ?thesis by auto
qed

lemma resultant_non_zero_imp_coprime:
  assumes nz: "resultant (f :: 'a :: field poly) g  0" 
  and nz': "f  0  g  0" 
shows "coprime f g" 
proof (cases "degree f = 0  degree g = 0")
  case False
  define r where "r = [:resultant f g:]" 
  from nz have r: "r  0" unfolding r_def by auto
  from False have "degree f > 0" "degree g > 0" by auto
  from resultant_as_nonzero_poly_weak[OF this nz]
  obtain p q where "degree p < degree g" "degree q < degree f" 
    and id: "r = p * f + q * g"
    and "p  0" "q  0" unfolding r_def by auto
  define h where "h = some_gcd f g"
  have "h dvd f" "h dvd g" unfolding h_def by auto
  then obtain j k where f: "f = h * j" and g: "g = h * k" unfolding dvd_def by auto
  from id[unfolded f g] have id: "h * (p * j + q * k) = r" by (auto simp: field_simps)
  from arg_cong[OF id, of degree] have "degree (h * (p * j + q * k)) = 0" 
    unfolding r_def by auto
  also have "degree (h * (p * j + q * k)) = degree h + degree (p * j + q * k)" 
    by (subst degree_mult_eq, insert id r, auto)
  finally have h: "degree h = 0" "h  0" using r id by auto
  thus ?thesis unfolding h_def using is_unit_iff_degree some_gcd.gcd_dvd_1 by blast
next
  case True
  thus ?thesis
  proof
    assume deg_g: "degree g = 0" 
    show ?thesis
    proof (cases "g = 0")
      case False
      then show ?thesis using divides_degree[of _ g, unfolded deg_g]
        by (simp add: is_unit_right_imp_coprime) 
    next
      case g: True
      then have "g = [:0:]" by auto
      from nz[unfolded this resultant_const] have "degree f = 0" by auto
      with nz' show ?thesis unfolding g by auto
    qed
  next
    assume deg_f: "degree f = 0" 
    show ?thesis
    proof (cases "f = 0")
      case False
      then show ?thesis using divides_degree[of _ f, unfolded deg_f]
        by (simp add: is_unit_left_imp_coprime) 
    next
      case f: True
      then have "f = [:0:]" by auto
      from nz[unfolded this resultant_const] have "degree g = 0" by auto
      with nz' show ?thesis unfolding f by auto
    qed
  qed
qed

end

Theory Algebraic_Numbers

(*  
    Author:       René Thiemann 
                  Akihisa Yamada
    Contributors: Manuel Eberl (algebraic integers)
    License:      BSD
*)
section ‹Algebraic Numbers: Addition and Multiplication›

text ‹This theory contains the remaining field operations for algebraic numbers, namely
  addition and multiplication.›

theory Algebraic_Numbers
  imports
  Algebraic_Numbers_Prelim
  Resultant
  Polynomial_Factorization.Polynomial_Divisibility
begin

interpretation coeff_hom: monoid_add_hom "λp. coeff p i" by (unfold_locales, auto)
interpretation coeff_hom: comm_monoid_add_hom "λp. coeff p i"..
interpretation coeff_hom: group_add_hom "λp. coeff p i"..
interpretation coeff_hom: ab_group_add_hom "λp. coeff p i"..
interpretation coeff_0_hom: monoid_mult_hom "λp. coeff p 0" by (unfold_locales, auto simp: coeff_mult)
interpretation coeff_0_hom: semiring_hom "λp. coeff p 0"..
interpretation coeff_0_hom: comm_monoid_mult_hom "λp. coeff p 0"..
interpretation coeff_0_hom: comm_semiring_hom "λp. coeff p 0"..

subsection ‹Addition of Algebraic Numbers›

definition "x_y  [: [: 0, 1 :], -1 :]"

definition "poly_x_minus_y p = poly_lift p p x_y"

lemma coeff_xy_power:
  assumes "k  n"
  shows  "coeff (x_y ^ n :: 'a :: comm_ring_1 poly poly) k =
          monom (of_nat (n choose (n - k)) * (- 1) ^ k) (n - k)"
proof -
  define X :: "'a poly poly" where "X = monom (monom 1 1) 0"
  define Y :: "'a poly poly" where "Y = monom (-1) 1"

  have [simp]: "monom 1 b * (-1) ^ k = monom ((-1)^k :: 'a) b" for b k
    by (auto simp: monom_altdef minus_one_power_iff)

  have "(X + Y) ^ n = (in. of_nat (n choose i) * X ^ i * Y ^ (n - i))"
    by (subst binomial_ring) auto
  also have " = (in. of_nat (n choose i) * monom (monom ((-1) ^ (n - i)) i) (n - i))"
    by (simp add: X_def Y_def monom_power mult_monom mult.assoc) 
  also have " = (in. monom (monom (of_nat (n choose i) * (-1) ^ (n - i)) i) (n - i))"
    by (simp add: of_nat_poly smult_monom)
  also have "coeff  k =
    (in. if n - i = k then monom (of_nat (n choose i) * (- 1) ^ (n - i)) i else 0)"
    by (simp add: of_nat_poly coeff_sum)
  also have " = (i{n-k}. monom (of_nat (n choose i) * (- 1) ^ (n - i)) i)"
    using k  n by (intro sum.mono_neutral_cong_right) auto
  also have "X + Y = x_y"
    by (simp add: X_def Y_def x_y_def monom_altdef)
  finally show ?thesis
    using k  n by simp
qed


text ‹The following polynomial represents the sum of two algebraic numbers.›

definition poly_add :: "'a :: comm_ring_1 poly  'a poly  'a poly" where
  "poly_add p q = resultant (poly_x_minus_y p) (poly_lift q)"

subsubsection @{term poly_add} has desired root›

interpretation poly_x_minus_y_hom:
  comm_ring_hom poly_x_minus_y by (unfold_locales; simp add: poly_x_minus_y_def hom_distribs)

lemma poly2_x_y[simp]:
  fixes x :: "'a :: comm_ring_1"
  shows "poly2 x_y x y = x - y" unfolding poly2_def by (simp add: x_y_def)

lemma degree_poly_x_minus_y[simp]:
  fixes p :: "'a::idom poly"
  shows "degree (poly_x_minus_y p) = degree p" unfolding poly_x_minus_y_def x_y_def by auto

lemma poly_x_minus_y_pCons[simp]:
  "poly_x_minus_y (pCons a p) = [:[: a :]:] + poly_x_minus_y p * x_y"
  unfolding poly_x_minus_y_def x_y_def by simp

lemma poly_poly_poly_x_minus_y[simp]:
  fixes p :: "'a :: comm_ring_1 poly"
  shows "poly (poly (poly_x_minus_y p) q) x = poly p (x - poly q x)"
  by (induct p; simp add: ring_distribs x_y_def)

lemma poly2_poly_x_minus_y[simp]:
  fixes p :: "'a :: comm_ring_1 poly"
  shows "poly2 (poly_x_minus_y p) x y = poly p (x-y)" unfolding poly2_def by simp

interpretation x_y_mult_hom: zero_hom_0 "λp :: 'a :: comm_ring_1 poly poly. x_y * p"
proof (unfold_locales)
  fix p :: "'a poly poly"
  assume "x_y * p = 0"
  then show "p = 0" apply (simp add: x_y_def)
    by (metis eq_neg_iff_add_eq_0 minus_equation_iff minus_pCons synthetic_div_unique_lemma)
qed

lemma x_y_nonzero[simp]: "x_y  0" by (simp add: x_y_def)

lemma degree_x_y[simp]: "degree x_y = 1" by (simp add: x_y_def)

interpretation x_y_mult_hom: inj_comm_monoid_add_hom "λp :: 'a :: idom poly poly. x_y * p"
proof (unfold_locales)
  show "x_y * p = x_y * q  p = q" for p q :: "'a poly poly"
  proof (induct p arbitrary:q)
    case 0
    then show ?case by simp
  next
    case p: (pCons a p)
    from p(3)[unfolded mult_pCons_right]
    have "x_y * (monom a 0 + pCons 0 1 * p) = x_y * q"
      apply (subst(asm) pCons_0_as_mult)
      apply (subst(asm) smult_prod) by (simp only: field_simps distrib_left)
    then have "monom a 0 + pCons 0 1 * p = q" by simp
    then show "pCons a p = q" using pCons_as_add by (simp add: monom_0 monom_Suc)
  qed
qed

interpretation poly_x_minus_y_hom: inj_idom_hom poly_x_minus_y
proof
  fix p :: "'a poly"
  assume 0: "poly_x_minus_y p = 0"
  then have "poly_lift p p x_y = 0" by (simp add: poly_x_minus_y_def)
  then show "p = 0"
  proof (induct p)
    case 0
    then show ?case by simp
  next
    case (pCons a p)
    note p = this[unfolded poly_lift_pCons pcompose_pCons]
    show ?case
    proof (cases "a=0")
      case a0: True
      with p have "x_y * poly_lift p p x_y = 0" by simp
      then have "poly_lift p p x_y = 0" by simp
      then show ?thesis using p by simp
    next
      case a0: False
      with p have p0: "p  0" by auto
      from p have "[:[:a:]:] = - x_y * poly_lift p p x_y" by (simp add: eq_neg_iff_add_eq_0)
      then have "degree [:[:a:]:] = degree (x_y * poly_lift p p x_y)" by simp
      also have "... = degree (x_y::'a poly poly) + degree (poly_lift p p x_y)"
        apply (subst degree_mult_eq)
          apply simp
         apply (subst pcompose_eq_0)
          apply (simp add: x_y_def)
         apply (simp add: p0)
        apply simp
       done
      finally have False by simp 
      then show ?thesis..
    qed
  qed
qed

lemma poly_add:
  fixes p q :: "'a ::comm_ring_1 poly"
  assumes q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0"
  shows "poly (poly_add p q) (x+y) = 0"
proof (unfold poly_add_def, rule poly_resultant_zero[OF disjI2])
  have "degree q > 0" using poly_zero q0 y by auto
  thus degq: "degree (poly_lift q) > 0" by auto
qed (insert x y, simp_all)


subsubsection @{const poly_add} is nonzero›

text ‹
  We first prove that @{const poly_lift} preserves factorization. The result will be essential
  also in the next section for division of algebraic numbers.
›

interpretation poly_lift_hom:
  unit_preserving_hom "poly_lift :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly  _"
proof
  fix x :: "'a poly"
  assume "poly_lift x dvd 1"
  then have "poly_y_x (poly_lift x) dvd poly_y_x 1"
    by simp
  then show "x dvd 1"
    by (auto simp add: poly_y_x_poly_lift)
qed

interpretation poly_lift_hom:
  factor_preserving_hom "poly_lift::'a::idom poly  'a poly poly"
proof unfold_locales
  fix p :: "'a poly"
  assume p: "irreducible p"
  show "irreducible (poly_lift p)"
  proof(rule ccontr)
    from p have p0: "p  0" and "¬ p dvd 1" by (auto dest: irreducible_not_unit)
    with poly_lift_hom.hom_dvd[of p 1] have p1: "¬ poly_lift p dvd 1" by auto
    assume "¬ irreducible (poly_lift p)"
    from this[unfolded irreducible_altdef,simplified] p0 p1
    obtain q where "q dvd poly_lift p" and pq: "¬ poly_lift p dvd q" and q: "¬ q dvd 1" by auto
    then obtain r where "q * r = poly_lift p" by (elim dvdE, auto)
    then have "poly_y_x (q * r) = poly_y_x (poly_lift p)" by auto
    also have "... = [:p:]" by (auto simp: poly_y_x_poly_lift monom_0)
    also have "poly_y_x (q * r) = poly_y_x q * poly_y_x r" by (auto simp: hom_distribs)
    finally have "... = [:p:]" by auto
    then have qp: "poly_y_x q dvd [:p:]" by (metis dvdI)
    from dvd_const[OF this] p0 have "degree (poly_y_x q) = 0" by auto
    from degree_0_id[OF this,symmetric] obtain s
      where qs: "poly_y_x q = [:s:]" by auto
    have "poly_lift s = poly_y_x (poly_y_x (poly_lift s))" by auto
      also have "... = poly_y_x [:s:]" by (auto simp: poly_y_x_poly_lift monom_0)
      also have "... = q" by (auto simp: qs[symmetric])
    finally have sq: "poly_lift s = q" by auto
    from qp[unfolded qs] have sp: "s dvd p" by (auto simp: const_poly_dvd)
    from irreducibleD'[OF p this] sq q pq show False by auto
  qed
qed

text ‹
  We now show that @{const poly_x_minus_y} is a factor-preserving homomorphism. This is
  essential for this section. This is easy since @{const poly_x_minus_y} can be represented
  as the composition of two factor-preserving homomorphisms.
›

lemma poly_x_minus_y_as_comp: "poly_x_minus_y = (λp. p p x_y)  poly_lift"
  by (intro ext, unfold poly_x_minus_y_def, auto)
context idom_isom begin
  sublocale comm_semiring_isom..
end

interpretation poly_x_minus_y_hom:
  factor_preserving_hom "poly_x_minus_y :: 'a :: idom poly  'a poly poly"
proof -
  have p p x_y p x_y = p for p :: 'a poly poly›
  proof (induction p)
    case 0
    show ?case
      by simp
  next
    case (pCons a p)
    then show ?case
      by (unfold x_y_def hom_distribs pcompose_pCons) simp
  qed
  then interpret x_y_hom: bijective "λp :: 'a poly poly. p p x_y"
    by (unfold bijective_eq_bij) (rule involuntory_imp_bij)
  interpret x_y_hom: idom_isom "λp :: 'a poly poly. p p x_y"
    by standard simp_all
  have ‹factor_preserving_hom (λp :: 'a poly poly. p p x_y)
    and ‹factor_preserving_hom (poly_lift :: 'a poly  'a poly poly)
    ..
  then show "factor_preserving_hom (poly_x_minus_y :: 'a poly  _)"
    by (unfold poly_x_minus_y_as_comp) (rule factor_preserving_hom_comp)
qed

text ‹
  Now we show that results of @{const poly_x_minus_y} and @{const poly_lift} are coprime.
›

lemma poly_y_x_const[simp]: "poly_y_x [:[:a:]:] = [:[:a:]:]" by (simp add: poly_y_x_def monom_0)

context begin

private abbreviation "y_x == [: [: 0, -1 :], 1 :]"

lemma poly_y_x_x_y[simp]: "poly_y_x x_y = y_x" by (simp add: x_y_def poly_y_x_def monom_Suc monom_0)

private lemma y_x[simp]: fixes x :: "'a :: comm_ring_1" shows "poly2 y_x x y = y - x"
  unfolding poly2_def by simp

private definition "poly_y_minus_x p  poly_lift p p y_x"

private lemma poly_y_minus_x_0[simp]: "poly_y_minus_x 0 = 0" by (simp add: poly_y_minus_x_def)

private lemma poly_y_minus_x_pCons[simp]:
  "poly_y_minus_x (pCons a p) = [:[: a :]:] + poly_y_minus_x p * y_x" by (simp add: poly_y_minus_x_def)

private lemma poly_y_x_poly_x_minus_y:
  fixes p :: "'a :: idom poly"
  shows "poly_y_x (poly_x_minus_y p) = poly_y_minus_x p"
  apply (induct p, simp)
  apply (unfold poly_x_minus_y_pCons hom_distribs) by simp

lemma degree_poly_y_minus_x[simp]:
  fixes p :: "'a :: idom poly"
  shows "degree (poly_y_x (poly_x_minus_y p)) = degree p" 
  by (simp add: poly_y_minus_x_def poly_y_x_poly_x_minus_y)

end

lemma dvd_all_coeffs_iff:
  fixes x :: "'a :: comm_semiring_1" (* No addition needed! *)
  shows "(pi  set (coeffs p). x dvd pi)  (i. x dvd coeff p i)" (is "?l = ?r")
proof-
  have "?r = (i{..degree p}  {Suc (degree p)..}. x dvd coeff p i)" by auto
  also have "... = (idegree p. x dvd coeff p i)" by (auto simp add: ball_Un coeff_eq_0)
  also have "... = ?l" by (auto simp: coeffs_def)
  finally show ?thesis..
qed

lemma primitive_imp_no_constant_factor:
  fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} poly"
  assumes pr: "primitive p" and F: "mset_factors F p" and fF: "f ∈# F"
  shows "degree f  0"
proof
  from F fF have irr: "irreducible f" and fp: "f dvd p" by (auto dest: mset_factors_imp_dvd)
  assume deg: "degree f = 0"
  then obtain f0 where f0: "f = [:f0:]" by (auto dest: degree0_coeffs)
  with fp have "[:f0:] dvd p" by simp
  then have "f0 dvd coeff p i" for i by (simp add: const_poly_dvd_iff)
  with primitiveD[OF pr] dvd_all_coeffs_iff have "f0 dvd 1" by (auto simp: coeffs_def)
  with f0 irr show False by auto
qed

lemma coprime_poly_x_minus_y_poly_lift:
  fixes p q :: "'a :: ufd poly"
  assumes degp: "degree p > 0" and degq: "degree q > 0"
    and pr: "primitive p"
  shows "coprime (poly_x_minus_y p) (poly_lift q)"
proof(rule ccontr)
  from degp have p: "¬ p dvd 1" by (auto simp: dvd_const)
  from degp have p0: "p  0" by auto
  from mset_factors_exist[of p, OF p0 p]
  obtain F where F: "mset_factors F p" by auto
  with poly_x_minus_y_hom.hom_mset_factors
  have pF: "mset_factors (image_mset poly_x_minus_y F) (poly_x_minus_y p)" by auto

  from degq have q: "¬ q dvd 1" by (auto simp: dvd_const)
  from degq have q0: "q  0" by auto
  from mset_factors_exist[OF q0 q]
  obtain G where G: "mset_factors G q" by auto
  with poly_lift_hom.hom_mset_factors
  have pG: "mset_factors (image_mset poly_lift G) (poly_lift q)" by auto

  assume "¬ coprime (poly_x_minus_y p) (poly_lift q)"
  from this[unfolded not_coprime_iff_common_factor]
  obtain r
  where rp: "r dvd (poly_x_minus_y p)"
    and rq: "r dvd (poly_lift q)"
    and rU: "¬ r dvd 1" by auto note poly_lift_hom.hom_dvd
  from rp p0 have r0: "r  0" by auto
  from mset_factors_exist[OF r0 rU]
  obtain H where H: "mset_factors H r" by auto
  then have "H  {#}" by auto
  then obtain h where hH: "h ∈# H" by fastforce
  with H mset_factors_imp_dvd have hr: "h dvd r" and h: "irreducible h" by auto
  from irreducible_not_unit[OF h] have hU: "¬ h dvd 1" by auto
  from hr rp have "h dvd (poly_x_minus_y p)" by (rule dvd_trans)
  from irreducible_dvd_imp_factor[OF this h pF] p0
  obtain f where f: "f ∈# F" and fh: "poly_x_minus_y f ddvd h" by auto
  from hr rq have "h dvd (poly_lift q)" by (rule dvd_trans)
  from irreducible_dvd_imp_factor[OF this h pG] q0
  obtain g where g: "g ∈# G" and gh: "poly_lift g ddvd h" by auto
  from fh gh have "poly_x_minus_y f ddvd poly_lift g" using ddvd_trans by auto
  then have "poly_y_x (poly_x_minus_y f) ddvd poly_y_x (poly_lift g)" by simp
  also have "poly_y_x (poly_lift g) = [:g:]" unfolding poly_y_x_poly_lift monom_0 by auto
  finally have ddvd: "poly_y_x (poly_x_minus_y f) ddvd [:g:]" by auto
  then have "degree (poly_y_x (poly_x_minus_y f)) = 0" by (metis degree_pCons_0 dvd_0_left_iff dvd_const)
  then have "degree f = 0" by simp
  with primitive_imp_no_constant_factor[OF pr F f] show False by auto
qed

lemma poly_add_nonzero:
  fixes p q :: "'a :: ufd poly"
  assumes p0: "p  0" and q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0"
      and pr: "primitive p"
  shows "poly_add p q  0"
proof
  have degp: "degree p > 0" using le_0_eq order_degree order_root p0 x by (metis gr0I)
  have degq: "degree q > 0" using le_0_eq order_degree order_root q0 y by (metis gr0I)
  assume 0: "poly_add p q = 0"
  from resultant_zero_imp_common_factor[OF _ this[unfolded poly_add_def]] degp
   and coprime_poly_x_minus_y_poly_lift[OF degp degq pr]
  show False by auto
qed


subsubsection ‹Summary for addition›

text ‹Now we lift the results to one that uses @{const ipoly}, by showing some homomorphism lemmas.›

lemma (in comm_ring_hom) map_poly_x_minus_y:
  "map_poly (map_poly hom) (poly_x_minus_y p) = poly_x_minus_y (map_poly hom p)"
proof-
  interpret mp: map_poly_comm_ring_hom hom..
  interpret mmp: map_poly_comm_ring_hom "map_poly hom"..
  show ?thesis
    apply (induct p, simp)
    apply(unfold x_y_def hom_distribs poly_x_minus_y_pCons, simp) done
qed

lemma (in comm_ring_hom) hom_poly_lift[simp]:
  "map_poly (map_poly hom) (poly_lift q) = poly_lift (map_poly hom q)"
proof -
  show ?thesis
    unfolding poly_lift_def
    unfolding map_poly_map_poly[of coeff_lift,OF coeff_lift_hom.hom_zero]
    unfolding map_poly_coeff_lift_hom by simp
qed


lemma lead_coeff_poly_x_minus_y:
  fixes p :: "'a::idom poly"
  shows "lead_coeff (poly_x_minus_y p) = [:lead_coeff p * ((- 1) ^ degree p):]" (is "?l = ?r")
proof-
  have "?l = Polynomial.smult (lead_coeff p) ((- 1) ^ degree p)"
    by (unfold poly_x_minus_y_def, subst lead_coeff_comp; simp add: x_y_def)
  also have "... = ?r" by (unfold hom_distribs, simp add: smult_as_map_poly[symmetric])
  finally show ?thesis.
qed

lemma degree_coeff_poly_x_minus_y:
  fixes p q :: "'a :: {idom, semiring_char_0} poly"
  shows "degree (coeff (poly_x_minus_y p) i) = degree p - i"
proof -
  consider "i = degree p" | "i > degree p" | "i < degree p"
    by force
  thus ?thesis
  proof cases
    assume "i > degree p"
    thus ?thesis by (subst coeff_eq_0) auto
  next
    assume "i = degree p"
    thus ?thesis using lead_coeff_poly_x_minus_y[of p]
      by (simp add: lead_coeff_poly_x_minus_y)
  next
    assume "i < degree p"
    define n where "n = degree p"
    have "degree (coeff (poly_x_minus_y p) i) =
            degree (jn. [:coeff p j:] * coeff (x_y ^ j) i)" (is "_ = degree (sum ?f _)")
      by (simp add: poly_x_minus_y_def pcompose_conv_poly poly_altdef coeff_sum n_def)
    also have "{..n} = insert n {..<n}"
      by auto
    also have "sum ?f  = ?f n + sum ?f {..<n}"
      by (subst sum.insert) auto
    also have "degree  = n - i"
    proof -
      have "degree (?f n) = n - i"
        using i < degree p by (simp add: n_def coeff_xy_power degree_monom_eq)
      moreover have "degree (sum ?f {..<n}) < n - i"
      proof (intro degree_sum_smaller)
        fix j assume "j  {..<n}"
        have "degree ([:coeff p j:] * coeff (x_y ^ j) i)  j - i"
        proof (cases "i  j")
          case True
          thus ?thesis
            by (auto simp: n_def coeff_xy_power degree_monom_eq)
        next
          case False
          hence "coeff (x_y ^ j :: 'a poly poly) i = 0"
            by (subst coeff_eq_0) (auto simp: degree_power_eq)
          thus ?thesis by simp
        qed
        also have " < n - i"
          using j  {..<n} i < degree p by (auto simp: n_def)
        finally show "degree ([:coeff p j:] * coeff (x_y ^ j) i) < n - i" .
      qed (use i < degree p in auto simp: n_def›)
      ultimately show ?thesis
        by (subst degree_add_eq_left) auto
    qed
    finally show ?thesis
      by (simp add: n_def)
  qed
qed

lemma coeff_0_poly_x_minus_y [simp]: "coeff (poly_x_minus_y p) 0 = p"
  by (induction p) (auto simp: poly_x_minus_y_def x_y_def)

lemma (in idom_hom) poly_add_hom:
  assumes p0: "hom (lead_coeff p)  0" and q0: "hom (lead_coeff q)  0"
  shows "map_poly hom (poly_add p q) = poly_add (map_poly hom p) (map_poly hom q)"
proof -
  interpret mh: map_poly_idom_hom..
  show ?thesis unfolding poly_add_def
    apply (subst mh.resultant_map_poly(1)[symmetric])
       apply (subst degree_map_poly_2)
       apply (unfold lead_coeff_poly_x_minus_y, unfold hom_distribs, simp add: p0)
      apply simp
     apply (subst degree_map_poly_2)
      apply (simp_all add: q0 map_poly_x_minus_y)
    done
qed

lemma(in zero_hom) hom_lead_coeff_nonzero_imp_map_poly_hom:
  assumes "hom (lead_coeff p)  0"
  shows "map_poly hom p  0"
proof
  assume "map_poly hom p = 0"
  then have "coeff (map_poly hom p) (degree p) = 0" by simp
  with assms show False by simp
qed

lemma ipoly_poly_add:
  fixes x y :: "'a :: idom"
  assumes p0: "(of_int (lead_coeff p) :: 'a)  0" and q0: "(of_int (lead_coeff q) :: 'a)  0"
      and x: "ipoly p x = 0" and y: "ipoly q y = 0"
  shows "ipoly (poly_add p q) (x+y) = 0"
  using assms of_int_hom.hom_lead_coeff_nonzero_imp_map_poly_hom[OF q0]
  by (auto intro: poly_add simp: of_int_hom.poly_add_hom[OF p0 q0])

lemma (in comm_monoid_gcd) gcd_list_eq_0_iff[simp]: "listgcd xs = 0  (x  set xs. x = 0)"
  by (induct xs, auto)

lemma primitive_field_poly[simp]: "primitive (p :: 'a :: field poly)  p  0"
  by (unfold primitive_iff_some_content_dvd_1,auto simp: dvd_field_iff coeffs_def)

lemma ipoly_poly_add_nonzero:
  fixes x y :: "'a :: field"
  assumes "p  0" and "q  0" and "ipoly p x = 0" and "ipoly q y = 0"
      and "(of_int (lead_coeff p) :: 'a)  0" and "(of_int (lead_coeff q) :: 'a)  0"
  shows "poly_add p q  0"
proof-
  from assms have "(of_int_poly (poly_add p q) :: 'a poly)  0"
    apply (subst of_int_hom.poly_add_hom,simp,simp)
    by (rule poly_add_nonzero, auto dest:of_int_hom.hom_lead_coeff_nonzero_imp_map_poly_hom)
  then show ?thesis by auto
qed

lemma represents_add:
  assumes x: "p represents x" and y: "q represents y"
  shows "(poly_add p q) represents (x + y)"
  using assms by (intro representsI ipoly_poly_add ipoly_poly_add_nonzero, auto)

subsection ‹Division of Algebraic Numbers›

definition poly_x_mult_y where
  [code del]: "poly_x_mult_y p  ( i  degree p. monom (monom (coeff p i) i) i)"

lemma coeff_poly_x_mult_y:
  shows "coeff (poly_x_mult_y p) i = monom (coeff p i) i" (is "?l = ?r")
proof(cases "degree p < i")
  case i: False
  have "?l = sum (λj. if j = i then (monom (coeff p j) j) else 0) {..degree p}"
   (is "_ = sum ?f ?A") by (simp add: poly_x_mult_y_def coeff_sum)
  also have "... = sum ?f {i}" using i by (intro sum.mono_neutral_right, auto)
  also have "... = ?f i" by simp
  also have "... = ?r" by auto
  finally show ?thesis.
next
  case True then show ?thesis by (auto simp: poly_x_mult_y_def coeff_eq_0 coeff_sum)
qed

lemma poly_x_mult_y_code[code]: "poly_x_mult_y p = (let cs = coeffs p
  in poly_of_list (map (λ (i, ai). monom ai i) (zip [0 ..< length cs] cs)))" 
  unfolding Let_def poly_of_list_def 
proof (rule poly_eqI, unfold coeff_poly_x_mult_y)
  fix n
  let ?xs = "zip [0..<length (coeffs p)] (coeffs p)" 
  let ?f = "(λ(i, ai). monom ai i)" 
  show "monom (coeff p n) n = coeff (Poly (map ?f ?xs)) n" 
  proof (cases "n < length (coeffs p)")
    case True
    hence n: "n < length (map ?f ?xs)" and nn: "n < length ?xs" 
      unfolding degree_eq_length_coeffs by auto
    show ?thesis unfolding coeff_Poly nth_default_nth[OF n] nth_map[OF nn]
      using True by (simp add: nth_coeffs_coeff)
  next
    case False
    hence id: "coeff (Poly (map ?f ?xs)) n = 0" unfolding coeff_Poly
      by (subst nth_default_beyond, auto)
    from False have "n > degree p  p = 0" unfolding degree_eq_length_coeffs by (cases n, auto)
    hence "monom (coeff p n) n = 0" using coeff_eq_0[of p n] by auto
    thus ?thesis unfolding id by simp
  qed
qed

definition poly_div :: "'a :: comm_ring_1 poly  'a poly  'a poly" where
  "poly_div p q = resultant (poly_x_mult_y p) (poly_lift q)"

text @{const poly_div} has desired roots.›

lemma poly2_poly_x_mult_y:
  fixes p :: "'a :: comm_ring_1 poly"
  shows "poly2 (poly_x_mult_y p) x y = poly p (x * y)"
  apply (subst(3) poly_as_sum_of_monoms[symmetric])
  apply (unfold poly_x_mult_y_def hom_distribs)
  by (auto simp: poly2_monom poly_monom power_mult_distrib ac_simps)

lemma poly_div:
  fixes p q :: "'a ::field poly"
  assumes q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0" and y0: "y  0"
  shows "poly (poly_div p q) (x/y) = 0"
proof (unfold poly_div_def, rule poly_resultant_zero[OF disjI2])
  have "degree q > 0" using poly_zero q0 y by auto
  thus degq: "degree (poly_lift q) > 0" by auto
qed (insert x y y0, simp_all add: poly2_poly_x_mult_y)


text @{const poly_div} is nonzero.›

interpretation poly_x_mult_y_hom: ring_hom "poly_x_mult_y :: 'a :: {idom,ring_char_0} poly  _"
  by (unfold_locales, auto intro: poly2_ext simp: poly2_poly_x_mult_y hom_distribs)

interpretation poly_x_mult_y_hom: inj_ring_hom "poly_x_mult_y :: 'a :: {idom,ring_char_0} poly  _"
proof
  let ?h = poly_x_mult_y
  fix f :: "'a poly"
  assume "?h f = 0"
  then have "poly2 (?h f) x 1 = 0" for x by simp
  from this[unfolded poly2_poly_x_mult_y]
  show "f = 0" by auto
qed

lemma degree_poly_x_mult_y[simp]:
  fixes p :: "'a :: {idom, ring_char_0} poly"
  shows "degree (poly_x_mult_y p) = degree p" (is "?l = ?r")
proof(rule antisym)
  show "?r  ?l" by (cases "p=0", auto intro: le_degree simp: coeff_poly_x_mult_y)
  show "?l  ?r" unfolding poly_x_mult_y_def
    by (auto intro: degree_sum_le le_trans[OF degree_monom_le])
qed

interpretation poly_x_mult_y_hom: unit_preserving_hom "poly_x_mult_y :: 'a :: field_char_0 poly  _"
proof(unfold_locales)
  let ?h = "poly_x_mult_y :: 'a poly  _"
  fix f :: "'a poly"
  assume unit: "?h f dvd 1"
  then have "degree (?h f) = 0" and "coeff (?h f) 0 dvd 1" unfolding poly_dvd_1 by auto
  then have deg: "degree f = 0" by (auto simp add: degree_monom_eq)
  with unit show "f dvd 1" by(cases "f = 0", auto)
qed

lemmas poly_y_x_o_poly_lift = o_def[of poly_y_x poly_lift, unfolded poly_y_x_poly_lift]

lemma irreducible_dvd_degree: assumes "(f::'a::field poly) dvd g"
 "irreducible g"
 "degree f > 0"
 shows "degree f = degree g"
  using assms
 by (metis irreducible_altdef degree_0 dvd_refl is_unit_field_poly linorder_neqE_nat poly_divides_conv0)

lemma coprime_poly_x_mult_y_poly_lift:
  fixes p q :: "'a :: field_char_0 poly"
  assumes degp: "degree p > 0" and degq: "degree q > 0"
    and nz: "poly p 0  0  poly q 0  0" 
  shows "coprime (poly_x_mult_y p) (poly_lift q)"
proof(rule ccontr)
  from degp have p: "¬ p dvd 1" by (auto simp: dvd_const)
  from degp have p0: "p  0" by auto
  from mset_factors_exist[of p, OF p0 p]
  obtain F where F: "mset_factors F p" by auto
  then have pF: "prod_mset (image_mset poly_x_mult_y F) = poly_x_mult_y p"
    by (auto simp: hom_distribs)

  from degq have q: "¬ is_unit q" by (auto simp: dvd_const)
  from degq have q0: "q  0" by auto
  from mset_factors_exist[OF q0 q]
  obtain G where G: "mset_factors G q" by auto
  with poly_lift_hom.hom_mset_factors
  have pG: "mset_factors (image_mset poly_lift G) (poly_lift q)" by auto
  from poly_y_x_hom.hom_mset_factors[OF this]
  have pG: "mset_factors (image_mset coeff_lift G) [:q:]"
    by (auto simp: poly_y_x_poly_lift monom_0 image_mset.compositionality poly_y_x_o_poly_lift)

  assume "¬ coprime (poly_x_mult_y p) (poly_lift q)"
  then have "¬ coprime (poly_y_x (poly_x_mult_y p)) (poly_y_x (poly_lift q))"
    by (simp del: coprime_iff_coprime)
  from this[unfolded not_coprime_iff_common_factor]
  obtain r
  where rp: "r dvd poly_y_x (poly_x_mult_y p)"
    and rq: "r dvd poly_y_x (poly_lift q)"
    and rU: "¬ r dvd 1" by auto
  from rp p0 have r0: "r  0" by auto
  from mset_factors_exist[OF r0 rU]
  obtain H where H: "mset_factors H r" by auto
  then have "H  {#}" by auto
  then obtain h where hH: "h ∈# H" by fastforce
  with H mset_factors_imp_dvd have hr: "h dvd r" and h: "irreducible h" by auto
  from irreducible_not_unit[OF h] have hU: "¬ h dvd 1" by auto
  from hr rp have "h dvd poly_y_x (poly_x_mult_y p)" by (rule dvd_trans)
  note this[folded pF,unfolded poly_y_x_hom.hom_prod_mset image_mset.compositionality]
  from prime_elem_dvd_prod_mset[OF h[folded prime_elem_iff_irreducible] this]
  obtain f where f: "f ∈# F" and hf: "h dvd poly_y_x (poly_x_mult_y f)" by auto
  have irrF: "irreducible f" using f F by blast
    from dvd_trans[OF hr rq] have "h dvd [:q:]" by (simp add: poly_y_x_poly_lift monom_0)
    from irreducible_dvd_imp_factor[OF this h pG] q0
    obtain g where g: "g ∈# G" and gh: "[:g:] dvd h" by auto
    from dvd_trans[OF gh hf] have *: "[:g:] dvd poly_y_x (poly_x_mult_y f)" using dvd_trans by auto
  show False
  proof (cases "poly f 0 = 0")
    case f_0: False
    from poly_hom.hom_dvd[OF *]
    have "g dvd poly (poly_y_x (poly_x_mult_y f)) [:0:]" by simp
    also have "... = [:poly f 0:]" by (intro poly_ext, fold poly2_def, simp add: poly2_poly_x_mult_y)
    also have "... dvd 1" using f_0 by auto
    finally have "g dvd 1".
    with g G show False by (auto elim!: mset_factorsE dest!: irreducible_not_unit)
  next
    case True
    hence "[:0,1:] dvd f" by (unfold dvd_iff_poly_eq_0, simp)
    from irreducible_dvd_degree[OF this irrF]
    have "degree f = 1" by auto
    from degree1_coeffs[OF this] True obtain c where c: "c  0" and f: "f = [:0,c:]" by auto
    from g G have irrG: "irreducible g" by auto
    from poly_hom.hom_dvd[OF *]
    have "g dvd poly (poly_y_x (poly_x_mult_y f)) 1" by simp
    also have " = f" by (auto simp: f poly_x_mult_y_code Let_def c poly_y_x_pCons map_poly_monom poly_monom poly_lift_def)
    also have " dvd [:0,1:]" unfolding f dvd_def using c 
      by (intro exI[of _ "[: inverse c :]"], auto)
    finally have g01: "g dvd [:0,1:]" .
    from divides_degree[OF this] irrG have "degree g = 1" by auto
    from degree1_coeffs[OF this] obtain a b where g: "g = [:b,a:]" and a: "a  0" by auto
    from g01[unfolded dvd_def] g obtain k where id: "[:0,1:] = g * k" by auto
    from id have 0: "g  0" "k  0" by auto
    from arg_cong[OF id, of degree] have "degree k = 0" unfolding degree_mult_eq[OF 0] 
      unfolding g using a by auto
    from degree0_coeffs[OF this] obtain kk where k: "k = [:kk:]" by auto
    from id[unfolded g k] a have "b = 0" by auto
    hence "poly g 0 = 0" by (auto simp: g)
    from True this nz f ∈# F g ∈# G F G
    show False by (auto dest!:mset_factors_imp_dvd elim:dvdE)
  qed
qed

lemma poly_div_nonzero:
  fixes p q :: "'a :: field_char_0 poly"
  assumes p0: "p  0" and q0: "q  0" and x: "poly p x = 0" and y: "poly q y = 0"
      and p_0: "poly p 0  0  poly q 0  0"
  shows "poly_div p q  0"
proof
  have degp: "degree p > 0" using le_0_eq order_degree order_root p0 x by (metis gr0I)
  have degq: "degree q > 0" using le_0_eq order_degree order_root q0 y by (metis gr0I)
  assume 0: "poly_div p q = 0"
  from resultant_zero_imp_common_factor[OF _ this[unfolded poly_div_def]] degp
   and coprime_poly_x_mult_y_poly_lift[OF degp degq] p_0
  show False by auto
qed

subsubsection ‹Summary for division›

text ‹Now we lift the results to one that uses @{const ipoly}, by showing some homomorphism lemmas.›

lemma (in inj_comm_ring_hom) poly_x_mult_y_hom:
  "poly_x_mult_y (map_poly hom p) = map_poly (map_poly hom) (poly_x_mult_y p)"
proof -
  interpret mh: map_poly_inj_comm_ring_hom..
  interpret mmh: map_poly_inj_comm_ring_hom "map_poly hom"..
  show ?thesis unfolding poly_x_mult_y_def by (simp add: hom_distribs)
qed

lemma (in inj_comm_ring_hom) poly_div_hom:
  "map_poly hom (poly_div p q) = poly_div (map_poly hom p) (map_poly hom q)"
proof -
  have zero: "x. hom x = 0  x = 0" by simp
  interpret mh: map_poly_inj_comm_ring_hom..
  show ?thesis unfolding poly_div_def mh.resultant_hom[symmetric]
    by (simp add: poly_x_mult_y_hom)
qed

lemma ipoly_poly_div:
  fixes x y :: "'a :: field_char_0"
  assumes "q  0" and "ipoly p x = 0" and "ipoly q y = 0" and "y  0"
  shows "ipoly (poly_div p q) (x/y) = 0"
  by (unfold of_int_hom.poly_div_hom, rule poly_div, insert assms, auto)

lemma ipoly_poly_div_nonzero:
  fixes x y :: "'a :: field_char_0"
  assumes "p  0" and "q  0" and "ipoly p x = 0" and "ipoly q y = 0" and "poly p 0  0  poly q 0  0"
  shows "poly_div p q  0"
proof-
  from assms have "(of_int_poly (poly_div p q) :: 'a poly)  0" using of_int_hom.poly_map_poly[of p]
    by (subst of_int_hom.poly_div_hom, subst poly_div_nonzero, auto) 
  then show ?thesis by auto
qed

lemma represents_div:
  fixes x y :: "'a :: field_char_0"
  assumes "p represents x" and "q represents y" and "poly q 0  0"
  shows "(poly_div p q) represents (x / y)"
  using assms by (intro representsI ipoly_poly_div ipoly_poly_div_nonzero, auto)


subsection ‹Multiplication of Algebraic Numbers›

definition poly_mult where "poly_mult p q  poly_div p (reflect_poly q)"

lemma represents_mult:
  assumes px: "p represents x" and qy: "q represents y" and q_0: "poly q 0  0" 
  shows "(poly_mult p q) represents (x * y)"
proof-
  from q_0 qy have y0: "y  0" by auto
  from represents_inverse[OF y0 qy] y0 px q_0
  have "poly_mult p q represents x / (inverse y)"
    unfolding poly_mult_def by (intro represents_div, auto)
  with y0 show ?thesis by (simp add: field_simps)
qed

subsection ‹Summary: Closure Properties of Algebraic Numbers›

lemma algebraic_representsI: "p represents x  algebraic x"
  unfolding represents_def algebraic_altdef_ipoly by auto

lemma algebraic_of_rat: "algebraic (of_rat x)"
  by (rule algebraic_representsI[OF poly_rat_represents_of_rat])

lemma algebraic_uminus: "algebraic x  algebraic (-x)"
  by (auto dest: algebraic_imp_represents_irreducible intro: algebraic_representsI represents_uminus)

lemma algebraic_inverse: "algebraic x  algebraic (inverse x)"
  using algebraic_of_rat[of 0]
  by (cases "x = 0", auto dest: algebraic_imp_represents_irreducible intro: algebraic_representsI represents_inverse)

lemma algebraic_plus: "algebraic x  algebraic y  algebraic (x + y)"
  by (auto dest!: algebraic_imp_represents_irreducible_cf_pos intro!: algebraic_representsI[OF represents_add])

lemma algebraic_div:
  assumes x: "algebraic x" and y: "algebraic y" shows "algebraic (x/y)"
proof(cases "y = 0  x = 0")
  case True
  then show ?thesis using algebraic_of_rat[of 0] by auto
next
  case False
  then have x0: "x  0" and y0: "y  0" by auto
  from x y obtain p q
  where px: "p represents x" and irr: "irreducible q" and qy: "q represents y"
    by (auto dest!: algebraic_imp_represents_irreducible)
  show ?thesis
    using False px represents_irr_non_0[OF irr qy]
    by (auto intro!: algebraic_representsI[OF represents_div] qy)
qed

lemma algebraic_times: "algebraic x  algebraic y  algebraic (x * y)"
  using algebraic_div[OF _ algebraic_inverse, of x y] by (simp add: field_simps)

lemma algebraic_root: "algebraic x  algebraic (root n x)"
proof -
  assume "algebraic x"
  then obtain p where p: "p represents x" by (auto dest: algebraic_imp_represents_irreducible_cf_pos)
  from 
    algebraic_representsI[OF represents_nth_root_neg_real[OF _ this, of n]]
    algebraic_representsI[OF represents_nth_root_pos_real[OF _ this, of n]]
    algebraic_of_rat[of 0]
  show ?thesis by (cases "n = 0", force, cases "n > 0", force, cases "n < 0", auto)
qed

lemma algebraic_nth_root: "n  0  algebraic x  y^n = x  algebraic y"
  by (auto dest: algebraic_imp_represents_irreducible_cf_pos intro: algebraic_representsI represents_nth_root)


subsection ‹More on algebraic integers›

(* TODO: this is actually equal to @{term "(-1)^(m*n)"}, but we need a bit more theory on
   permutations to show this with a reasonable amount of effort. *)
definition poly_add_sign :: "nat  nat  'a :: comm_ring_1" where
  "poly_add_sign m n = signof (λi. if i < n then m + i else if i < m + n then i - n else i)"