# Theory Unique_Factorization

```theory Unique_Factorization
imports
Polynomial_Interpolation.Ring_Hom_Poly
Polynomial_Factorization.Polynomial_Divisibility
"HOL-Combinatorics.Permutations"
"HOL-Computational_Algebra.Euclidean_Algorithm"
Containers.Containers_Auxiliary (* only for a lemma *)
More_Missing_Multiset
"HOL-Algebra.Divisibility"
begin

hide_const(open)
Divisibility.prime
Divisibility.irreducible

hide_fact(open)
Divisibility.irreducible_def
Divisibility.irreducibleI
Divisibility.irreducibleD
Divisibility.irreducibleE

hide_const (open) Rings.coprime

lemma irreducible_uminus [simp]:
fixes a::"'a::idom"
shows "irreducible (-a) ⟷ irreducible a"
using irreducible_mult_unit_left[of "-1::'a"] by auto

context comm_monoid_mult begin

definition coprime :: "'a ⇒ 'a ⇒ bool"
where coprime_def': "coprime p q ≡ ∀r. r dvd p ⟶ r dvd q ⟶ r dvd 1"

lemma coprimeI:
assumes "⋀r. r dvd p ⟹ r dvd q ⟹ r dvd 1"
shows "coprime p q" using assms by (auto simp: coprime_def')

lemma coprimeE:
assumes "coprime p q"
and "(⋀r. r dvd p ⟹ r dvd q ⟹ r dvd 1) ⟹ thesis"
shows thesis using assms by (auto simp: coprime_def')

lemma coprime_commute [ac_simps]:
"coprime p q ⟷ coprime q p"

lemma not_coprime_iff_common_factor:
"¬ coprime p q ⟷ (∃r. r dvd p ∧ r dvd q ∧ ¬ r dvd 1)"

end

lemma (in algebraic_semidom) coprime_iff_coprime [simp, code]:
"coprime = Rings.coprime"
by (simp add: fun_eq_iff coprime_def coprime_def')

lemma (in comm_semiring_1) coprime_0 [simp]:
"coprime p 0 ⟷ p dvd 1" "coprime 0 p ⟷ p dvd 1"
by (auto intro: coprimeI elim: coprimeE dest: dvd_trans)

(**** until here ****)

(* TODO: move or...? *)
lemma dvd_rewrites: "dvd.dvd ((*)) = (dvd)" by (unfold dvd.dvd_def dvd_def, rule)

subsection ‹Interfacing UFD properties›
hide_const (open) Divisibility.irreducible

context comm_monoid_mult_isom begin
lemma coprime_hom[simp]: "coprime (hom x) y' ⟷ coprime x (Hilbert_Choice.inv hom y')"
proof-
show ?thesis by (unfold coprime_def', fold ball_UNIV, subst surj[symmetric], simp)
qed
lemma coprime_inv_hom[simp]: "coprime (Hilbert_Choice.inv hom x') y ⟷ coprime x' (hom y)"
proof-
interpret inv: comm_monoid_mult_isom "Hilbert_Choice.inv hom"..
show ?thesis by simp
qed
end

subsubsection ‹Original part›

lemma dvd_dvd_imp_smult:
fixes p q :: "'a :: idom poly"
assumes pq: "p dvd q" and qp: "q dvd p" shows "∃c. p = smult c q"
proof (cases "p = 0")
case True then show ?thesis by auto
next
case False
from qp obtain r where r: "p = q * r" by (elim dvdE, auto)
with False qp have r0: "r ≠ 0" and q0: "q ≠ 0" by auto
with divides_degree[OF pq] divides_degree[OF qp] False
have "degree p = degree q" by auto
with r degree_mult_eq[OF q0 r0] have "degree r = 0" by auto
from degree_0_id[OF this] obtain c where "r = [:c:]" by metis
from r[unfolded this] show ?thesis by auto
qed

lemma dvd_const:
assumes pq: "(p::'a::semidom poly) dvd q" and q0: "q ≠ 0" and degq: "degree q = 0"
shows "degree p = 0"
proof-
from dvdE[OF pq] obtain r where *: "q = p * r".
with q0 have "p ≠ 0" "r ≠ 0" by auto
from degree_mult_eq[OF this] degq * show "degree p = 0" by auto
qed

context Rings.dvd begin
abbreviation ddvd (infix "ddvd" 40) where "x ddvd y ≡ x dvd y ∧ y dvd x"
lemma ddvd_sym[sym]: "x ddvd y ⟹ y ddvd x" by auto
end

context comm_monoid_mult begin
lemma ddvd_trans[trans]: "x ddvd y ⟹ y ddvd z ⟹ x ddvd z" using dvd_trans by auto
lemma ddvd_transp: "transp (ddvd)" by (intro transpI, fact ddvd_trans)
end

context comm_semiring_1 begin

definition mset_factors where "mset_factors F p ≡
F ≠ {#} ∧ (∀f. f ∈# F ⟶ irreducible f) ∧ p = prod_mset F"

lemma mset_factorsI[intro!]:
assumes "⋀f. f ∈# F ⟹ irreducible f" and "F ≠ {#}" and "prod_mset F = p"
shows "mset_factors F p"
unfolding mset_factors_def using assms by auto

lemma mset_factorsD:
assumes "mset_factors F p"
shows "f ∈# F ⟹ irreducible f" and "F ≠ {#}" and "prod_mset F = p"
using assms[unfolded mset_factors_def] by auto

lemma mset_factorsE[elim]:
assumes "mset_factors F p"
and "(⋀f. f ∈# F ⟹ irreducible f) ⟹ F ≠ {#} ⟹ prod_mset F = p ⟹ thesis"
shows thesis
using assms[unfolded mset_factors_def] by auto

lemma mset_factors_imp_not_is_unit:
assumes "mset_factors F p"
shows "¬ p dvd 1"
proof(cases F)
case empty with assms show ?thesis by auto
next
with assms have "¬ f dvd 1" "p = f * prod_mset F" by (auto intro!: irreducible_not_unit)
then show ?thesis by auto
qed

definition primitive_poly where "primitive_poly f ≡ ∀d. (∀i. d dvd coeff f i) ⟶ d dvd 1"

end

lemma(in semidom) mset_factors_imp_nonzero:
assumes "mset_factors F p"
shows "p ≠ 0"
proof
assume "p = 0"
moreover from assms have "prod_mset F = p" by auto
ultimately obtain f where "f ∈# F" "f = 0" by auto
with assms show False by auto
qed

class ufd = idom +
assumes mset_factors_exist: "⋀x. x ≠ 0 ⟹ ¬ x dvd 1 ⟹ ∃F. mset_factors F x"
and mset_factors_unique: "⋀x F G. mset_factors F x ⟹ mset_factors G x ⟹ rel_mset (ddvd) F G"

subsubsection ‹Connecting to HOL/Divisibility›

context comm_semiring_1 begin

abbreviation "mk_monoid ≡ ⦇carrier = UNIV - {0}, mult = (*), one = 1⦈"

lemma carrier_0[simp]: "x ∈ carrier mk_monoid ⟷ x ≠ 0" by auto

lemmas mk_monoid_simps = carrier_0 monoid.simps

abbreviation irred where "irred ≡ Divisibility.irreducible mk_monoid"
abbreviation factor where "factor ≡ Divisibility.factor mk_monoid"
abbreviation factors where "factors ≡ Divisibility.factors mk_monoid"
abbreviation properfactor where "properfactor ≡ Divisibility.properfactor mk_monoid"

lemma factors: "factors fs y ⟷ prod_list fs = y ∧ Ball (set fs) irred"
proof -
have "prod_list fs = foldr (*) fs 1" by (induct fs, auto)
thus ?thesis unfolding factors_def by auto
qed

lemma factor: "factor x y ⟷ (∃z. z ≠ 0 ∧ x * z = y)" unfolding factor_def by auto

lemma properfactor_nz:
shows "(y :: 'a) ≠ 0 ⟹ properfactor x y ⟷ x dvd y ∧ ¬ y dvd x"
by (auto simp: properfactor_def factor_def dvd_def)

lemma mem_Units[simp]: "y ∈ Units mk_monoid ⟷ y dvd 1"
unfolding dvd_def Units_def by (auto simp: ac_simps)

end

context idom begin
lemma irred_0[simp]: "irred (0::'a)" by (unfold Divisibility.irreducible_def, auto simp: factor properfactor_def)
lemma factor_idom[simp]: "factor (x::'a) y ⟷ (if y = 0 then x = 0 else x dvd y)"
by (cases "y = 0"; auto intro: exI[of _ 1] elim: dvdE simp: factor)

lemma associated_connect[simp]: "(∼⇘mk_monoid⇙) = (ddvd)" by (intro ext, unfold associated_def, auto)

lemma essentially_equal_connect[simp]:
"essentially_equal mk_monoid fs gs ⟷ rel_mset (ddvd) (mset fs) (mset gs)"
by (auto simp: essentially_equal_def rel_mset_via_perm)

lemma irred_idom_nz:
assumes x0: "(x::'a) ≠ 0"
shows "irred x ⟷ irreducible x"
using x0 by (auto simp: irreducible_altdef Divisibility.irreducible_def properfactor_nz)

lemma dvd_dvd_imp_unit_mult:
assumes xy: "x dvd y" and yx: "y dvd x"
shows "∃z. z dvd 1 ∧ y = x * z"
proof(cases "x = 0")
case True with xy show ?thesis by (auto intro: exI[of _ 1])
next
case x0: False
from xy obtain z where z: "y = x * z" by (elim dvdE, auto)
from yx obtain w where w: "x = y * w" by (elim dvdE, auto)
from z w have "x * (z * w) = x" by (auto simp: ac_simps)
then have "z * w = 1" using x0 by auto
with z show ?thesis by (auto intro: exI[of _ z])
qed

lemma irred_inner_nz:
assumes x0: "x ≠ 0"
shows "(∀b. b dvd x ⟶ ¬ x dvd b ⟶ b dvd 1) ⟷ (∀a b. x = a * b ⟶ a dvd 1 ∨ b dvd 1)" (is "?l ⟷ ?r")
proof (intro iffI allI impI)
assume l: ?l
fix a b
assume xab: "x = a * b"
then have ax: "a dvd x" and bx: "b dvd x" by auto
{ assume a1: "¬ a dvd 1"
with l ax have xa: "x dvd a" by auto
from dvd_dvd_imp_unit_mult[OF ax xa] obtain z where z1: "z dvd 1" and xaz: "x = a * z" by auto
from xab x0 have "a ≠ 0" by auto
with xab xaz have "b = z" by auto
with z1 have "b dvd 1" by auto
}
then show "a dvd 1 ∨ b dvd 1" by auto
next
assume r: ?r
fix b assume bx: "b dvd x" and xb: "¬ x dvd b"
then obtain a where xab: "x = a * b" by (elim dvdE, auto simp: ac_simps)
with r consider "a dvd 1" | "b dvd 1" by auto
then show "b dvd 1"
proof(cases)
case 2 then show ?thesis by auto
next
case 1
then obtain c where ac1: "a * c = 1" by (elim dvdE, auto)
from xab have "x * c = b * (a * c)" by (auto simp: ac_simps)
with ac1 have "x * c = b" by auto
then have "x dvd b" by auto
with xb show ?thesis by auto
qed
qed

lemma irred_idom[simp]: "irred x ⟷ x = 0 ∨ irreducible x"
by (cases "x = 0"; simp add: irred_idom_nz irred_inner_nz irreducible_def)

lemma assumes "x ≠ 0" and "factors fs x" and "f ∈ set fs" shows "f ≠ 0"
using assms by (auto simp: factors)

lemma factors_as_mset_factors:
assumes x0: "x ≠ 0" and x1: "x ≠ 1"
shows "factors fs x ⟷ mset_factors (mset fs) x" using assms
by (auto simp: factors prod_mset_prod_list)

end

context ufd begin
interpretation comm_monoid_cancel: comm_monoid_cancel "mk_monoid::'a monoid"
apply (unfold_locales)
apply simp_all
using mult_left_cancel
apply (auto simp: ac_simps)
done
lemma factors_exist:
assumes "a ≠ 0"
and "¬ a dvd 1"
shows "∃fs. set fs ⊆ UNIV - {0} ∧ factors fs a"
proof-
from mset_factors_exist[OF assms]
obtain F where "mset_factors F a" by auto
also from ex_mset obtain fs where "F = mset fs" by metis
finally have fs: "mset_factors (mset fs) a".
then have "factors fs a" using assms by (subst factors_as_mset_factors, auto)
moreover have "set fs ⊆ UNIV - {0}" using fs by (auto elim!: mset_factorsE)
ultimately show ?thesis by auto
qed

lemma factors_unique:
assumes fs: "factors fs a"
and gs: "factors gs a"
and a0: "a ≠ 0"
and a1: "¬ a dvd 1"
shows "rel_mset (ddvd) (mset fs) (mset gs)"
proof-
from a1 have "a ≠ 1" by auto
with a0 fs gs have "mset_factors (mset fs) a" "mset_factors (mset gs) a" by (unfold factors_as_mset_factors)
from mset_factors_unique[OF this] show ?thesis.
qed

lemma factorial_monoid: "factorial_monoid (mk_monoid :: 'a monoid)"
by (unfold_locales; auto simp add: factors_exist factors_unique)

end

lemma (in idom) factorial_monoid_imp_ufd:
assumes "factorial_monoid (mk_monoid :: 'a monoid)"
shows "class.ufd ((*) :: 'a ⇒ _) 1 (+) 0 (-) uminus"
proof (unfold_locales)
interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact assms)
{
fix x assume x: "x ≠ 0" "¬ x dvd 1"
note * = factors_exist[simplified, OF this]
with x show "∃F. mset_factors F x" by (subst(asm) factors_as_mset_factors, auto)
}
fix x F G assume FG: "mset_factors F x" "mset_factors G x"
with mset_factors_imp_not_is_unit have x1: "¬ x dvd 1" by auto
from FG(1) have x0: "x ≠ 0" by (rule mset_factors_imp_nonzero)
obtain fs gs where fsgs: "F = mset fs" "G = mset gs" using ex_mset by metis
note FG = FG[unfolded this]
then have 0: "0 ∉ set fs" "0 ∉ set gs" by (auto elim!: mset_factorsE)
from x1 have "x ≠ 1" by auto
note FG[folded factors_as_mset_factors[OF x0 this]]
from factors_unique[OF this, simplified, OF x0 x1, folded fsgs] 0
show "rel_mset (ddvd) F G" by auto
qed

subsection ‹Preservation of Irreducibility›

locale comm_semiring_1_hom = comm_monoid_mult_hom hom + zero_hom hom
for hom :: "'a :: comm_semiring_1 ⇒ 'b :: comm_semiring_1"

locale irreducibility_hom = comm_semiring_1_hom +
assumes irreducible_imp_irreducible_hom: "irreducible a ⟹ irreducible (hom a)"
begin
lemma hom_mset_factors:
assumes F: "mset_factors F p"
shows "mset_factors (image_mset hom F) (hom p)"
proof (unfold mset_factors_def, intro conjI allI impI)
from F show "hom p = prod_mset (image_mset hom F)" "image_mset hom F ≠ {#}" by (auto simp: hom_distribs)
fix f' assume "f' ∈# image_mset hom F"
then obtain f where f: "f ∈# F" and f'f: "f' = hom f" by auto
with F irreducible_imp_irreducible_hom show "irreducible f'" unfolding f'f by auto
qed
end

locale unit_preserving_hom = comm_semiring_1_hom +
assumes is_unit_hom_if: "⋀x. hom x dvd 1 ⟹ x dvd 1"
begin
lemma is_unit_hom_iff[simp]: "hom x dvd 1 ⟷ x dvd 1" using is_unit_hom_if hom_dvd by force

lemma irreducible_hom_imp_irreducible:
assumes irr: "irreducible (hom a)" shows "irreducible a"
proof (intro irreducibleI)
from irr show "a ≠ 0" by auto
from irr show "¬ a dvd 1" by (auto dest: irreducible_not_unit)
fix b c assume "a = b * c"
then have "hom a = hom b * hom c" by (simp add: hom_distribs)
with irr have "hom b dvd 1 ∨ hom c dvd 1" by (auto dest: irreducibleD)
then show "b dvd 1 ∨ c dvd 1" by simp
qed
end

locale factor_preserving_hom = unit_preserving_hom + irreducibility_hom
begin
lemma irreducible_hom[simp]: "irreducible (hom a) ⟷ irreducible a"
using irreducible_hom_imp_irreducible irreducible_imp_irreducible_hom by metis
end

lemma factor_preserving_hom_comp:
assumes f: "factor_preserving_hom f" and g: "factor_preserving_hom g"
shows "factor_preserving_hom (f o g)"
proof-
interpret f: factor_preserving_hom f by (rule f)
interpret g: factor_preserving_hom g by (rule g)
show ?thesis by (unfold_locales, auto simp: hom_distribs)
qed

context comm_semiring_isom begin
sublocale unit_preserving_hom by (unfold_locales, auto)
sublocale factor_preserving_hom
proof (standard)
fix a :: 'a
assume "irreducible a"
note a = this[unfolded irreducible_def]
show "irreducible (hom a)"
proof (rule ccontr)
assume "¬ irreducible (hom a)"
from this[unfolded Factorial_Ring.irreducible_def,simplified] a
obtain hb hc where eq: "hom a = hb * hc" and nu: "¬ hb dvd 1" "¬ hc dvd 1" by auto
from bij obtain b where hb: "hb = hom b" by (elim bij_pointE)
from bij obtain c where hc: "hc = hom c" by (elim bij_pointE)
from eq[unfolded hb hc, folded hom_mult] have "a = b * c" by auto
with nu hb hc have "a = b * c" "¬ b dvd 1" "¬ c dvd 1" by auto
with a show False by auto
qed
qed
end

subsubsection‹Back to divisibility›

lemma(in comm_semiring_1) mset_factors_mult:
assumes F: "mset_factors F a"
and G: "mset_factors G b"
shows "mset_factors (F+G) (a*b)"
proof(intro mset_factorsI)
fix f assume "f ∈# F + G"
then consider "f ∈# F" | "f ∈# G" by auto
then show "irreducible f" by(cases, insert F G, auto)
qed (insert F G, auto)

lemma(in ufd) dvd_imp_subset_factors:
assumes ab: "a dvd b"
and F: "mset_factors F a"
and G: "mset_factors G b"
shows "∃G'. G' ⊆# G ∧ rel_mset (ddvd) F G'"
proof-
from F G have a0: "a ≠ 0" and b0: "b ≠ 0" by (simp_all add: mset_factors_imp_nonzero)
from ab obtain c where c: "b = a * c" by (elim dvdE, auto)
with b0 have c0: "c ≠ 0" by auto
show ?thesis
proof(cases "c dvd 1")
case True
show ?thesis
proof(cases F)
case empty with F show ?thesis by auto
next
with F
have a: "f * prod_mset F' = a"
and F': "⋀f. f ∈# F' ⟹ irreducible f"
and irrf: "irreducible f" by auto
from irrf have f0: "f ≠ 0" and f1: "¬f dvd 1" by (auto dest: irreducible_not_unit)
from a c have "(f * c) * prod_mset F' = b" by (auto simp: ac_simps)
moreover {
have "irreducible (f * c)" using True irrf by (subst irreducible_mult_unit_right)
with F' irrf have "⋀f'. f' ∈# F' + {#f * c#} ⟹ irreducible f'" by auto
}
ultimately have "mset_factors (F' + {#f * c#}) b" by (intro mset_factorsI, auto)
from mset_factors_unique[OF this G]
have F'G: "rel_mset (ddvd) (F' + {#f * c#}) G".
from True add have FF': "rel_mset (ddvd) F (F' + {#f * c#})"
by (auto simp add: multiset.rel_refl intro!: rel_mset_Plus)
have "rel_mset (ddvd) F G"
apply(rule transpD[OF multiset.rel_transp[OF transpI] FF' F'G])
using ddvd_trans.
then show ?thesis by auto
qed
next
case False
from mset_factors_exist[OF c0 this] obtain H where H: "mset_factors H c" by auto
from c mset_factors_mult[OF F H] have "mset_factors (F + H) b" by auto
note mset_factors_unique[OF this G]
from rel_mset_split[OF this] obtain G1 G2
where "G = G1 + G2" "rel_mset (ddvd) F G1" "rel_mset (ddvd) H G2" by auto
then show ?thesis by (intro exI[of _ "G1"], auto)
qed
qed

lemma(in idom) irreducible_factor_singleton:
assumes a: "irreducible a"
shows "mset_factors F a ⟷ F = {#a#}"
proof(cases F)
case empty with mset_factorsD show ?thesis by auto
next
show ?thesis
proof
assume F: "mset_factors F a"
from add mset_factorsD[OF F] have *: "a = f * prod_mset F'" by auto
then have fa: "f dvd a" by auto
from * a have f0: "f ≠ 0" by auto
from add have "f ∈# F" by auto
with F have f: "irreducible f" by auto
from add have "F' ⊆# F" by auto
then have unitemp: "prod_mset F' dvd 1 ⟹ F' = {#}"
proof(induct F')
case empty then show ?case by auto
next
with F irreducible_not_unit have "¬ f dvd 1" by auto
then have "¬ (prod_mset F' * f) dvd 1" by simp
with add show ?case by auto
qed
show "F = {#a#}"
proof(cases "a dvd f")
case True
then obtain r where "f = a * r" by (elim dvdE, auto)
with * have "f = (r * prod_mset F') * f" by (auto simp: ac_simps)
with f0 have "r * prod_mset F' = 1" by auto
then have "prod_mset F' dvd 1" by (metis dvd_triv_right)
with unitemp * add show ?thesis by auto
next
case False with fa a f show ?thesis by (auto simp: irreducible_altdef)
qed
qed (insert a, auto)
qed

lemma(in ufd) irreducible_dvd_imp_factor:
assumes ab: "a dvd b"
and a: "irreducible a"
and G: "mset_factors G b"
shows "∃g ∈# G. a ddvd g"
proof-
from a have "mset_factors {#a#} a" by auto
from dvd_imp_subset_factors[OF ab this G]
obtain G' where G'G: "G' ⊆# G" and rel: "rel_mset (ddvd) {#a#} G'" by auto
with rel_mset_size size_1_singleton_mset size_single
obtain g where gG': "G' = {#g#}" by fastforce
from rel[unfolded this rel_mset_def]
have "a ddvd g" by auto
with gG' G'G show ?thesis by auto
qed

lemma(in idom) prod_mset_remove_units:
"prod_mset F ddvd prod_mset {# f ∈# F. ¬f dvd 1 #}"
proof(induct F)
case (add f F) then show ?case by (cases "f = 0", auto)
qed auto

lemma(in comm_semiring_1) mset_factors_imp_dvd:
assumes "mset_factors F x" and "f ∈# F" shows "f dvd x"
using assms by (simp add: dvd_prod_mset mset_factors_def)

lemma(in ufd) prime_elem_iff_irreducible[iff]:
"prime_elem x ⟷ irreducible x"
proof (intro iffI, fact prime_elem_imp_irreducible, rule prime_elemI)
assume r: "irreducible x"
then show x0: "x ≠ 0" and x1: "¬ x dvd 1" by (auto dest: irreducible_not_unit)
from irreducible_factor_singleton[OF r]
have *: "mset_factors {#x#} x" by auto
fix a b
assume "x dvd a * b"
then obtain c where abxc: "a * b = x * c" by (elim dvdE, auto)
show "x dvd a ∨ x dvd b"
proof(cases "c = 0 ∨ a = 0 ∨ b = 0")
case True with abxc show ?thesis by auto
next
case False
then have a0: "a ≠ 0" and b0: "b ≠ 0" and c0: "c ≠ 0" by auto
from x0 c0 have xc0: "x * c ≠ 0" by auto
from x1 have xc1: "¬ x * c dvd 1" by auto
show ?thesis
proof (cases "a dvd 1 ∨ b dvd 1")
case False
then have a1: "¬ a dvd 1" and b1: "¬ b dvd 1" by auto
from mset_factors_exist[OF a0 a1]
obtain F where Fa: "mset_factors F a" by auto
then have F0: "F ≠ {#}" by auto
from mset_factors_exist[OF b0 b1]
obtain G where Gb: "mset_factors G b" by auto
then have G0: "G ≠ {#}" by auto
from mset_factors_mult[OF Fa Gb]
have FGxc: "mset_factors (F + G) (x * c)" by (simp add: abxc)
show ?thesis
proof (cases "c dvd 1")
case True
from r irreducible_mult_unit_right[OF this] have "irreducible (x*c)" by simp
note irreducible_factor_singleton[OF this] FGxc
with F0 G0 have False by (cases F; cases G; auto)
then show ?thesis by auto
next
case False
from mset_factors_exist[OF c0 this] obtain H where "mset_factors H c" by auto
with * have xHxc: "mset_factors (add_mset x H) (x * c)" by force
note rel = mset_factors_unique[OF this FGxc]
obtain hs where "mset hs = H" using ex_mset by auto
then have "mset (x#hs) = add_mset x H" by auto
from rel_mset_free[OF rel this]
obtain jjs where jjsGH: "mset jjs = F + G" and rel: "list_all2 (ddvd) (x # hs) jjs" by auto
then obtain j js where jjs: "jjs = j # js" by (cases jjs, auto)
with rel have xj: "x ddvd j" by auto
from jjs jjsGH have j: "j ∈ set_mset (F + G)" by (intro union_single_eq_member, auto)
from j consider "j ∈# F" | "j ∈# G" by auto
then show ?thesis
proof(cases)
case 1
with Fa have "j dvd a" by (auto intro: mset_factors_imp_dvd)
with xj dvd_trans have "x dvd a" by auto
then show ?thesis by auto
next
case 2
with Gb have "j dvd b" by (auto intro: mset_factors_imp_dvd)
with xj dvd_trans have "x dvd b" by auto
then show ?thesis by auto
qed
qed
next
case True
then consider "a dvd 1" | "b dvd 1" by auto
then show ?thesis
proof(cases)
case 1
then obtain d where ad: "a * d = 1" by (elim dvdE, auto)
from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps)
also have "... = a * d * b" by (auto simp: ac_simps)
finally have "x dvd b" by (intro dvdI, auto simp: ad)
then show ?thesis by auto
next
case 2
then obtain d where bd: "b * d = 1" by (elim dvdE, auto)
from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps)
also have "... = (b * d) * a" by (auto simp: ac_simps)
finally have "x dvd a" by (intro dvdI, auto simp:bd)
then show ?thesis by auto
qed
qed
qed
qed

subsection‹Results for GCDs etc.›

lemma prod_list_remove1: "(x :: 'b :: comm_monoid_mult) ∈ set xs ⟹ prod_list (remove1 x xs) * x = prod_list xs"
by (induct xs, auto simp: ac_simps)

(* Isabelle 2015-style and generalized gcd-class without normalization and factors *)
class comm_monoid_gcd = gcd + comm_semiring_1 +
assumes gcd_dvd1[iff]: "gcd a b dvd a"
and gcd_dvd2[iff]: "gcd a b dvd b"
and gcd_greatest: "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b"
begin

lemma gcd_0_0[simp]: "gcd 0 0 = 0"
using gcd_greatest[OF dvd_0_right dvd_0_right, of 0] by auto

lemma gcd_zero_iff[simp]: "gcd a b = 0 ⟷ a = 0 ∧ b = 0"
proof
assume "gcd a b = 0"
from gcd_dvd1[of a b, unfolded this] gcd_dvd2[of a b, unfolded this]
show "a = 0 ∧ b = 0" by auto
qed auto

lemma gcd_zero_iff'[simp]: "0 = gcd a b ⟷ a = 0 ∧ b = 0"
using gcd_zero_iff by metis

lemma dvd_gcd_0_iff[simp]:
shows "x dvd gcd 0 a ⟷ x dvd a" (is ?g1)
and "x dvd gcd a 0 ⟷ x dvd a" (is ?g2)
proof-
have "a dvd gcd a 0" "a dvd gcd 0 a" by (auto intro: gcd_greatest)
with dvd_refl show ?g1 ?g2 by (auto dest: dvd_trans)
qed

lemma gcd_dvd_1[simp]: "gcd a b dvd 1 ⟷ coprime a b"
using dvd_trans[OF gcd_greatest[of _ a b], of _ 1]
by (cases "a = 0 ∧ b = 0") (auto intro!: coprimeI elim: coprimeE)

lemma dvd_imp_gcd_dvd_gcd: "b dvd c ⟹ gcd a b dvd gcd a c"
by (meson gcd_dvd1 gcd_dvd2 gcd_greatest dvd_trans)

definition listgcd :: "'a list ⇒ 'a" where
"listgcd xs = foldr gcd xs 0"

lemma listgcd_simps[simp]: "listgcd [] = 0" "listgcd (x # xs) = gcd x (listgcd xs)"
by (auto simp: listgcd_def)

lemma listgcd: "x ∈ set xs ⟹ listgcd xs dvd x"
proof (induct xs)
case (Cons y ys)
show ?case
proof (cases "x = y")
case False
with Cons have dvd: "listgcd ys dvd x" by auto
thus ?thesis unfolding listgcd_simps using dvd_trans by blast
next
case True
thus ?thesis unfolding listgcd_simps using dvd_trans by blast
qed
qed simp

lemma listgcd_greatest: "(⋀ x. x ∈ set xs ⟹ y dvd x) ⟹ y dvd listgcd xs"
by (induct xs arbitrary:y, auto intro: gcd_greatest)

end

context Rings.dvd begin

definition "is_gcd x a b ≡ x dvd a ∧ x dvd b ∧ (∀y. y dvd a ⟶ y dvd b ⟶ y dvd x)"

definition "some_gcd a b ≡ SOME x. is_gcd x a b"

lemma is_gcdI[intro!]:
assumes "x dvd a" "x dvd b" "⋀y. y dvd a ⟹ y dvd b ⟹ y dvd x"
shows "is_gcd x a b" by (insert assms, auto simp: is_gcd_def)

lemma is_gcdE[elim!]:
assumes "is_gcd x a b"
and "x dvd a ⟹ x dvd b ⟹ (⋀y. y dvd a ⟹ y dvd b ⟹ y dvd x) ⟹ thesis"
shows thesis by (insert assms, auto simp: is_gcd_def)

lemma is_gcd_some_gcdI:
assumes "∃x. is_gcd x a b" shows "is_gcd (some_gcd a b) a b"
by (unfold some_gcd_def, rule someI_ex[OF assms])

end

context comm_semiring_1 begin

lemma some_gcd_0[intro!]: "is_gcd (some_gcd a 0) a 0" "is_gcd (some_gcd 0 b) 0 b"
by (auto intro!: is_gcd_some_gcdI intro: exI[of _ a] exI[of _ b])

lemma some_gcd_0_dvd[intro!]:
"some_gcd a 0 dvd a" "some_gcd 0 b dvd b" using some_gcd_0 by auto

lemma dvd_some_gcd_0[intro!]:
"a dvd some_gcd a 0" "b dvd some_gcd 0 b" using some_gcd_0[of a] some_gcd_0[of b] by auto

end

context idom begin

lemma is_gcd_connect:
assumes "a ≠ 0" "b ≠ 0" shows "isgcd mk_monoid x a b ⟷ is_gcd x a b"
using assms by (force simp: isgcd_def)

lemma some_gcd_connect:
assumes "a ≠ 0" and "b ≠ 0" shows "somegcd mk_monoid a b = some_gcd a b"
using assms by (auto intro!: arg_cong[of _ _ Eps] simp: is_gcd_connect some_gcd_def somegcd_def)
end

context comm_monoid_gcd
begin
lemma is_gcd_gcd: "is_gcd (gcd a b) a b" using gcd_greatest by auto
lemma is_gcd_some_gcd: "is_gcd (some_gcd a b) a b" by (insert is_gcd_gcd, auto intro!: is_gcd_some_gcdI)
lemma gcd_dvd_some_gcd: "gcd a b dvd some_gcd a b" using is_gcd_some_gcd by auto
lemma some_gcd_dvd_gcd: "some_gcd a b dvd gcd a b" using is_gcd_some_gcd by (auto intro: gcd_greatest)
lemma some_gcd_ddvd_gcd: "some_gcd a b ddvd gcd a b" by (auto intro: gcd_dvd_some_gcd some_gcd_dvd_gcd)
lemma some_gcd_dvd: "some_gcd a b dvd d ⟷ gcd a b dvd d" "d dvd some_gcd a b ⟷ d dvd gcd a b"
using some_gcd_ddvd_gcd[of a b] by (auto dest:dvd_trans)

end

class idom_gcd = comm_monoid_gcd + idom
begin

interpretation raw: comm_monoid_cancel "mk_monoid :: 'a monoid"
by (unfold_locales, auto intro: mult_commute mult_assoc)

interpretation raw: gcd_condition_monoid "mk_monoid :: 'a monoid"
by (unfold_locales, auto simp: is_gcd_connect intro!: exI[of _ "gcd _ _"] dest: gcd_greatest)

lemma gcd_mult_ddvd:
"d * gcd a b ddvd gcd (d * a) (d * b)"
proof (cases "d = 0")
case True then show ?thesis by auto
next
case d0: False
show ?thesis
proof (cases "a = 0 ∨ b = 0")
case False
note some_gcd_ddvd_gcd[of a b]
with d0 have "d * gcd a b ddvd d * some_gcd a b" by auto
also have "d * some_gcd a b ddvd some_gcd (d * a) (d * b)"
using False d0 raw.gcd_mult by (simp add: some_gcd_connect)
also note some_gcd_ddvd_gcd
finally show ?thesis.
next
case True
with d0 show ?thesis
apply (elim disjE)
apply (rule ddvd_trans[of _ "d * b"]; force)
apply (rule ddvd_trans[of _ "d * a"]; force)
done
qed
qed

lemma gcd_greatest_mult: assumes cad: "c dvd a * d" and cbd: "c dvd b * d"
shows "c dvd gcd a b * d"
proof-
from gcd_greatest[OF assms] have c: "c dvd gcd (d * a) (d * b)" by (auto simp: ac_simps)
note gcd_mult_ddvd[of d a b]
then have "gcd (d * a) (d * b) dvd gcd a b * d" by (auto simp: ac_simps)
from dvd_trans[OF c this] show ?thesis .
qed

lemma listgcd_greatest_mult: "(⋀ x :: 'a. x ∈ set xs ⟹ y dvd x * z) ⟹ y dvd listgcd xs * z"
proof (induct xs)
case (Cons x xs)
from Cons have "y dvd x * z" "y dvd listgcd xs * z" by auto
thus ?case unfolding listgcd_simps by (rule gcd_greatest_mult)
qed (simp)

lemma dvd_factor_mult_gcd:
assumes dvd: "k dvd p * q" "k dvd p * r"
and q0: "q ≠ 0" and r0: "r ≠ 0"
shows "k dvd p * gcd q r"
proof -
from dvd gcd_greatest[of k "p * q" "p * r"]
have "k dvd gcd (p * q) (p * r)" by simp
also from gcd_mult_ddvd[of p q r]
have "... dvd (p * gcd q r)" by auto
finally show ?thesis .
qed

lemma coprime_mult_cross_dvd:
assumes coprime: "coprime p q" and eq: "p' * p = q' * q"
shows "p dvd q'" (is ?g1) and "q dvd p'" (is ?g2)
proof (atomize(full), cases "p = 0 ∨ q = 0")
case True
then show "?g1 ∧ ?g2"
proof
assume p0: "p = 0" with coprime have "q dvd 1" by auto
with eq p0 show ?thesis by auto
next
assume q0: "q = 0" with coprime have "p dvd 1" by auto
with eq q0 show ?thesis by auto
qed
next
case False
{
fix p q r p' q' :: 'a
assume cop: "coprime p q" and eq: "p' * p = q' * q" and p: "p ≠ 0" and q: "q ≠ 0"
and r: "r dvd p" "r dvd q"
let ?gcd = "gcd q p"
from eq have "p' * p dvd q' * q" by auto
hence d1: "p dvd q' * q" by (rule dvd_mult_right)
have d2: "p dvd q' * p" by auto
from dvd_factor_mult_gcd[OF d1 d2 q p] have 1: "p dvd q' * ?gcd" .
from q p have 2: "?gcd dvd q" by auto
from q p have 3: "?gcd dvd p" by auto
from cop[unfolded coprime_def', rule_format, OF 3 2] have "?gcd dvd 1" .
from 1 dvd_mult_unit_iff[OF this] have "p dvd q'" by auto
} note main = this
from main[OF coprime eq,of 1] False coprime coprime_commute main[OF _ eq[symmetric], of 1]
show "?g1 ∧ ?g2" by auto
qed

end

subclass (in ring_gcd) idom_gcd by (unfold_locales, auto)

lemma coprime_rewrites: "comm_monoid_mult.coprime ((*)) 1 = coprime"
apply (intro ext)
apply (subst comm_monoid_mult.coprime_def')
apply (unfold_locales)
apply (unfold dvd_rewrites)
apply (fold coprime_def') ..

(* TODO: incorporate into the default class hierarchy *)
locale gcd_condition =
fixes ty :: "'a :: idom itself"
assumes gcd_exists: "⋀a b :: 'a. ∃x. is_gcd x a b"
begin
sublocale idom_gcd "(*)" "1 :: 'a" "(+)" 0 "(-)" uminus some_gcd
rewrites "dvd.dvd ((*)) = (dvd)"
and "comm_monoid_mult.coprime ((*) ) 1 = Unique_Factorization.coprime"
proof-
have "is_gcd (some_gcd a b) a b" for a b :: 'a by (intro is_gcd_some_gcdI gcd_exists)
from this[unfolded is_gcd_def]
show "class.idom_gcd (*) (1 :: 'a) (+) 0 (-) uminus some_gcd" by (unfold_locales, auto simp: dvd_rewrites)
end

instance semiring_gcd ⊆ comm_monoid_gcd by (intro_classes, auto)

lemma listgcd_connect: "listgcd = gcd_list"
proof (intro ext)
fix xs :: "'a list"
show "listgcd xs = gcd_list xs" by(induct xs, auto)
qed

interpretation some_gcd: gcd_condition "TYPE('a::ufd)"
proof(unfold_locales, intro exI)
interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact factorial_monoid)
note d = dvd.dvd_def some_gcd_def carrier_0
fix a b :: 'a
show "is_gcd (some_gcd a b) a b"
proof (cases "a = 0 ∨ b = 0")
case True
thus ?thesis using some_gcd_0 by auto
next
case False
with gcdof_exists[of a b]
show ?thesis by (auto intro!: is_gcd_some_gcdI simp add: is_gcd_connect some_gcd_connect)
qed
qed

lemma some_gcd_listgcd_dvd_listgcd: "some_gcd.listgcd xs dvd listgcd xs"
by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd)

lemma listgcd_dvd_some_gcd_listgcd: "listgcd xs dvd some_gcd.listgcd xs"
by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd)

context factorial_ring_gcd begin

text ‹Do not declare the following as subclass, to avoid conflict in
‹field ⊆ gcd_condition› vs. ‹factorial_ring_gcd ⊆ gcd_condition›.
›
sublocale as_ufd: ufd
proof(unfold_locales, goal_cases)
case (1 x)
from prime_factorization_exists[OF ‹x ≠ 0›]
obtain F where f: "⋀f. f ∈# F ⟹ prime_elem f"
and Fx: "normalize (prod_mset F) = normalize x" by auto
from associatedE2[OF Fx] obtain u where u: "is_unit u" "x = u * prod_mset F"
by blast
from ‹¬ is_unit x› Fx have "F ≠ {#}" by auto
then obtain g G where F: "F = add_mset g G" by (cases F, auto)
then have "g ∈# F" by auto
with f[OF this]prime_elem_iff_irreducible
irreducible_mult_unit_left[OF unit_factor_is_unit[OF ‹x ≠ 0›]]
have g: "irreducible (u * g)" using u(1)
by (subst irreducible_mult_unit_left) simp_all
show ?case
proof (intro exI conjI mset_factorsI)
show "prod_mset (add_mset (u * g) G) = x"
using ‹x ≠ 0› by (simp add: F ac_simps u)
fix f assume "f ∈# add_mset (u * g) G"
with f[unfolded F] g prime_elem_iff_irreducible
show "irreducible f" by auto
qed auto
next
case (2 x F G)
note transpD[OF multiset.rel_transp[OF ddvd_transp],trans]
obtain fs where F: "F = mset fs" by (metis ex_mset)
have "list_all2 (ddvd) fs (map normalize fs)" by (intro list_all2_all_nthI, auto)
then have FH: "rel_mset (ddvd) F (image_mset normalize F)" by (unfold rel_mset_def F, force)
also
have FG: "image_mset normalize F = image_mset normalize G"
proof (intro prime_factorization_unique'')
from 2 have xF: "x = prod_mset F" and xG: "x = prod_mset G" by auto
from xF have "normalize x = normalize (prod_mset (image_mset normalize F))"
with xG have nFG: "… = normalize (prod_mset (image_mset normalize G))"
then show "normalize (∏i∈#image_mset normalize F. i) =
normalize (∏i∈#image_mset normalize G. i)" by auto
next
from 2 prime_elem_iff_irreducible have "f ∈# F ⟹ prime_elem f" "g ∈# G ⟹ prime_elem g" for f g
by (auto intro: prime_elemI)
then show " Multiset.Ball (image_mset normalize F) prime"
"Multiset.Ball (image_mset normalize G) prime" by auto
qed
also
obtain gs where G: "G = mset gs" by (metis ex_mset)
have "list_all2 ((ddvd)¯¯) gs (map normalize gs)" by (intro list_all2_all_nthI, auto)
then have "rel_mset (ddvd) (image_mset normalize G) G"
by (subst multiset.rel_flip[symmetric], unfold rel_mset_def G, force)
finally show ?case.
qed

end

instance int :: ufd by (intro ufd.intro_of_class as_ufd.ufd_axioms)
instance int :: idom_gcd by (intro_classes, auto)

instance field ⊆ ufd by (intro_classes, auto simp: dvd_field_iff)

end
```