Theory GCD
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 = ❙⊥"
by (simp add: eq_fold)
lemma set_eq_fold [code]:
"F (set xs) = fold f xs ❙⊤"
by (simp add: eq_fold fold_set_fold)
lemma empty [simp]:
"F {} = ❙⊤"
by (simp add: eq_fold)
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)
(simp_all add: ac_simps)
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"
by (simp add: unit_eq_div2)
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
by (simp add: normalize_mult)
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"
by (simp add: lcm_gcd dvd_normalize_div)
lemma lcm_0_left [simp]: "lcm 0 a = 0"
by (simp add: lcm_gcd)
lemma lcm_0_right [simp]: "lcm a 0 = 0"
by (simp add: lcm_gcd)
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
by (simp add: normalize_mult)
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"
by (simp add: unit_eq_div2)
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"
by (simp add: gcd_dvdI1 gcd_dvdI2)
lemma lcm_mono: "a dvd c ⟹ b dvd d ⟹ lcm a b dvd lcm c d"
by (simp add: dvd_lcmI1 dvd_lcmI2)
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"
by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
using gcd_add1 [of n m] by (simp add: ac_simps)
lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
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"
by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp)
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)"
by (simp add: Gcd_Lcm unit_factor_Lcm)
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})"
by (simp add: Lcm_Un [symmetric])
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)"
by (simp add: dvd_Gcd_fin_iff)
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)"
by (simp add: Lcm_fin_dvd_iff)
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)"
by (simp add: finite_image_iff)
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"
by (simp add: Gcd_fin.set_eq_fold [symmetric])
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"
by (simp add: Lcm_fin.set_eq_fold [symmetric])
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
by (simp add: t_def)
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"
by rule (simp_all add: gcd_eq_1_imp_coprime)
lemma is_unit_gcd [simp]:
"is_unit (gcd a b) ⟷ coprime a b"
by (simp add: coprime_iff_gcd_eq_1)
lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
by (simp add: gcd_eq_1_imp_coprime ac_simps)
lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
using coprime_add_one_left [of a] by (simp add: ac_simps)
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"
by (simp add: d is_unit_mult_iff)
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"
by (simp add: dvd_mult_unit_iff unit)
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"
by (simp add: ac_simps)
with ‹coprime a b› have "a dvd b'"
by (simp add: coprime_dvd_mult_left_iff)
then obtain a' where "b' = a * a'" ..
with ‹c = b * b'› have "c = (a * b) * a'"
by (simp add: ac_simps)
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"
by (simp add: ab'(1,2)[symmetric])
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'"
by (simp add: m ac_simps)
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)
(simp_all add: mult_dvd_mono)
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]
by (simp add: ac_simps)
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]
by (simp add: ac_simps)
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]
by (simp add: ac_simps)
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)"
by (simp add: mult_ac)
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"
by (simp add: ac_simps)
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))"
by (simp add: lcm_coprime)
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)"
by (simp add: gcd_mult_distrib')
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)"
by (simp add: lcm_mult_distrib')
then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
by simp
then have "normalize k * unit_factor k * lcm a b = lcm (k * a) (k * b)</