Theory Polynomial_Factorization.Square_Free_Factorization

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Square Free Factorization›

text ‹We implemented Yun's algorithm to perform a square-free factorization of a polynomial.
We further show properties of a square-free factorization, namely that the exponents in
the square-free factorization are exactly the orders of the roots. We also show that 
factorizing the result of square-free factorization further will again result in a 
square-free factorization, and that square-free factorizations can be lifted homomorphically.›

theory Square_Free_Factorization
imports 
  Matrix.Utility
  Polynomial_Irreducibility
  Order_Polynomial
  Fundamental_Theorem_Algebra_Factorized
  Polynomial_Interpolation.Ring_Hom_Poly
begin

definition square_free :: "'a :: comm_semiring_1 poly  bool" where 
  "square_free p = (p  0  ( q. degree q > 0  ¬ (q * q dvd p)))"

lemma square_freeI:  
  assumes " q. degree q > 0  q  0  q * q dvd p  False"
  and p: "p  0"
  shows "square_free p" unfolding square_free_def
proof (intro allI conjI[OF p] impI notI, goal_cases)
  case (1 q)
  from assms(1)[OF 1(1) _ 1(2)] 1(1) show False by (cases "q = 0", auto)
qed

lemma square_free_multD:
  assumes sf: "square_free (f * g)"
  shows "h dvd f  h dvd g  degree h = 0" "square_free f" "square_free g"
proof -
  from sf[unfolded square_free_def] have 0: "f  0" "g  0"
    and dvd: " q. q * q dvd f * g  degree q = 0" by auto
  then show "square_free f" "square_free g" by (auto simp: square_free_def)
  assume "h dvd f" "h dvd g"
  then have "h * h dvd f * g" by (rule mult_dvd_mono)
  from dvd[OF this] show "degree h = 0".
qed

lemma irreducibled_square_free:
  fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} poly"
  shows "irreducibled p  square_free p"
  by (metis degree_0 degree_mult_eq degree_mult_eq_0 irreducibledD(1) irreducibledD(2) irreducibled_dvd_smult irreducibled_smultI less_add_same_cancel2 not_gr_zero square_free_def)

lemma square_free_factor: assumes dvd: "a dvd p"
  and sf: "square_free p"
  shows "square_free a"
proof (intro square_freeI)
  fix q
  assume q: "degree q > 0" and "q * q dvd a"
  hence "q * q dvd p" using dvd dvd_trans sf square_free_def by blast
  with sf[unfolded square_free_def] q show False by auto
qed (insert dvd sf, auto simp: square_free_def)

lemma square_free_prod_list_distinct: 
  assumes sf: "square_free (prod_list us :: 'a :: idom poly)"
  and us: " u. u  set us  degree u > 0"
  shows "distinct us"
proof (rule ccontr)
  assume "¬ distinct us"
  from not_distinct_decomp[OF this] obtain xs ys zs u where
     "us = xs @ u # ys @ u # zs" by auto
  hence dvd: "u * u dvd prod_list us" and u: "u  set us" by auto
  from dvd us[OF u] sf have "prod_list us = 0" unfolding square_free_def by auto
  hence "0  set us" by (simp add: prod_list_zero_iff)
  from us[OF this] show False by auto
qed

definition separable where 
  "separable f = coprime f (pderiv f)" 

lemma separable_imp_square_free:
  assumes sep: "separable (f :: 'a::{field, factorial_ring_gcd, semiring_gcd_mult_normalize} poly)" 
  shows "square_free f" 
proof (rule ccontr)
  note sep = sep[unfolded separable_def]
  from sep have f0: "f  0" by (cases f, auto)
  assume "¬ square_free f"
  then obtain g where g: "degree g  0" and "g * g dvd f" using f0 unfolding square_free_def by auto
  then obtain h where f: "f = g * (g * h)" unfolding dvd_def by (auto simp: ac_simps)
  have "pderiv f = g * ((g * pderiv h + h * pderiv g) + h * pderiv g)" 
    unfolding f pderiv_mult[of g] by (simp add: field_simps)
  hence "g dvd pderiv f" unfolding dvd_def by blast
  moreover have "g dvd f" unfolding f dvd_def by blast
  ultimately have dvd: "g dvd (gcd f (pderiv f))" by simp
  have "gcd f (pderiv f)  0" using f0 by simp
  with g dvd have "degree (gcd f (pderiv f))  0"
    by (simp add: sep poly_dvd_1)
  hence "¬ coprime f (pderiv f)" by auto
  with sep show False by simp
qed

lemma square_free_rsquarefree: assumes f: "square_free f" 
  shows "rsquarefree f"
  unfolding rsquarefree_def
proof (intro conjI allI)
  fix x
  show "order x f = 0  order x f = 1"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then obtain n where ord: "order x f = Suc (Suc n)" 
      by (cases "order x f"; cases "order x f - 1"; auto)
    define p where "p = [:-x,1:]"
    from order_divides[of x "Suc (Suc 0)" f, unfolded ord]
    have "p * p dvd f" "degree p  0" unfolding p_def by auto
    hence "¬ square_free f" using f(1) unfolding square_free_def by auto
    with assms show False by auto
  qed
qed (insert f, auto simp: square_free_def)

lemma square_free_prodD: 
  fixes fs :: "'a :: {field,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly set"
  assumes sf: "square_free ( fs)"
  and fin: "finite fs"
  and f: "f  fs"
  and g: "g  fs"
  and fg: "f  g"
  shows "coprime f g"
proof -
  have "( fs) = f * ( (fs - {f}))"
    by (rule prod.remove[OF fin f])
  also have "( (fs - {f})) = g * ( (fs - {f} - {g}))"
    by (rule prod.remove, insert fin g fg, auto)
  finally obtain k where sf: "square_free (f * g * k)" using sf by (simp add: ac_simps)
  from sf[unfolded square_free_def] have 0: "f  0" "g  0" 
    and dvd: " q. q * q dvd f * g * k  degree q = 0"
    by auto
  have "gcd f g * gcd f g dvd f * g * k" by (simp add: mult_dvd_mono)
  from dvd[OF this] have "degree (gcd f g) = 0" . 
  moreover have "gcd f g  0" using 0 by auto
  ultimately show "coprime f g" using is_unit_gcd[of f g] is_unit_iff_degree[of "gcd f g"] by simp    
qed

lemma rsquarefree_square_free_complex: assumes "rsquarefree (p :: complex poly)"
  shows "square_free p"
proof (rule square_freeI)
  fix q
  assume d: "degree q > 0" and dvd: "q * q dvd p"
  from d have "¬ constant (poly q)" by (simp add: constant_degree)
  from fundamental_theorem_of_algebra[OF this] obtain x where "poly q x = 0" by auto
  hence "[:-x,1:] dvd q" by (simp add: poly_eq_0_iff_dvd)
  then obtain k where q: "q = [:-x,1:] * k" unfolding dvd_def by auto
  from dvd obtain l where p: "p = q * q * l" unfolding dvd_def by auto
  from p[unfolded q] have "p = [:-x,1:]^2 * (k * k * l)" by algebra
  hence "[:-x,1:]^2 dvd p" unfolding dvd_def by blast
  from this[unfolded order_divides] have "p = 0  ¬ order x p  1" by auto
  thus False using assms unfolding rsquarefree_def' by auto
