# Theory GCD

```(*  Title:      HOL/GCD.thy
Author:     Christophe Tabacznyj
Author:     Lawrence C. Paulson
Author:     Amine Chaieb
Author:     Thomas M. Rasmussen
Author:     Tobias Nipkow

This file deals with the functions gcd and lcm.  Definitions and
lemmas are proved uniformly for the natural numbers and integers.

This file combines and revises a number of prior developments.

The original theories "GCD" and "Primes" were by Christophe Tabacznyj
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
gcd, lcm, and prime for the natural numbers.

The original theory "IntPrimes" was by Thomas M. Rasmussen, and
extended gcd, lcm, primes to the integers. Amine Chaieb provided
another extension of the notions to the integers, and added a number
of results to "Primes" and "GCD". IntPrimes also defined and developed
the congruence relations on the integers. The notion was extended to
the natural numbers by Chaieb.

natural numbers and the integers, and added a number of new theorems.

Tobias Nipkow cleaned up a lot.
*)

section ‹Greatest common divisor and least common multiple›

theory GCD
imports Groups_List Code_Numeral
begin

subsection ‹Abstract bounded quasi semilattices as common foundation›

locale bounded_quasi_semilattice = abel_semigroup +
fixes top :: 'a  ("❙⊤") and bot :: 'a  ("❙⊥")
and normalize :: "'a ⇒ 'a"
assumes idem_normalize [simp]: "a ❙* a = normalize a"
and normalize_left_idem [simp]: "normalize a ❙* b = a ❙* b"
and normalize_idem [simp]: "normalize (a ❙* b) = a ❙* b"
and normalize_top [simp]: "normalize ❙⊤ = ❙⊤"
and normalize_bottom [simp]: "normalize ❙⊥ = ❙⊥"
and top_left_normalize [simp]: "❙⊤ ❙* a = normalize a"
and bottom_left_bottom [simp]: "❙⊥ ❙* a = ❙⊥"
begin

lemma left_idem [simp]:
"a ❙* (a ❙* b) = a ❙* b"
using assoc [of a a b, symmetric] by simp

lemma right_idem [simp]:
"(a ❙* b) ❙* b = a ❙* b"
using left_idem [of b a] by (simp add: ac_simps)

lemma comp_fun_idem: "comp_fun_idem f"
by standard (simp_all add: fun_eq_iff ac_simps)

interpretation comp_fun_idem f
by (fact comp_fun_idem)

lemma top_right_normalize [simp]:
"a ❙* ❙⊤ = normalize a"
using top_left_normalize [of a] by (simp add: ac_simps)

lemma bottom_right_bottom [simp]:
"a ❙* ❙⊥ = ❙⊥"
using bottom_left_bottom [of a] by (simp add: ac_simps)

lemma normalize_right_idem [simp]:
"a ❙* normalize b = a ❙* b"
using normalize_left_idem [of b a] by (simp add: ac_simps)

end

locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
begin

interpretation comp_fun_idem f
by (fact comp_fun_idem)

definition F :: "'a set ⇒ 'a"
where
eq_fold: "F A = (if finite A then Finite_Set.fold f ❙⊤ A else ❙⊥)"

lemma infinite [simp]:
"infinite A ⟹ F A = ❙⊥"

lemma set_eq_fold [code]:
"F (set xs) = fold f xs ❙⊤"

lemma empty [simp]:
"F {} = ❙⊤"

lemma insert [simp]:
"F (insert a A) = a ❙* F A"
by (cases "finite A") (simp_all add: eq_fold)

lemma normalize [simp]:
"normalize (F A) = F A"
by (induct A rule: infinite_finite_induct) simp_all

lemma in_idem:
assumes "a ∈ A"
shows "a ❙* F A = F A"
using assms by (induct A rule: infinite_finite_induct)
(auto simp: left_commute [of a])

lemma union:
"F (A ∪ B) = F A ❙* F B"
by (induct A rule: infinite_finite_induct)

lemma remove:
assumes "a ∈ A"
shows "F A = a ❙* F (A - {a})"
proof -
from assms obtain B where "A = insert a B" and "a ∉ B"
by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
qed

lemma insert_remove:
"F (insert a A) = a ❙* F (A - {a})"
by (cases "a ∈ A") (simp_all add: insert_absorb remove)

lemma subset:
assumes "B ⊆ A"
shows "F B ❙* F A = F A"
using assms by (simp add: union [symmetric] Un_absorb1)

end

subsection ‹Abstract GCD and LCM›

class gcd = zero + one + dvd +
fixes gcd :: "'a ⇒ 'a ⇒ 'a"
and lcm :: "'a ⇒ 'a ⇒ 'a"

class Gcd = gcd +
fixes Gcd :: "'a set ⇒ 'a"
and Lcm :: "'a set ⇒ 'a"

syntax
"_GCD1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3GCD _./ _)" [0, 10] 10)
"_GCD"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3GCD _∈_./ _)" [0, 0, 10] 10)
"_LCM1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3LCM _./ _)" [0, 10] 10)
"_LCM"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3LCM _∈_./ _)" [0, 0, 10] 10)

translations
"GCD x y. f"   ⇌ "GCD x. GCD y. f"
"GCD x. f"     ⇌ "CONST Gcd (CONST range (λx. f))"
"GCD x∈A. f"   ⇌ "CONST Gcd ((λx. f) ` A)"
"LCM x y. f"   ⇌ "LCM x. LCM y. f"
"LCM x. f"     ⇌ "CONST Lcm (CONST range (λx. f))"
"LCM x∈A. f"   ⇌ "CONST Lcm ((λx. f) ` A)"

class semiring_gcd = normalization_semidom + gcd +
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"
and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
and lcm_gcd: "lcm a b = normalize (a * b div gcd a b)"
begin

lemma gcd_greatest_iff [simp]: "a dvd gcd b c ⟷ a dvd b ∧ a dvd c"
by (blast intro!: gcd_greatest intro: dvd_trans)

lemma gcd_dvdI1: "a dvd c ⟹ gcd a b dvd c"
by (rule dvd_trans) (rule gcd_dvd1)

lemma gcd_dvdI2: "b dvd c ⟹ gcd a b dvd c"
by (rule dvd_trans) (rule gcd_dvd2)

lemma dvd_gcdD1: "a dvd gcd b c ⟹ a dvd b"
using gcd_dvd1 [of b c] by (blast intro: dvd_trans)

lemma dvd_gcdD2: "a dvd gcd b c ⟹ a dvd c"
using gcd_dvd2 [of b c] by (blast intro: dvd_trans)

lemma gcd_0_left [simp]: "gcd 0 a = normalize a"
by (rule associated_eqI) simp_all

lemma gcd_0_right [simp]: "gcd a 0 = normalize a"
by (rule associated_eqI) simp_all

