Theory HOL-Number_Theory.Cong
section ‹Congruence›
theory Cong
imports "HOL-Computational_Algebra.Primes"
begin
subsection ‹Generic congruences›
context unique_euclidean_semiring
begin
definition cong :: "'a ⇒ 'a ⇒ 'a ⇒ bool" (‹(1[_ = _] '(' mod _'))›)
where "cong b c a ⟷ b mod a = c mod a"
abbreviation notcong :: "'a ⇒ 'a ⇒ 'a ⇒ bool" (‹(1[_ ≠ _] '(' mod _'))›)
where "notcong b c a ≡ ¬ cong b c a"
lemma cong_refl [simp]:
"[b = b] (mod a)"
by (simp add: cong_def)
lemma cong_sym:
"[b = c] (mod a) ⟹ [c = b] (mod a)"
by (simp add: cong_def)
lemma cong_sym_eq:
"[b = c] (mod a) ⟷ [c = b] (mod a)"
by (auto simp add: cong_def)
lemma cong_trans [trans]:
"[b = c] (mod a) ⟹ [c = d] (mod a) ⟹ [b = d] (mod a)"
by (simp add: cong_def)
lemma cong_mult_self_right:
"[b * a = 0] (mod a)"
by (simp add: cong_def)
lemma cong_mult_self_left:
"[a * b = 0] (mod a)"
by (simp add: cong_def)
lemma cong_mod_left [simp]:
"[b mod a = c] (mod a) ⟷ [b = c] (mod a)"
by (simp add: cong_def)
lemma cong_mod_right [simp]:
"[b = c mod a] (mod a) ⟷ [b = c] (mod a)"
by (simp add: cong_def)
lemma cong_0 [simp, presburger]:
"[b = c] (mod 0) ⟷ b = c"
by (simp add: cong_def)
lemma cong_1 [simp, presburger]:
"[b = c] (mod 1)"
by (simp add: cong_def)
lemma cong_dvd_iff:
"a dvd b ⟷ a dvd c" if "[b = c] (mod a)"
using that by (auto simp: cong_def dvd_eq_mod_eq_0)
lemma cong_0_iff: "[b = 0] (mod a) ⟷ a dvd b"
by (simp add: cong_def dvd_eq_mod_eq_0)
lemma cong_add:
"[b = c] (mod a) ⟹ [d = e] (mod a) ⟹ [b + d = c + e] (mod a)"
by (auto simp add: cong_def intro: mod_add_cong)
lemma cong_mult:
"[b = c] (mod a) ⟹ [d = e] (mod a) ⟹ [b * d = c * e] (mod a)"
by (auto simp add: cong_def intro: mod_mult_cong)
lemma cong_scalar_right:
"[b = c] (mod a) ⟹ [b * d = c * d] (mod a)"
by (simp add: cong_mult)
lemma cong_scalar_left:
"[b = c] (mod a) ⟹ [d * b = d * c] (mod a)"
by (simp add: cong_mult)
lemma cong_pow:
"[b = c] (mod a) ⟹ [b ^ n = c ^ n] (mod a)"
by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a])
lemma cong_sum:
"[sum f A = sum g A] (mod a)" if "⋀x. x ∈ A ⟹ [f x = g x] (mod a)"
using that by (induct A rule: infinite_finite_induct) (auto intro: cong_add)
lemma cong_prod:
"[prod f A = prod g A] (mod a)" if "(⋀x. x ∈ A ⟹ [f x = g x] (mod a))"
using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult)
lemma mod_mult_cong_right:
"[c mod (a * b) = d] (mod a) ⟷ [c = d] (mod a)"
by (simp add: cong_def mod_mod_cancel mod_add_left_eq)
lemma mod_mult_cong_left:
"[c mod (b * a) = d] (mod a) ⟷ [c = d] (mod a)"
using mod_mult_cong_right [of c a b d] by (simp add: ac_simps)
end
context unique_euclidean_ring
begin
lemma cong_diff:
"[b = c] (mod a) ⟹ [d = e] (mod a) ⟹ [b - d = c - e] (mod a)"
by (auto simp add: cong_def intro: mod_diff_cong)
lemma cong_diff_iff_cong_0:
"[b - c = 0] (mod a) ⟷ [b = c] (mod a)" (is "?P ⟷ ?Q")
proof
assume ?P
then have "[b - c + c = 0 + c] (mod a)"
by (rule cong_add) simp
then show ?Q
by simp
next
assume ?Q
with cong_diff [of b c a c c] show ?P
by simp
qed
lemma cong_minus_minus_iff:
"[- b = - c] (mod a) ⟷ [b = c] (mod a)"
using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
by (simp add: cong_0_iff dvd_diff_commute)
lemma cong_modulus_minus_iff [iff]:
"[b = c] (mod - a) ⟷ [b = c] (mod a)"
using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]
by (simp add: cong_0_iff)
lemma cong_iff_dvd_diff:
"[a = b] (mod m) ⟷ m dvd (a - b)"
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
lemma cong_iff_lin:
"[a = b] (mod m) ⟷ (∃k. b = a + m * k)" (is "?P ⟷ ?Q")
proof -
have "?P ⟷ m dvd b - a"
by (simp add: cong_iff_dvd_diff dvd_diff_commute)
also have "… ⟷ ?Q"
by (auto simp add: algebra_simps elim!: dvdE)
finally show ?thesis
by simp
qed
lemma cong_add_lcancel:
"[a + x = a + y] (mod n) ⟷ [x = y] (mod n)"
by (simp add: cong_iff_lin algebra_simps)
lemma cong_add_rcancel:
"[x + a = y + a] (mod n) ⟷ [x = y] (mod n)"
by (simp add: cong_iff_lin algebra_simps)
lemma cong_add_lcancel_0:
"[a + x = a] (mod n) ⟷ [x = 0] (mod n)"
using cong_add_lcancel [of a x 0 n] by simp
lemma cong_add_rcancel_0:
"[x + a = a] (mod n) ⟷ [x = 0] (mod n)"
using cong_add_rcancel [of x a 0 n] by simp
lemma cong_dvd_modulus:
"[x = y] (mod n)" if "[x = y] (mod m)" and "n dvd m"
using that by (auto intro: dvd_trans simp add: cong_iff_dvd_diff)
lemma cong_modulus_mult:
"[x = y] (mod m)" if "[x = y] (mod m * n)"
using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left)
end
lemma cong_abs [simp]:
"[x = y] (mod ¦m¦) ⟷ [x = y] (mod m)"
for x y :: "'a :: {unique_euclidean_ring, linordered_idom}"
by (simp add: cong_iff_dvd_diff)
lemma cong_square:
"prime p ⟹ 0 < a ⟹ [a * a = 1] (mod p) ⟹ [a = 1] (mod p) ∨ [a = - 1] (mod p)"
for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}"
by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest: prime_dvd_multD)
lemma cong_mult_rcancel:
"[a * k = b * k] (mod m) ⟷ [a = b] (mod m)"
if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
using that by (auto simp add: cong_iff_dvd_diff left_diff_distrib [symmetric] ac_simps coprime_dvd_mult_right_iff)
lemma cong_mult_lcancel:
"[k * a = k * b] (mod m) = [a = b] (mod m)"
if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
using that cong_mult_rcancel [of k m a b] by (simp add: ac_simps)
lemma coprime_cong_mult:
"[a = b] (mod m) ⟹ [a = b] (mod n) ⟹ coprime m n ⟹ [a = b] (mod m * n)"
for a b :: "'a :: {unique_euclidean_ring, semiring_gcd}"
by (simp add: cong_iff_dvd_diff divides_mult)
lemma cong_gcd_eq:
"gcd a m = gcd b m" if "[a = b] (mod m)"
for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
proof (cases "m = 0")
case True
with that show ?thesis
by simp
next
case False
moreover have "gcd (a mod m) m = gcd (b mod m) m"
using that by (simp add: cong_def)
ultimately show ?thesis
by simp
qed
lemma cong_imp_coprime:
"[a = b] (mod m) ⟹ coprime a m ⟹ coprime b m"
for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq)
lemma cong_cong_prod_coprime:
"[x = y] (mod (∏i∈A. m i))" if
"(∀i∈A. [x = y] (mod m i))"
"(∀i∈A. (∀j∈A. i ≠ j ⟶ coprime (m i) (m j)))"
for x y :: "'a :: {unique_euclidean_ring, semiring_gcd}"
using that by (induct A rule: infinite_finite_induct)
(auto intro!: coprime_cong_mult prod_coprime_right)
subsection ‹Congruences on \<^typ>‹nat› and \<^typ>‹int››
lemma cong_int_iff:
"[int m = int q] (mod int n) ⟷ [m = q] (mod n)"
by (simp add: cong_def of_nat_mod [symmetric])
lemma cong_Suc_0 [simp, presburger]:
"[m = n] (mod Suc 0)"
using cong_1 [of m n] by simp
lemma cong_diff_nat:
"[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
and "a ≥ c" "b ≥ d" for a b c d m :: nat
proof -
have "[c + (a - c) = d + (b - d)] (mod m)"
using that by simp
with ‹[c = d] (mod m)› have "[c + (a - c) = c + (b - d)] (mod m)"
using mod_add_cong by (auto simp add: cong_def) fastforce
then show ?thesis
by (simp add: cong_def nat_mod_eq_iff)
qed
lemma cong_diff_iff_cong_0_nat:
"[a - b = 0] (mod m) ⟷ [a = b] (mod m)" if "a ≥ b" for a b :: nat
using that by (simp add: cong_0_iff) (simp add: cong_def mod_eq_dvd_iff_nat)
lemma cong_diff_iff_cong_0_nat':
"[nat ¦int a - int b¦ = 0] (mod m) ⟷ [a = b] (mod m)"
proof (cases "b ≤ a")
case True
then show ?thesis
by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m])
next
case False
then have "a ≤ b"
by simp
then show ?thesis
by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m])
(auto simp add: cong_def)
qed
lemma cong_altdef_nat:
"a ≥ b ⟹ [a = b] (mod m) ⟷ m dvd (a - b)"
for a b :: nat
by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
lemma cong_altdef_nat':
"[a = b] (mod m) ⟷ m dvd nat ¦int a - int b¦"
using cong_diff_iff_cong_0_nat' [of a b m]
by (simp only: cong_0_iff [symmetric])
lemma cong_mult_rcancel_nat:
"[a * k = b * k] (mod m) ⟷ [a = b] (mod m)"
if "coprime k m" for a k m :: nat
proof -
have "[a * k = b * k] (mod m) ⟷ m dvd nat ¦int (a * k) - int (b * k)¦"
by (simp add: cong_altdef_nat')
also have "… ⟷ m dvd nat ¦(int a - int b) * int k¦"
by (simp add: algebra_simps)
also have "… ⟷ m dvd nat ¦int a - int b¦ * k"
by (simp add: abs_mult nat_times_as_int)
also have "… ⟷ m dvd nat ¦int a - int b¦"
by (rule coprime_dvd_mult_left_iff) (use ‹coprime k m› in ‹simp add: ac_simps›)
also have "… ⟷ [a = b] (mod m)"
by (simp add: cong_altdef_nat')
finally show ?thesis .
qed
lemma cong_mult_lcancel_nat:
"[k * a = k * b] (mod m) = [a = b] (mod m)"
if "coprime k m" for a k m :: nat
using that by (simp add: cong_mult_rcancel_nat ac_simps)
lemma coprime_cong_mult_nat:
"[a = b] (mod m) ⟹ [a = b] (mod n) ⟹ coprime m n ⟹ [a = b] (mod m * n)"
for a b :: nat
by (simp add: cong_altdef_nat' divides_mult)
lemma cong_less_imp_eq_nat: "0 ≤ a ⟹ a < m ⟹ 0 ≤ b ⟹ b < m ⟹ [a = b] (mod m) ⟹ a = b"
for a b :: nat
by (auto simp add: cong_def)
lemma cong_less_imp_eq_int: "0 ≤ a ⟹ a < m ⟹ 0 ≤ b ⟹ b < m ⟹ [a = b] (mod m) ⟹ a = b"
for a b :: int
by (auto simp add: cong_def)
lemma cong_less_unique_nat: "0 < m ⟹ (∃!b. 0 ≤ b ∧ b < m ∧ [a = b] (mod m))"
for a m :: nat
by (auto simp: cong_def) (metis mod_mod_trivial mod_less_divisor)
lemma cong_less_unique_int: "0 < m ⟹ (∃!b. 0 ≤ b ∧ b < m ∧ [a = b] (mod m))"
for a m :: int
by (auto simp add: cong_def) (metis mod_mod_trivial pos_mod_bound pos_mod_sign)
lemma cong_iff_lin_nat: "[a = b] (mod m) ⟷ (∃k1 k2. b + k1 * m = a + k2 * m)"
for a b :: nat
apply (auto simp add: cong_def nat_mod_eq_iff)
apply (metis mult.commute)
apply (metis mult.commute)
done
lemma cong_cong_mod_nat: "[a = b] (mod m) ⟷ [a mod m = b mod m] (mod m)"
for a b :: nat
by simp
lemma cong_cong_mod_int: "[a = b] (mod m) ⟷ [a mod m = b mod m] (mod m)"
for a b :: int
by simp
lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) ⟷ [x = y] (mod n)"
for a x y :: nat
by (simp add: cong_iff_lin_nat)
lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) ⟷ [x = y] (mod n)"
for a x y :: nat
by (simp add: cong_iff_lin_nat)
lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) ⟷ [x = 0] (mod n)"
for a x :: nat
using cong_add_lcancel_nat [of a x 0 n] by simp
lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) ⟷ [x = 0] (mod n)"
for a x :: nat
using cong_add_rcancel_nat [of x a 0 n] by simp
lemma cong_dvd_modulus_nat: "[x = y] (mod m) ⟹ n dvd m ⟹ [x = y] (mod n)"
for x y :: nat
by (auto simp add: cong_altdef_nat')
lemma cong_to_1_nat:
fixes a :: nat
assumes "[a = 1] (mod n)"
shows "n dvd (a - 1)"
proof (cases "a = 0")
case True
then show ?thesis by force
next
case False
with assms show ?thesis by (metis cong_altdef_nat leI less_one)
qed
lemma cong_0_1_nat': "[0 = Suc 0] (mod n) ⟷ n = Suc 0"
by (auto simp: cong_def)
lemma cong_0_1_nat: "[0 = 1] (mod n) ⟷ n = 1"
for n :: nat
by (auto simp: cong_def)
lemma cong_0_1_int: "[0 = 1] (mod n) ⟷ n = 1 ∨ n = - 1"
for n :: int
by (auto simp: cong_def zmult_eq_1_iff)
lemma cong_to_1'_nat: "[a = 1] (mod n) ⟷ a = 0 ∧ n = 1 ∨ (∃m. a = 1 + m * n)"
for a :: nat
by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat
dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
lemma cong_le_nat: "y ≤ x ⟹ [x = y] (mod n) ⟷ (∃q. x = q * n + y)"
for x y :: nat
by (auto simp add: cong_altdef_nat le_imp_diff_is_add)
lemma cong_solve_nat:
fixes a :: nat
shows "∃x. [a * x = gcd a n] (mod n)"
proof (cases "a = 0 ∨ n = 0")
case True
then show ?thesis
by (force simp add: cong_0_iff cong_sym)
next
case False
then show ?thesis
using bezout_nat [of a n]
by auto (metis cong_add_rcancel_0_nat cong_mult_self_left)
qed
lemma cong_solve_int:
fixes a :: int
shows "∃x. [a * x = gcd a n] (mod n)"
by (metis bezout_int cong_iff_lin mult.commute)
lemma cong_solve_dvd_nat:
fixes a :: nat
assumes "gcd a n dvd d"
shows "∃x. [a * x = d] (mod n)"
proof -
from cong_solve_nat [of a] obtain x where "[a * x = gcd a n](mod n)"
by auto
then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
using cong_scalar_left by blast
also from assms have "(d div gcd a n) * gcd a n = d"
by (rule dvd_div_mult_self)
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
by auto
finally show ?thesis
by auto
qed
lemma cong_solve_dvd_int:
fixes a::int
assumes b: "gcd a n dvd d"
shows "∃x. [a * x = d] (mod n)"
proof -
from cong_solve_int [of a] obtain x where "[a * x = gcd a n](mod n)"
by auto
then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
using cong_scalar_left by blast
also from b have "(d div gcd a n) * gcd a n = d"
by (rule dvd_div_mult_self)
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
by auto
finally show ?thesis
by auto
qed
lemma cong_solve_coprime_nat:
"∃x. [a * x = Suc 0] (mod n)" if "coprime a n"
using that cong_solve_nat [of a n] by auto
lemma cong_solve_coprime_int:
"∃x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
using that cong_solve_int [of a n] by (auto simp add: zabs_def split: if_splits)
lemma coprime_iff_invertible_nat:
"coprime a m ⟷ (∃x. [a * x = Suc 0] (mod m))" (is "?P ⟷ ?Q")
proof
assume ?P then show ?Q
by (auto dest!: cong_solve_coprime_nat)
next
assume ?Q
then obtain b where "[a * b = Suc 0] (mod m)"
by blast
with coprime_mod_left_iff [of m "a * b"] show ?P
by (cases "m = 0 ∨ m = 1")
(unfold cong_def, auto simp add: cong_def)
qed
lemma coprime_iff_invertible_int:
"coprime a m ⟷ (∃x. [a * x = 1] (mod m))" (is "?P ⟷ ?Q") for m :: int
proof
assume ?P then show ?Q
by (auto dest: cong_solve_coprime_int)
next
assume ?Q
then obtain b where "[a * b = 1] (mod m)"
by blast
with coprime_mod_left_iff [of m "a * b"] show ?P
by (cases "m = 0 ∨ m = 1")
(unfold cong_def, auto simp add: zmult_eq_1_iff)
qed
lemma coprime_iff_invertible'_nat:
assumes "m > 0"
shows "coprime a m ⟷ (∃x. 0 ≤ x ∧ x < m ∧ [a * x = Suc 0] (mod m))"
proof -
have "⋀b. ⟦0 < m; [a * b = Suc 0] (mod m)⟧ ⟹ ∃b'<m. [a * b' = Suc 0] (mod m)"
by (metis cong_def mod_less_divisor [OF assms] mod_mult_right_eq)
then show ?thesis
using assms coprime_iff_invertible_nat by auto
qed
lemma coprime_iff_invertible'_int:
fixes m :: int
assumes "m > 0"
shows "coprime a m ⟷ (∃x. 0 ≤ x ∧ x < m ∧ [a * x = 1] (mod m))"
using assms by (simp add: coprime_iff_invertible_int)
(metis assms cong_mod_left mod_mult_right_eq pos_mod_bound pos_mod_sign)
lemma cong_cong_lcm_nat: "[x = y] (mod a) ⟹ [x = y] (mod b) ⟹ [x = y] (mod lcm a b)"
for x y :: nat
by (meson cong_altdef_nat' lcm_least)
lemma cong_cong_lcm_int: "[x = y] (mod a) ⟹ [x = y] (mod b) ⟹ [x = y] (mod lcm a b)"
for x y :: int
by (auto simp add: cong_iff_dvd_diff lcm_least)
lemma cong_cong_prod_coprime_nat:
"[x = y] (mod (∏i∈A. m i))" if
"(∀i∈A. [x = y] (mod m i))"
"(∀i∈A. (∀j∈A. i ≠ j ⟶ coprime (m i) (m j)))"
for x y :: nat
using that by (induct A rule: infinite_finite_induct)
(auto intro!: coprime_cong_mult_nat prod_coprime_right)
lemma binary_chinese_remainder_nat:
fixes m1 m2 :: nat
assumes a: "coprime m1 m2"
shows "∃x. [x = u1] (mod m1) ∧ [x = u2] (mod m2)"
proof -
have "∃b1 b2. [b1 = 1] (mod m1) ∧ [b1 = 0] (mod m2) ∧ [b2 = 0] (mod m1) ∧ [b2 = 1] (mod m2)"
proof -
from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
by (simp add: ac_simps)
from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
by (simp add: cong_mult_self_left)
moreover have "[m2 * x2 = 0] (mod m2)"
by (simp add: cong_mult_self_left)
ultimately show ?thesis
using 1 2 by blast
qed
then obtain b1 b2
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
by blast
let ?x = "u1 * b1 + u2 * b2"
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
using ‹[b1 = 1] (mod m1)› ‹[b2 = 0] (mod m1)› cong_add cong_scalar_left by blast
then have "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
using ‹[b1 = 0] (mod m2)› ‹[b2 = 1] (mod m2)› cong_add cong_scalar_left by blast
then have "[?x = u2] (mod m2)"
by simp
with ‹[?x = u1] (mod m1)› show ?thesis
by blast
qed
lemma binary_chinese_remainder_int:
fixes m1 m2 :: int
assumes a: "coprime m1 m2"
shows "∃x. [x = u1] (mod m1) ∧ [x = u2] (mod m2)"
proof -
have "∃b1 b2. [b1 = 1] (mod m1) ∧ [b1 = 0] (mod m2) ∧ [b2 = 0] (mod m1) ∧ [b2 = 1] (mod m2)"
proof -
from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
by (simp add: ac_simps)
from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
by (simp add: cong_mult_self_left)
moreover have "[m2 * x2 = 0] (mod m2)"
by (simp add: cong_mult_self_left)
ultimately show ?thesis
using 1 2 by blast
qed
then obtain b1 b2
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
by blast
let ?x = "u1 * b1 + u2 * b2"
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
using ‹[b1 = 1] (mod m1)› ‹[b2 = 0] (mod m1)› cong_add cong_scalar_left by blast
then have "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
using ‹[b1 = 0] (mod m2)› ‹[b2 = 1] (mod m2)› cong_add cong_scalar_left by blast
then have "[?x = u2] (mod m2)" by simp
with ‹[?x = u1] (mod m1)› show ?thesis
by blast
qed
lemma cong_modulus_mult_nat: "[x = y] (mod m * n) ⟹ [x = y] (mod m)"
for x y :: nat
by (metis cong_def mod_mult_cong_right)
lemma cong_less_modulus_unique_nat: "[x = y] (mod m) ⟹ x < m ⟹ y < m ⟹ x = y"
for x y :: nat
by (simp add: cong_def)
lemma binary_chinese_remainder_unique_nat:
fixes m1 m2 :: nat
assumes a: "coprime m1 m2"
and nz: "m1 ≠ 0" "m2 ≠ 0"
shows "∃!x. x < m1 * m2 ∧ [x = u1] (mod m1) ∧ [x = u2] (mod m2)"
proof -
obtain y where y1: "[y = u1] (mod m1)" and y2: "[y = u2] (mod m2)"
using binary_chinese_remainder_nat [OF a] by blast
let ?x = "y mod (m1 * m2)"
from nz have less: "?x < m1 * m2"
by auto
have 1: "[?x = u1] (mod m1)"
using y1 mod_mult_cong_right by blast
have 2: "[?x = u2] (mod m2)"
using y2 mod_mult_cong_left by blast
have "z = ?x" if "z < m1 * m2" "[z = u1] (mod m1)" "[z = u2] (mod m2)" for z
proof -
have "[?x = z] (mod m1)"
by (metis "1" cong_def that(2))
moreover have "[?x = z] (mod m2)"
by (metis "2" cong_def that(3))
ultimately have "[?x = z] (mod m1 * m2)"
using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right)
with ‹z < m1 * m2› ‹?x < m1 * m2› show "z = ?x"
by (auto simp add: cong_def)
qed
with less 1 2 show ?thesis
by blast
qed
lemma chinese_remainder_nat:
fixes A :: "'a set"
and m :: "'a ⇒ nat"
and u :: "'a ⇒ nat"
assumes fin: "finite A"
and cop: "∀i ∈ A. ∀j ∈ A. i ≠ j ⟶ coprime (m i) (m j)"
shows "∃x. ∀i ∈ A. [x = u i] (mod m i)"
proof -
have "∃b. (∀i ∈ A. [b i = 1] (mod m i) ∧ [b i = 0] (mod (∏j ∈ A - {i}. m j)))"
proof (rule finite_set_choice, rule fin, rule ballI)
fix i
assume "i ∈ A"
with cop have "coprime (∏j ∈ A - {i}. m j) (m i)"
by (intro prod_coprime_left) auto
then have "∃x. [(∏j ∈ A - {i}. m j) * x = Suc 0] (mod m i)"
by (elim cong_solve_coprime_nat)
then obtain x where "[(∏j ∈ A - {i}. m j) * x = 1] (mod m i)"
by auto
moreover have "[(∏j ∈ A - {i}. m j) * x = 0] (mod (∏j ∈ A - {i}. m j))"
by (simp add: cong_0_iff)
ultimately show "∃a. [a = 1] (mod m i) ∧ [a = 0] (mod prod m (A - {i}))"
by blast
qed
then obtain b where b: "⋀i. i ∈ A ⟹ [b i = 1] (mod m i) ∧ [b i = 0] (mod (∏j ∈ A - {i}. m j))"
by blast
let ?x = "∑i∈A. (u i) * (b i)"
show ?thesis
proof (rule exI, clarify)
fix i
assume a: "i ∈ A"
show "[?x = u i] (mod m i)"
proof -
from fin a have "?x = (∑j ∈ {i}. u j * b j) + (∑j ∈ A - {i}. u j * b j)"
by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong)
then have "[?x = u i * b i + (∑j ∈ A - {i}. u j * b j)] (mod m i)"
by auto
also have "[u i * b i + (∑j ∈ A - {i}. u j * b j) =
u i * 1 + (∑j ∈ A - {i}. u j * 0)] (mod m i)"
proof (intro cong_add cong_scalar_left cong_sum)
show "[b i = 1] (mod m i)"
using a b by blast
show "[b x = 0] (mod m i)" if "x ∈ A - {i}" for x
proof -
have "x ∈ A" "x ≠ i"
using that by auto
then show ?thesis
using a b [OF ‹x ∈ A›] cong_dvd_modulus_nat fin by blast
qed
qed
finally show ?thesis
by simp
qed
qed
qed
lemma coprime_cong_prod_nat: "[x = y] (mod (∏i∈A. m i))"
if "⋀i j. ⟦i ∈ A; j ∈ A; i ≠ j⟧ ⟹ coprime (m i) (m j)"
and "⋀i. i ∈ A ⟹ [x = y] (mod m i)" for x y :: nat
using that
proof (induct A rule: infinite_finite_induct)
case (insert x A)
then show ?case
by simp (metis coprime_cong_mult_nat prod_coprime_right)
qed auto
lemma chinese_remainder_unique_nat:
fixes A :: "'a set"
and m :: "'a ⇒ nat"
and u :: "'a ⇒ nat"
assumes fin: "finite A"
and nz: "∀i∈A. m i ≠ 0"
and cop: "∀i∈A. ∀j∈A. i ≠ j ⟶ coprime (m i) (m j)"
shows "∃!x. x < (∏i∈A. m i) ∧ (∀i∈A. [x = u i] (mod m i))"
proof -
from chinese_remainder_nat [OF fin cop]
obtain y where one: "(∀i∈A. [y = u i] (mod m i))"
by blast
let ?x = "y mod (∏i∈A. m i)"
from fin nz have prodnz: "(∏i∈A. m i) ≠ 0"
by auto
then have less: "?x < (∏i∈A. m i)"
by auto
have cong: "∀i∈A. [?x = u i] (mod m i)"
using fin one
by (auto simp add: cong_def dvd_prod_eqI mod_mod_cancel)
have unique: "∀z. z < (∏i∈A. m i) ∧ (∀i∈A. [z = u i] (mod m i)) ⟶ z = ?x"
proof clarify
fix z
assume zless: "z < (∏i∈A. m i)"
assume zcong: "(∀i∈A. [z = u i] (mod m i))"
have "∀i∈A. [?x = z] (mod m i)"
using cong zcong by (auto simp add: cong_def)
with fin cop have "[?x = z] (mod (∏i∈A. m i))"
by (intro coprime_cong_prod_nat) auto
with zless less show "z = ?x"
by (auto simp add: cong_def)
qed
from less cong unique show ?thesis
by blast
qed
lemma (in semiring_1_cancel) of_nat_eq_iff_cong_CHAR:
"of_nat x = (of_nat y :: 'a) ⟷ [x = y] (mod CHAR('a))"
proof (induction x y rule: linorder_wlog)
case (le x y)
define z where "z = y - x"
have [simp]: "y = x + z"
using le by (auto simp: z_def)
have "(CHAR('a) dvd z) = [x = x + z] (mod CHAR('a))"
by (metis ‹y = x + z› cong_def le mod_eq_dvd_iff_nat z_def)
thus ?case
by (simp add: of_nat_eq_0_iff_char_dvd)
qed (simp add: eq_commute cong_sym_eq)
lemma (in ring_1) of_int_eq_iff_cong_CHAR:
"of_int x = (of_int y :: 'a) ⟷ [x = y] (mod int CHAR('a))"
proof -
have "of_int x = (of_int y :: 'a) ⟷ of_int (x - y) = (0 :: 'a)"
by auto
also have "… ⟷ (int CHAR('a) dvd x - y)"
by (rule of_int_eq_0_iff_char_dvd)
also have "… ⟷ [x = y] (mod int CHAR('a))"
by (simp add: cong_iff_dvd_diff)
finally show ?thesis .
qed
end