qed (insert assms, auto simp: rsquarefree_def)
   
lemma square_free_separable_main:
  fixes f :: "'a :: {field,factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
  assumes "square_free f"
  and sep: "¬ separable f"
  shows " g k. f = g * k  degree g  0  pderiv g = 0"
proof -
  note cop = sep[unfolded separable_def]
  from assms have f: "f  0" unfolding square_free_def by auto
  let ?g = "gcd f (pderiv f)"
  define G where "G = ?g"
  from poly_gcd_monic[of f "pderiv f"] f have mon: "monic ?g"
    by auto
  have deg: "degree G > 0" 
  proof (cases "degree G")
    case 0
    from degree0_coeffs[OF this] cop mon show ?thesis
      by (auto simp: G_def coprime_iff_gcd_eq_1)
  qed auto
  have gf: "G dvd f" unfolding G_def by auto
  have gf': "G dvd pderiv f" unfolding G_def by auto
  from irreducibled_factor[OF deg] obtain g r where g: "irreducible g" and G: "G = g * r" by auto
  from gf have gf: "g dvd f" unfolding G by (rule dvd_mult_left)
  from gf' have gf': "g dvd pderiv f" unfolding G by (rule dvd_mult_left)
  have g0: "degree g  0" using g unfolding irreducibled_def by auto
  from gf obtain k where fgk: "f = g * k" unfolding dvd_def by auto
  have id1: "pderiv f = g * pderiv k + k * pderiv g" unfolding fgk pderiv_mult by simp
  from gf' obtain h where "pderiv f = g * h" unfolding dvd_def by auto
  from id1[unfolded this] have "k * pderiv g = g * (h - pderiv k)" by (simp add: field_simps)
  hence dvd: "g dvd k * pderiv g" unfolding dvd_def by auto
  {
    assume "g dvd k" 
    then obtain h where k: "k = g * h" unfolding dvd_def by auto
    with fgk have "g * g dvd f" by auto
    with g0 have "¬ square_free f" unfolding square_free_def using f by auto
    with assms have False by simp
  }
  with  g dvd 
  have "g dvd pderiv g" by auto
  from divides_degree[OF this] degree_pderiv_le[of g] g0
  have "pderiv g = 0" by linarith
  with fgk g0 show ?thesis by auto
qed

lemma square_free_imp_separable: fixes f :: "'a :: {field_char_0,factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
  assumes "square_free f"
  shows "separable f"
proof (rule ccontr)
  assume "¬ separable f" 
  from square_free_separable_main[OF assms this]
  obtain g k where *: "f = g * k" "degree g  0" "pderiv g = 0" by auto
  hence "g dvd pderiv g" by auto
  thus False unfolding dvd_pderiv_iff using * by auto
qed
   

lemma square_free_iff_separable: 
  "square_free (f :: 'a :: {field_char_0,factorial_ring_gcd,semiring_gcd_mult_normalize} poly) = separable f"
  using separable_imp_square_free[of f] square_free_imp_separable[of f] by auto

context
  assumes "SORT_CONSTRAINT('a::{field,factorial_ring_gcd})"
begin
lemma square_free_smult: "c  0  square_free (f :: 'a poly)  square_free (smult c f)"
  by (unfold square_free_def, insert dvd_smult_cancel[of _ c], auto)

lemma square_free_smult_iff[simp]: "c  0  square_free (smult c f) = square_free (f :: 'a poly)"
  using square_free_smult[of c f] square_free_smult[of "inverse c" "smult c f"] by auto
end

context
  assumes "SORT_CONSTRAINT('a::factorial_ring_gcd)"
begin
definition square_free_factorization :: "'a poly  'a × ('a poly × nat) list  bool" where
  "square_free_factorization p cbs  case cbs of (c,bs) 
    (p = smult c ((a, i) set bs. a ^ i))
   (p = 0  c = 0  bs = [])
   ( a i. (a,i)  set bs  square_free a  degree a > 0  i > 0)
   ( a i b j. (a,i)  set bs  (b,j)  set bs  (a,i)  (b,j)  coprime a b)
   distinct bs"

lemma square_free_factorizationD: assumes "square_free_factorization p (c,bs)"
  shows "p = smult c ((a, i) set bs. a ^ i)"
  "(a,i)  set bs  square_free a  degree a  0  i > 0"
  "(a,i)  set bs  (b,j)  set bs  (a,i)  (b,j)  coprime a b"
  "p = 0  c = 0  bs = []"
  "distinct bs"
  using assms unfolding square_free_factorization_def split by blast+

lemma square_free_factorization_prod_list: assumes "square_free_factorization p (c,bs)"
  shows "p = smult c (prod_list (map (λ (a,i). a ^ i) bs))"
proof -
  note sff = square_free_factorizationD[OF assms]
  show ?thesis unfolding sff(1) 
    by (simp add: prod.distinct_set_conv_list[OF sff(5)])
qed
end

subsection ‹Yun's factorization algorithm›
locale yun_gcd = 
  fixes Gcd :: "'a :: factorial_ring_gcd poly  'a poly  'a poly"
begin

partial_function (tailrec) yun_factorization_main :: 
  "'a poly  'a poly 
    nat  ('a poly × nat)list  ('a poly × nat)list" where
  [code]: "yun_factorization_main bn cn i sqr = (
    if bn = 1 then sqr
    else (
    let 
      dn = cn - pderiv bn;
      an = Gcd bn dn
    in yun_factorization_main (bn div an) (dn div an) (Suc i) ((an,Suc i) # sqr)))"

definition yun_monic_factorization :: "'a poly  ('a poly × nat)list" where
  "yun_monic_factorization p = (let
    pp = pderiv p;
    u = Gcd p pp;
    b0 = p div u;
    c0 = pp div u
    in 
      (filter (λ (a,i). a  1) (yun_factorization_main b0 c0 0 [])))"

definition square_free_monic_poly :: "'a poly  'a poly" where
  "square_free_monic_poly p = (p div (Gcd p (pderiv p)))"
end

declare yun_gcd.yun_monic_factorization_def [code] 
declare yun_gcd.yun_factorization_main.simps [code] 
declare yun_gcd.square_free_monic_poly_def [code]

context 
  fixes Gcd :: "'a :: {field_char_0,euclidean_ring_gcd} poly  'a poly  'a poly"
begin
interpretation yun_gcd Gcd .

definition square_free_poly :: "'a poly  'a poly" where
  "square_free_poly p = (if p = 0 then 0 else 
     square_free_monic_poly (smult (inverse (coeff p (degree p))) p))"


definition yun_factorization :: "'a poly  'a × ('a poly × nat)list" where
  "yun_factorization p = (if p = 0
    then (0,[]) else (let 
      c = coeff p (degree p);
      q = smult (inverse c) p
    in (c, yun_monic_factorization q)))"