lemma gcd_eq_0_iff [simp]: "gcd a b = 0 ⟷ a = 0 ∧ b = 0"
(is "?P ⟷ ?Q")
proof
assume ?P
then have "0 dvd gcd a b"
by simp
then have "0 dvd a" and "0 dvd b"
by (blast intro: dvd_trans)+
then show ?Q
by simp
next
assume ?Q
then show ?P
by simp
qed

lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 ∧ b = 0 then 0 else 1)"
proof (cases "gcd a b = 0")
case True
then show ?thesis by simp
next
case False
have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
by (rule unit_factor_mult_normalize)
then have "unit_factor (gcd a b) * gcd a b = gcd a b"
by simp
then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
by simp
with False show ?thesis
by simp
qed

lemma is_unit_gcd_iff [simp]:
"is_unit (gcd a b) ⟷ gcd a b = 1"
by (cases "a = 0 ∧ b = 0") (auto simp: unit_factor_gcd dest: is_unit_unit_factor)

sublocale gcd: abel_semigroup gcd
proof
fix a b c
show "gcd a b = gcd b a"
by (rule associated_eqI) simp_all
from gcd_dvd1 have "gcd (gcd a b) c dvd a"
by (rule dvd_trans) simp
moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
by (rule dvd_trans) simp
ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
by (auto intro!: gcd_greatest)
from gcd_dvd2 have "gcd a (gcd b c) dvd b"
by (rule dvd_trans) simp
moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
by (rule dvd_trans) simp
ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
by (auto intro!: gcd_greatest)
from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
by (rule associated_eqI) simp_all
qed

sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
proof
show "gcd a a = normalize a" for a
proof -
have "a dvd gcd a a"
by (rule gcd_greatest) simp_all
then show ?thesis
by (auto intro: associated_eqI)
qed
show "gcd (normalize a) b = gcd a b" for a b
using gcd_dvd1 [of "normalize a" b]
by (auto intro: associated_eqI)
show "gcd 1 a = 1" for a
by (rule associated_eqI) simp_all
qed simp_all

lemma gcd_self: "gcd a a = normalize a"
by (fact gcd.idem_normalize)

lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
by (fact gcd.left_idem)

lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
by (fact gcd.right_idem)

lemma gcdI:
assumes "c dvd a" and "c dvd b"
and greatest: "⋀d. d dvd a ⟹ d dvd b ⟹ d dvd c"
and "normalize c = c"
shows "c = gcd a b"
by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)

lemma gcd_unique:
"d dvd a ∧ d dvd b ∧ normalize d = d ∧ (∀e. e dvd a ∧ e dvd b ⟶ e dvd d) ⟷ d = gcd a b"
by rule (auto intro: gcdI simp: gcd_greatest)

lemma gcd_dvd_prod: "gcd a b dvd k * b"
using mult_dvd_mono [of 1] by auto

lemma gcd_proj2_if_dvd: "b dvd a ⟹ gcd a b = normalize b"
by (rule gcdI [symmetric]) simp_all

lemma gcd_proj1_if_dvd: "a dvd b ⟹ gcd a b = normalize a"
by (rule gcdI [symmetric]) simp_all

lemma gcd_proj1_iff: "gcd m n = normalize m ⟷ m dvd n"
proof
assume *: "gcd m n = normalize m"
show "m dvd n"
proof (cases "m = 0")
case True
with * show ?thesis by simp
next
case [simp]: False
from * have **: "m = gcd m n * unit_factor m"
show ?thesis
by (subst **) (simp add: mult_unit_dvd_iff)
qed
next
assume "m dvd n"
then show "gcd m n = normalize m"
by (rule gcd_proj1_if_dvd)
qed

lemma gcd_proj2_iff: "gcd m n = normalize n ⟷ n dvd m"
using gcd_proj1_iff [of n m] by (simp add: ac_simps)

lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize (c * gcd a b)"
proof (cases "c = 0")
case True
then show ?thesis by simp
next
case False
then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
by (auto intro: gcd_greatest)
moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
by (auto intro: associated_eqI)
then show ?thesis
qed

lemma gcd_mult_right: "gcd (a * c) (b * c) = normalize (gcd b a * c)"
using gcd_mult_left [of c a b] by (simp add: ac_simps)

lemma dvd_lcm1 [iff]: "a dvd lcm a b"
by (metis div_mult_swap dvd_mult2 dvd_normalize_iff dvd_refl gcd_dvd2 lcm_gcd)

lemma dvd_lcm2 [iff]: "b dvd lcm a b"
by (metis dvd_div_mult dvd_mult dvd_normalize_iff dvd_refl gcd_dvd1 lcm_gcd)

lemma dvd_lcmI1: "a dvd b ⟹ a dvd lcm b c"
by (rule dvd_trans) (assumption, blast)

lemma dvd_lcmI2: "a dvd c ⟹ a dvd lcm b c"
by (rule dvd_trans) (assumption, blast)

lemma lcm_dvdD1: "lcm a b dvd c ⟹ a dvd c"
using dvd_lcm1 [of a b] by (blast intro: dvd_trans)

lemma lcm_dvdD2: "lcm a b dvd c ⟹ b dvd c"
using dvd_lcm2 [of a b] by (blast intro: dvd_trans)

lemma lcm_least:
assumes "a dvd c" and "b dvd c"
shows "lcm a b dvd c"
proof (cases "c = 0")
case True
then show ?thesis by simp
next
case False
then have *: "is_unit (unit_factor c)"
by simp
show ?thesis
proof (cases "gcd a b = 0")
case True
with assms show ?thesis by simp
next
case False
have "a * b dvd normalize (c * gcd a b)"
using assms by (subst gcd_mult_left [symmetric]) (auto intro!: gcd_greatest simp: mult_ac)
with False have "(a * b div gcd a b) dvd c"
by (subst div_dvd_iff_mult) auto
thus ?thesis by (simp add: lcm_gcd)
qed
qed

lemma lcm_least_iff [simp]: "lcm a b dvd c ⟷ a dvd c ∧ b dvd c"
by (blast intro!: lcm_least intro: dvd_trans)

lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"

lemma lcm_0_left [simp]: "lcm 0 a = 0"

lemma lcm_0_right [simp]: "lcm a 0 = 0"

lemma lcm_eq_0_iff: "lcm a b = 0 ⟷ a = 0 ∨ b = 0"
(is "?P ⟷ ?Q")
proof
assume ?P
then have "0 dvd lcm a b"
by simp
also have "lcm a b dvd (a * b)"
by simp
finally show ?Q
by auto
next
assume ?Q
then show ?P
by auto
qed

lemma zero_eq_lcm_iff: "0 = lcm a b ⟷ a = 0 ∨ b = 0"
using lcm_eq_0_iff[of a b] by auto

lemma lcm_eq_1_iff [simp]: "lcm a b = 1 ⟷ is_unit a ∧ is_unit b"
by (auto intro: associated_eqI)

lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 ∨ b = 0 then 0 else 1)"
using lcm_eq_0_iff[of a b] by (cases "lcm a b = 0") (auto simp: lcm_gcd)

