Theory Missing_Polynomial_Factorial

section ‹More on Polynomials›

text ‹This theory contains several results on content, gcd, primitive part, etc..
  Moreover, there is a slightly improved code-equation for computing the gcd.›

theory Missing_Polynomial_Factorial
  imports "HOL-Computational_Algebra.Polynomial_Factorial"
   Polynomial_Interpolation.Missing_Polynomial  
begin

text ‹Improved code equation for @{const gcd_poly_code}
  which avoids computing the content twice.›
lemma gcd_poly_code_code[code]: "gcd_poly_code p q =
           (if p = 0 then normalize q else if q = 0 then normalize p else let
              c1 = content p;
              c2 = content q;
              p' = map_poly (λ x. x div c1) p;
              q' = map_poly (λ x. x div c2) q
              in smult (gcd c1 c2) (gcd_poly_code_aux p' q'))"
  unfolding gcd_poly_code_def Let_def primitive_part_def by simp

lemma gcd_smult: fixes f g :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
  defines cf: "cf ≡ content f"
  and cg: "cg ≡ content g"
shows "gcd (smult a f) g = (if a = 0 ∨ f = 0 then normalize g else
  smult (gcd a (cg div (gcd cf cg))) (gcd f g))"
proof (cases "a = 0 ∨ f = 0")
  case False
  let ?c = "content"
  let ?pp = primitive_part
  let ?ua = "unit_factor a"
  let ?na = "normalize a"
  define H where "H = gcd (?c f) (?c g)"
  have "H dvd ?c f" unfolding H_def by auto
  then obtain F where fh: "?c f = H * F" unfolding dvd_def by blast
  from False have cf0: "?c f ≠ 0" by auto
  hence H: "H ≠ 0" unfolding H_def by auto
  from arg_cong[OF fh, of "λ f. f div H"] H have F: "F = ?c f div H" by auto
  have "H dvd ?c g" unfolding H_def by auto
  then obtain G where gh: "?c g = H * G" unfolding dvd_def by blast
  from arg_cong[OF gh, of "λ f. f div H"] H have G: "G = ?c g div H" by auto
  have "coprime F G" using H unfolding F G H_def
    using cf0 div_gcd_coprime by blast
  have "is_unit ?ua" using False by simp
  then have ua: "is_unit [: ?ua :]"
    by (simp add: is_unit_const_poly_iff)
  have "gcd (smult a f) g = smult (gcd (?na * ?c f) (?c g))
     (gcd (smult ?ua (?pp f)) (?pp g))"
    unfolding gcd_poly_decompose[of "smult a f"]
    content_smult primitive_part_smult by simp
  also have "smult ?ua (?pp f) = ?pp f * [: ?ua :]" by simp
  also have "gcd … (?pp g) = gcd (?pp f) (?pp g)"
    unfolding gcd_mult_unit1[OF ua] ..
  also have "gcd (?na * ?c f) (?c g) = gcd ((?na * F) * H) (G * H)"
    unfolding fh gh by (simp add: ac_simps)
  also have "… = gcd (?na * F) G * normalize H" unfolding gcd_mult_right gcd.commute[of G]
    by (simp add: normalize_mult)
  also have "normalize H = H" by (metis H_def normalize_gcd)
  finally
  have "gcd (smult a f) g = smult (gcd (?na * F) G) (smult  H (gcd (?pp f) (?pp g)))" by simp
  also have "smult H (gcd (?pp f) (?pp g)) = gcd f g" unfolding H_def
    by (rule gcd_poly_decompose[symmetric])
  also have "gcd (?na * F) G = gcd (F * ?na) G" by (simp add: ac_simps)
  also have "… = gcd ?na G"
    using ‹coprime F G› by (simp add: gcd_mult_right_left_cancel ac_simps)
  finally show ?thesis unfolding G H_def cg cf using False by simp
next
  case True
  hence "gcd (smult a f) g = normalize g" by (cases "a = 0", auto)
  thus ?thesis using True by simp
qed

lemma gcd_smult_ex: assumes "a ≠ 0"
  shows "∃ b. gcd (smult a f) g = smult b (gcd f g) ∧ b ≠ 0"
proof (cases "f = 0")
  case True
  thus ?thesis by (intro exI[of _ 1], auto)
