Theory Polynomial_Factorization.Gauss_Lemma

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
(*TODO: Rename! *)
section ‹Gauss Lemma›

text ‹We formalized Gauss Lemma, that the content of a product of two polynomials $p$ and $q$
  is the product of the contents of $p$ and $q$. As a corollary we provide an algorithm
  to convert a rational factor of an integer polynomial into an integer factor.
  
  In contrast to the theory on unique factorization domains -- where Gauss Lemma is also proven 
   in a more generic setting --
  we are here in an executable setting and do not use the unspecified $some-gcd$ function.
  Moreover, there is a slight difference in the definition of content: in this theory it is only
  defined for integer-polynomials, whereas in the UFD theory, the content is defined for 
  polynomials in the fraction field.›

theory Gauss_Lemma
imports 
  "HOL-Computational_Algebra.Primes"
  "HOL-Computational_Algebra.Field_as_Ring"
  Polynomial_Interpolation.Ring_Hom_Poly
  Missing_Polynomial_Factorial
begin

lemma primitive_part_alt_def:
  "primitive_part p = sdiv_poly p (content p)"
  by (simp add: primitive_part_def sdiv_poly_def)

definition common_denom :: "rat list  int × int list" where
  "common_denom xs  let 
     nds = map quotient_of xs;
     denom = list_lcm (map snd nds);
     ints = map (λ (n,d). n * denom div d) nds
   in (denom, ints)"

definition rat_to_int_poly :: "rat poly  int × int poly" where
  "rat_to_int_poly p  let
     ais = coeffs p;
     d = fst (common_denom ais)
   in (d, map_poly (λ x. case quotient_of x of (p,q)  p * d div q) p)"

definition rat_to_normalized_int_poly :: "rat poly  rat × int poly" where
  "rat_to_normalized_int_poly p  if p = 0 then (1,0) else case rat_to_int_poly p of (s,q)
     (of_int (content q) / of_int s, primitive_part q)"

lemma rat_to_normalized_int_poly_code[code]:
  "rat_to_normalized_int_poly p = (if p = 0 then (1,0) else case rat_to_int_poly p of (s,q)
     let c = content q in (of_int c / of_int s, sdiv_poly q c))"
    unfolding Let_def rat_to_normalized_int_poly_def primitive_part_alt_def ..

lemma common_denom: assumes cd: "common_denom xs = (dd,ys)"
  shows "xs = map (λ i. of_int i / of_int dd) ys" "dd > 0"
  "x. x  set xs  rat_of_int (case quotient_of x of (n, x)  n * dd div x) / rat_of_int dd = x"
proof -
  let ?nds = "map quotient_of xs"
  define nds where "nds = ?nds"
  let ?denom = "list_lcm (map snd nds)"
  let ?ints = "map (λ (n,d). n * dd div d) nds"
  from cd[unfolded common_denom_def Let_def]
  have dd: "dd = ?denom" and ys: "ys = ?ints" unfolding nds_def by auto
  show dd0: "dd > 0" unfolding dd 
    by (intro list_lcm_pos(3), auto simp: nds_def quotient_of_nonzero)
  {
    fix x
    assume x: "x  set xs"
    obtain p q where quot: "quotient_of x = (p,q)" by force
    from x have "(p,q)  set nds" unfolding nds_def using quot by force
    hence "q  set (map snd nds)" by force
    from list_lcm[OF this] have q: "q dvd dd" unfolding dd .
    show "rat_of_int (case quotient_of x of (n, x)  n * dd div x) / rat_of_int dd = x"
      unfolding quot split unfolding quotient_of_div[OF quot]  
    proof -
      have f1: "q * (dd div q) = dd"
        using dvd_mult_div_cancel q by blast
      have "rat_of_int (dd div q)  0"
        using dd0 dvd_mult_div_cancel q by fastforce
      thus "rat_of_int (p * dd div q) / rat_of_int dd = rat_of_int p / rat_of_int q"
        using f1 by (metis (no_types) div_mult_swap mult_divide_mult_cancel_right of_int_mult q)
    qed
  } note main = this
  show "xs = map (λ i. of_int i / of_int dd) ys" unfolding ys map_map o_def nds_def
    by (rule sym, rule map_idI, rule main)