sublocale lcm: abel_semigroup lcm
proof
fix a b c
show "lcm a b = lcm b a"
by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
have "lcm (lcm a b) c dvd lcm a (lcm b c)"
and "lcm a (lcm b c) dvd lcm (lcm a b) c"
by (auto intro: lcm_least
dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
then show "lcm (lcm a b) c = lcm a (lcm b c)"
by (rule associated_eqI) simp_all
qed

sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
proof
show "lcm a a = normalize a" for a
proof -
have "lcm a a dvd a"
by (rule lcm_least) simp_all
then show ?thesis
by (auto intro: associated_eqI)
qed
show "lcm (normalize a) b = lcm a b" for a b
using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
by (auto intro: associated_eqI)
show "lcm 1 a = normalize a" for a
by (rule associated_eqI) simp_all
qed simp_all

lemma lcm_self: "lcm a a = normalize a"
by (fact lcm.idem_normalize)

lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
by (fact lcm.left_idem)

lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
by (fact lcm.right_idem)

lemma gcd_lcm:
assumes "a ≠ 0" and "b ≠ 0"
shows "gcd a b = normalize (a * b div lcm a b)"
proof -
from assms have [simp]: "a * b div gcd a b ≠ 0"
by (subst dvd_div_eq_0_iff) auto
let ?u = "unit_factor (a * b div gcd a b)"
have "gcd a b * normalize (a * b div gcd a b) =
gcd a b * ((a * b div gcd a b) * (1 div ?u))"
by simp
also have "… = a * b div ?u"
by (subst mult.assoc [symmetric]) auto
also have "… dvd a * b"
by (subst div_unit_dvd_iff) auto
finally have "gcd a b dvd ((a * b) div lcm a b)"
by (intro dvd_mult_imp_div) (auto simp: lcm_gcd)
moreover have "a * b div lcm a b dvd a" and "a * b div lcm a b dvd b"
using assms by (subst div_dvd_iff_mult; simp add: lcm_eq_0_iff mult.commute[of b "lcm a b"])+
ultimately have "normalize (gcd a b) = normalize (a * b div lcm a b)"
apply -
apply (rule associated_eqI)
using assms
apply (auto simp: div_dvd_iff_mult zero_eq_lcm_iff)
done
thus ?thesis by simp
qed

lemma lcm_1_left: "lcm 1 a = normalize a"
by (fact lcm.top_left_normalize)

lemma lcm_1_right: "lcm a 1 = normalize a"
by (fact lcm.top_right_normalize)

lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize (c * lcm a b)"
proof (cases "c = 0")
case True
then show ?thesis by simp
next
case False
then have *: "lcm (c * a) (c * b) dvd c * lcm a b"
by (auto intro: lcm_least)
moreover have "lcm a b dvd lcm (c * a) (c * b) div c"
by (intro lcm_least) (auto intro!: dvd_mult_imp_div simp: mult_ac)
hence "c * lcm a b dvd lcm (c * a) (c * b)"
using False by (subst (asm) dvd_div_iff_mult) (auto simp: mult_ac intro: dvd_lcmI1)
ultimately have "normalize (lcm (c * a) (c * b)) = normalize (c * lcm a b)"
by (auto intro: associated_eqI)
then show ?thesis
qed

lemma lcm_mult_right: "lcm (a * c) (b * c) = normalize (lcm b a * c)"
using lcm_mult_left [of c a b] by (simp add: ac_simps)

lemma lcm_mult_unit1: "is_unit a ⟹ lcm (b * a) c = lcm b c"
by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)

lemma lcm_mult_unit2: "is_unit a ⟹ lcm b (c * a) = lcm b c"
using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)

lemma lcm_div_unit1:
"is_unit a ⟹ lcm (b div a) c = lcm b c"
by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)

lemma lcm_div_unit2: "is_unit a ⟹ lcm b (c div a) = lcm b c"
by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)

lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
by (fact lcm.normalize_left_idem)

lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
by (fact lcm.normalize_right_idem)

lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
by standard (simp_all add: fun_eq_iff ac_simps)

lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
by standard (simp_all add: fun_eq_iff ac_simps)

lemma gcd_dvd_antisym: "gcd a b dvd gcd c d ⟹ gcd c d dvd gcd a b ⟹ gcd a b = gcd c d"
proof (rule gcdI)
assume *: "gcd a b dvd gcd c d"
and **: "gcd c d dvd gcd a b"
have "gcd c d dvd c"
by simp
with * show "gcd a b dvd c"
by (rule dvd_trans)
have "gcd c d dvd d"
by simp
with * show "gcd a b dvd d"
by (rule dvd_trans)
show "normalize (gcd a b) = gcd a b"
by simp
fix l assume "l dvd c" and "l dvd d"
then have "l dvd gcd c d"
by (rule gcd_greatest)
from this and ** show "l dvd gcd a b"
by (rule dvd_trans)
qed

declare unit_factor_lcm [simp]

lemma lcmI:
assumes "a dvd c" and "b dvd c" and "⋀d. a dvd d ⟹ b dvd d ⟹ c dvd d"
and "normalize c = c"
shows "c = lcm a b"
by (rule associated_eqI) (auto simp: assms intro: lcm_least)

lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b"
using gcd_dvd2 by (rule dvd_lcmI2)

lemmas lcm_0 = lcm_0_right

lemma lcm_unique:
"a dvd d ∧ b dvd d ∧ normalize d = d ∧ (∀e. a dvd e ∧ b dvd e ⟶ d dvd e) ⟷ d = lcm a b"
by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)

lemma lcm_proj1_if_dvd:
assumes "b dvd a" shows "lcm a b = normalize a"
proof -
have "normalize (lcm a b) = normalize a"
by (rule associatedI) (use assms in auto)
thus ?thesis by simp
qed

lemma lcm_proj2_if_dvd: "a dvd b ⟹ lcm a b = normalize b"
using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)

lemma lcm_proj1_iff: "lcm m n = normalize m ⟷ n dvd m"
proof
assume *: "lcm m n = normalize m"
show "n dvd m"
proof (cases "m = 0")
case True
then show ?thesis by simp
next
case [simp]: False
from * have **: "m = lcm m n * unit_factor m"
show ?thesis by (subst **) simp
qed
next
assume "n dvd m"
then show "lcm m n = normalize m"
by (rule lcm_proj1_if_dvd)
qed

lemma lcm_proj2_iff: "lcm m n = normalize n ⟷ m dvd n"
using lcm_proj1_iff [of n m] by (simp add: ac_simps)

lemma gcd_mono: "a dvd c ⟹ b dvd d ⟹ gcd a b dvd gcd c d"

lemma lcm_mono: "a dvd c ⟹ b dvd d ⟹ lcm a b dvd lcm c d"