next
  case False
  hence id: "(a = 0 ∨ f = 0) = False" using assms by auto
  show ?thesis unfolding gcd_smult id if_False
    by (intro exI conjI, rule refl, insert assms, auto)
qed

lemma primitive_part_idemp[simp]:
  fixes f :: "'a :: {semiring_gcd,normalization_semidom_multiplicative} poly"
  shows "primitive_part (primitive_part f) = primitive_part f"
  by (metis content_primitive_part[of f] primitive_part_eq_0_iff primitive_part_prim)

lemma content_gcd_primitive:
   "f ≠ 0 ⟹ content (gcd (primitive_part f) g) = 1"
   "f ≠ 0 ⟹ content (gcd (primitive_part f) (primitive_part g)) = 1"
  by (metis (no_types, lifting) content_dvd_contentI content_primitive_part gcd_dvd1 is_unit_content_iff)+

lemma content_gcd_content: "content (gcd f g) = gcd (content f) (content g)"
  (is "?l = ?r")
proof -
  let ?c = "content"
  have "?l = normalize (gcd (?c f) (?c g)) *
    ?c (gcd (primitive_part f) (primitive_part g))"
    unfolding gcd_poly_decompose[of f g] content_smult ..
  also have "… = gcd (?c f) (?c g) *
    ?c (gcd (primitive_part f) (primitive_part g))" by simp
  also have "… = ?r" using content_gcd_primitive[of f g]
    by (metis (no_types, lifting) content_dvd_contentI content_eq_zero_iff
    content_primitive_part gcd_dvd2 gcd_eq_0_iff is_unit_content_iff mult_cancel_left1)
  finally show ?thesis .
qed

lemma gcd_primitive_part:
  "gcd (primitive_part f) (primitive_part g) = normalize (primitive_part (gcd f g))"
  proof(cases "f = 0")
    case True
    show ?thesis unfolding gcd_poly_decompose[of f g] gcd_0_left primitive_part_0 True
      by (simp add: associatedI primitive_part_dvd_primitive_partI)
  next
    case False
    have "normalize 1 = normalize (unit_factor (gcd (content f) (content g)))"
      by (simp add: False)
    then show ?thesis unfolding gcd_poly_decompose[of f g]
      by (metis (no_types) Polynomial.normalize_smult content_gcd_primitive(1)[OF False] content_times_primitive_part normalize_gcd primitive_part_smult)
qed

lemma primitive_part_gcd: "primitive_part (gcd f g)
  = unit_factor (gcd f g) * gcd (primitive_part f) (primitive_part g)"
  unfolding gcd_primitive_part
  by (metis (no_types, lifting)
  content_times_primitive_part gcd.normalize_idem mult_cancel_left2 mult_smult_left
  normalize_eq_0_iff normalize_mult_unit_factor primitive_part_eq_0_iff
  smult_content_normalize_primitive_part unit_factor_mult_normalize)

lemma primitive_part_normalize: 
  fixes f :: "'a :: {semiring_gcd,idom_divide,normalization_semidom_multiplicative} poly"
  shows "primitive_part (normalize f) = normalize (primitive_part f)"
proof (cases "f = 0")
  case True
  thus ?thesis by simp
next
  case False
  have "normalize (content (normalize (primitive_part f))) = 1"
    using content_primitive_part[OF False] content_dvd content_const
          content_dvd_contentI dvd_normalize_iff is_unit_content_iff by (metis (no_types))
  then have "content (normalize (primitive_part f)) = 1" by fastforce
  then have "content (normalize f) = 1 * content f"
    by (metis (no_types) content_smult mult.commute normalize_content
    smult_content_normalize_primitive_part)
  then have "content f = content (normalize f)"
    by simp
  then show ?thesis unfolding smult_content_normalize_primitive_part[of f,symmetric]
    by (metis (no_types) False content_times_primitive_part mult.commute mult_cancel_left
                                   mult_smult_right smult_content_normalize_primitive_part)
qed

lemma length_coeffs_primitive_part[simp]: "length (coeffs (primitive_part f)) = length (coeffs f)"
proof (cases "f = 0")
  case False
  hence "length (coeffs f) ≠ 0" "length (coeffs (primitive_part f)) ≠ 0" by auto
  thus ?thesis using degree_primitive_part[of f, unfolded degree_eq_length_coeffs] by linarith