qed

lemma rat_to_int_poly: assumes "rat_to_int_poly p = (d,q)"
  shows "p = smult (inverse (of_int d)) (map_poly of_int q)" "d > 0"
proof -
  let ?f = "λ x. case quotient_of x of (pa, x)  pa * d div x"
  define f where "f = ?f"
  from assms[unfolded rat_to_int_poly_def Let_def] 
    obtain xs where cd: "common_denom (coeffs p) = (d,xs)"
    and q: "q = map_poly f p" unfolding f_def by (cases "common_denom (coeffs p)", auto)
  from common_denom[OF cd] have d: "d > 0"  and 
    id: " x. x  set (coeffs p)  rat_of_int (f x) / rat_of_int d = x" 
    unfolding f_def by auto
  have f0: "f 0 = 0" unfolding f_def by auto
  have id: "rat_of_int (f (coeff p n)) / rat_of_int d = coeff p n" for n
    using id[of "coeff p n"] f0 range_coeff by (cases "coeff p n = 0", auto)
  show "d > 0" by fact
  show "p = smult (inverse (of_int d)) (map_poly of_int q)"
    unfolding q smult_as_map_poly using id f0
    by (intro poly_eqI, auto simp: field_simps coeff_map_poly)
qed

lemma content_ge_0_int: "content p  (0 :: int)"
  unfolding content_def
  by (cases "coeffs p", auto)

lemma abs_content_int[simp]: fixes p :: "int poly"
  shows "abs (content p) = content p" using content_ge_0_int[of p] by auto

lemma content_smult_int: fixes p :: "int poly" 
  shows "content (smult a p) = abs a * content p" by simp

lemma normalize_non_0_smult: " a. (a :: 'a :: semiring_gcd)  0  smult a (primitive_part p) = p"
  by (cases "p = 0", rule exI[of _ 1], simp, rule exI[of _ "content p"], auto)

lemma rat_to_normalized_int_poly: assumes "rat_to_normalized_int_poly p = (d,q)"
  shows "p = smult d (map_poly of_int q)" "d > 0" "p  0  content q = 1" "degree q = degree p"
proof -
  have "p = smult d (map_poly of_int q)  d > 0  (p  0  content q = 1)"
  proof (cases "p = 0")
    case True
    thus ?thesis using assms unfolding rat_to_normalized_int_poly_def
      by (auto simp: eval_poly_def)
  next
    case False
    hence p0: "p  0" by auto
    obtain s r where id: "rat_to_int_poly p = (s,r)" by force
    let ?cr = "rat_of_int (content r)"
    let ?s = "rat_of_int s"
    let ?q = "map_poly rat_of_int q"
    from rat_to_int_poly[OF id] have p: "p = smult (inverse ?s) (map_poly of_int r)"
    and s: "s > 0" by auto
    let ?q = "map_poly rat_of_int q"
    from p0 assms[unfolded rat_to_normalized_int_poly_def id split]
    have d: "d = ?cr / ?s" and q: "q = primitive_part r" by auto
    from content_times_primitive_part[of r, folded q] have qr: "smult (content r) q = r" .
    have "smult d ?q = smult (?cr / ?s) ?q"
      unfolding d by simp
    also have "?cr / ?s = ?cr * inverse ?s" by (rule divide_inverse)
    also have " = inverse ?s * ?cr" by simp
    also have "smult (inverse ?s * ?cr) ?q = smult (inverse ?s) (smult ?cr ?q)" by simp
    also have "smult ?cr ?q = map_poly of_int (smult (content r) q)" by (simp add: hom_distribs)
    also have " = map_poly of_int r" unfolding qr ..
    finally have pq: "p = smult d ?q" unfolding p by simp
    from p p0 have r0: "r  0" by auto
    from content_eq_zero_iff[of r] content_ge_0_int[of r] r0 have cr: "?cr > 0" by linarith
    with s have d0: "d > 0" unfolding d by auto
    from content_primitive_part[OF r0] have cq: "content q = 1" unfolding q .
    from pq d0 cq show ?thesis by auto
  qed
  thus p: "p = smult d (map_poly of_int q)" and d: "d > 0" and "p  0  content q = 1" by auto
  show "degree q = degree p" unfolding p smult_as_map_poly
    by (rule sym, subst map_poly_map_poly, force+, rule degree_map_poly, insert d, auto)