lemma dvd_productE:
assumes "p dvd a * b"
obtains x y where "p = x * y" "x dvd a" "y dvd b"
proof (cases "a = 0")
case True
thus ?thesis by (intro that[of p 1]) simp_all
next
case False
define x y where "x = gcd a p" and "y = p div x"
have "p = x * y" by (simp add: x_def y_def)
moreover have "x dvd a" by (simp add: x_def)
moreover from assms have "p dvd gcd (b * a) (b * p)"
by (intro gcd_greatest) (simp_all add: mult.commute)
hence "p dvd b * gcd a p" by (subst (asm) gcd_mult_left) auto
with False have "y dvd b"
by (simp add: x_def y_def div_dvd_iff_mult assms)
ultimately show ?thesis by (rule that)
qed

lemma gcd_mult_unit1:
assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
proof -
have "gcd (b * a) c dvd b"
using assms dvd_mult_unit_iff by blast
then show ?thesis
by (rule gcdI) simp_all
qed

lemma gcd_mult_unit2: "is_unit a ⟹ gcd b (c * a) = gcd b c"
using gcd.commute gcd_mult_unit1 by auto

lemma gcd_div_unit1: "is_unit a ⟹ gcd (b div a) c = gcd b c"
by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)

lemma gcd_div_unit2: "is_unit a ⟹ gcd b (c div a) = gcd b c"
by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)

lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
by (fact gcd.normalize_left_idem)

lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
by (fact gcd.normalize_right_idem)

lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"

lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"

lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"

end

class ring_gcd = comm_ring_1 + semiring_gcd
begin

lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
by (rule sym, rule gcdI) (simp_all add: gcd_greatest)

lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b"
by (rule sym, rule gcdI) (simp_all add: gcd_greatest)

lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a"
by (fact gcd_neg1)

lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)"
by (fact gcd_neg2)

lemma gcd_diff1: "gcd (m - n) n = gcd m n"

lemma gcd_diff2: "gcd (n - m) n = gcd m n"
by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1)

lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)

lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)

lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
by (fact lcm_neg1)

lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
by (fact lcm_neg2)

end

class semiring_Gcd = semiring_gcd + Gcd +
assumes Gcd_dvd: "a ∈ A ⟹ Gcd A dvd a"
and Gcd_greatest: "(⋀b. b ∈ A ⟹ a dvd b) ⟹ a dvd Gcd A"
and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
assumes dvd_Lcm: "a ∈ A ⟹ a dvd Lcm A"
and Lcm_least: "(⋀b. b ∈ A ⟹ b dvd a) ⟹ Lcm A dvd a"
and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
begin

lemma Lcm_Gcd: "Lcm A = Gcd {b. ∀a∈A. a dvd b}"
by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)

lemma Gcd_Lcm: "Gcd A = Lcm {b. ∀a∈A. b dvd a}"
by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)

lemma Gcd_empty [simp]: "Gcd {} = 0"
by (rule dvd_0_left, rule Gcd_greatest) simp

lemma Lcm_empty [simp]: "Lcm {} = 1"
by (auto intro: associated_eqI Lcm_least)

lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
proof -
have "Gcd (insert a A) dvd gcd a (Gcd A)"
by (auto intro: Gcd_dvd Gcd_greatest)
moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
proof (rule Gcd_greatest)
fix b
assume "b ∈ insert a A"
then show "gcd a (Gcd A) dvd b"
proof
assume "b = a"
then show ?thesis
by simp
next
assume "b ∈ A"
then have "Gcd A dvd b"
by (rule Gcd_dvd)
moreover have "gcd a (Gcd A) dvd Gcd A"
by simp
ultimately show ?thesis
by (blast intro: dvd_trans)
qed
qed
ultimately show ?thesis
by (auto intro: associated_eqI)
qed

lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)"
proof (rule sym)
have "lcm a (Lcm A) dvd Lcm (insert a A)"
by (auto intro: dvd_Lcm Lcm_least)
moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
proof (rule Lcm_least)
fix b
assume "b ∈ insert a A"
then show "b dvd lcm a (Lcm A)"
proof
assume "b = a"
then show ?thesis by simp
next
assume "b ∈ A"
then have "b dvd Lcm A"
by (rule dvd_Lcm)
moreover have "Lcm A dvd lcm a (Lcm A)"
by simp
ultimately show ?thesis
by (blast intro: dvd_trans)
qed
qed
ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
qed

lemma LcmI:
assumes "⋀a. a ∈ A ⟹ a dvd b"
and "⋀c. (⋀a. a ∈ A ⟹ a dvd c) ⟹ b dvd c"
and "normalize b = b"
shows "b = Lcm A"
by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)

lemma Lcm_subset: "A ⊆ B ⟹ Lcm A dvd Lcm B"
by (blast intro: Lcm_least dvd_Lcm)

lemma Lcm_Un: "Lcm (A ∪ B) = lcm (Lcm A) (Lcm B)"
proof -
have "⋀d. ⟦Lcm A dvd d; Lcm B dvd d⟧ ⟹ Lcm (A ∪ B) dvd d"
by (meson UnE Lcm_least dvd_Lcm dvd_trans)
then show ?thesis
by (meson Lcm_subset lcm_unique normalize_Lcm sup.cobounded1 sup.cobounded2)
qed

lemma Gcd_0_iff [simp]: "Gcd A = 0 ⟷ A ⊆ {0}"
(is "?P ⟷ ?Q")
proof
assume ?P
show ?Q
proof
fix a
assume "a ∈ A"
then have "Gcd A dvd a"
by (rule Gcd_dvd)
with ‹?P› have "a = 0"
by simp
then show "a ∈ {0}"
by simp
qed
next
assume ?Q
have "0 dvd Gcd A"
proof (rule Gcd_greatest)
fix a
assume "a ∈ A"
with ‹?Q› have "a = 0"
by auto
then show "0 dvd a"
by simp
qed
then show ?P
by simp
qed

lemma Lcm_1_iff [simp]: "Lcm A = 1 ⟷ (∀a∈A. is_unit a)"
(is "?P ⟷ ?Q")
proof
assume ?P
show ?Q
proof
fix a
assume "a ∈ A"
then have "a dvd Lcm A"
by (rule dvd_Lcm)
with ‹?P› show "is_unit a"
by simp
qed
next
assume ?Q
then have "is_unit (Lcm A)"
by (blast intro: Lcm_least)
then have "normalize (Lcm A) = 1"
by (rule is_unit_normalize)
then show ?P
by simp
qed

lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
proof (cases "Lcm A = 0")
case True
then show ?thesis
by simp
next
case False
with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
by blast
with False show ?thesis
by simp
qed

lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"

lemma GcdI:
assumes "⋀a. a ∈ A ⟹ b dvd a"
and "⋀c. (⋀a. a ∈ A ⟹ c dvd a) ⟹ c dvd b"
and "normalize b = b"
shows "b = Gcd A"
by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)

