Theory Square_Free_Int_To_Square_Free_GFp

(*
    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
*)
section ‹Reconstructing Factors of Integer Polynomials›

subsection ‹Square-Free Polynomials over Finite Fields and Integers›
theory Square_Free_Int_To_Square_Free_GFp
imports   
  Subresultants.Subresultant_Gcd 
  Polynomial_Factorization.Rational_Factorization
  Finite_Field
  Polynomial_Factorization.Square_Free_Factorization
begin

lemma square_free_int_rat: assumes sf: "square_free f"
  shows "square_free (map_poly rat_of_int f)"
proof -
  let ?r = "map_poly rat_of_int" 
  from sf[unfolded square_free_def] have f0: "f  0" " q. degree q  0  ¬ q * q dvd f" by auto
  show ?thesis
  proof (rule square_freeI)
    show "?r f  0" using f0 by auto
    fix q
    assume dq: "degree q > 0" and dvd: "q * q dvd ?r f" 
    hence q0: "q  0" by auto
    obtain q' c where norm: "rat_to_normalized_int_poly q = (c,q')" by force
    from rat_to_normalized_int_poly[OF norm] have c0: "c  0" by auto
    note q = rat_to_normalized_int_poly(1)[OF norm]
    from dvd obtain k where rf: "?r f = q * (q * k)" unfolding dvd_def by (auto simp: ac_simps)
    from rat_to_int_factor_explicit[OF this norm] obtain s where 
      f: "f = q' * smult (content f) s" by auto
    let ?s = "smult (content f) s" 
    from arg_cong[OF f, of ?r] c0 
    have "?r f = q * (smult (inverse c) (?r ?s))" 
      by (simp add: field_simps q hom_distribs)
    from arg_cong[OF this[unfolded rf], of "λ f. f div q"] q0 
    have "q * k = smult (inverse c) (?r ?s)" 
      by (metis nonzero_mult_div_cancel_left)
    from arg_cong[OF this, of "smult c"] have "?r ?s = q * smult c k" using c0
      by (auto simp: field_simps)
    from rat_to_int_factor_explicit[OF this norm] obtain t where "?s = q' * t" by blast
    from f[unfolded this] sf[unfolded square_free_def] f0 have "degree q' = 0" by auto
    with rat_to_normalized_int_poly(4)[OF norm] dq show False by auto
  qed
qed

lemma content_free_unit:
  assumes "content (p::'a::{idom,semiring_gcd} poly) = 1"
  shows "p dvd 1  degree p = 0"
  by (insert assms, auto dest!:degree0_coeffs simp: normalize_1_iff poly_dvd_1)

lemma square_free_imp_resultant_non_zero: assumes sf: "square_free (f :: int poly)"
  shows "resultant f (pderiv f)  0" 
proof (cases "degree f = 0")
  case True
  from degree0_coeffs[OF this] obtain c where f: "f = [:c:]" by auto
  with sf have c: "c  0" unfolding square_free_def by auto  
  show ?thesis unfolding f by simp