qed

lemma content_dvd_1:
  "content g = 1" if "content f = (1 :: 'a :: semiring_gcd)" "g dvd f" 
proof -
  from g dvd f have "content g dvd content f"
    by (rule content_dvd_contentI)
  with content f = 1 show ?thesis
    by simp
qed

lemma dvd_smult_int: fixes c :: int assumes c: "c  0"
  and dvd: "q dvd (smult c p)"
  shows "primitive_part q dvd p"
proof (cases "p = 0")
  case True thus ?thesis by auto
next
  case False note p0 = this
  let ?cp = "smult c p"
  from p0 c have cp0: "?cp  0" by auto
  from dvd obtain r where prod: "?cp = q * r" unfolding dvd_def by auto
  from prod cp0 have q0: "q  0" and r0: "r  0" by auto
  let ?c = "content :: int poly  int"
  let ?n = "primitive_part :: int poly  int poly"
  let ?pn = "λ p. smult (?c p) (?n p)"
  have cq: "(?c q = 0) = False" using content_eq_zero_iff q0 by auto
  from prod have id1: "?cp = ?pn q * ?pn r" unfolding content_times_primitive_part by simp
  from arg_cong[OF this, of content, unfolded content_smult_int content_mult
    content_primitive_part[OF r0] content_primitive_part[OF q0], symmetric]
    p0[folded content_eq_zero_iff] c
  have "abs c dvd ?c q * ?c r" unfolding dvd_def by auto
  hence "c dvd ?c q * ?c r" by auto
  then obtain d where id: "?c q * ?c r = c * d" unfolding dvd_def by auto
  have "?cp = ?pn q * ?pn r" by fact
  also have " = smult (c * d) (?n q * ?n r)" unfolding id [symmetric]
    by (metis content_mult content_times_primitive_part primitive_part_mult)
  finally have id: "?cp = smult c (?n q * smult d (?n r))" by (simp add: mult.commute)
  interpret map_poly_inj_zero_hom "(*) c" using c by (unfold_locales, auto)
  have "p = ?n q * smult d (?n r)" using id[unfolded smult_as_map_poly[of c]] by auto
  thus dvd: "?n q dvd p" unfolding dvd_def by blast
qed

lemma irreducibled_primitive_part:
  fixes p :: "int poly" (* can be relaxed but primitive_part_mult has bad type constraint *)
  shows "irreducibled (primitive_part p)  irreducibled p" (is "?l  ?r")
proof (rule iffI, rule irreducibledI)
  assume l: ?l
  show "degree p > 0" using l by auto
  have dpp: "degree (primitive_part p) = degree p" by simp
  fix q r
  assume deg: "degree q < degree p" "degree r < degree p" and "p = q * r"
  then have pp: "primitive_part p = primitive_part q * primitive_part r" by (simp add: primitive_part_mult)
  have "¬ irreducibled (primitive_part p)"
    apply (intro reducibledI, rule exI[of _ "primitive_part q"], rule exI[of _ "primitive_part r"], unfold dpp)
    using deg pp by auto
  with l show False by auto
next
  show "?r  ?l" by (metis irreducibled_smultI normalize_non_0_smult)
qed

lemma irreducibled_smult_int:
  fixes c :: int assumes c: "c  0"
  shows "irreducibled (smult c p) = irreducibled p" (is "?l = ?r")
  using irreducibled_primitive_part[of "smult c p", unfolded primitive_part_smult] c
  apply (cases "c < 0", simp)
  apply (metis add.inverse_inverse add.inverse_neutral c irreducibled_smultI normalize_non_0_smult smult_1_left smult_minus_left)
  apply (simp add: irreducibled_primitive_part)
  done

