Theory Fundamental_Theorem_Algebra_Factorized

(*  
    Author:      René Thiemann 
    License:     BSD
*)
subsection ‹Fundamental Theorem of Algebra for Factorizations›

text ‹Via the existing formulation of the fundamental theorem of algebra,
  we prove that we always get a linear factorization of a complex polynomial.
  Using this factorization we show that root-square-freeness of complex polynomial
  is identical to the statement that the cardinality of the set of all roots 
  is equal to the degree of the polynomial.›

theory Fundamental_Theorem_Algebra_Factorized
imports 
  Order_Polynomial
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
begin

lemma fundamental_theorem_algebra_factorized: fixes p :: "complex poly"
  shows "∃ as. smult (coeff p (degree p)) (∏ a ← as. [:- a, 1:]) = p ∧ length as = degree p"
proof -
  define n where "n = degree p"
  have "degree p = n" unfolding n_def by simp
  thus ?thesis
  proof (induct n arbitrary: p)
    case (0 p)
    hence "∃ c. p = [: c :]" by (cases p, auto split: if_splits)
    thus ?case by (intro exI[of _ Nil], auto)
  next
    case (Suc n p)
    have dp: "degree p = Suc n" by fact
    hence "¬ constant (poly p)" by (simp add: constant_degree)
    from fundamental_theorem_of_algebra[OF this] obtain c where rt: "poly p c = 0" by auto
    hence "[:-c,1 :] dvd p" by (simp add: dvd_iff_poly_eq_0)
    then obtain q where p: "p = q * [: -c,1 :]" by (metis dvd_def mult.commute)
    from ‹degree p = Suc n› have dq: "degree q = n" using p
      by simp (metis add.right_neutral degree_synthetic_div diff_Suc_1 mult.commute mult_left_cancel p pCons_eq_0_iff rt synthetic_div_correct' zero_neq_one) 
    from Suc(1)[OF this] obtain as where q: "[:coeff q (degree q):] * (∏a←as. [:- a, 1:]) = q"
      and deg: "length as = degree q" by auto
    have dc: "degree p = degree q + degree [: -c, 1 :]" unfolding dq dp by simp
    have cq: "coeff q (degree q) = coeff p (degree p)" unfolding dc unfolding p coeff_mult_degree_sum unfolding dq by simp
    show ?case using p[unfolded q[unfolded cq, symmetric]] 
      by (intro exI[of _ "c # as"], auto simp: ac_simps, insert deg dc, auto)
  qed
qed

lemma rsquarefree_card_degree: assumes p0: "(p :: complex poly) ≠ 0"
  shows "rsquarefree p = (card {x. poly p x = 0} = degree p)"
proof -
  from fundamental_theorem_algebra_factorized[of p] obtain c as
    where p: "p = smult c (∏ a ← as. [:- a, 1:])" and pas: "degree p = length as"
    and c: "c = coeff p (degree p)" by metis
  let ?prod = "(∏a←as. [:- a, 1:])"
  from p0 have c: "c ≠ 0" unfolding c by auto
  have roots: "{x. poly p x = 0} = set as" unfolding p poly_smult_zero_iff poly_prod_list prod_list_zero_iff
    using c by auto
  have idr: "(card {x. poly p x = 0} = degree p) = distinct as" unfolding roots pas
    using card_distinct distinct_card by blast
  have id: "⋀ q. (p ≠ 0 ∧ q) = q" using p0 by simp
  have dist: "distinct as = (∀a. (∑x←as. if x = a then 1 else 0) ≤ Suc 0)" (is "?l = (∀ a. ?r a)")
  proof (cases "distinct as")
    case False
    from not_distinct_decomp[OF this] obtain xs ys zs a where "as = xs @ [a] @ ys @ [a] @ zs" by auto
    hence "¬ ?r a" by auto
    thus ?thesis using False by auto
  next
    case True
    {
      fix a
      from True have "?r a"
      proof (induct as)
        case (Cons b bs)
        show ?case
        proof (cases "a = b")
          case False
          with Cons show ?thesis by auto
        next
          case True
          with Cons(2) have "a ∉ set bs" by auto
          hence "(∑x← bs. if x = a then 1 else 0) = (0 :: nat)" by (induct bs, auto)
          thus ?thesis unfolding True by auto
        qed
      qed simp
    }
    thus ?thesis using True by auto
  qed
  have "rsquarefree p = distinct as" unfolding rsquarefree_def' id unfolding p order_smult[OF c]
    by (subst order_prod_list, auto simp: o_def order_linear' dist)
  thus ?thesis unfolding idr by simp
qed


end