lemma yun_factorization_0[simp]: "yun_factorization 0 = (0,[])"
  unfolding yun_factorization_def by simp
end

locale monic_factorization =
  fixes as :: "('a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly × nat) set"
  and p :: "'a poly"
  assumes p: "p = prod (λ (a,i). a ^ Suc i) as"
  and fin: "finite as"
  assumes as_distinct: " a i b j. (a,i)  as  (b,j)  as  (a,i)  (b,j)  a  b"
  and as_irred: " a i. (a,i)  as  irreducibled a"
  and as_monic: " a i. (a,i)  as  monic a"
begin

lemma poly_exp_expand: 
  "p = (prod (λ (a,i). a ^ i) as) * prod (λ (a,i). a) as"
  unfolding p prod.distrib[symmetric]
  by (rule prod.cong, auto)

lemma pderiv_exp_prod: 
  "pderiv p = (prod (λ (a,i). a ^ i) as * sum (λ (a,i). 
    prod (λ (b,j). b) (as - {(a,i)}) * smult (of_nat (Suc i)) (pderiv a)) as)"
  unfolding p pderiv_prod sum_distrib_left
proof (rule sum.cong[OF refl])
  fix x
  assume "x  as"
  then obtain a i where x: "x = (a,i)" and mem: "(a,i)  as" by (cases x, auto)
  let ?si = "smult (of_nat (Suc i)) :: 'a poly  'a poly"
  show "((a, i)as - {x}. a ^ Suc i) * pderiv (case x of (a, i)  a ^ Suc i) =
         ((a, i)as. a ^ i) *
         (case x of (a, i)  ((a, i)as - {(a, i)}. a) * smult (of_nat (Suc i)) (pderiv a))"
    unfolding x split pderiv_power_Suc
  proof -
    let ?prod = "(a, i)as - {(a, i)}. a ^ Suc i"
    let ?l = "?prod * (?si (a ^ i) * pderiv a)"
    let ?r = "((a, i)as. a ^ i) * (((a, i)as - {(a, i)}. a) * ?si (pderiv a))"
    have "?r = a ^ i * (((a, i)as - {(a, i)}. a ^ i) * ((a, i)as - {(a, i)}. a) * ?si (pderiv a))"
      unfolding prod.remove[OF fin mem] by (simp add: ac_simps)
    also have "((a, i)as - {(a, i)}. a ^ i) * ((a, i)as - {(a, i)}. a) 
      = ?prod" unfolding prod.distrib[symmetric]
      by (rule prod.cong[OF refl], auto)
    finally show "?l = ?r"
      by (simp add: ac_simps)
  qed
qed

lemma monic_gen: assumes "bs  as"
  shows "monic ( (a, i)  bs. a)"
  by (rule monic_prod, insert assms as_monic, auto)

lemma nonzero_gen: assumes "bs  as"
  shows "( (a, i)  bs. a)  0"
  using monic_gen[OF assms] by auto

lemma monic_Prod: "monic (((a, i)as. a ^ i))"
  by (rule monic_prod, insert as_monic, auto intro: monic_power)

lemma coprime_generic:
  assumes bs: "bs  as"
  and f: " a i. (a,i)  bs  f i > 0"
  shows "coprime ((a, i)  bs. a)
     ((a, i) bs. ((b, j) bs - {(a, i)} . b) * smult (of_nat (f i)) (pderiv a))"
  (is "coprime ?single ?onederiv")
proof -
  have single: "?single  0" by (rule nonzero_gen[OF bs])
  show ?thesis
  proof (rule gcd_eq_1_imp_coprime, rule gcdI [symmetric])
    fix k
    assume dvd: "k dvd ?single" "k dvd ?onederiv"
    note bs_monic = as_monic[OF subsetD[OF bs]]
    from dvd(1) single have k: "k  0" by auto
    show "k dvd 1"
    proof (cases "degree k > 0")
      case False
      with k obtain c where "k = [:c:]"
        by (auto dest: degree0_coeffs)
      with k have "c  0"
        by auto
      with k = [:c:] show "is_unit k"
        using dvdI [of 1 "[:c:]" "[:1 / c:]"] by auto
    next
      case True
      from irreducibled_factor[OF this]
      obtain p q where k: "k = p * q" and p: "irreducible p" by auto
      from k dvd have dvd: "p dvd ?single" "p dvd ?onederiv" unfolding dvd_def by auto
      from irreducible_dvd_prod[OF p dvd(1)] obtain a i where ai: "(a,i)  bs" and pa: "p dvd a"
        by force
      then obtain q where a: "a = p * q" unfolding dvd_def by auto
      from p[unfolded irreducibled_def] have p0: "degree p > 0" by auto
      from irreducibled_dvd_smult[OF p0 as_irred pa] ai bs
        obtain c where c: "c  0" and ap: "a = smult c p" by auto
      hence ap': "p = smult (1/c) a" by auto
      let ?prod = "λ a i. ((b, j)bs - {(a, i)}. b) * smult (of_nat (f i)) (pderiv a)"
      let ?prod' = "λ aa ii a i. ((b, j)bs - {(a, i),(aa,ii)}. b) * smult (of_nat (f i)) (pderiv a)"
      define factor where "factor = sum (λ (b,j). ?prod' a i b j ) (bs - {(a,i)})"
      define fac where "fac = q * factor"
      from fin finite_subset[OF bs] have fin: "finite bs" by auto
      have "?onederiv = ?prod a i + sum (λ (b,j). ?prod b j) (bs - {(a,i)})"
        by (subst sum.remove[OF fin ai], auto)
      also have "sum (λ (b,j). ?prod b j) (bs - {(a,i)})
        = a * factor"
        unfolding factor_def sum_distrib_left
      proof (rule sum.cong[OF refl])
        fix bj
        assume mem: "bj  bs - {(a,i)}"
        obtain b j where bj: "bj = (b,j)" by force
        from mem bj ai have ai: "(a,i)  bs - {(b,j)}" by auto
        have id: "bs - {(b, j)} - {(a, i)} = bs - {(b,j),(a,i)}" by auto
        show "(λ (b,j). ?prod b j) bj = a * (λ (b,j). ?prod' a i b j) bj"
          unfolding bj split
          by (subst prod.remove[OF _ ai], insert fin, auto simp: id ac_simps)
      qed
      finally have "?onederiv = ?prod a i + p * fac" unfolding fac_def a by simp
      from dvd(2)[unfolded this] have "p dvd ?prod a i" by algebra
      from this[unfolded field_poly_irreducible_dvd_mult[OF p]]
      have False
      proof
        assume "p dvd ((b, j)bs - {(a, i)}. b)" 
        from irreducible_dvd_prod[OF p this] obtain b j where bj': "(b,j)  bs - {(a,i)}"
          and pb: "p dvd b" by auto
        hence bj: "(b,j)  bs" by auto
        from as_irred bj bs have "irreducibled b" by auto
        from irreducibled_dvd_smult[OF p0 this pb] obtain d where d: "d  0" 
          and b: "b = smult d p" by auto
        with ap c have id: "smult (c/d) b = a" and deg: "degree a = degree b" by auto
        from coeff_smult[of "c/d" b "degree b", unfolded id] deg bs_monic[OF ai] bs_monic[OF bj]
        have "c / d = 1" by simp
        from id[unfolded this] have "a = b" by simp
        with as_distinct[OF subsetD[OF bs ai] subsetD[OF bs bj]] bj'
        show False by auto
      next
        from f[OF ai] obtain k where fi: "f i = Suc k" by (cases "f i", auto)
        assume "p dvd smult (of_nat (f i)) (pderiv a)"
        hence "p dvd (pderiv a)" unfolding fi using dvd_smult_cancel of_nat_eq_0_iff by blast
        from this[unfolded ap] have "p dvd pderiv p" using c
          by (metis p dvd pderiv a ap' dvd_trans dvd_triv_right mult.left_neutral pderiv_smult smult_dvd_cancel)
        with not_dvd_pderiv p0 show False by auto
      qed
      thus "k dvd 1" by simp
    qed
  qed (insert ?single  0, auto)
qed

lemma pderiv_exp_gcd: 
  "gcd p (pderiv p) = ((a, i)as. a ^ i)" (is "_ = ?prod")
proof -
  let ?sum = "((a, i)as. ((b, j)as - {(a, i)}. b) * smult (of_nat (Suc i)) (pderiv a))"
  let ?single = "((a, i)as. a)"
  let ?prd = "λ a i. ((b, j)as - {(a, i)}. b) * smult (of_nat (Suc i)) (pderiv a)"
  let ?onederiv = "(a, i)as. ?prd a i"
  have pp: "pderiv p = ?prod * ?sum" by (rule pderiv_exp_prod)
  have p: "p = ?prod * ?single" by (rule poly_exp_expand)
  have monic: "monic ?prod" by (rule monic_Prod)
  have gcd: "coprime ?single ?onederiv" 
    by (rule coprime_generic, auto)
  then have gcd: "gcd ?single ?onederiv = 1"
    by simp
  show ?thesis unfolding pp unfolding p poly_gcd_monic_factor [OF monic] gcd by simp
qed

lemma p_div_gcd_p_pderiv: "p div (gcd p (pderiv p)) = ((a, i)as. a)"
  unfolding pderiv_exp_gcd unfolding poly_exp_expand
  by (rule nonzero_mult_div_cancel_left, insert monic_Prod, auto)

fun A B C D :: "nat  'a poly" where
  "A n = gcd (B n) (D n)"
| "B 0 = p div (gcd p (pderiv p))"
| "B (Suc n) = B n div A n"
| "C 0 = pderiv p div (gcd p (pderiv p))"
| "C (Suc n) = D n div A n"
| "D n = C n - pderiv (B n)"

lemma A_B_C_D: "A n = ( (a, i)  as  UNIV × {n}. a)"
  "B n = ( (a, i)  as - UNIV × {0 ..< n}. a)"
  "C n = ((a, i)as - UNIV × {0 ..< n}. 
    ((b, j)as - UNIV × {0 ..< n} - {(a, i)}. b) * smult (of_nat (Suc i - n)) (pderiv a))"
  "D n = ( (a, i)  as  UNIV × {n}. a) * 
    ( (a,i)as - UNIV × {0 ..< Suc n}. 
      ((b, j) as - UNIV × {0 ..< Suc n} - {(a, i)}. b) * (smult (of_nat (i - n)) (pderiv a)))"
