# Theory Algebraic_Numbers_Prelim

(*
Author:      René Thiemann
Sebastiaan Joosten
*)
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 ..."
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 "irreducible⇩d p"
proof(intro irreducible⇩dI 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)

"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: "irreducible⇩d 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 ≡ ∑i≤degree 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

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]

"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

"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 (∏a←as. [:- 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
*)
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-
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 ≡ ∑i≤degree p. ∑j≤degree (coeff p i). monom (monom (coeff (coeff p i) j) i) j"

lemma poly_y_x_fix_y_deg:
assumes ydeg: "∀i≤degree p. degree (coeff p i) ≤ d"
shows "poly_y_x p = (∑i≤degree p. ∑j≤d. 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 = (∑i≤degree p. ∑j≤d. 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 = (∑j≤d. ∑i≤degree 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 = (∑j≤degree p. monom [:coeff p j:] j)"
unfolding poly_y_x_def by (simp add: monom_0)
also have "... = poly_lift (∑x≤degree 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 *: "(∑j≤degree (pCons 0 (coeff p i)). ?l i j) = (∑j≤degree (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 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
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)

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 = (∑i≤degree 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 "... = (∑i≤degree p. monom (c * coeff p i) i)"
by auto
also have "poly_y_x ... = poly_lift c * (∑i≤degree 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 (∑i≤degree 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 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)
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 Max_degree_coeff_pCons
unfolding IH[symmetric]
unfolding max_absorb1[OF dge] by simp
qed
qed
qed auto

end


# Theory Resultant

(*
Author:      René Thiemann
*)
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: "j≤l" 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 "(∑j≤l. ?f j) = (∑j≤l. (?g∘?p) j)" using l by auto also have "... = (∑j≤l. ?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 "(∑j≤l. ?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: "j≤l"
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 "(∑j≤l. ?f j) = (∑j≤l. (?g∘?p) j)" by auto
also have "... = (∑j≤l. ?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 "(∑j≤l. ?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 (0⇩v 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 = 0⇩v (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 (∑x∈A. f x) < n"
using ‹finite A›
by(induct rule: finite_induct)

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) = (∑i≤j. 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 = (∑i≤j. (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 "... =
(∑x≤i. (if x < n then vec_first v n $(n - Suc x) else 0) * coeff p (i - x)) + (∑x≤i. (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 (0⇩v (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)
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)
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 ≠ 0⇩v (m+n)" and "S *⇩v v = 0⇩v (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 = 0⇩v m" unfolding poly_of_vec_0_iff by auto
also have "vec_first v n @⇩v ... = 0⇩v (m+n)" using p'0 unfolding poly_of_vec_0_iff by auto
finally have "v = 0⇩v (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 = 0⇩v n" unfolding poly_of_vec_0_iff by auto
also have "... @⇩v vec_last v m = 0⇩v (m+n)" using q'0 unfolding poly_of_vec_0_iff by auto
finally have "v = 0⇩v (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
Contributors: Manuel Eberl (algebraic integers)
*)
section ‹Algebraic Numbers: Addition and Multiplication›

text ‹This theory contains the remaining field operations for algebraic numbers, namely

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 = (∑i≤n. of_nat (n choose i) * X ^ i * Y ^ (n - i))"
by (subst binomial_ring) auto
also have "… = (∑i≤n. 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 "… = (∑i≤n. 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 =
(∑i≤n. 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

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 "... = (∀i≤degree 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

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

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]
next
assume "i < degree p"
define n where "n = degree p"
have "degree (coeff (poly_x_minus_y p) i) =
degree (∑j≤n. [: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

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

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)

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"
then show ?thesis by auto
qed

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)"

`