lemma irreducibled_as_irreducible:
  fixes p :: "int poly"
  shows "irreducibled p  irreducible (primitive_part p)"
  using irreducible_primitive_connect[of "primitive_part p"]
  by (cases "p = 0", auto simp: irreducibled_primitive_part)


lemma rat_to_int_factor_content_1: fixes p :: "int poly" 
  assumes cp: "content p = 1"
  and pgh: "map_poly rat_of_int p = g * h"
  and g: "rat_to_normalized_int_poly g = (r,rg)"
  and h: "rat_to_normalized_int_poly h = (s,sh)"
  and p: "p  0"
  shows "p = rg * sh"
proof -
  let ?r = "rat_of_int"
  let ?rp = "map_poly ?r"
  from p have rp0: "?rp p  0" by simp
  with pgh have g0: "g  0" and h0: "h  0" by auto
  from rat_to_normalized_int_poly[OF g] g0 
  have r: "r > 0" "r  0" and g: "g = smult r (?rp rg)" and crg: "content rg = 1" by auto
  from rat_to_normalized_int_poly[OF h] h0 
  have s: "s > 0" "s  0" and h: "h = smult s (?rp sh)" and csh: "content sh = 1" by auto
  let ?irs = "inverse (r * s)"
  from r s have irs0: "?irs  0" by (auto simp: field_simps)
  have "?rp (rg * sh) = ?rp rg * ?rp sh" by (simp add: hom_distribs)
  also have " = smult ?irs (?rp p)" unfolding pgh g h using r s
    by (simp add: field_simps)
  finally have id: "?rp (rg * sh) = smult ?irs (?rp p)" by auto
  have rsZ: "?irs  "
  proof (rule ccontr)
    assume not: "¬ ?irs  "
    obtain n d where irs': "quotient_of ?irs = (n,d)" by force
    from quotient_of_denom_pos[OF irs'] have "d > 0" .
    from not quotient_of_div[OF irs'] have "d  1" "d  0" and irs: "?irs = ?r n / ?r d" by auto
    with irs0 have n0: "n  0" by auto
    from d > 0 d  1 have "d  2" and "¬ d dvd 1" by auto
    with content_iff[of d p, unfolded cp] obtain c where 
      c: "c  set (coeffs p)" and dc: "¬ d dvd c" 
      by auto
    from c range_coeff[of p] obtain i where "c = coeff p i" by auto 
    from arg_cong[OF id, of "λ p. coeff p i", 
      unfolded coeff_smult of_int_hom.coeff_map_poly_hom this[symmetric] irs]
    have "?r n / ?r d * ?r c  " by (metis Ints_of_int)
    also have "?r n / ?r d * ?r c = ?r (n * c) / ?r d" by simp
    finally have inZ: "?r (n * c) / ?r d  " .
    have cop: "coprime n d" by (rule quotient_of_coprime[OF irs'])
    (* now there comes tedious reasoning that `coprime n d` `¬ d dvd c` ` nc / d ∈ ℤ` yields a 
       contradiction *)
    define prod where "prod = ?r (n * c) / ?r d"
    obtain n' d' where quot: "quotient_of prod = (n',d')" by force
    have qr: " x. quotient_of (?r x) = (x, 1)"
      using Rat.of_int_def quotient_of_int by auto
    from quotient_of_denom_pos[OF quot] have "d' > 0" .
    with quotient_of_div[OF quot] inZ[folded prod_def] have "d' = 1"
      by (metis Ints_cases Rat.of_int_def old.prod.inject quot quotient_of_int)
    with quotient_of_div[OF quot] have "prod = ?r n'" by auto
    from arg_cong[OF this, of quotient_of, unfolded prod_def rat_divide_code qr Let_def split]
    have "Rat.normalize (n * c, d) = (n',1)" by simp
    from normalize_crossproduct[OF d  0, of 1 "n * c" n', unfolded this]
    have id: "n * c = n' * d" by auto 
    from quotient_of_coprime[OF irs'] have "coprime n d" .
    with id have "d dvd c"
      by (metis coprime_commute coprime_dvd_mult_right_iff dvd_triv_right)
    with dc show False ..
  qed
  then obtain irs where irs: "?irs = ?r irs" unfolding Ints_def by blast
  from id[unfolded irs, folded hom_distribs, unfolded of_int_poly_hom.eq_iff]
  have p: "rg * sh = smult irs p" by auto
  have "content (rg * sh) = 1" unfolding content_mult crg csh by auto
  from this[unfolded p content_smult_int cp] have "abs irs = 1" by simp
  hence "abs ?irs = 1" using irs by auto
  with r s have "?irs = 1" by auto
  with irs have "irs = 1" by auto
  with p show p: "p = rg * sh" by auto
qed

lemma rat_to_int_factor_explicit: fixes p :: "int poly" 
  assumes pgh: "map_poly rat_of_int p = g * h"
  and g: "rat_to_normalized_int_poly g = (r,rg)"
  shows " r. p = rg * smult (content p) r"
proof -
  show ?thesis
  proof (cases "p = 0")
    case True
    show ?thesis unfolding True
      by (rule exI[of _ 0], auto simp: degree_monom_eq)
  next
    case False
    hence p: "p  0" by auto
    let ?r = "rat_of_int"
    let ?rp = "map_poly ?r"
    define q where "q = primitive_part p"
    from content_times_primitive_part[of p, folded q_def] content_eq_zero_iff[of p] p
      obtain a where a: "a  0" and pq: "p = smult a q" and acp: "content p = a" by metis
    from a pq p have ra: "?r a  0" and q0: "q  0" by auto
    from content_primitive_part[OF p, folded q_def] have cq: "content q = 1" by auto
    obtain s sh where h: "rat_to_normalized_int_poly (smult (inverse (?r a)) h) = (s,sh)" by force
    from arg_cong[OF pgh[unfolded pq], of "smult (inverse (?r a))"] ra
    have "?rp q = g * smult (inverse (?r a)) h" by (auto simp: hom_distribs)
    from rat_to_int_factor_content_1[OF cq this g h q0]
    have qrs: "q = rg * sh" .
    show ?thesis unfolding acp unfolding pq qrs 
      by (rule exI[of _ sh], auto)
  qed
qed

lemma rat_to_int_factor: fixes p :: "int poly" 
  assumes pgh: "map_poly rat_of_int p = g * h"
  shows " g' h'. p = g' * h'  degree g' = degree g  degree h' = degree h"
proof(cases "p = 0")
  case True
  with pgh have "g = 0  h = 0" by auto
  then show ?thesis
    by (metis True degree_0 mult_hom.hom_zero mult_zero_left rat_to_normalized_int_poly(4) surj_pair)
next
  case False
  obtain r rg where ri: "rat_to_normalized_int_poly (smult (1 / of_int (content p)) g) = (r,rg)" by force
  obtain q qh where ri2: "rat_to_normalized_int_poly h = (q,qh)" by force
  show ?thesis
  proof (intro exI conjI)
    have "of_int_poly (primitive_part p) = smult (1 / of_int (content p)) (g * h)"
      apply (auto simp: primitive_part_def pgh[symmetric] smult_map_poly map_poly_map_poly o_def intro!: map_poly_cong)
      by (metis (no_types, lifting) content_dvd_coeffs div_by_0 dvd_mult_div_cancel floor_of_int nonzero_mult_div_cancel_left of_int_hom.hom_zero of_int_mult)
    also have " = smult (1 / of_int (content p)) g * h" by simp
    finally have "of_int_poly (primitive_part p) = ".
    note main = rat_to_int_factor_content_1[OF _ this ri ri2, simplified, OF False]
    show "p = smult (content p) rg * qh" by (simp add: main[symmetric])
    from ri2 show "degree qh = degree h" by (fact rat_to_normalized_int_poly)
    from rat_to_normalized_int_poly(4)[OF ri] False
    show "degree (smult (content p) rg) = degree g" by auto
  qed
qed

lemma rat_to_int_factor_normalized_int_poly: fixes p :: "rat poly" 
  assumes pgh: "p = g * h"
  and p: "rat_to_normalized_int_poly p = (i,ip)"
  shows " g' h'. ip = g' * h'  degree g' = degree g"
proof -
  from rat_to_normalized_int_poly[OF p]
  have p: "p = smult i (map_poly rat_of_int ip)" and i: "i  0" by auto
  from arg_cong[OF p, of "smult (inverse i)", unfolded pgh] i
  have "map_poly rat_of_int ip = g * smult (inverse i) h" by auto
  from rat_to_int_factor[OF this] show ?thesis by auto
qed

(* TODO: move *)
lemma irreducible_smult [simp]:
  fixes c :: "'a :: field"
  shows "irreducible (smult c p)  irreducible p  c  0"
  using irreducible_mult_unit_left[of "[:c:]", simplified] by force

text ‹A polynomial with integer coefficients is
   irreducible over the rationals, if it is irreducible over the integers.›
theorem irreducibled_int_rat: fixes p :: "int poly" 
  assumes p: "irreducibled p"
  shows "irreducibled (map_poly rat_of_int p)"
proof (rule irreducibledI)
  from irreducibledD[OF p]
  have p: "degree p  0" and irr: " q r. degree q < degree p  degree r < degree p  p  q * r" by auto
  let ?r = "rat_of_int"
  let ?rp = "map_poly ?r"
  from p show rp: "degree (?rp p) > 0" by auto
  from p have p0: "p  0" by auto
  fix g h :: "rat poly"
  assume deg: "degree g > 0" "degree g < degree (?rp p)" "degree h > 0" "degree h < degree (?rp p)" and pgh: "?rp p = g * h"
  from rat_to_int_factor[OF pgh] obtain g' h' where p: "p = g' * h'" and dg: "degree g' = degree g" "degree h' = degree h"
    by auto
  from irr[of g' h'] deg[unfolded dg]
  show False using degree_mult_eq[of g' h'] by (auto simp: p dg)
qed

corollary irreducibled_rat_to_normalized_int_poly: 
  assumes rp: "rat_to_normalized_int_poly rp = (a, ip)"
  and ip: "irreducibled ip"
  shows "irreducibled rp"
proof -
  from rat_to_normalized_int_poly[OF rp] 
  have rp: "rp = smult a (map_poly rat_of_int ip)" and a: "a  0" by auto
  with irreducibled_int_rat[OF ip] show ?thesis by auto
qed

lemma dvd_content_dvd: assumes dvd: "content f dvd content g" "primitive_part f dvd primitive_part g"
  shows "f dvd g" 
proof -
  let ?cf = "content f" let ?nf = "primitive_part f" 
  let ?cg = "content g" let ?ng = "primitive_part g" 
  have "f dvd g = (smult ?cf ?nf dvd smult ?cg ?ng)" 
    unfolding content_times_primitive_part by auto
  from dvd(1) obtain ch where cg: "?cg = ?cf * ch" unfolding dvd_def by auto
  from dvd(2) obtain nh where ng: "?ng = ?nf * nh" unfolding dvd_def by auto
  have "f dvd g = (smult ?cf ?nf dvd smult ?cg ?ng)" 
    unfolding content_times_primitive_part[of f] content_times_primitive_part[of g] by auto
  also have " = (smult ?cf ?nf dvd smult ?cf ?nf * smult ch nh)" unfolding cg ng
    by (metis mult.commute mult_smult_right smult_smult)
  also have "" by (rule dvd_triv_left)
  finally show ?thesis .
qed

lemma sdiv_poly_smult: "c  0  sdiv_poly (smult c f) c = f"
  by (intro poly_eqI, unfold coeff_sdiv_poly coeff_smult, auto)

lemma primitive_part_smult_int: fixes f :: "int poly" shows
  "primitive_part (smult d f) = smult (sgn d) (primitive_part f)" 
proof (cases "d = 0  f = 0")
  case False
  obtain cf where cf: "content f = cf" by auto
  with False have 0: "d  0" "f  0" "cf  0" by auto
  show ?thesis 
  proof (rule poly_eqI, unfold primitive_part_alt_def coeff_sdiv_poly content_smult_int coeff_smult cf)
    fix n
    consider (pos) "d > 0" | (neg) "d < 0" using 0(1) by linarith
    thus "d * coeff f n div (¦d¦ * cf) = sgn d * (coeff f n div cf)"
    proof cases
      case neg
      hence "?thesis = (d * coeff f n div - (d * cf) = - (coeff f n div cf))" by auto
      also have "d * coeff f n div - (d * cf) = - (d * coeff f n div (d * cf))" 
        by (subst dvd_div_neg, insert 0(1), auto simp: cf[symmetric])
      also have "d * coeff f n div (d * cf) = coeff f n div cf" using 0(1) by auto
      finally show ?thesis by simp
    qed auto
  qed
qed auto

lemma gcd_smult_left: assumes "c  0"
  shows "gcd (smult c f) g = gcd f (g :: 'b :: {field_gcd} poly)"
proof -
  from assms have "normalize c = 1"
    by (meson dvd_field_iff is_unit_normalize)
  then show ?thesis
    by (metis (no_types) Polynomial.normalize_smult gcd.commute gcd.left_commute gcd_left_idem gcd_self smult_1_left)
qed

lemma gcd_smult_right: "c  0  gcd f (smult c g) = gcd f (g :: 'b :: {field_gcd} poly)"
  using gcd_smult_left[of c g f] by (simp add: gcd.commute)

lemma gcd_rat_to_gcd_int: "gcd (of_int_poly f :: rat poly) (of_int_poly g) = 
  smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))" 
proof (cases "f = 0  g = 0")
  case True
  thus ?thesis by simp
next
  case False
  let ?r = rat_of_int
  let ?rp = "map_poly ?r" 
  from False have gcd0: "gcd f g  0" by auto
  hence lc0: "lead_coeff (gcd f g)  0" by auto
  hence inv: "inverse (?r (lead_coeff (gcd f g)))  0" by auto
  show ?thesis
  proof (rule sym, rule gcdI, goal_cases)
    case 1
    have "gcd f g dvd f" by auto
    then obtain h where f: "f = gcd f g * h" unfolding dvd_def by auto    
    show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF f, of ?rp], simp add: hom_distribs) 
  next
    case 2
    have "gcd f g dvd g" by auto
    then obtain h where g: "g = gcd f g * h" unfolding dvd_def by auto    
    show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF g, of ?rp], simp add: hom_distribs) 
  next
    case (3 h)    
    show ?case 
    proof (rule dvd_smult)
      obtain ch ph where h: "rat_to_normalized_int_poly h = (ch, ph)" by force
      from 3 obtain ff where f: "?rp f = h * ff" unfolding dvd_def by auto
      from 3 obtain gg where g: "?rp g = h * gg" unfolding dvd_def by auto
      from rat_to_int_factor_explicit[OF f h] obtain f' where f: "f = ph * f'" by blast
      from rat_to_int_factor_explicit[OF g h] obtain g' where g: "g = ph * g'" by blast
      from f g have "ph dvd gcd f g" by auto
      then obtain gg where gcd: "gcd f g = ph * gg" unfolding dvd_def by auto
      note * = rat_to_normalized_int_poly[OF h]
      show "h dvd ?rp (gcd f g)" unfolding gcd *(1)
        by (rule smult_dvd, insert *(2), auto)
    qed
  next
    case 4
    have [simp]: "[:1:] = 1" by simp
    show ?case unfolding normalize_poly_def 
      by (rule poly_eqI, simp)
  qed
qed

end