proof (induct n and n and n and n rule: A_B_C_D.induct)
  case (1 n) (* A *)
  note Bn = 1(1)
  note Dn = 1(2)
  have "((a, i)as - UNIV × {0..< n}. a) = ((a, i)as  UNIV × {n}. a) * ((a, i)as - UNIV × {0..<Suc n}. a)"
    by (subst prod.union_disjoint[symmetric], auto, insert fin, auto intro: prod.cong)
  note Bn' = Bn[unfolded this]
  let ?an = "( (a, i)  as  UNIV × {n}. a)"
  let ?bn = "((a, i)as - UNIV × {0..<Suc n}. a)"
  show "A n = ?an" unfolding A.simps
  proof (rule gcdI[symmetric, OF _ _ _ normalize_monic[OF monic_gen]])
    have monB1: "monic (B n)" unfolding Bn by (rule monic_gen, auto)
    hence "B n  0" by auto
    let ?dn = "( (a,i)as - UNIV × {0 ..< Suc n}. 
        ((b, j) as - UNIV × {0 ..< Suc n} - {(a, i)}. b) * (smult (of_nat (i - n)) (pderiv a)))"
    have Dn: "D n = ?an * ?dn" unfolding Dn by auto
    show dvd1: "?an dvd B n" unfolding Bn' dvd_def by blast
    show dvd2: "?an dvd D n" unfolding Dn dvd_def by blast
    {
      fix k
      assume "k dvd B n" "k dvd D n"
      from dvd_gcd_mult[OF this[unfolded Bn' Dn]]
      have "k dvd ?an * (gcd ?bn ?dn)" .
      moreover have "coprime ?bn ?dn"
        by (rule coprime_generic, auto)
      ultimately show "k dvd ?an" by simp
    }
  qed auto
next
  case 2 (* B 0 *)
  have as: "as - UNIV × {0..<0} = as" by auto
  show ?case unfolding B.simps as p_div_gcd_p_pderiv by auto
next
  case (3 n) (* B n *)
  have id: "((a, i)as - UNIV × {0..< n}. a) = ((a, i)as - UNIV × {0..<Suc n}. a) * ((a, i)as  UNIV × {n}. a)"
    by (subst prod.union_disjoint[symmetric], auto, insert fin, auto intro: prod.cong)
  show ?case unfolding B.simps 3 id
    by (subst nonzero_mult_div_cancel_right[OF nonzero_gen], auto)
next
  case 4 (* C 0 *)
  have as: "as - UNIV × {0..<0} = as" " i. Suc i - 0 = Suc i" by auto
  show ?case unfolding C.simps pderiv_exp_gcd unfolding pderiv_exp_prod as
    by (rule nonzero_mult_div_cancel_left, insert monic_Prod, auto)
next
  case (5 n) (* C n *)
  show ?case unfolding C.simps 5
    by (subst nonzero_mult_div_cancel_left, rule nonzero_gen, auto)
next
  case (6 n) (* D n *)
  let ?f = "λ (a,i). ((b, j)as - UNIV × {0 ..< n} - {(a, i)}. b) * (smult (of_nat (i - n)) (pderiv a))"
  have "D n = ( (a,i)as - UNIV × {0 ..< n}. ((b, j)as - UNIV × {0 ..< n} - {(a, i)}. b) * 
    (smult (of_nat (Suc i - n)) (pderiv a) - pderiv a))"
    unfolding D.simps 6 pderiv_prod sum_subtractf[symmetric] right_diff_distrib
    by (rule sum.cong, auto)
  also have " = sum ?f (as - UNIV × {0 ..< n})"
  proof (rule sum.cong[OF refl])
    fix x
    assume "x  as - UNIV × {0 ..< n}"
    then obtain a i where x: "x = (a,i)" and i: "Suc i > n" by (cases x, auto)
    hence id: "Suc i - n = Suc (i - n)" by arith
    have id: "of_nat (Suc i - n) = of_nat (i - n) + (1 :: 'a)" unfolding id by simp
    have id: "smult (of_nat (Suc i - n)) (pderiv a) - pderiv a = smult (of_nat (i - n)) (pderiv a)" 
      unfolding id smult_add_left by auto
    have cong: " x y z :: 'a poly. x = y  x * z = y * z" by auto
    show "(case x of
          (a, i) 
            ((b, j)as - UNIV × {0..<n} - {(a, i)}. b) *
            (smult (of_nat (Suc i - n)) (pderiv a) - pderiv a)) =
         (case x of
          (a, i)  ((b, j)as - UNIV × {0..<n} - {(a, i)}. b) * smult (of_nat (i - n)) (pderiv a))"
      unfolding x split id
      by (rule cong, auto)
  qed
  also have " = sum ?f (as - UNIV × {0 ..< Suc n}) + sum ?f (as  UNIV × {n})"
    by (subst sum.union_disjoint[symmetric], insert fin, auto intro: sum.cong)
  also have "sum ?f (as  UNIV × {n}) = 0"
    by (rule sum.neutral, auto)
  finally have id: "D n = sum ?f (as - UNIV × {0 ..< Suc n})" by simp
  show ?case unfolding id sum_distrib_left
  proof (rule sum.cong[OF refl])
    fix x
    assume mem: "x  as - UNIV × {0 ..< Suc n}"
    obtain a i where x: "x = (a,i)" by force
    with mem have i: "i > n" by auto
    have cong: " x y z v :: 'a poly. x = y * v  x * z = y * (v * z)" by auto
    show "(case x of
          (a, i)  ((b, j)as - UNIV × {0..<n} - {(a, i)}. b) * smult (of_nat (i - n)) (pderiv a)) =
         ((a, i)as  UNIV × {n}. a) *
         (case x of (a, i) 
            ((b, j)as - UNIV × {0..<Suc n} - {(a, i)}. b) * smult (of_nat (i - n)) (pderiv a))"
      unfolding x split
      by (rule cong, subst prod.union_disjoint[symmetric], insert fin, (auto)[3],
        rule prod.cong, insert i, auto) 
  qed
