Theory Polynomial_Factorization.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):] * (aas. [:- 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 = "(aas. [:- 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. (xas. 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