lemma Gcd_eq_1_I:
assumes "is_unit a" and "a ∈ A"
shows "Gcd A = 1"
proof -
from assms have "is_unit (Gcd A)"
by (blast intro: Gcd_dvd dvd_unit_imp_unit)
then have "normalize (Gcd A) = 1"
by (rule is_unit_normalize)
then show ?thesis
by simp
qed

lemma Lcm_eq_0_I:
assumes "0 ∈ A"
shows "Lcm A = 0"
proof -
from assms have "0 dvd Lcm A"
by (rule dvd_Lcm)
then show ?thesis
by simp
qed

lemma Gcd_UNIV [simp]: "Gcd UNIV = 1"
using dvd_refl by (rule Gcd_eq_1_I) simp

lemma Lcm_UNIV [simp]: "Lcm UNIV = 0"
by (rule Lcm_eq_0_I) simp

lemma Lcm_0_iff:
assumes "finite A"
shows "Lcm A = 0 ⟷ 0 ∈ A"
proof (cases "A = {}")
case True
then show ?thesis by simp
next
case False
with assms show ?thesis
by (induct A rule: finite_ne_induct) (auto simp: lcm_eq_0_iff)
qed

lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
proof -
have "Gcd (normalize ` A) dvd a" if "a ∈ A" for a
proof -
from that obtain B where "A = insert a B"
by blast
moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
by (rule gcd_dvd1)
ultimately show "Gcd (normalize ` A) dvd a"
by simp
qed
then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
by (auto intro!: Gcd_greatest intro: Gcd_dvd)
then show ?thesis
by (auto intro: associated_eqI)
qed

lemma Gcd_eqI:
assumes "normalize a = a"
assumes "⋀b. b ∈ A ⟹ a dvd b"
and "⋀c. (⋀b. b ∈ A ⟹ c dvd b) ⟹ c dvd a"
shows "Gcd A = a"
using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)

lemma dvd_GcdD: "x dvd Gcd A ⟹ y ∈ A ⟹ x dvd y"
using Gcd_dvd dvd_trans by blast

lemma dvd_Gcd_iff: "x dvd Gcd A ⟷ (∀y∈A. x dvd y)"
by (blast dest: dvd_GcdD intro: Gcd_greatest)

lemma Gcd_mult: "Gcd ((*) c ` A) = normalize (c * Gcd A)"
proof (cases "c = 0")
case True
then show ?thesis by auto
next
case [simp]: False
have "Gcd ((*) c ` A) div c dvd Gcd A"
by (intro Gcd_greatest, subst div_dvd_iff_mult)
(auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
then have "Gcd ((*) c ` A) dvd c * Gcd A"
by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
moreover have "c * Gcd A dvd Gcd ((*) c ` A)"
by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
ultimately have "normalize (Gcd ((*) c ` A)) = normalize (c * Gcd A)"
by (rule associatedI)
then show ?thesis by simp
qed

lemma Lcm_eqI:
assumes "normalize a = a"
and "⋀b. b ∈ A ⟹ b dvd a"
and "⋀c. (⋀b. b ∈ A ⟹ b dvd c) ⟹ a dvd c"
shows "Lcm A = a"
using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)

lemma Lcm_dvdD: "Lcm A dvd x ⟹ y ∈ A ⟹ y dvd x"
using dvd_Lcm dvd_trans by blast

lemma Lcm_dvd_iff: "Lcm A dvd x ⟷ (∀y∈A. y dvd x)"
by (blast dest: Lcm_dvdD intro: Lcm_least)

lemma Lcm_mult:
assumes "A ≠ {}"
shows "Lcm ((*) c ` A) = normalize (c * Lcm A)"
proof (cases "c = 0")
case True
with assms have "(*) c ` A = {0}"
by auto
with True show ?thesis by auto
next
case [simp]: False
from assms obtain x where x: "x ∈ A"
by blast
have "c dvd c * x"
by simp
also from x have "c * x dvd Lcm ((*) c ` A)"
by (intro dvd_Lcm) auto
finally have dvd: "c dvd Lcm ((*) c ` A)" .
moreover have "Lcm A dvd Lcm ((*) c ` A) div c"
by (intro Lcm_least dvd_mult_imp_div)
(auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
ultimately have "c * Lcm A dvd Lcm ((*) c ` A)"
by auto
moreover have "Lcm ((*) c ` A) dvd c * Lcm A"
by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
ultimately have "normalize (c * Lcm A) = normalize (Lcm ((*) c ` A))"
by (rule associatedI)
then show ?thesis by simp
qed

lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
proof -
have "(A - {a. is_unit a}) ∪ {a∈A. is_unit a} = A"
by blast
then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a∈A. is_unit a})"
also have "Lcm {a∈A. is_unit a} = 1"
by simp
finally show ?thesis
by simp
qed

lemma Lcm_0_iff': "Lcm A = 0 ⟷ (∄l. l ≠ 0 ∧ (∀a∈A. a dvd l))"
by (metis Lcm_least dvd_0_left dvd_Lcm)