qed

lemmas A = A_B_C_D(1)
lemmas B = A_B_C_D(2)

lemmas ABCD_simps = A.simps B.simps C.simps D.simps
declare ABCD_simps[simp del]

lemma prod_A: 
  "(i = 0..< n. A i ^ Suc i) = ((a, i) as  UNIV × {0 ..< n}. a ^ Suc i)"
proof (induct n)
  case (Suc n)
  have id: "{0 ..< Suc n} = insert n {0 ..< n}" by auto
  have id2: "as  UNIV × {0 ..< Suc n} = as  UNIV × {n}  as  UNIV × {0 ..< n}" by auto
  have cong: " x y z. x = y  x * z = y * z" by auto
  show ?case unfolding id2 unfolding id 
  proof (subst prod.insert; (subst prod.union_disjoint)?; (unfold Suc)?; 
    (unfold A, rule cong)?)
    show "((a, i)as  UNIV × {n}. a) ^ Suc n = ((a, i)as  UNIV × {n}. a ^ Suc i)"
      unfolding prod_power_distrib
      by (rule prod.cong, auto)
  qed (insert fin, auto)
qed simp

lemma prod_A_is_p_unknown: assumes " a i. (a,i)  as  i < n"
  shows "p = (i = 0..< n. A i ^ Suc i)"
proof -
  have "p = ((a, i)as. a ^ Suc i)" by (rule p)
  also have " = (i = 0..< n. A i ^ Suc i)" unfolding prod_A
    by (rule prod.cong, insert assms, auto)
  finally show ?thesis .
qed

definition bound :: nat where
  "bound = Suc (Max (snd ` as))"

lemma bound: assumes m: "m  bound"
  shows "B m = 1"
proof -
  let ?set = "as - UNIV × {0..<m}"
  {
    fix a i
    assume ai: "(a,i)  ?set"
    hence "i  snd ` as" by force
    from Max_ge[OF _ this] fin have "i  Max (snd ` as)" by auto
    with ai m[unfolded bound_def] have False by auto
  }
  hence id: "?set = {}" by force
  show "B m = 1" unfolding B id by simp
qed

lemma coprime_A_A: assumes "i  j"
  shows "coprime (A i) (A j)"
proof (rule coprimeI)
  fix k  
  assume dvd: "k dvd A i" "k dvd A j"
  have Ai: "A i  0" unfolding A
    by (rule nonzero_gen, auto)
  with dvd have k: "k  0" by auto
  show "is_unit k"
  proof (cases "degree k > 0")
    case False
    then obtain c where kc: "k = [: c :]" by (auto dest: degree0_coeffs)
    with k have "1 = k * [:1 / c:]"
      by simp
    thus ?thesis unfolding dvd_def by blast
  next
    case True
    from irreducible_monic_factor[OF this]
    obtain q r where k: "k = q * r" and q: "irreducible q" and mq: "monic q" by auto
    with dvd have dvd: "q dvd A i" "q dvd A j" unfolding dvd_def by auto
    from q have q0: "degree q > 0" unfolding irreducibled_def by auto
    from irreducible_dvd_prod[OF q dvd(1)[unfolded A]]
      obtain a where ai: "(a,i)  as" and qa: "q dvd a" by auto
    from irreducible_dvd_prod[OF q dvd(2)[unfolded A]]
      obtain b where bj: "(b,j)  as" and qb: "q dvd b" by auto
    from as_distinct[OF ai bj] assms have neq: "a  b" by auto
    from irreducibled_dvd_smult[OF q0 as_irred[OF ai] qa]
      irreducibled_dvd_smult[OF q0 as_irred[OF bj] qb]
    obtain c d where "c  0" "d  0" "a = smult c q" "b = smult d q" by auto
    hence ab: "a = smult (c / d) b" and "c / d  0" by auto
    with as_monic[OF bj] as_monic[OF ai] arg_cong[OF ab, of "λ p. coeff p (degree p)"] 
    have "a = b" unfolding coeff_smult degree_smult_eq by auto
    with neq show ?thesis by auto
  qed
qed

lemma A_monic: "monic (A i)"
  unfolding A by (rule monic_gen, auto)

