# Theory Cong

theory Cong
imports Primes
```(*  Title:      HOL/Number_Theory/Cong.thy
Author:     Christophe Tabacznyj
Author:     Lawrence C. Paulson
Author:     Amine Chaieb
Author:     Thomas M. Rasmussen

Defines congruence (notation: [x = y] (mod z)) for 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".

The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
developed the congruence relations on the integers. The notion was
extended to the natural numbers by Chaieb. Jeremy Avigad combined
these, revised and tidied them, made the development uniform for the
natural numbers and the integers, and added a number of new theorems.
*)

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)"

lemma cong_sym:
"[b = c] (mod a) ⟹ [c = b] (mod a)"

lemma cong_sym_eq:
"[b = c] (mod a) ⟷ [c = b] (mod a)"

lemma cong_trans [trans]:
"[b = c] (mod a) ⟹ [c = d] (mod a) ⟹ [b = d] (mod a)"

lemma cong_mult_self_right:
"[b * a = 0] (mod a)"

lemma cong_mult_self_left:
"[a * b = 0] (mod a)"

lemma cong_mod_left [simp]:
"[b mod a = c] (mod a) ⟷ [b = c] (mod a)"

lemma cong_mod_right [simp]:
"[b = c mod a] (mod a) ⟷ [b = c] (mod a)"

lemma cong_0 [simp, presburger]:
"[b = c] (mod 0) ⟷ b = c"

lemma cong_1 [simp, presburger]:
"[b = c] (mod 1)"

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"

"[b = c] (mod a) ⟹ [d = e] (mod a) ⟹ [b + d = c + e] (mod a)"

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)"

lemma cong_scalar_left:
"[b = c] (mod a) ⟹ [d * b = d * c] (mod a)"

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)"

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)"
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]

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"]

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"
also have "… ⟷ ?Q"
by (auto simp add: algebra_simps elim!: dvdE)
finally show ?thesis
by simp
qed

"[a + x = a + y] (mod n) ⟷ [x = y] (mod n)"

"[x + a = y + a] (mod n) ⟷ [x = y] (mod n)"

"[a + x = a] (mod n) ⟷ [x = 0] (mod n)"
using cong_add_lcancel [of a x 0 n] by simp

"[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}"

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}"

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)"
then show ?thesis
qed

lemma cong_diff_iff_cong_0_nat:
"[a - b = 0] (mod m) ⟷ [a = b] (mod m)" if "a ≥ b" for a b :: 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])
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)¦"
also have "… ⟷ m dvd nat ¦(int a - int b) * int k¦"
also have "… ⟷ m dvd nat ¦int a - int b¦ * k"
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)"
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

lemma cong_less_imp_eq_nat: "0 ≤ a ⟹ a < m ⟹ 0 ≤ b ⟹ b < m ⟹ [a = b] (mod m) ⟹ a = b"
for a b :: nat

lemma cong_less_imp_eq_int: "0 ≤ a ⟹ a < m ⟹ 0 ≤ b ⟹ b < m ⟹ [a = b] (mod m) ⟹ a = b"
for a b :: int

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_less_divisor mod_mod_trivial)

lemma cong_less_unique_int: "0 < m ⟹ (∃!b. 0 ≤ b ∧ b < m ∧ [a = b] (mod m))"
for a m :: int
by (auto simp: cong_def)  (metis mod_mod_trivial pos_mod_conj)

lemma cong_iff_lin_nat: "([a = b] (mod m)) ⟷ (∃k1 k2. b + k1 * m = a + k2 * m)"
(is "?lhs = ?rhs")
for a b :: nat
proof
assume ?lhs
show ?rhs
proof (cases "b ≤ a")
case True
with ‹?lhs› show ?rhs
next
case False
with ‹?lhs› show ?rhs
by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma)
qed
next
assume ?rhs
then show ?lhs
by (metis cong_def mult.commute nat_mod_eq_iff)
qed

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

lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) ⟷ [x = y] (mod n)"
for a x y :: 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
apply (auto simp add: cong_iff_lin_nat dvd_def)
apply (rule_tac x= "k1 * k" in exI)
apply (rule_tac x= "k2 * k" in exI)
done

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

lemma cong_le_nat: "y ≤ x ⟹ [x = y] (mod n) ⟷ (∃q. x = q * n + y)"
for x y :: nat

lemma cong_solve_nat:
fixes a :: nat
assumes "a ≠ 0"
shows "∃x. [a * x = gcd a n] (mod n)"
proof (cases "n = 0")
case True
then show ?thesis by force
next
case False
then show ?thesis
using bezout_nat [of a n, OF ‹a ≠ 0›]
qed

lemma cong_solve_int: "a ≠ 0 ⟹ ∃x. [a * x = gcd a n] (mod n)"
for a :: int
apply (cases "n = 0")
apply (cases "a ≥ 0")
apply auto
apply (rule_tac x = "-1" in exI)
apply auto
apply (insert bezout_int [of a n], auto)
apply (metis cong_iff_lin mult.commute)
done

lemma cong_solve_dvd_nat:
fixes a :: nat
assumes a: "a ≠ 0" and b: "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 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_dvd_int:
assumes a: "(a::int) ≠ 0" and 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 (cases "a = 0") simp_all

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 (cases "a = 0")
(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:
"m > 0 ⟹ coprime a m ⟷ (∃x. 0 ≤ x ∧ x < m ∧ [a * x = Suc 0] (mod m))"
apply (subst coprime_iff_invertible_nat)
apply auto
apply (metis mod_less_divisor mod_mult_right_eq)
done

lemma coprime_iff_invertible'_int:
"m > 0 ⟹ coprime a m ⟷ (∃x. 0 ≤ x ∧ x < m ∧ [a * x = 1] (mod m))"
for m :: int
apply (subst coprime_iff_invertible_int)
apply (metis mod_mult_right_eq pos_mod_conj)
done

lemma cong_cong_lcm_nat: "[x = y] (mod a) ⟹ [x = y] (mod b) ⟹ [x = y] (mod lcm a b)"
for x y :: nat
apply (cases "y ≤ x")
apply (meson cong_altdef_nat cong_sym lcm_least_iff nat_le_linear)
done

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"
from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
moreover have "[m2 * x2 = 0] (mod m2)"
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"
from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
moreover have "[m2 * x2 = 0] (mod m2)"
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
apply (cases "y ≤ x")
apply (auto simp add: cong_altdef_nat elim: dvd_mult_left)
apply (metis cong_def mod_mult_cong_right)
done

lemma cong_less_modulus_unique_nat: "[x = y] (mod m) ⟹ x < m ⟹ y < m ⟹ x = y"
for x y :: nat

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 -
from binary_chinese_remainder_nat [OF a] obtain y
where "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
by blast
let ?x = "y mod (m1 * m2)"
from nz have less: "?x < m1 * m2"
by auto
have 1: "[?x = u1] (mod m1)"
apply (rule cong_trans)
prefer 2
apply (rule ‹[y = u1] (mod m1)›)
apply (rule cong_modulus_mult_nat [of _ _ _ m2])
apply simp
done
have 2: "[?x = u2] (mod m2)"
apply (rule cong_trans)
prefer 2
apply (rule ‹[y = u2] (mod m2)›)
apply (subst mult.commute)
apply (rule cong_modulus_mult_nat [of _ _ _ m1])
apply simp
done
have "∀z. z < m1 * m2 ∧ [z = u1] (mod m1) ∧ [z = u2] (mod m2) ⟶ z = ?x"
proof clarify
fix z
assume "z < m1 * m2"
assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
have "[?x = z] (mod m1)"
apply (rule cong_trans)
apply (rule ‹[?x = u1] (mod m1)›)
apply (rule cong_sym)
apply (rule ‹[z = u1] (mod m1)›)
done
moreover have "[?x = z] (mod m2)"
apply (rule cong_trans)
apply (rule ‹[?x = u2] (mod m2)›)
apply (rule cong_sym)
apply (rule ‹[z = u2] (mod m2)›)
done
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"
qed
with less 1 2 show ?thesis by auto
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))"
ultimately show "∃a. [a = 1] (mod m i) ∧ [a = 0] (mod prod m (A - {i}))"
by blast
qed
then obtain b where b: "∀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)"
apply (rule cong_scalar_left)
using b a apply blast
apply (rule cong_sum)
apply (rule cong_scalar_left)
using b apply (auto simp add: mod_eq_0_iff_dvd cong_def)
apply (rule dvd_trans [of _ "prod m (A - {x})" "b x" for x])
using a fin apply auto
done
finally show ?thesis
by simp
qed
qed
qed

lemma coprime_cong_prod_nat:
"[x = y] (mod (∏i∈A. m i))"
if "∀i∈A. (∀j∈A. i ≠ j ⟶ coprime (m i) (m j))"
and "∀i∈A. [x = y] (mod m i)" for x y :: nat
using that apply (induct A rule: infinite_finite_induct)
apply auto
apply (metis coprime_cong_mult_nat prod_coprime_right)
done

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"
qed
from less cong unique show ?thesis
by blast
qed

subsection ‹Aliasses›

lemma cong_altdef_int:
"[a = b] (mod m) ⟷ m dvd (a - b)"
for a b :: int
by (fact cong_iff_dvd_diff)

lemma cong_iff_lin_int: "[a = b] (mod m) ⟷ (∃k. b = a + m * k)"
for a b :: int
by (fact cong_iff_lin)

lemma cong_minus_int: "[a = b] (mod - m) ⟷ [a = b] (mod m)"
for a b :: int
by (fact cong_modulus_minus_iff)

lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) ⟷ [x = y] (mod n)"
for a x y :: int

lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) ⟷ [x = y] (mod n)"
for a x y :: int

"[a + x = a] (mod n) ⟷ [x = 0] (mod n)"
for a x :: int

"[x + a = a] (mod n) ⟷ [x = 0] (mod n)"
for a x :: int

lemma cong_dvd_modulus_int: "[x = y] (mod m) ⟹ n dvd m ⟹ [x = y] (mod n)"
for x y :: int
by (fact cong_dvd_modulus)

lemma cong_abs_int:
"[x = y] (mod ¦m¦) ⟷ [x = y] (mod m)"
for x y :: int
by (fact cong_abs)

lemma cong_square_int:
"prime p ⟹ 0 < a ⟹ [a * a = 1] (mod p) ⟹ [a = 1] (mod p) ∨ [a = - 1] (mod p)"
for a :: int
by (fact cong_square)

lemma cong_mult_rcancel_int:
"[a * k = b * k] (mod m) ⟷ [a = b] (mod m)"
if "coprime k m" for a k m :: int
using that by (fact cong_mult_rcancel)

lemma cong_mult_lcancel_int:
"[k * a = k * b] (mod m) = [a = b] (mod m)"
if "coprime k m" for a k m :: int
using that by (fact cong_mult_lcancel)

lemma coprime_cong_mult_int:
"[a = b] (mod m) ⟹ [a = b] (mod n) ⟹ coprime m n ⟹ [a = b] (mod m * n)"
for a b :: int
by (fact coprime_cong_mult)

lemma cong_gcd_eq_nat: "[a = b] (mod m) ⟹ gcd a m = gcd b m"
for a b :: nat
by (fact cong_gcd_eq)

lemma cong_gcd_eq_int: "[a = b] (mod m) ⟹ gcd a m = gcd b m"
for a b :: int
by (fact cong_gcd_eq)

lemma cong_imp_coprime_nat: "[a = b] (mod m) ⟹ coprime a m ⟹ coprime b m"
for a b :: nat
by (fact cong_imp_coprime)

lemma cong_imp_coprime_int: "[a = b] (mod m) ⟹ coprime a m ⟹ coprime b m"
for a b :: int
by (fact cong_imp_coprime)

lemma cong_cong_prod_coprime_int:
"[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 :: int
using that by (fact cong_cong_prod_coprime)

lemma cong_modulus_mult_int: "[x = y] (mod m * n) ⟹ [x = y] (mod m)"
for x y :: int
by (fact cong_modulus_mult)

end
```