lemma Lcm_no_multiple: "(∀m. m ≠ 0 ⟶ (∃a∈A. ¬ a dvd m)) ⟹ Lcm A = 0"
by (auto simp: Lcm_0_iff')

lemma Lcm_singleton [simp]: "Lcm {a} = normalize a"
by simp

lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
by simp

lemma Gcd_1: "1 ∈ A ⟹ Gcd A = 1"
by (auto intro!: Gcd_eq_1_I)

lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
by simp

lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
by simp

lemma Gcd_mono:
assumes "⋀x. x ∈ A ⟹ f x dvd g x"
shows   "(GCD x∈A. f x) dvd (GCD x∈A. g x)"
proof (intro Gcd_greatest, safe)
fix x assume "x ∈ A"
hence "(GCD x∈A. f x) dvd f x"
by (intro Gcd_dvd) auto
also have "f x dvd g x"
using ‹x ∈ A› assms by blast
finally show "(GCD x∈A. f x) dvd …" .
qed

lemma Lcm_mono:
assumes "⋀x. x ∈ A ⟹ f x dvd g x"
shows   "(LCM x∈A. f x) dvd (LCM x∈A. g x)"
proof (intro Lcm_least, safe)
fix x assume "x ∈ A"
hence "f x dvd g x" by (rule assms)
also have "g x dvd (LCM x∈A. g x)"
using ‹x ∈ A› by (intro dvd_Lcm) auto
finally show "f x dvd …" .
qed

end

subsection ‹An aside: GCD and LCM on finite sets for incomplete gcd rings›

context semiring_gcd
begin

sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
defines
Gcd_fin ("Gcd⇩f⇩i⇩n") = "Gcd_fin.F :: 'a set ⇒ 'a" ..

abbreviation gcd_list :: "'a list ⇒ 'a"
where "gcd_list xs ≡ Gcd⇩f⇩i⇩n (set xs)"

sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
defines
Lcm_fin ("Lcm⇩f⇩i⇩n") = Lcm_fin.F ..

abbreviation lcm_list :: "'a list ⇒ 'a"
where "lcm_list xs ≡ Lcm⇩f⇩i⇩n (set xs)"

lemma Gcd_fin_dvd:
"a ∈ A ⟹ Gcd⇩f⇩i⇩n A dvd a"
by (induct A rule: infinite_finite_induct)
(auto intro: dvd_trans)

lemma dvd_Lcm_fin:
"a ∈ A ⟹ a dvd Lcm⇩f⇩i⇩n A"
by (induct A rule: infinite_finite_induct)
(auto intro: dvd_trans)

lemma Gcd_fin_greatest:
"a dvd Gcd⇩f⇩i⇩n A" if "finite A" and "⋀b. b ∈ A ⟹ a dvd b"
using that by (induct A) simp_all

lemma Lcm_fin_least:
"Lcm⇩f⇩i⇩n A dvd a" if "finite A" and "⋀b. b ∈ A ⟹ b dvd a"
using that by (induct A) simp_all

lemma gcd_list_greatest:
"a dvd gcd_list bs" if "⋀b. b ∈ set bs ⟹ a dvd b"
by (rule Gcd_fin_greatest) (simp_all add: that)

lemma lcm_list_least:
"lcm_list bs dvd a" if "⋀b. b ∈ set bs ⟹ b dvd a"
by (rule Lcm_fin_least) (simp_all add: that)

lemma dvd_Gcd_fin_iff:
"b dvd Gcd⇩f⇩i⇩n A ⟷ (∀a∈A. b dvd a)" if "finite A"
using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd⇩f⇩i⇩n A"])

lemma dvd_gcd_list_iff:
"b dvd gcd_list xs ⟷ (∀a∈set xs. b dvd a)"

lemma Lcm_fin_dvd_iff:
"Lcm⇩f⇩i⇩n A dvd b  ⟷ (∀a∈A. a dvd b)" if "finite A"
using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm⇩f⇩i⇩n A" b])

lemma lcm_list_dvd_iff:
"lcm_list xs dvd b  ⟷ (∀a∈set xs. a dvd b)"

lemma Gcd_fin_mult:
"Gcd⇩f⇩i⇩n (image (times b) A) = normalize (b * Gcd⇩f⇩i⇩n A)" if "finite A"
using that by induction (auto simp: gcd_mult_left)

lemma Lcm_fin_mult:
"Lcm⇩f⇩i⇩n (image (times b) A) = normalize (b * Lcm⇩f⇩i⇩n A)" if "A ≠ {}"
proof (cases "b = 0")
case True
moreover from that have "times 0 ` A = {0}"
by auto
ultimately show ?thesis
by simp
next
case False
show ?thesis proof (cases "finite A")
case False
moreover have "inj_on (times b) A"
using ‹b ≠ 0› by (rule inj_on_mult)
ultimately have "infinite (times b ` A)"
with False show ?thesis
by simp
next
case True
then show ?thesis using that
by (induct A rule: finite_ne_induct) (auto simp: lcm_mult_left)
qed
qed

lemma unit_factor_Gcd_fin:
"unit_factor (Gcd⇩f⇩i⇩n A) = of_bool (Gcd⇩f⇩i⇩n A ≠ 0)"
by (rule normalize_idem_imp_unit_factor_eq) simp

lemma unit_factor_Lcm_fin:
"unit_factor (Lcm⇩f⇩i⇩n A) = of_bool (Lcm⇩f⇩i⇩n A ≠ 0)"
by (rule normalize_idem_imp_unit_factor_eq) simp

lemma is_unit_Gcd_fin_iff [simp]:
"is_unit (Gcd⇩f⇩i⇩n A) ⟷ Gcd⇩f⇩i⇩n A = 1"
by (rule normalize_idem_imp_is_unit_iff) simp

lemma is_unit_Lcm_fin_iff [simp]:
"is_unit (Lcm⇩f⇩i⇩n A) ⟷ Lcm⇩f⇩i⇩n A = 1"
by (rule normalize_idem_imp_is_unit_iff) simp

lemma Gcd_fin_0_iff:
"Gcd⇩f⇩i⇩n A = 0 ⟷ A ⊆ {0} ∧ finite A"
by (induct A rule: infinite_finite_induct) simp_all

lemma Lcm_fin_0_iff:
"Lcm⇩f⇩i⇩n A = 0 ⟷ 0 ∈ A" if "finite A"
using that by (induct A) (auto simp: lcm_eq_0_iff)

lemma Lcm_fin_1_iff:
"Lcm⇩f⇩i⇩n A = 1 ⟷ (∀a∈A. is_unit a) ∧ finite A"
by (induct A rule: infinite_finite_induct) simp_all

end

context semiring_Gcd
begin

lemma Gcd_fin_eq_Gcd [simp]:
"Gcd⇩f⇩i⇩n A = Gcd A" if "finite A" for A :: "'a set"
using that by induct simp_all

lemma Gcd_set_eq_fold [code_unfold]:
"Gcd (set xs) = fold gcd xs 0"

lemma Lcm_fin_eq_Lcm [simp]:
"Lcm⇩f⇩i⇩n A = Lcm A" if "finite A" for A :: "'a set"
using that by induct simp_all

lemma Lcm_set_eq_fold [code_unfold]:
"Lcm (set xs) = fold lcm xs 1"

end

subsection ‹Coprimality›

context semiring_gcd
begin

lemma coprime_imp_gcd_eq_1 [simp]:
"gcd a b = 1" if "coprime a b"
proof -
define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
then have "a = t * r" and "b = t * s"
by simp_all
with that have "coprime (t * r) (t * s)"
by simp
then show ?thesis
qed

lemma gcd_eq_1_imp_coprime [dest!]:
"coprime a b" if "gcd a b = 1"
proof (rule coprimeI)
fix c
assume "c dvd a" and "c dvd b"
then have "c dvd gcd a b"
by (rule gcd_greatest)
with that show "is_unit c"
by simp
qed

lemma coprime_iff_gcd_eq_1 [presburger, code]:
"coprime a b ⟷ gcd a b = 1"

lemma is_unit_gcd [simp]:
"is_unit (gcd a b) ⟷ coprime a b"

lemma coprime_add_one_left [simp]: "coprime (a + 1) a"

lemma coprime_add_one_right [simp]: "coprime a (a + 1)"

lemma coprime_mult_left_iff [simp]:
"coprime (a * b) c ⟷ coprime a c ∧ coprime b c"
proof
assume "coprime (a * b) c"
with coprime_common_divisor [of "a * b" c]
have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
using that by blast
have "coprime a c"
by (rule coprimeI, rule *) simp_all
moreover have "coprime b c"
by (rule coprimeI, rule *) simp_all
ultimately show "coprime a c ∧ coprime b c" ..
next
assume "coprime a c ∧ coprime b c"
then have "coprime a c" "coprime b c"
by simp_all
show "coprime (a * b) c"
proof (rule coprimeI)
fix d
assume "d dvd a * b"
then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
by (rule dvd_productE)
assume "d dvd c"
with d have "r * s dvd c"
by simp
then have "r dvd c" "s dvd c"
by (auto intro: dvd_mult_left dvd_mult_right)
from ‹coprime a c› ‹r dvd a› ‹r dvd c›
have "is_unit r"
by (rule coprime_common_divisor)
moreover from ‹coprime b c› ‹s dvd b› ‹s dvd c›
have "is_unit s"
by (rule coprime_common_divisor)
ultimately show "is_unit d"
qed
qed

lemma coprime_mult_right_iff [simp]:
"coprime c (a * b) ⟷ coprime c a ∧ coprime c b"
using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)