lemma A_square_free: "square_free (A i)"
proof (rule square_freeI)
  fix q k
  have mon: "monic (A i)" by (rule A_monic)
  hence Ai: "A i  0" by auto
  assume q: "degree q > 0" and dvd: "q * q dvd A i"
  from irreducible_monic_factor[OF q] obtain r s where q: "q = r * s" and 
    irr: "irreducible r" and mr: "monic r" by auto
  from dvd[unfolded q] have dvd2: "r * r dvd A i" and dvd1: "r dvd A i" unfolding dvd_def by auto
  from irreducible_dvd_prod[OF irr dvd1[unfolded A]] 
    obtain a where ai: "(a,i)  as" and ra: "r dvd a" by auto
  let ?rem = "((a, i)as  UNIV × {i} - {(a,i)}. a)"
  have a: "irreducibled a" by (rule as_irred[OF ai])
  from irreducibled_dvd_smult[OF _ a ra] irr
    obtain c where ar: "a = smult c r"  and "c  0" by force
  with mr as_monic[OF ai] arg_cong[OF ar, of "λ p. coeff p (degree p)"] 
  have "a = r" unfolding coeff_smult degree_smult_eq by auto 
  with dvd2 have dvd: "a * a dvd A i" by simp
  have id: "A i = a * ?rem" unfolding A
    by (subst prod.remove[of _ "(a,i)"], insert ai fin, auto)
  with dvd have "a dvd ?rem" using a id Ai by auto
  from irreducible_dvd_prod[OF _ this] a obtain b where bi: "(b,i)  as" 
    and neq: "b  a" and ab: "a dvd b" by auto
  from as_irred[OF bi] have b: "irreducibled b" . 
  from irreducibled_dvd_smult[OF _ b ab] a[unfolded irreducibled_def]
  obtain c where "c  0" and ba: "b = smult c a" by auto
  with as_monic[OF bi] as_monic[OF ai] arg_cong[OF ba, of "λ p. coeff p (degree p)"] 
  have "a = b" unfolding coeff_smult degree_smult_eq by auto
  with neq show False by auto
qed (insert A_monic[of i], auto)


lemma prod_A_is_p_B_bound: assumes "B n = 1"
  shows "p = (i = 0..< n. A i ^ Suc i)"
proof (rule prod_A_is_p_unknown)
  fix a i
  assume ai: "(a,i)  as"
  let ?rem = "((a, i)as - UNIV × {0..<n} - {(a,i)}. a)"
  have rem: "?rem  0"
    by (rule nonzero_gen, auto)
  have "irreducibled a" using as_irred[OF ai] .
  hence a: "a  0" "degree a  0" unfolding irreducibled_def by auto
  show "i < n"
  proof (rule ccontr)
    assume "¬ ?thesis"
    hence "i  n" by auto
    with ai have mem: "(a,i)  as - UNIV × {0 ..< n}" by auto
    have "0 = degree ((a, i)as - UNIV × {0..<n}. a)" using assms unfolding B by simp
    also have " = degree (a * ?rem)"
      by (subst prod.remove[OF _ mem], insert fin, auto)
    also have " = degree a + degree ?rem"
      by (rule degree_mult_eq[OF a(1) rem])
    finally show False using a(2) by auto
  qed
qed

interpretation yun_gcd gcd .

lemma square_free_monic_poly: "(poly (square_free_monic_poly p) x = 0) = (poly p x = 0)"
proof -
  show ?thesis unfolding square_free_monic_poly_def unfolding p_div_gcd_p_pderiv
    unfolding p poly_prod prod_zero_iff[OF fin] by force
qed

lemma yun_factorization_induct: assumes base: " bn cn. bn = 1  P bn cn"
  and step: " bn cn. bn  1  P (bn div (gcd bn (cn - pderiv bn))) 
    ((cn - pderiv bn) div (gcd bn (cn - pderiv bn)))  P bn cn"
  and id: "bn = p div gcd p (pderiv p)" "cn = pderiv p div gcd p (pderiv p)"
  shows "P bn cn"
proof -
  define n where "n = (0 :: nat)"
  let ?m = "λ n. bound - n"
  have "P (B n) (C n)"
  proof (induct n rule: wf_induct[OF wf_measure[of ?m]])
    case (1 n)
    note IH = 1(1)[rule_format]
    show ?case
    proof (cases "B n = 1")
      case True
      with base show ?thesis by auto
    next
      case False note Bn = this
      with bound[of n] have "¬ bound  n" by auto
      hence "(Suc n, n)  measure ?m" by auto
      note IH = IH[OF this]
      show ?thesis
        by (rule step[OF Bn], insert IH, simp add: D.simps C.simps B.simps A.simps)
    qed
  qed
  thus ?thesis unfolding id n_def B.simps C.simps .
qed

lemma yun_factorization_main: assumes "yun_factorization_main (B n) (C n) n bs = cs"
  "set bs = {(A i, Suc i) | i. i < n}" "distinct (map snd bs)"
  shows " m. set cs = {(A i, Suc i) | i. i < m}  B m = 1  distinct (map snd cs)"
  using assms
proof -
  let ?m = "λ n. bound - n"
  show ?thesis using assms 
  proof (induct n arbitrary: bs rule: wf_induct[OF wf_measure[of ?m]])
    case (1 n)
    note IH = 1(1)[rule_format]
    have res: "yun_factorization_main (B n) (C n) n bs = cs" by fact
    note res = res[unfolded yun_factorization_main.simps[of "B n"]]
    have bs: "set bs = {(A i, Suc i) |i. i < n}" "distinct (map snd bs)" by fact+
    show ?case
    proof (cases "B n = 1")
      case True
      with res have "bs = cs" by auto
      with True bs show ?thesis by auto
    next
      case False note Bn = this
      with bound[of n] have "¬ bound  n" by auto
      hence "(Suc n, n)  measure ?m" by auto
      note IH = IH[OF this]
      from Bn res[unfolded Let_def, folded D.simps C.simps B.simps A.simps] 
      have res: "yun_factorization_main (B (Suc n)) (C (Suc n)) (Suc n) ((A n, Suc n) # bs) = cs"
        by simp
      note IH = IH[OF this]
      {
        fix i 
        assume "i < Suc n" "¬ i < n"
        hence "n = i" by arith
      } note missing = this
      have "set ((A n, Suc n) # bs) = {(A i, Suc i) |i. i < Suc n}"
        unfolding list.simps bs by (auto, subst missing, auto)
      note IH = IH[OF this]
      from bs have "distinct (map snd ((A n, Suc n) # bs))" by auto
      note IH = IH[OF this]
      show ?thesis by (rule IH)
    qed
  qed
qed

lemma yun_monic_factorization_res: assumes res: "yun_monic_factorization p = bs"
  shows " m. set bs = {(A i, Suc i) | i. i < m  A i  1}  B m = 1  distinct (map snd bs)"
proof -
  from res[unfolded yun_monic_factorization_def Let_def, 
    folded B.simps C.simps]
  obtain cs where yun: "yun_factorization_main (B 0) (C 0) 0 [] = cs" and bs: "bs = filter (λ (a,i). a  1) cs" 
    by auto
  from yun_factorization_main[OF yun] obtain m where "set cs = {(A i, Suc i) |i. i < m}" 
    "B m = 1" "distinct (map snd cs)" 
    by auto 
  thus ?thesis unfolding bs by (auto simp: distinct_map_filter)
qed                                                    