qed simp

lemma degree_unit_factor[simp]: "degree (unit_factor f) = 0"
  by (simp add: monom_0 unit_factor_poly_def)

lemma degree_normalize[simp]: "degree (normalize f) = degree f"
proof (cases "f = 0")
  case False
  have "degree f = degree (unit_factor f * normalize f)" by simp
  also have "… = degree (unit_factor f) + degree (normalize f)"
    by (rule degree_mult_eq, insert False, auto)
  finally show ?thesis by simp
qed simp
  
lemma content_iff: "x dvd content p ⟷ (∀ c ∈ set (coeffs p). x dvd c)"
  by (simp add: content_def dvd_gcd_list_iff)
  
lemma is_unit_field_poly[simp]: "(p::'a::field poly) dvd 1 ⟷ p ≠ 0 ∧ degree p = 0"
proof(intro iffI conjI, unfold conj_imp_eq_imp_imp)
  assume "is_unit p"
  then obtain q where *: "p * q = 1" by (elim dvdE, auto)
  from * show p0: "p ≠ 0" by auto
  from * have q0: "q ≠ 0" by auto
  from * degree_mult_eq[OF p0 q0]
  show "degree p = 0" by auto
next
  assume "degree p = 0"
  from degree0_coeffs[OF this]
  obtain c where c: "p = [:c:]" by auto
  assume "p ≠ 0"
  with c have "c ≠ 0" by auto
  with c have "1 = p * [:1/c:]" by auto
  from dvdI[OF this] show "is_unit p".
qed

definition primitive where
  "primitive f ⟷ (∀x. (∀y ∈ set (coeffs f). x dvd y) ⟶ x dvd 1)"

lemma primitiveI:
  assumes "(⋀x. (⋀y. y ∈ set (coeffs f) ⟹ x dvd y) ⟹ x dvd 1)"
  shows "primitive f" by (insert assms, auto simp: primitive_def)

lemma primitiveD:
  assumes "primitive f"
  shows "(⋀y. y ∈ set (coeffs f) ⟹ x dvd y) ⟹ x dvd 1"
    by (insert assms, auto simp: primitive_def)

lemma not_primitiveE:
  assumes "¬ primitive f"
      and "⋀x. (⋀y. y ∈ set (coeffs f) ⟹ x dvd y) ⟹ ¬ x dvd 1 ⟹ thesis"
  shows thesis by (insert assms, auto simp: primitive_def)

lemma primitive_iff_content_eq_1[simp]:
  fixes f :: "'a :: semiring_gcd poly"
  shows "primitive f ⟷ content f = 1"
proof(intro iffI primitiveI)
  fix x
  assume "(⋀y. y ∈ set (coeffs f) ⟹ x dvd y)"
  from gcd_list_greatest[of "coeffs f", OF this]
  have "x dvd content f" by (simp add: content_def)
  also assume "content f = 1"
  finally show "x dvd 1".
next
  assume "primitive f"
  from primitiveD[OF this list_gcd[of _ "coeffs f"], folded content_def]
  show "content f = 1" by simp
qed

lemma primitive_prod_list:
  fixes fs :: "'a :: {factorial_semiring,semiring_Gcd,normalization_semidom_multiplicative} poly list"
  assumes "primitive (prod_list fs)" and "f ∈ set fs" shows "primitive f"
