(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
Thomas M. Rasmussen, Jeremy Avigad, 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.
Jeremy Avigad combined all of these, made everything uniform for the
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 Main
begin
subsection \Abstract GCD and LCM\
class gcd = zero + one + dvd +
fixes gcd :: "'a \ 'a \ 'a"
and lcm :: "'a \ 'a \ 'a"
begin
abbreviation coprime :: "'a \ 'a \ bool"
where "coprime x y \ gcd x y = 1"
end
class Gcd = gcd +
fixes Gcd :: "'a set \ 'a"
and Lcm :: "'a set \ '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 [simp]:
"is_unit (gcd a b) \ coprime a b"
by (cases "a = 0 \ b = 0") (auto simp add: 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
lemma gcd_self [simp]:
"gcd a a = normalize a"
proof -
have "a dvd gcd a a"
by (rule gcd_greatest) simp_all
then show ?thesis
by (auto intro: associated_eqI)
qed
lemma gcd_left_idem [simp]:
"gcd a (gcd a b) = gcd a b"
by (auto intro: associated_eqI)
lemma gcd_right_idem [simp]:
"gcd (gcd a b) b = gcd a b"
unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
lemma coprime_1_left [simp]:
"coprime 1 a"
by (rule associated_eqI) simp_all
lemma coprime_1_right [simp]:
"coprime a 1"
using coprime_1_left [of a] 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 calculation 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) = gcd b a * normalize c"
using gcd_mult_left [of c a b] by (simp add: ac_simps)
lemma mult_gcd_left:
"c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
by (simp add: gcd_mult_left 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 dvd_lcm1 [iff]:
"a dvd lcm a b"
proof -
have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
by (simp add: lcm_gcd normalize_mult div_mult_swap)
then show ?thesis
by (simp add: lcm_gcd)
qed
lemma dvd_lcm2 [iff]:
"b dvd lcm a b"
proof -
have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
then show ?thesis
by (simp add: lcm_gcd)
qed
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 U: "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 then have "a \ 0 \ b \ 0" by simp
with \c \ 0\ assms have "a * b dvd a * c" "a * b dvd c * b"
by (simp_all add: mult_dvd_mono)
then have "normalize (a * b) dvd gcd (a * c) (b * c)"
by (auto intro: gcd_greatest simp add: ac_simps)
then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
using U by (simp add: dvd_mult_unit_iff)
then have "normalize (a * b) dvd gcd a b * c"
by (simp add: mult_gcd_right [of a b c])
then have "normalize (a * b) div gcd a b dvd c"
using False by (simp add: div_dvd_iff_mult ac_simps)
then show ?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
then have "0 dvd normalize (a * b) div gcd a b"
by (simp add: lcm_gcd)
then have "0 * gcd a b dvd normalize (a * b)"
using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
then have "normalize (a * b) = 0"
by simp
then show ?Q by simp
next
assume ?Q then show ?P by auto
qed
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)"
by (simp add: unit_factor_gcd dvd_unit_factor_div 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
lemma lcm_self [simp]:
"lcm a a = normalize a"
proof -
have "lcm a a dvd a"
by (rule lcm_least) simp_all
then show ?thesis
by (auto intro: associated_eqI)
qed
lemma lcm_left_idem [simp]:
"lcm a (lcm a b) = lcm a b"
by (auto intro: associated_eqI)
lemma lcm_right_idem [simp]:
"lcm (lcm a b) b = lcm a b"
unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
lemma gcd_mult_lcm [simp]:
"gcd a b * lcm a b = normalize a * normalize b"
by (simp add: lcm_gcd normalize_mult)
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 gcd_lcm:
assumes "a \ 0" and "b \ 0"
shows "gcd a b = normalize (a * b) div lcm a b"
proof -
from assms have "lcm a b \ 0"
by (simp add: lcm_eq_0_iff)
have "gcd a b * lcm a b = normalize a * normalize b" by simp
then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
by (simp_all add: normalize_mult)
with \lcm a b \ 0\ show ?thesis
using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
qed
lemma lcm_1_left [simp]:
"lcm 1 a = normalize a"
by (simp add: lcm_gcd)
lemma lcm_1_right [simp]:
"lcm a 1 = normalize a"
by (simp add: lcm_gcd)
lemma lcm_mult_left:
"lcm (c * a) (c * b) = normalize c * lcm a b"
by (cases "c = 0")
(simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
lemma lcm_mult_right:
"lcm (a * c) (b * c) = lcm b a * normalize c"
using lcm_mult_left [of c 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])
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)
end
class ring_gcd = comm_ring_1 + semiring_gcd
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 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_Gcd:
"unit_factor (Gcd A) = (if \a\A. a = 0 then 0 else 1)"
proof (cases "Gcd A = 0")
case True then show ?thesis by auto
next
case False
from unit_factor_mult_normalize
have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
with False have "unit_factor (Gcd A) = 1" by simp
with False show ?thesis by auto
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 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 add: lcm_eq_0_iff)
qed
lemma dvd_Gcd: \ \FIXME remove\
"\b\A. a dvd b \ a dvd Gcd A"
by (blast intro: Gcd_greatest)
lemma Gcd_set [code_unfold]:
"Gcd (set as) = foldr gcd as 0"
by (induct as) simp_all
lemma Lcm_set [code_unfold]:
"Lcm (set as) = foldr lcm as 1"
by (induct as) simp_all
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 Lcm_eqI:
assumes "normalize a = a"
assumes "\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)
end
subsection \GCD and LCM on @{typ nat} and @{typ int}\
instantiation nat :: gcd
begin
fun gcd_nat :: "nat \ nat \ nat"
where "gcd_nat x y =
(if y = 0 then x else gcd y (x mod y))"
definition lcm_nat :: "nat \ nat \ nat"
where
"lcm_nat x y = x * y div (gcd x y)"
instance proof qed
end
instantiation int :: gcd
begin
definition gcd_int :: "int \ int \ int"
where "gcd_int x y = int (gcd (nat \x\) (nat \y\))"
definition lcm_int :: "int \ int \ int"
where "lcm_int x y = int (lcm (nat \x\) (nat \y\))"
instance ..
end
text \Transfer setup\
lemma transfer_nat_int_gcd:
"(x::int) >= 0 \ y >= 0 \ gcd (nat x) (nat y) = nat (gcd x y)"
"(x::int) >= 0 \ y >= 0 \ lcm (nat x) (nat y) = nat (lcm x y)"
unfolding gcd_int_def lcm_int_def
by auto
lemma transfer_nat_int_gcd_closures:
"x >= (0::int) \ y >= 0 \ gcd x y >= 0"
"x >= (0::int) \ y >= 0 \ lcm x y >= 0"
by (auto simp add: gcd_int_def lcm_int_def)
declare transfer_morphism_nat_int[transfer add return:
transfer_nat_int_gcd transfer_nat_int_gcd_closures]
lemma transfer_int_nat_gcd:
"gcd (int x) (int y) = int (gcd x y)"
"lcm (int x) (int y) = int (lcm x y)"
by (unfold gcd_int_def lcm_int_def, auto)
lemma transfer_int_nat_gcd_closures:
"is_nat x \ is_nat y \ gcd x y >= 0"
"is_nat x \ is_nat y \ lcm x y >= 0"
by (auto simp add: gcd_int_def lcm_int_def)
declare transfer_morphism_int_nat[transfer add return:
transfer_int_nat_gcd transfer_int_nat_gcd_closures]
lemma gcd_nat_induct:
fixes m n :: nat
assumes "\m. P m 0"
and "\m n. 0 < n \ P n (m mod n) \ P m n"
shows "P m n"
apply (rule gcd_nat.induct)
apply (case_tac "y = 0")
using assms apply simp_all
done
(* specific to int *)
lemma gcd_eq_int_iff:
"gcd k l = int n \ gcd (nat \k\) (nat \l\) = n"
by (simp add: gcd_int_def)
lemma lcm_eq_int_iff:
"lcm k l = int n \ lcm (nat \k\) (nat \l\) = n"
by (simp add: lcm_int_def)
lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
by (simp add: gcd_int_def)
lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
by (simp add: gcd_int_def)
lemma abs_gcd_int[simp]: "\gcd (x::int) y\ = gcd x y"
by(simp add: gcd_int_def)
lemma gcd_abs_int: "gcd (x::int) y = gcd \x\ \y\"
by (simp add: gcd_int_def)
lemma gcd_abs1_int[simp]: "gcd \x\ (y::int) = gcd x y"
by (metis abs_idempotent gcd_abs_int)
lemma gcd_abs2_int[simp]: "gcd x \y::int\ = gcd x y"
by (metis abs_idempotent gcd_abs_int)
lemma gcd_cases_int:
fixes x :: int and y
assumes "x >= 0 \ y >= 0 \ P (gcd x y)"
and "x >= 0 \ y <= 0 \ P (gcd x (-y))"
and "x <= 0 \ y >= 0 \ P (gcd (-x) y)"
and "x <= 0 \ y <= 0 \ P (gcd (-x) (-y))"
shows "P (gcd x y)"
by (insert assms, auto, arith)
lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
by (simp add: gcd_int_def)
lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
by (simp add: lcm_int_def)
lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
by (simp add: lcm_int_def)
lemma lcm_abs_int: "lcm (x::int) y = lcm \x\ \y\"
by (simp add: lcm_int_def)
lemma abs_lcm_int [simp]: "\lcm i j::int\ = lcm i j"
by (simp add:lcm_int_def)
lemma lcm_abs1_int[simp]: "lcm \x\ (y::int) = lcm x y"
by (metis abs_idempotent lcm_int_def)
lemma lcm_abs2_int[simp]: "lcm x \y::int\ = lcm x y"
by (metis abs_idempotent lcm_int_def)
lemma lcm_cases_int:
fixes x :: int and y
assumes "x >= 0 \ y >= 0 \ P (lcm x y)"
and "x >= 0 \ y <= 0 \ P (lcm x (-y))"
and "x <= 0 \ y >= 0 \ P (lcm (-x) y)"
and "x <= 0 \ y <= 0 \ P (lcm (-x) (-y))"
shows "P (lcm x y)"
using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
by (simp add: lcm_int_def)
lemma gcd_0_nat: "gcd (x::nat) 0 = x"
by simp
lemma gcd_0_int [simp]: "gcd (x::int) 0 = \x\"
by (unfold gcd_int_def, auto)
lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
by simp
lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \x\"
by (unfold gcd_int_def, auto)
lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
by (case_tac "y = 0", auto)
(* weaker, but useful for the simplifier *)
lemma gcd_non_0_nat: "y \ (0::nat) \ gcd (x::nat) y = gcd y (x mod y)"
by simp
lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
by simp
lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
by simp
lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
by (simp add: gcd_int_def)
lemma gcd_idem_nat: "gcd (x::nat) x = x"
by simp
lemma gcd_idem_int: "gcd (x::int) x = \x\"
by (auto simp add: gcd_int_def)
declare gcd_nat.simps [simp del]
text \
\medskip @{term "gcd m n"} divides \m\ and \n\. The
conjunctions don't seem provable separately.
\
instance nat :: semiring_gcd
proof
fix m n :: nat
show "gcd m n dvd m" and "gcd m n dvd n"
proof (induct m n rule: gcd_nat_induct)
fix m n :: nat
assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
then have "gcd n (m mod n) dvd m"
by (rule dvd_mod_imp_dvd)
moreover assume "0 < n"
ultimately show "gcd m n dvd m"
by (simp add: gcd_non_0_nat)
qed (simp_all add: gcd_0_nat gcd_non_0_nat)
next
fix m n k :: nat
assume "k dvd m" and "k dvd n"
then show "k dvd gcd m n"
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
qed (simp_all add: lcm_nat_def)
instance int :: ring_gcd
by standard
(simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
lemma gcd_le1_nat [simp]: "a \ 0 \ gcd (a::nat) b \ a"
by (rule dvd_imp_le, auto)
lemma gcd_le2_nat [simp]: "b \ 0 \ gcd (a::nat) b \ b"
by (rule dvd_imp_le, auto)
lemma gcd_le1_int [simp]: "a > 0 \ gcd (a::int) b \ a"
by (rule zdvd_imp_le, auto)
lemma gcd_le2_int [simp]: "b > 0 \ gcd (a::int) b \ b"
by (rule zdvd_imp_le, auto)
lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
by (insert gcd_eq_0_iff [of m n], arith)
lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
lemma gcd_unique_nat: "(d::nat) dvd a \ d dvd b \
(\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b"
apply auto
apply (rule dvd_antisym)
apply (erule (1) gcd_greatest)
apply auto
done
lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \ d dvd b \
(\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b"
apply (case_tac "d = 0")
apply simp
apply (rule iffI)
apply (rule zdvd_antisym_nonneg)
apply (auto intro: gcd_greatest)
done
interpretation gcd_nat:
semilattice_neutr_order gcd "0::nat" Rings.dvd "\m n. m dvd n \ m \ n"
by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \ gcd (x::int) y = \x\"
by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \ gcd (x::int) y = \y\"
by (metis gcd_proj1_if_dvd_int gcd.commute)
text \
\medskip Multiplication laws
\
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
\ \@{cite \page 27\ davenport92}\
apply (induct m n rule: gcd_nat_induct)
apply simp
apply (case_tac "k = 0")
apply (simp_all add: gcd_non_0_nat)
done
lemma gcd_mult_distrib_int: "\k::int\ * gcd m n = gcd (k * m) (k * n)"
apply (subst (1 2) gcd_abs_int)
apply (subst (1 2) abs_mult)
apply (rule gcd_mult_distrib_nat [transferred])
apply auto
done
context semiring_gcd
begin
lemma coprime_dvd_mult:
assumes "coprime a b" and "a dvd c * b"
shows "a dvd c"
proof (cases "c = 0")
case True then show ?thesis by simp
next
case False
then have unit: "is_unit (unit_factor c)" by simp
from \coprime a b\ mult_gcd_left [of c a b]
have "gcd (c * a) (c * b) * unit_factor c = c"
by (simp add: ac_simps)
moreover from \