lemma yun_monic_factorization: assumes yun: "yun_monic_factorization p = bs"
  shows "square_free_factorization p (1,bs)" "(b,i)  set bs  monic b" "distinct (map snd bs)" 
proof -
  from yun_monic_factorization_res[OF yun]
  obtain m where bs: "set bs = {(A i, Suc i) | i. i < m  A i  1}" and B: "B m = 1" 
    and dist: "distinct (map snd bs)" by auto
  have id: "{0 ..< m} = {i. i < m  A i = 1}  {i. i < m  A i  1}" (is "_ = ?ignore  _") by auto
  have "p = (i = 0..<m. A i ^ Suc i)"
    by (rule prod_A_is_p_B_bound[OF B])
  also have " = prod (λ i. A i ^ Suc i) {i. i < m  A i  1}"
    unfolding id by (subst prod.union_disjoint, (force+)[3],
      subst prod.neutral[of ?ignore], auto)
  also have " = ((a, i) set bs. a ^ i)" unfolding bs
    by (rule prod.reindex_cong[of "(λ n. n - 1) o snd"], auto simp: inj_on_def, force)
  finally have 1: "p = ((a, i) set bs. a ^ i)" .
  {
    fix a i
    assume "(a,i)  set bs"
    then obtain j where A: "a = A j" "A j  1" and i: "i  0" unfolding bs by auto
    with A_square_free[of j] A_monic[of j] have "square_free a  degree a  0" "monic a" "i  0" 
      by (auto simp: monic_degree_0)
  } note 2 = this
  {
    fix a i b j
    assume ai: "(a,i)  set bs" and bj: "(b,j)  set bs" and neq: "(a,i)  (b,j)"
    then obtain i' j' where a: "a = A i'" and b: "b = A j'" and ij': "i = Suc i'" "j = Suc j'" 
      unfolding bs by auto
    from neq dist ai bj have neq: "i'  j'" using a b ij' by blast
    from coprime_A_A [OF neq] have "coprime a b" unfolding a b .
  } note 3 = this
  have "monic p" unfolding p 
    by (rule monic_prod, insert as_monic, auto intro: monic_power monic_mult)
  hence 4: "p  0" by auto
  from dist have 5: "distinct bs" unfolding distinct_map ..
  show "square_free_factorization p (1,bs)"
    unfolding square_free_factorization_def using 1 2 3 4 5
    by auto
  show "(b,i)  set bs  monic b" using 2 by auto
  show "distinct (map snd bs)" by fact
qed
end

lemma monic_factorization: assumes "monic p"
  shows " as. monic_factorization as p"
proof -
  from monic_irreducible_factorization[OF assms]
  obtain as f where fin: "finite as" and p: "p = (aas. a ^ Suc (f a))" 
    and as: "as  {q. irreducibled q  monic q}"
    by auto
  define cs where "cs = {(a, f a) | a. a  as}"
  show ?thesis
  proof (rule exI, standard)  
    show "finite cs" unfolding cs_def using fin by auto
    {
      fix a i
      assume "(a,i)  cs"
      thus "irreducibled a" "monic a" unfolding cs_def using as by auto
    } note irr = this
    show "a i b j. (a, i)  cs  (b, j)  cs  (a, i)  (b, j)  a  b" unfolding cs_def by auto
    show "p = ((a, i)cs. a ^ Suc i)" unfolding p cs_def
      by (rule prod.reindex_cong, auto, auto simp: inj_on_def)
  qed
qed

lemma square_free_monic_poly:
  assumes "monic (p :: 'a :: {field_char_0, euclidean_ring_gcd,semiring_gcd_mult_normalize} poly)"
  shows "(poly (yun_gcd.square_free_monic_poly gcd p) x = 0) = (poly p x = 0)"
proof -
  from monic_factorization[OF assms] obtain as where "monic_factorization as p" ..
  from monic_factorization.square_free_monic_poly[OF this] show ?thesis .
qed

lemma yun_factorization_induct: 
  assumes base: " bn cn. bn = 1  P bn cn"
  and step: " bn cn. bn  1  P (bn div (gcd bn (cn - pderiv bn))) 
    ((cn - pderiv bn) div (gcd bn (cn - pderiv bn)))  P bn cn"
  and id: "bn = p div gcd p (pderiv p)" "cn = pderiv p div gcd p (pderiv p)"
  and monic: "monic (p :: 'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly)"
  shows "P bn cn"
proof -
  from monic_factorization[OF monic] obtain as where "monic_factorization as p" ..
  from monic_factorization.yun_factorization_induct[OF this base step id] show ?thesis .
qed

lemma square_free_poly: 
  "(poly (square_free_poly gcd p) x = 0) = (poly p x = 0)"
proof (cases "p = 0")
  case True
  thus ?thesis unfolding square_free_poly_def by auto
next
  case False
  let ?c = "coeff p (degree p)"
  let ?ic = "inverse ?c"
  have id: "square_free_poly gcd p = yun_gcd.square_free_monic_poly gcd (smult ?ic p)"
    unfolding square_free_poly_def using False by auto
  from False have mon: "monic (smult ?ic p)" and ic: "?ic  0" by auto
  show ?thesis unfolding id square_free_monic_poly[OF mon]
    using ic by simp
qed  


lemma yun_monic_factorization:
  fixes p :: "'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly" 
  assumes res: "yun_gcd.yun_monic_factorization gcd p = bs"
  and monic: "monic p"
  shows "square_free_factorization p (1,bs)" "(b,i)  set bs  monic b" "distinct (map snd bs)" 
proof -
  from monic_factorization[OF monic] obtain as where "monic_factorization as p" ..
  from "monic_factorization.yun_monic_factorization"[OF this res]
  show "square_free_factorization p (1,bs)" "(b,i)  set bs  monic b" "distinct (map snd bs)" 
    by auto
qed

lemma square_free_factorization_smult: assumes c: "c  0"
  and sf: "square_free_factorization p (d,bs)"
  shows "square_free_factorization (smult c p) (c * d, bs)"
proof -
  from sf[unfolded square_free_factorization_def split]
  have p: "p = smult d ((a, i)set bs. a ^ i)"
    and eq: "p = 0  d = 0  bs = []" by blast+
  from eq c have eq: "smult c p = 0  c * d = 0  bs = []" by auto
  from p have p: "smult c p = smult (c * d) ((a, i)set bs. a ^ i)" by auto
  from eq p sf show ?thesis unfolding square_free_factorization_def by blast
qed

lemma yun_factorization: assumes res: "yun_factorization gcd p = c_bs"
  shows "square_free_factorization p c_bs" "(b,i)  set (snd c_bs)  monic b"