proof (insert assms, induct fs arbitrary: f)
  case (Cons f' fs)
  from Cons.prems
  have "is_unit (content f' * content (prod_list fs))" by (auto simp: content_mult)
  from this[unfolded is_unit_mult_iff]
  have "content f' = 1" and "content (prod_list fs) = 1" by auto
  moreover from Cons.prems have "f = f' ∨ f ∈ set fs" by auto
  ultimately show ?case using Cons.hyps[of f] by auto
qed auto

lemma irreducible_imp_primitive:
  fixes f :: "'a :: {idom,semiring_gcd} poly"
  assumes irr: "irreducible f" and deg: "degree f ≠ 0" shows "primitive f"
proof (rule ccontr)
  assume not: "¬ ?thesis"
  then have "¬ [:content f:] dvd 1" by simp
  moreover have "f = [:content f:] * primitive_part f" by simp
    note Factorial_Ring.irreducibleD[OF irr this]
  ultimately
  have "primitive_part f dvd 1" by auto
  from this[unfolded poly_dvd_1] have "degree f = 0" by auto
  with deg show False by auto
qed
  
lemma irreducible_primitive_connect:
  fixes f :: "'a :: {idom,semiring_gcd} poly"
  assumes cf: "primitive f" shows "irreducible⇩d f ⟷ irreducible f" (is "?l ⟷ ?r")
proof
  assume l: ?l show ?r
  proof(rule ccontr, elim not_irreducibleE)
    from l have deg: "degree f > 0" by (auto dest: irreducible⇩dD)
    from cf have f0: "f ≠ 0" by auto
    then show "f = 0 ⟹ False" by auto
    show "f dvd 1 ⟹ False" using deg by (auto simp:poly_dvd_1)
    fix a b assume fab: "f = a * b" and a1: "¬ a dvd 1" and b1: "¬ b dvd 1"
    then have af: "a dvd f" and bf: "b dvd f" by auto
    with f0 have a0: "a ≠ 0" and b0: "b ≠ 0" by auto
    from irreducible⇩dD(2)[OF l, of a] af dvd_imp_degree_le[OF af f0]
    have "degree a = 0 ∨ degree a = degree f"
      by (metis degree_smult_le irreducible⇩d_dvd_smult l le_antisym Nat.neq0_conv)
    then show False
    proof(elim disjE)
      assume "degree a = 0"
      then obtain c where ac: "a = [:c:]" by (auto dest: degree0_coeffs)
      from fab[unfolded ac] have "c dvd content f" by (simp add: content_iff coeffs_smult)
      with cf have "c dvd 1" by simp
      then have "a dvd 1" by (auto simp: ac)
      with a1 show False by auto
    next
      assume dega: "degree a = degree f"
      with f0 degree_mult_eq[OF a0 b0] fab have "degree b = 0" by (auto simp: ac_simps)
      then obtain c where bc: "b = [:c:]" by (auto dest: degree0_coeffs)
      from fab[unfolded bc] have "c dvd content f" by (simp add: content_iff coeffs_smult)
      with cf have "c dvd 1" by simp
      then have "b dvd 1" by (auto simp: bc)
      with b1 show False by auto
    qed
  qed
next
  assume r: ?r
  show ?l
  proof(intro irreducible⇩dI)
    show "degree f > 0"
    proof (rule ccontr)
      assume "¬degree f > 0"
      then obtain f0 where f: "f = [:f0:]" by (auto dest: degree0_coeffs)
      from cf[unfolded this] have "normalize f0 = 1" by auto
      then have "f0 dvd 1" by (unfold normalize_1_iff)
      with r[unfolded f irreducible_const_poly_iff] show False by auto
    qed
  next
    fix g h assume deg_g: "degree g > 0" and deg_gf: "degree g < degree f" and fgh: "f = g * h"
    with r have "g dvd 1 ∨ h dvd 1" by auto
    with deg_g have "degree h = 0" by (auto simp: poly_dvd_1)
    with deg_gf[unfolded fgh] degree_mult_eq[of g h] show False by (cases "g = 0 ∨ h = 0", auto)
  qed
qed

lemma deg_not_zero_imp_not_unit: 
  fixes f:: "'a::{idom_divide,semidom_divide_unit_factor} poly"
  assumes deg_f: "degree f > 0"
  shows "¬ is_unit f"
proof -
  have "degree (normalize f) > 0" 
    using deg_f degree_normalize by auto  
  hence "normalize f ≠ 1"
    by fastforce
  thus "¬ is_unit f" using normalize_1_iff by auto
qed

lemma content_pCons[simp]: "content (pCons a p) = gcd a (content p)"
proof(induct p arbitrary: a)
  case 0 show ?case by simp
next
  case (pCons c p)
  then show ?case by (cases "p = 0", auto simp: content_def cCons_def)
qed

lemma content_field_poly:
  fixes f :: "'a :: {field,semiring_gcd} poly"
  shows "content f = (if f = 0 then 0 else 1)"
  by(induct f, auto simp: dvd_field_iff is_unit_normalize)


end