Theory Factor_Algebraic_Polynomial.Factor_Complex_Poly

section ‹Factorization of Polynomials with Algebraic Coefficients›

subsection ‹Complex Algebraic Coefficients›

theory Factor_Complex_Poly
  imports 
    Roots_of_Real_Complex_Poly
begin
hide_const (open) MPoly_Type.smult MPoly_Type.degree MPoly_Type.coeff MPoly_Type.coeffs

definition factor_complex_main :: "complex poly ⇒ complex × (complex × nat) list" where
  "factor_complex_main p ≡ let (c,pis) = yun_rf (yun_polys p) in
    (c, concat (map (λ (p,i). map (λ r. (r,i)) (roots_of_complex_rf_poly p)) pis))"

lemma roots_of_complex_poly_via_factor_complex_main: 
  "map fst (snd (factor_complex_main p)) = roots_of_complex_poly p"
proof (cases "p = 0")
  case True
  have [simp]: "yun_rf (yun_polys 0) = (0,[])"
    by (transfer, simp)
  show ?thesis 
    unfolding factor_complex_main_def Let_def roots_of_complex_poly_def True
    by simp
next
  case False
  hence p: "(p = 0) = False" by simp
  obtain c rts where yun: "yun_rf (yun_polys p) = (c,rts)" by force
  show ?thesis 
    unfolding factor_complex_main_def Let_def roots_of_complex_poly_def p if_False
      roots_of_complex_rf_polys_def polys_rf_def o_def yun split snd_conv map_map
    by (induct rts, auto simp: o_def)
qed

lemma distinct_factor_complex_main:
  "distinct (map fst (snd (factor_complex_main p)))" 
  unfolding roots_of_complex_poly_via_factor_complex_main
  by (rule distinct_roots_of_complex_poly)
    
lemma factor_complex_main: assumes rt: "factor_complex_main p = (c,xis)"
  shows "p = smult c (∏(x, i)←xis. [:- x, 1:] ^ i)" 
    "0 ∉ snd ` set xis"