proof -
  interpret yun_gcd gcd .
  note res = res[unfolded yun_factorization_def Let_def]
  have "square_free_factorization p c_bs  ((b,i)  set (snd c_bs)  monic b)"
  proof (cases "p = 0")
    case True
    with res have "c_bs = (0, [])" by auto    
    thus ?thesis unfolding True by (auto simp: square_free_factorization_def)
  next
    case False
    let ?c = "coeff p (degree p)"
    let ?ic = "inverse ?c"
    obtain c bs where cbs: "c_bs = (c,bs)" by force
    with False res
    have c: "c = ?c" "?c  0" and fact: "yun_monic_factorization (smult ?ic p) = bs" by auto
    from False have mon: "monic (smult ?ic p)" by auto
    from yun_monic_factorization[OF fact mon]
    have sff: "square_free_factorization (smult ?ic p) (1, bs)" "(b, i)  set bs  monic b" by auto
    have id: "smult ?c (smult ?ic p) = p" using False by auto
    from square_free_factorization_smult[OF c(2) sff(1), unfolded id] sff
    show ?thesis unfolding cbs c by simp
  qed
  thus "square_free_factorization p c_bs" "(b,i)  set (snd c_bs)  monic b" by blast+
qed


lemma prod_list_pow: "(xbs. (x :: 'a :: comm_monoid_mult) ^ i) 
  = prod_list bs ^ i" 
  by (induct bs, auto simp: field_simps)

declare irreducible_linear_field_poly[intro!]

context 
  assumes "SORT_CONSTRAINT('a :: {field, factorial_ring_gcd,semiring_gcd_mult_normalize})" 
begin
lemma square_free_factorization_order_root_mem: 
  assumes sff: "square_free_factorization p (c,bs)"
    and p: "p  (0 :: 'a poly)"
    and ai: "(a,i)  set bs" and rt: "poly a x = 0"
  shows "order x p = i"
proof -
  note sff = square_free_factorizationD[OF sff]
  let ?prod = "((a, i)set bs. a ^ i)"
  from sff have pf: "p = smult c ?prod" by blast
  with p have c: "c  0" by auto
  have ord: "order x p = order x ?prod" unfolding pf 
    using order_smult[OF c] by auto
  define q where "q = [: -x, 1 :]"
  have q0: "q  0" unfolding q_def by auto
  have iq: "irreducible q" by (auto simp: q_def)
  from rt have qa: "q dvd a" unfolding q_def poly_eq_0_iff_dvd .
  then obtain b where aqb: "a = q * b" unfolding dvd_def by auto
  from sff(2)[OF ai] have sq: "square_free a" and mon: "degree a  0" by auto
  let ?rem = "((a, i)set bs - {(a,i)}. a ^ i)"
  have p0: "?prod  0" using p pf by auto
  have "?prod = a ^ i * ?rem"
    by (subst prod.remove[OF _ ai], auto)
  also have "a ^ i = q ^ i * b ^ i" unfolding aqb by (simp add: field_simps)
  finally have id: "?prod = q ^ i * (b ^ i * ?rem)" by simp
  hence dvd: "q ^ i dvd ?prod" by auto
  {
    assume "q ^ Suc i dvd ?prod"
    hence "q dvd ?prod div q ^ i"
      by (metis dvd dvd_0_left_iff dvd_div_iff_mult p0 power_Suc)
    also have "?prod div q ^ i = b ^ i * ?rem"
      unfolding id by (rule nonzero_mult_div_cancel_left, insert q0, auto)
    finally have "q dvd b  q dvd ?rem"
      using iq irreducible_dvd_pow[OF iq] by auto
    hence False
    proof
      assume "q dvd b"
      with aqb have "q * q dvd a" by auto
      with sq[unfolded square_free_def] mon iq show False
        unfolding irreducibled_def by auto
    next
      assume "q dvd ?rem"
      from irreducible_dvd_prod[OF iq this]
      obtain b j where bj: "(b,j)  set bs" and neq: "(a,i)  (b,j)" and dvd: "q dvd b ^ j" by auto
      from irreducible_dvd_pow[OF iq dvd] have qb: "q dvd b" .
      from sff(3)[OF ai bj neq] have gcd: "coprime a b" .
      from qb qa have "q dvd gcd a b" by simp
      from dvd_imp_degree_le[OF this[unfolded gcd]] iq q0 show False
        using gcd by auto
    qed
  }
  hence ndvd: "¬ q ^ Suc i dvd ?prod" by blast
  with dvd have "order x ?prod = i" unfolding q_def
    by (metis order_unique_lemma)
  thus ?thesis unfolding ord .
qed

lemma square_free_factorization_order_root_no_mem: 
  assumes sff: "square_free_factorization p (c,bs)"
    and p: "p  (0 :: 'a poly)"
    and no_root: " a i. (a,i)  set bs  poly a x  0"
  shows "order x p = 0"
proof (rule ccontr)
  assume o0: "order x p  0"
  with order_root[of p x] p have 0: "poly p x = 0" by auto
  note sff = square_free_factorizationD[OF sff]
  let ?prod = "((a, i)set bs. a ^ i)"
  from sff have pf: "p = smult c ?prod" by blast
  with p have c: "c  0" by auto
  with 0 have 0: "poly ?prod x = 0" unfolding pf by auto
  define q where "q = [: -x, 1 :]"
  from 0 have dvd: "q dvd ?prod" unfolding poly_eq_0_iff_dvd by (simp add: q_def)  
  have q0: "q  0" unfolding q_def by auto
  have iq: "irreducible q" by (unfold q_def, auto intro:)
  from irreducible_dvd_prod[OF iq dvd]
  obtain a i where ai: "(a,i)  set bs" and dvd: "q dvd a ^ Suc i" by auto
  from irreducible_dvd_pow[OF iq dvd] have dvd: "q dvd a" .
  hence "poly a x = 0" unfolding q_def by (simp add: poly_eq_0_iff_dvd q_def)
  with no_root[OF ai] show False by simp
qed

lemma square_free_factorization_order_root: 
  assumes sff: "square_free_factorization p (c,bs)"
    and p: "p  (0 :: 'a poly)"
  shows "order x p = i  (i = 0  ( a j. (a,j)  set bs  poly a x  0) 
     ( a j. (a,j)  set bs  poly a x = 0  i = j))" (is "?l = (?r1  ?r2)")
proof -
  note mem = square_free_factorization_order_root_mem[OF sff p]
  note no_mem = square_free_factorization_order_root_no_mem[OF sff p]
  show ?thesis
  proof
    assume "?r1  ?r2"
    thus ?l
    proof
      assume ?r2
      then obtain a j where aj: "(a,j)  set bs" "poly a x = 0" and i: "i = j" by auto
      from mem[OF aj] i show ?l by simp
    next
      assume ?r1 
      with no_mem[of x] show ?l by auto
    qed
  next
    assume ?l
    show "?r1  ?r2"
    proof (cases "a j. (a, j)  set bs  poly a x = 0")
      case True
      then obtain a j where "(a, j)  set bs" "poly a x = 0" by auto
      with mem[OF this] ?l
      have ?r2 by auto
      thus ?thesis ..
    next
      case False
      with no_mem[of x] ?l have ?r1 by auto
      thus ?thesis ..
    qed
  qed
qed

lemma square_free_factorization_root: 
  assumes sff: "square_free_factorization p (c,bs)"
    and p: "p  (0 :: 'a poly)"
  shows "{x. poly p x