lemma coprime_power_left_iff [simp]:
"coprime (a ^ n) b ⟷ coprime a b ∨ n = 0"
proof (cases "n = 0")
case True
then show ?thesis
by simp
next
case False
then have "n > 0"
by simp
then show ?thesis
by (induction n rule: nat_induct_non_zero) simp_all
qed

lemma coprime_power_right_iff [simp]:
"coprime a (b ^ n) ⟷ coprime a b ∨ n = 0"
using coprime_power_left_iff [of b n a] by (simp add: ac_simps)

lemma prod_coprime_left:
"coprime (∏i∈A. f i) a" if "⋀i. i ∈ A ⟹ coprime (f i) a"
using that by (induct A rule: infinite_finite_induct) simp_all

lemma prod_coprime_right:
"coprime a (∏i∈A. f i)" if "⋀i. i ∈ A ⟹ coprime a (f i)"
using that prod_coprime_left [of A f a] by (simp add: ac_simps)

lemma prod_list_coprime_left:
"coprime (prod_list xs) a" if "⋀x. x ∈ set xs ⟹ coprime x a"
using that by (induct xs) simp_all

lemma prod_list_coprime_right:
"coprime a (prod_list xs)" if "⋀x. x ∈ set xs ⟹ coprime a x"
using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)

lemma coprime_dvd_mult_left_iff:
"a dvd b * c ⟷ a dvd b" if "coprime a c"
proof
assume "a dvd b"
then show "a dvd b * c"
by simp
next
assume "a dvd b * c"
show "a dvd b"
proof (cases "b = 0")
case True
then show ?thesis
by simp
next
case False
then have unit: "is_unit (unit_factor b)"
by simp
from ‹coprime a c›
have "gcd (b * a) (b * c) * unit_factor b = b"
by (subst gcd_mult_left) (simp add: ac_simps)
moreover from ‹a dvd b * c›
have "a dvd gcd (b * a) (b * c) * unit_factor b"
ultimately show ?thesis
by simp
qed
qed

lemma coprime_dvd_mult_right_iff:
"a dvd c * b ⟷ a dvd b" if "coprime a c"
using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)

lemma divides_mult:
"a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
proof -
from ‹b dvd c› obtain b' where "c = b * b'" ..
with ‹a dvd c› have "a dvd b' * b"
with ‹coprime a b› have "a dvd b'"
then obtain a' where "b' = a * a'" ..
with ‹c = b * b'› have "c = (a * b) * a'"
then show ?thesis ..
qed