proof -
  obtain d pis where yun: "yun_factorization gcd p = (d,pis)" by force
  obtain d' pis' where yun_rf: "yun_rf (yun_polys p) = (d',pis')" by force
  let ?p = poly_rf
  let ?map = "map (λ (p,i). (?p p, i))" 
  from yun yun_rf have d': "d' = d" and pis: "pis = ?map pis'" 
    by (atomize(full), transfer, auto)  
  from rt[unfolded factor_complex_main_def yun_rf split Let_def d']
  have xis: "xis = concat (map (λ(p, i). map (λr. (r, i)) (roots_of_complex_rf_poly p)) pis')"
    and d: "d = c"
    by (auto split: if_splits)
  note yun = yun_factorization[OF yun[unfolded d]]
  note yun = square_free_factorizationD[OF yun(1)] yun(2)[unfolded snd_conv]
  let ?exp = "λ pis. ∏(x, i)←concat
    (map (λ(p, i). map (λr. (r, i)) (roots_of_complex_rf_poly p)) pis). [:- x, 1:] ^ i"
  from yun(1) have p: "p = smult c (∏(a, i)∈set pis. a ^ i)" .
  also have "(∏(a, i)∈set pis. a ^ i) = (∏(a, i)←pis. a ^ i)"
    by (rule prod.distinct_set_conv_list[OF yun(5)])
  also have "… = ?exp pis'" using yun(2,6) unfolding pis 
  proof (induct pis')
    case (Cons pi pis)
    obtain p i where pi: "pi = (p,i)" by force
    let ?rts = "roots_of_complex_rf_poly p"
    note Cons = Cons[unfolded pi]
    have IH: "(∏(a, i)←?map pis. a ^ i) = (?exp pis)"
      by (rule Cons(1)[OF Cons(2-3)], auto)
    from Cons(2-3)[of "?p p" i] have p: "square_free (?p p)" "degree (?p p) ≠ 0" "?p p ≠ 0" "monic (?p p)" by auto
    have "(∏(a, i)←?map (pi # pis). a ^ i) = ?p p ^ i * (∏(a, i)←?map pis. a ^ i)"
      unfolding pi by simp
    also have "(∏(a, i)←?map pis. a ^ i) = ?exp pis" by (rule IH)
    finally have id: "(∏(a, i)←?map (pi # pis). a ^ i) = ?p p ^ i * ?exp pis" by simp
    have "?exp (pi # pis) = ?exp [(p,i)] * ?exp pis" unfolding pi by simp
    also have "?exp [(p,i)] = (∏(x, i)← (map (λr. (r, i)) ?rts). [:- x, 1:] ^ i)" 
      by simp
    also have "… = (∏ x ← ?rts. [:- x, 1:])^ i"
      unfolding prod_list_power by (rule arg_cong[of _ _ prod_list], auto)
    also have "(∏ x ← ?rts. [:- x, 1:]) = ?p p" 
    proof -
      from fundamental_theorem_algebra_factorized[of "?p p", unfolded ‹monic (?p p)›]
      obtain as where as: "?p p = (∏a←as. [:- a, 1:])" by (metis smult_1_left)
      also have "… = (∏a∈set as. [:- a, 1:])"
      proof (rule sym, rule prod.distinct_set_conv_list, rule ccontr)
        assume "¬ distinct as" 
        from not_distinct_decomp[OF this] obtain as1 as2 as3 a where
          a: "as = as1 @ [a] @ as2 @ [a] @ as3" by blast
        define q where "q = (∏a←as1 @ as2 @ as3. [:- a, 1:])"
        have "?p p = (∏a←as. [:- a, 1:])" by fact
        also have "… = (∏a←([a] @ [a]). [:- a, 1:]) * q"
          unfolding q_def a map_append prod_list.append by (simp only: ac_simps)
        also have "… = [:-a,1:] * [:-a,1:] * q" by simp
        finally have "?p p = ([:-a,1:] * [:-a,1:]) * q" by simp
        hence "[:-a,1:] * [:-a,1:] dvd ?p p" unfolding dvd_def ..
        with ‹square_free (?p p)›[unfolded square_free_def, THEN conjunct2, rule_format, of "[:-a,1:]"] 
        show False by auto
      qed
      also have "set as = {x. poly (?p p) x = 0}" unfolding as poly_prod_list 
        by (simp add: o_def, induct as, auto)
      also have "… = set ?rts" by (simp add: roots_of_complex_rf_poly(1))
      also have "(∏a∈set ?rts. [:- a, 1:]) = (∏a←?rts. [:- a, 1:])"
        by (rule prod.distinct_set_conv_list[OF roots_of_complex_rf_poly(2)])
      finally show ?thesis by simp
    qed
    finally have id2: "?exp (pi # pis) = ?p p ^ i * ?exp pis" by simp
    show ?case unfolding id id2 ..
  qed simp
  also have "?exp pis' = (∏(x, i)←xis. [:- x, 1:] ^ i)" unfolding xis ..
  finally show "p = smult c (∏(x, i)←xis. [:- x, 1:] ^ i)" unfolding p xis by simp

  from yun(2) have "0 ∉ snd ` set pis" by force
  with pis have "0 ∉ snd ` set pis'" by force
  thus "0 ∉ snd ` set xis" unfolding xis by force
qed

definition factor_complex_poly :: "complex poly ⇒ complex × (complex poly × nat) list" where
  "factor_complex_poly p = (case factor_complex_main p of
     (c,ris) ⇒ (c, map (λ (r,i). ([:-r,1:],i)) ris))"

lemma distinct_factor_complex_poly:
  "distinct (map fst (snd (factor_complex_poly p)))" 
proof -
  obtain c ris where main: "factor_complex_main p = (c,ris)" by force
  show ?thesis unfolding factor_complex_poly_def main split
    using distinct_factor_complex_main[of p, unfolded main]
    unfolding snd_conv o_def
    unfolding distinct_map by (force simp: inj_on_def)
qed


theorem factor_complex_poly: assumes fp: "factor_complex_poly p = (c,qis)"
  shows 
  "p = smult c (∏(q, i)←qis. q ^ i)" 
  "(q,i) ∈ set qis ⟹ irreducible q ∧ i ≠ 0 ∧ monic q ∧ degree q = 1"
proof -
  from fp[unfolded factor_complex_poly_def]
  obtain pis where fp: "factor_complex_main p = (c,pis)"
    and qis: "qis = map (λ(r, i). ([:- r, 1:], i)) pis"
    by (cases "factor_complex_main p", auto)
  from factor_complex_main[OF fp] have p: "p = smult c (∏(x, i)←pis. [:- x, 1:] ^ i)" and 0: "0 ∉ snd ` set pis" by auto
  show "p = smult c (∏(q, i)←qis. q ^ i)" unfolding p qis
    by (rule arg_cong[of _ _ "λ p. smult c (prod_list p)"], auto)
  show "(q,i) ∈ set qis ⟹ irreducible q ∧ i ≠ 0 ∧ monic q ∧ degree q = 1"
    using linear_irreducible_field[of q] using 0 unfolding qis by force
qed

end