next
  case False note deg = this
  define pp where "pp = primitive_part f" 
  define c where "c = content f"
  from sf have f0: "f  0" unfolding square_free_def by auto
  hence c0: "c  0" unfolding c_def by auto
  have f: "f = smult c pp" unfolding c_def pp_def unfolding content_times_primitive_part[of f] ..
  from sf[unfolded f] c0 have sf': "square_free pp" by (metis dvd_smult smult_0_right square_free_def)  
  from deg[unfolded f] c0 have deg': " x. degree pp > 0  x" by auto
  from content_primitive_part[OF f0] have cp: "content pp = 1" unfolding pp_def .
  let ?p' = "pderiv pp" 
  {
    assume "resultant pp ?p' = 0" 
    from this[unfolded resultant_0_gcd] have "¬ coprime pp ?p'" by auto
    then obtain r where r: "r dvd pp" "r dvd ?p'" "¬ r dvd 1"
      by (blast elim: not_coprimeE) 
    from r(1) obtain k where "pp = r * k" ..
    from pos_zmult_eq_1_iff_lemma[OF arg_cong[OF this, 
      of content, unfolded content_mult cp, symmetric]] content_ge_0_int[of r]
    have cr: "content r = 1" by auto
    with r(3) content_free_unit have dr: "degree r  0" by auto
    let ?r = "map_poly rat_of_int"
    from r(1) have dvd: "?r r dvd ?r pp" unfolding dvd_def by (auto simp: hom_distribs)
    from r(2) have "?r r dvd ?r ?p'" apply (intro of_int_poly_hom.hom_dvd) by auto
    also have "?r ?p' = pderiv (?r pp)" unfolding of_int_hom.map_poly_pderiv ..
    finally have dvd': "?r r dvd pderiv (?r pp)" by auto
    from dr have dr': "degree (?r r)  0" by simp
    from square_free_imp_separable[OF square_free_int_rat[OF sf']]
    have "separable (?r pp)" .
    hence cop: "coprime (?r pp) (pderiv (?r pp))" unfolding separable_def .
    from f0 f have pp0: "pp  0" by auto
    from dvd dvd' have "?r r dvd gcd (?r pp) (pderiv (?r pp))" by auto
    from divides_degree[OF this] pp0 have "degree (?r r)  degree (gcd (?r pp) (pderiv (?r pp)))" 
      by auto
    with dr' have "degree (gcd (?r pp) (pderiv (?r pp)))  0" by auto
    hence "¬ coprime (?r pp) (pderiv (?r pp))" by auto
    with cop have False by auto
  }
  hence "resultant pp ?p'  0" by auto
  with resultant_smult_left[OF c0, of pp ?p', folded f] c0 
  have "resultant f ?p'  0" by auto
  with resultant_smult_right[OF c0, of f ?p', folded pderiv_smult f] c0
  show "resultant f (pderiv f)  0" by auto
qed

lemma large_mod_0: assumes "(n :: int) > 1" "¦k¦ < n" "k mod n = 0" shows "k = 0" 
proof -
  from k mod n = 0 have "n dvd k"
    by auto
  then obtain m where "k = n * m" ..
  with n > 1 ¦k¦ < n show ?thesis
    by (auto simp add: abs_mult)
qed

definition separable_bound :: "int poly  int" where
  "separable_bound f = max (abs (resultant f (pderiv f))) 
    (max (abs (lead_coeff f)) (abs (lead_coeff (pderiv f))))"

lemma square_free_int_imp_resultant_non_zero_mod_ring: assumes sf: "square_free f" 
  and large: "int CARD('a) > separable_bound f"
  shows "resultant (map_poly of_int f :: 'a :: prime_card mod_ring poly) (pderiv (map_poly of_int f))  0
   map_poly of_int f  (0 :: 'a mod_ring poly)" 
proof (intro conjI, rule notI)
  let ?i = "of_int :: int  'a mod_ring"
  let ?m = "of_int_poly :: _  'a mod_ring poly"
  let ?f = "?m f" 
  from sf[unfolded square_free_def] have f0: "f  0" by auto
  hence lf: "lead_coeff f  0" by auto
  {
    fix k :: int
    have C1: "int CARD('a) > 1" using prime_card[where 'a = 'a] by (auto simp: prime_nat_iff)
    assume "abs k < CARD('a)" and "?i k = 0" 
    hence "k = 0" unfolding of_int_of_int_mod_ring
        by (transfer) (rule large_mod_0[OF C1])
  } note of_int_0 = this
  from square_free_imp_resultant_non_zero[OF sf]
  have non0: "resultant f (pderiv f)  0" .
  {
    fix g :: "int poly" 
    assume abs: "abs (lead_coeff g) < CARD('a)"
    have "degree (?m g) = degree g" by (rule degree_map_poly, insert of_int_0[OF abs], auto)
  } note deg = this
  note large = large[unfolded separable_bound_def]
  from of_int_0[of "lead_coeff f"] large lf have "?i (lead_coeff f)  0" by auto
  thus f0: "?f  0" unfolding poly_eq_iff by auto  
  assume 0: "resultant ?f (pderiv ?f) = 0" 
  have "resultant ?f (pderiv ?f) = ?i (resultant f (pderiv f))"
    unfolding of_int_hom.map_poly_pderiv[symmetric]
    by (subst of_int_hom.resultant_map_poly(1)[OF deg deg], insert large, auto simp: hom_distribs)
  from of_int_0[OF _ this[symmetric, unfolded 0]] non0
  show False using large by auto
qed

lemma square_free_int_imp_separable_mod_ring: assumes sf: "square_free f" 
  and large: "int CARD('a) > separable_bound f"
  shows "separable (map_poly of_int f :: 'a :: prime_card mod_ring poly)" 
proof - 
  define g where "g = map_poly (of_int :: int  'a mod_ring) f"
  from square_free_int_imp_resultant_non_zero_mod_ring[OF sf large]
  have res: "resultant g (pderiv g)  0" and g: "g  0" unfolding g_def by auto
  from res[unfolded resultant_0_gcd] have "degree (gcd g (pderiv g)) = 0" by auto
  from degree0_coeffs[OF this]
  have "separable g" unfolding separable_def
    by (metis degree_pCons_0 g gcd_eq_0_iff is_unit_gcd is_unit_iff_degree)
  thus ?thesis unfolding g_def .
qed

lemma square_free_int_imp_square_free_mod_ring: assumes sf: "square_free f" 
  and large: "int CARD('a) > separable_bound f"
shows "square_free (map_poly of_int f :: 'a :: prime_card mod_ring poly)" 
  using separable_imp_square_free[OF square_free_int_imp_separable_mod_ring[OF assms]] .

end