lemma div_gcd_coprime:
assumes "a ≠ 0 ∨ b ≠ 0"
shows "coprime (a div gcd a b) (b div gcd a b)"
proof -
let ?g = "gcd a b"
let ?a' = "a div ?g"
let ?b' = "b div ?g"
let ?g' = "gcd ?a' ?b'"
have dvdg: "?g dvd a" "?g dvd b"
by simp_all
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
by simp_all
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
by (auto simp: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
have "?g ≠ 0"
using assms by simp
moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
ultimately show ?thesis
using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
by simp (simp only: coprime_iff_gcd_eq_1)
qed

lemma gcd_coprime:
assumes c: "gcd a b ≠ 0"
and a: "a = a' * gcd a b"
and b: "b = b' * gcd a b"
shows "coprime a' b'"
proof -
from c have "a ≠ 0 ∨ b ≠ 0"
by simp
with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
also from assms have "a div gcd a b = a'"
using dvd_div_eq_mult gcd_dvd1 by blast
also from assms have "b div gcd a b = b'"
using dvd_div_eq_mult gcd_dvd1 by blast
finally show ?thesis .
qed

lemma gcd_coprime_exists:
assumes "gcd a b ≠ 0"
shows "∃a' b'. a = a' * gcd a b ∧ b = b' * gcd a b ∧ coprime a' b'"
proof -
have "coprime (a div gcd a b) (b div gcd a b)"
using assms div_gcd_coprime by auto
then show ?thesis
by force
qed

lemma pow_divides_pow_iff [simp]:
"a ^ n dvd b ^ n ⟷ a dvd b" if "n > 0"
proof (cases "gcd a b = 0")
case True
then show ?thesis
by simp
next
case False
show ?thesis
proof
let ?d = "gcd a b"
from ‹n > 0› obtain m where m: "n = Suc m"
by (cases n) simp_all
from False have zn: "?d ^ n ≠ 0"
by (rule power_not_zero)
from gcd_coprime_exists [OF False]
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
by blast
assume "a ^ n dvd b ^ n"
then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
then have "?d^n * a'^n dvd ?d^n * b'^n"
by (simp only: power_mult_distrib ac_simps)
with zn have "a' ^ n dvd b' ^ n"
by simp
then have "a' dvd b' ^ n"
using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
then have "a' dvd b' ^ m * b'"
moreover have "coprime a' (b' ^ n)"
using ‹coprime a' b'› by simp
then have "a' dvd b'"
using ‹a' dvd b' ^ n› coprime_dvd_mult_left_iff dvd_mult by blast
then have "a' * ?d dvd b' * ?d"
by (rule mult_dvd_mono) simp
with ab'(1,2) show "a dvd b"
by simp
next
assume "a dvd b"
with ‹n > 0› show "a ^ n dvd b ^ n"
by (induction rule: nat_induct_non_zero)
qed
qed

lemma coprime_crossproduct:
fixes a b c d :: 'a
assumes "coprime a d" and "coprime b c"
shows "normalize a * normalize c = normalize b * normalize d ⟷
normalize a = normalize b ∧ normalize c = normalize d"
(is "?lhs ⟷ ?rhs")
proof
assume ?rhs
then show ?lhs by simp
next
assume ?lhs
from ‹?lhs› have "normalize a dvd normalize b * normalize d"
by (auto intro: dvdI dest: sym)
with ‹coprime a d› have "a dvd b"
by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
from ‹?lhs› have "normalize b dvd normalize a * normalize c"
by (auto intro: dvdI dest: sym)
with ‹coprime b c› have "b dvd a"
by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
from ‹?lhs› have "normalize c dvd normalize d * normalize b"
by (auto intro: dvdI dest: sym simp add: mult.commute)
with ‹coprime b c› have "c dvd d"
by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
from ‹?lhs› have "normalize d dvd normalize c * normalize a"
by (auto intro: dvdI dest: sym simp add: mult.commute)
with ‹coprime a d› have "d dvd c"
by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
from ‹a dvd b› ‹b dvd a› have "normalize a = normalize b"
by (rule associatedI)
moreover from ‹c dvd d› ‹d dvd c› have "normalize c = normalize d"
by (rule associatedI)
ultimately show ?rhs ..
qed

lemma gcd_mult_left_left_cancel:
"gcd (c * a) b = gcd a b" if "coprime b c"
proof -
have "coprime (gcd b (a * c)) c"
by (rule coprimeI) (auto intro: that coprime_common_divisor)
then have "gcd b (a * c) dvd a"
using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
by simp
then show ?thesis
by (auto intro: associated_eqI simp add: ac_simps)
qed

lemma gcd_mult_left_right_cancel:
"gcd (a * c) b = gcd a b" if "coprime b c"
using that gcd_mult_left_left_cancel [of b c a]

lemma gcd_mult_right_left_cancel:
"gcd a (c * b) = gcd a b" if "coprime a c"
using that gcd_mult_left_left_cancel [of a c b]

lemma gcd_mult_right_right_cancel:
"gcd a (b * c) = gcd a b" if "coprime a c"
using that gcd_mult_right_left_cancel [of a c b]

lemma gcd_exp_weak:
"gcd (a ^ n) (b ^ n) = normalize (gcd a b ^ n)"
proof (cases "a = 0 ∧ b = 0 ∨ n = 0")
case True
then show ?thesis
by (cases n) simp_all
next
case False
then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
by (auto intro: div_gcd_coprime)
then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
by simp
then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
by simp
then have "normalize (gcd a b ^ n) = normalize (gcd a b ^ n * …)"
by simp
also have "… = gcd (gcd a b ^ n * (a div gcd a b) ^ n) (gcd a b ^ n * (b div gcd a b) ^ n)"
by (rule gcd_mult_left [symmetric])
also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
by (simp add: ac_simps div_power dvd_power_same)
also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
by (simp add: ac_simps div_power dvd_power_same)
finally show ?thesis by simp
qed

lemma division_decomp:
assumes "a dvd b * c"
shows "∃b' c'. a = b' * c' ∧ b' dvd b ∧ c' dvd c"
proof (cases "gcd a b = 0")
case True
then have "a = 0 ∧ b = 0"
by simp
then have "a = 0 * c ∧ 0 dvd b ∧ c dvd c"
by simp
then show ?thesis by blast
next
case False
let ?d = "gcd a b"
from gcd_coprime_exists [OF False]
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
by blast
from ab'(1) have "a' dvd a" ..
with assms have "a' dvd b * c"
using dvd_trans [of a' a "b * c"] by simp
from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
by simp
then have "?d * a' dvd ?d * (b' * c)"
with ‹?d ≠ 0› have "a' dvd b' * c"
by simp
then have "a' dvd c"
using ‹coprime a' b'› by (simp add: coprime_dvd_mult_right_iff)
with ab'(1) have "a = ?d * a' ∧ ?d dvd b ∧ a' dvd c"
then show ?thesis by blast
qed

lemma lcm_coprime: "coprime a b ⟹ lcm a b = normalize (a * b)"
by (subst lcm_gcd) simp

end

context ring_gcd
begin

lemma coprime_minus_left_iff [simp]:
"coprime (- a) b ⟷ coprime a b"
by (rule; rule coprimeI) (auto intro: coprime_common_divisor)

lemma coprime_minus_right_iff [simp]:
"coprime a (- b) ⟷ coprime a b"
using coprime_minus_left_iff [of b a] by (simp add: ac_simps)

lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
using coprime_add_one_right [of "a - 1"] by simp

lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
using coprime_diff_one_left [of a] by (simp add: ac_simps)

end

context semiring_Gcd
begin

lemma Lcm_coprime:
assumes "finite A"
and "A ≠ {}"
and "⋀a b. a ∈ A ⟹ b ∈ A ⟹ a ≠ b ⟹ coprime a b"
shows "Lcm A = normalize (∏A)"
using assms
proof (induct rule: finite_ne_induct)
case singleton
then show ?case by simp
next
case (insert a A)
have "Lcm (insert a A) = lcm a (Lcm A)"
by simp
also from insert have "Lcm A = normalize (∏A)"
by blast
also have "lcm a … = lcm a (∏A)"
by (cases "∏A = 0") (simp_all add: lcm_div_unit2)
also from insert have "coprime a (∏A)"
by (subst coprime_commute, intro prod_coprime_left) auto
with insert have "lcm a (∏A) = normalize (∏(insert a A))"
finally show ?case .
qed

lemma Lcm_coprime':
"card A ≠ 0 ⟹
(⋀a b. a ∈ A ⟹ b ∈ A ⟹ a ≠ b ⟹ coprime a b) ⟹
Lcm A = normalize (∏A)"
by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)

end

text ‹And some consequences: cancellation modulo @{term m}›
lemma mult_mod_cancel_right:
fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n"
shows "a mod m = b mod m"
proof -
have "m dvd (a*n - b*n)"
using eq mod_eq_dvd_iff by blast
then have "m dvd a-b"
by (metis ‹coprime m n› coprime_dvd_mult_left_iff left_diff_distrib')
then show ?thesis
using mod_eq_dvd_iff by blast
qed

lemma mult_mod_cancel_left:
fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
assumes "(n * a) mod m = (n * b) mod m" and "coprime m n"
shows "a mod m = b mod m"
by (metis assms mult.commute mult_mod_cancel_right)

subsection ‹GCD and LCM for multiplicative normalisation functions›

class semiring_gcd_mult_normalize = semiring_gcd + normalization_semidom_multiplicative
begin

lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
by (simp add: gcd_mult_left normalize_mult mult.assoc [symmetric])

lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
using mult_gcd_left [of c a b] by (simp add: ac_simps)

lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
by (subst gcd_mult_left) (simp_all add: normalize_mult)

lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
proof-
have "normalize k * gcd a b = gcd (k * a) (k * b)"
then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
by simp
then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
by (simp only: ac_simps)
then show ?thesis
by simp
qed

lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
by (simp add: lcm_gcd normalize_mult dvd_normalize_div)

lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
using gcd_mult_lcm [of a b] by (simp add: ac_simps)

lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
by (simp add: lcm_mult_left mult.assoc [symmetric] normalize_mult)

lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
using mult_lcm_left [of c a b] by (simp add: ac_simps)

lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
by (simp add: lcm_gcd dvd_normalize_div normalize_mult)

lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
by (subst lcm_mult_left) (simp add: normalize_mult)

lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
proof-
have "normalize k * lcm a b = lcm (k * a) (k * b)"