src/HOL/Number_Theory/Cong.thy
changeset 32479 521cc9bf2958
parent 31952 40501bb2d57c
child 33718 06e9aff51d17
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,1091 @@
     1.4 +(*  Title:      HOL/Library/Cong.thy
     1.5 +    ID:         
     1.6 +    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     1.7 +                Thomas M. Rasmussen, Jeremy Avigad
     1.8 +
     1.9 +
    1.10 +Defines congruence (notation: [x = y] (mod z)) for natural numbers and
    1.11 +integers.
    1.12 +
    1.13 +This file combines and revises a number of prior developments.
    1.14 +
    1.15 +The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    1.16 +and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    1.17 +gcd, lcm, and prime for the natural numbers.
    1.18 +
    1.19 +The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    1.20 +extended gcd, lcm, primes to the integers. Amine Chaieb provided
    1.21 +another extension of the notions to the integers, and added a number
    1.22 +of results to "Primes" and "GCD". 
    1.23 +
    1.24 +The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
    1.25 +developed the congruence relations on the integers. The notion was
    1.26 +extended to the natural numbers by Chiaeb. Jeremy Avigad combined
    1.27 +these, revised and tidied them, made the development uniform for the
    1.28 +natural numbers and the integers, and added a number of new theorems.
    1.29 +
    1.30 +*)
    1.31 +
    1.32 +
    1.33 +header {* Congruence *}
    1.34 +
    1.35 +theory Cong
    1.36 +imports GCD Primes
    1.37 +begin
    1.38 +
    1.39 +subsection {* Turn off One_nat_def *}
    1.40 +
    1.41 +lemma induct'_nat [case_names zero plus1, induct type: nat]: 
    1.42 +    "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
    1.43 +by (erule nat_induct) (simp add:One_nat_def)
    1.44 +
    1.45 +lemma cases_nat [case_names zero plus1, cases type: nat]: 
    1.46 +    "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
    1.47 +by(metis induct'_nat)
    1.48 +
    1.49 +lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
    1.50 +by (simp add: One_nat_def)
    1.51 +
    1.52 +lemma power_eq_one_eq_nat [simp]: 
    1.53 +  "((x::nat)^m = 1) = (m = 0 | x = 1)"
    1.54 +by (induct m, auto)
    1.55 +
    1.56 +lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
    1.57 +  card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
    1.58 +by (auto simp add: insert_absorb)
    1.59 +
    1.60 +(* why wasn't card_insert_if a simp rule? *)
    1.61 +declare card_insert_disjoint [simp del]
    1.62 +
    1.63 +lemma nat_1' [simp]: "nat 1 = 1"
    1.64 +by simp
    1.65 +
    1.66 +(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
    1.67 +
    1.68 +declare nat_1 [simp del]
    1.69 +declare add_2_eq_Suc [simp del] 
    1.70 +declare add_2_eq_Suc' [simp del]
    1.71 +
    1.72 +
    1.73 +declare mod_pos_pos_trivial [simp]
    1.74 +
    1.75 +
    1.76 +subsection {* Main definitions *}
    1.77 +
    1.78 +class cong =
    1.79 +
    1.80 +fixes 
    1.81 +  cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
    1.82 +
    1.83 +begin
    1.84 +
    1.85 +abbreviation
    1.86 +  notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
    1.87 +where
    1.88 +  "notcong x y m == (~cong x y m)" 
    1.89 +
    1.90 +end
    1.91 +
    1.92 +(* definitions for the natural numbers *)
    1.93 +
    1.94 +instantiation nat :: cong
    1.95 +
    1.96 +begin 
    1.97 +
    1.98 +definition 
    1.99 +  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   1.100 +where 
   1.101 +  "cong_nat x y m = ((x mod m) = (y mod m))"
   1.102 +
   1.103 +instance proof qed
   1.104 +
   1.105 +end
   1.106 +
   1.107 +
   1.108 +(* definitions for the integers *)
   1.109 +
   1.110 +instantiation int :: cong
   1.111 +
   1.112 +begin 
   1.113 +
   1.114 +definition 
   1.115 +  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
   1.116 +where 
   1.117 +  "cong_int x y m = ((x mod m) = (y mod m))"
   1.118 +
   1.119 +instance proof qed
   1.120 +
   1.121 +end
   1.122 +
   1.123 +
   1.124 +subsection {* Set up Transfer *}
   1.125 +
   1.126 +
   1.127 +lemma transfer_nat_int_cong:
   1.128 +  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
   1.129 +    ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
   1.130 +  unfolding cong_int_def cong_nat_def 
   1.131 +  apply (auto simp add: nat_mod_distrib [symmetric])
   1.132 +  apply (subst (asm) eq_nat_nat_iff)
   1.133 +  apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
   1.134 +  apply assumption
   1.135 +done
   1.136 +
   1.137 +declare TransferMorphism_nat_int[transfer add return: 
   1.138 +    transfer_nat_int_cong]
   1.139 +
   1.140 +lemma transfer_int_nat_cong:
   1.141 +  "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
   1.142 +  apply (auto simp add: cong_int_def cong_nat_def)
   1.143 +  apply (auto simp add: zmod_int [symmetric])
   1.144 +done
   1.145 +
   1.146 +declare TransferMorphism_int_nat[transfer add return: 
   1.147 +    transfer_int_nat_cong]
   1.148 +
   1.149 +
   1.150 +subsection {* Congruence *}
   1.151 +
   1.152 +(* was zcong_0, etc. *)
   1.153 +lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
   1.154 +  by (unfold cong_nat_def, auto)
   1.155 +
   1.156 +lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
   1.157 +  by (unfold cong_int_def, auto)
   1.158 +
   1.159 +lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
   1.160 +  by (unfold cong_nat_def, auto)
   1.161 +
   1.162 +lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
   1.163 +  by (unfold cong_nat_def, auto simp add: One_nat_def)
   1.164 +
   1.165 +lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
   1.166 +  by (unfold cong_int_def, auto)
   1.167 +
   1.168 +lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
   1.169 +  by (unfold cong_nat_def, auto)
   1.170 +
   1.171 +lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
   1.172 +  by (unfold cong_int_def, auto)
   1.173 +
   1.174 +lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   1.175 +  by (unfold cong_nat_def, auto)
   1.176 +
   1.177 +lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   1.178 +  by (unfold cong_int_def, auto)
   1.179 +
   1.180 +lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
   1.181 +  by (unfold cong_nat_def, auto)
   1.182 +
   1.183 +lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
   1.184 +  by (unfold cong_int_def, auto)
   1.185 +
   1.186 +lemma cong_trans_nat [trans]:
   1.187 +    "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   1.188 +  by (unfold cong_nat_def, auto)
   1.189 +
   1.190 +lemma cong_trans_int [trans]:
   1.191 +    "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   1.192 +  by (unfold cong_int_def, auto)
   1.193 +
   1.194 +lemma cong_add_nat:
   1.195 +    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   1.196 +  apply (unfold cong_nat_def)
   1.197 +  apply (subst (1 2) mod_add_eq)
   1.198 +  apply simp
   1.199 +done
   1.200 +
   1.201 +lemma cong_add_int:
   1.202 +    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   1.203 +  apply (unfold cong_int_def)
   1.204 +  apply (subst (1 2) mod_add_left_eq)
   1.205 +  apply (subst (1 2) mod_add_right_eq)
   1.206 +  apply simp
   1.207 +done
   1.208 +
   1.209 +lemma cong_diff_int:
   1.210 +    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
   1.211 +  apply (unfold cong_int_def)
   1.212 +  apply (subst (1 2) mod_diff_eq)
   1.213 +  apply simp
   1.214 +done
   1.215 +
   1.216 +lemma cong_diff_aux_int:
   1.217 +  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
   1.218 +      [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
   1.219 +  apply (subst (1 2) tsub_eq)
   1.220 +  apply (auto intro: cong_diff_int)
   1.221 +done;
   1.222 +
   1.223 +lemma cong_diff_nat:
   1.224 +  assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
   1.225 +    "[c = d] (mod m)"
   1.226 +  shows "[a - c = b - d] (mod m)"
   1.227 +
   1.228 +  using prems by (rule cong_diff_aux_int [transferred]);
   1.229 +
   1.230 +lemma cong_mult_nat:
   1.231 +    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   1.232 +  apply (unfold cong_nat_def)
   1.233 +  apply (subst (1 2) mod_mult_eq)
   1.234 +  apply simp
   1.235 +done
   1.236 +
   1.237 +lemma cong_mult_int:
   1.238 +    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   1.239 +  apply (unfold cong_int_def)
   1.240 +  apply (subst (1 2) zmod_zmult1_eq)
   1.241 +  apply (subst (1 2) mult_commute)
   1.242 +  apply (subst (1 2) zmod_zmult1_eq)
   1.243 +  apply simp
   1.244 +done
   1.245 +
   1.246 +lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   1.247 +  apply (induct k)
   1.248 +  apply (auto simp add: cong_refl_nat cong_mult_nat)
   1.249 +done
   1.250 +
   1.251 +lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   1.252 +  apply (induct k)
   1.253 +  apply (auto simp add: cong_refl_int cong_mult_int)
   1.254 +done
   1.255 +
   1.256 +lemma cong_setsum_nat [rule_format]: 
   1.257 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
   1.258 +      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
   1.259 +  apply (case_tac "finite A")
   1.260 +  apply (induct set: finite)
   1.261 +  apply (auto intro: cong_add_nat)
   1.262 +done
   1.263 +
   1.264 +lemma cong_setsum_int [rule_format]:
   1.265 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
   1.266 +      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
   1.267 +  apply (case_tac "finite A")
   1.268 +  apply (induct set: finite)
   1.269 +  apply (auto intro: cong_add_int)
   1.270 +done
   1.271 +
   1.272 +lemma cong_setprod_nat [rule_format]: 
   1.273 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
   1.274 +      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
   1.275 +  apply (case_tac "finite A")
   1.276 +  apply (induct set: finite)
   1.277 +  apply (auto intro: cong_mult_nat)
   1.278 +done
   1.279 +
   1.280 +lemma cong_setprod_int [rule_format]: 
   1.281 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
   1.282 +      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
   1.283 +  apply (case_tac "finite A")
   1.284 +  apply (induct set: finite)
   1.285 +  apply (auto intro: cong_mult_int)
   1.286 +done
   1.287 +
   1.288 +lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   1.289 +  by (rule cong_mult_nat, simp_all)
   1.290 +
   1.291 +lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   1.292 +  by (rule cong_mult_int, simp_all)
   1.293 +
   1.294 +lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   1.295 +  by (rule cong_mult_nat, simp_all)
   1.296 +
   1.297 +lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   1.298 +  by (rule cong_mult_int, simp_all)
   1.299 +
   1.300 +lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
   1.301 +  by (unfold cong_nat_def, auto)
   1.302 +
   1.303 +lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
   1.304 +  by (unfold cong_int_def, auto)
   1.305 +
   1.306 +lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
   1.307 +  apply (rule iffI)
   1.308 +  apply (erule cong_diff_int [of a b m b b, simplified])
   1.309 +  apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
   1.310 +done
   1.311 +
   1.312 +lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
   1.313 +    [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
   1.314 +  by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
   1.315 +
   1.316 +lemma cong_eq_diff_cong_0_nat:
   1.317 +  assumes "(a::nat) >= b"
   1.318 +  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
   1.319 +
   1.320 +  using prems by (rule cong_eq_diff_cong_0_aux_int [transferred])
   1.321 +
   1.322 +lemma cong_diff_cong_0'_nat: 
   1.323 +  "[(x::nat) = y] (mod n) \<longleftrightarrow> 
   1.324 +    (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
   1.325 +  apply (case_tac "y <= x")
   1.326 +  apply (frule cong_eq_diff_cong_0_nat [where m = n])
   1.327 +  apply auto [1]
   1.328 +  apply (subgoal_tac "x <= y")
   1.329 +  apply (frule cong_eq_diff_cong_0_nat [where m = n])
   1.330 +  apply (subst cong_sym_eq_nat)
   1.331 +  apply auto
   1.332 +done
   1.333 +
   1.334 +lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
   1.335 +  apply (subst cong_eq_diff_cong_0_nat, assumption)
   1.336 +  apply (unfold cong_nat_def)
   1.337 +  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   1.338 +done
   1.339 +
   1.340 +lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
   1.341 +  apply (subst cong_eq_diff_cong_0_int)
   1.342 +  apply (unfold cong_int_def)
   1.343 +  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   1.344 +done
   1.345 +
   1.346 +lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   1.347 +  by (simp add: cong_altdef_int)
   1.348 +
   1.349 +lemma cong_square_int:
   1.350 +   "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
   1.351 +    \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   1.352 +  apply (simp only: cong_altdef_int)
   1.353 +  apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
   1.354 +  (* any way around this? *)
   1.355 +  apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   1.356 +  apply (auto simp add: ring_simps)
   1.357 +done
   1.358 +
   1.359 +lemma cong_mult_rcancel_int:
   1.360 +  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   1.361 +  apply (subst (1 2) cong_altdef_int)
   1.362 +  apply (subst left_diff_distrib [symmetric])
   1.363 +  apply (rule coprime_dvd_mult_iff_int)
   1.364 +  apply (subst gcd_commute_int, assumption)
   1.365 +done
   1.366 +
   1.367 +lemma cong_mult_rcancel_nat:
   1.368 +  assumes  "coprime k (m::nat)"
   1.369 +  shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
   1.370 +
   1.371 +  apply (rule cong_mult_rcancel_int [transferred])
   1.372 +  using prems apply auto
   1.373 +done
   1.374 +
   1.375 +lemma cong_mult_lcancel_nat:
   1.376 +  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
   1.377 +  by (simp add: mult_commute cong_mult_rcancel_nat)
   1.378 +
   1.379 +lemma cong_mult_lcancel_int:
   1.380 +  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
   1.381 +  by (simp add: mult_commute cong_mult_rcancel_int)
   1.382 +
   1.383 +(* was zcong_zgcd_zmult_zmod *)
   1.384 +lemma coprime_cong_mult_int:
   1.385 +  "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
   1.386 +    \<Longrightarrow> [a = b] (mod m * n)"
   1.387 +  apply (simp only: cong_altdef_int)
   1.388 +  apply (erule (2) divides_mult_int)
   1.389 +done
   1.390 +
   1.391 +lemma coprime_cong_mult_nat:
   1.392 +  assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
   1.393 +  shows "[a = b] (mod m * n)"
   1.394 +
   1.395 +  apply (rule coprime_cong_mult_int [transferred])
   1.396 +  using prems apply auto
   1.397 +done
   1.398 +
   1.399 +lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
   1.400 +    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   1.401 +  by (auto simp add: cong_nat_def mod_pos_pos_trivial)
   1.402 +
   1.403 +lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
   1.404 +    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   1.405 +  by (auto simp add: cong_int_def mod_pos_pos_trivial)
   1.406 +
   1.407 +lemma cong_less_unique_nat:
   1.408 +    "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   1.409 +  apply auto
   1.410 +  apply (rule_tac x = "a mod m" in exI)
   1.411 +  apply (unfold cong_nat_def, auto)
   1.412 +done
   1.413 +
   1.414 +lemma cong_less_unique_int:
   1.415 +    "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   1.416 +  apply auto
   1.417 +  apply (rule_tac x = "a mod m" in exI)
   1.418 +  apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
   1.419 +done
   1.420 +
   1.421 +lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   1.422 +  apply (auto simp add: cong_altdef_int dvd_def ring_simps)
   1.423 +  apply (rule_tac [!] x = "-k" in exI, auto)
   1.424 +done
   1.425 +
   1.426 +lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
   1.427 +    (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   1.428 +  apply (rule iffI)
   1.429 +  apply (case_tac "b <= a")
   1.430 +  apply (subst (asm) cong_altdef_nat, assumption)
   1.431 +  apply (unfold dvd_def, auto)
   1.432 +  apply (rule_tac x = k in exI)
   1.433 +  apply (rule_tac x = 0 in exI)
   1.434 +  apply (auto simp add: ring_simps)
   1.435 +  apply (subst (asm) cong_sym_eq_nat)
   1.436 +  apply (subst (asm) cong_altdef_nat)
   1.437 +  apply force
   1.438 +  apply (unfold dvd_def, auto)
   1.439 +  apply (rule_tac x = 0 in exI)
   1.440 +  apply (rule_tac x = k in exI)
   1.441 +  apply (auto simp add: ring_simps)
   1.442 +  apply (unfold cong_nat_def)
   1.443 +  apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
   1.444 +  apply (erule ssubst)back
   1.445 +  apply (erule subst)
   1.446 +  apply auto
   1.447 +done
   1.448 +
   1.449 +lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   1.450 +  apply (subst (asm) cong_iff_lin_int, auto)
   1.451 +  apply (subst add_commute) 
   1.452 +  apply (subst (2) gcd_commute_int)
   1.453 +  apply (subst mult_commute)
   1.454 +  apply (subst gcd_add_mult_int)
   1.455 +  apply (rule gcd_commute_int)
   1.456 +done
   1.457 +
   1.458 +lemma cong_gcd_eq_nat: 
   1.459 +  assumes "[(a::nat) = b] (mod m)"
   1.460 +  shows "gcd a m = gcd b m"
   1.461 +
   1.462 +  apply (rule cong_gcd_eq_int [transferred])
   1.463 +  using prems apply auto
   1.464 +done
   1.465 +
   1.466 +lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
   1.467 +    coprime b m"
   1.468 +  by (auto simp add: cong_gcd_eq_nat)
   1.469 +
   1.470 +lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
   1.471 +    coprime b m"
   1.472 +  by (auto simp add: cong_gcd_eq_int)
   1.473 +
   1.474 +lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = 
   1.475 +    [a mod m = b mod m] (mod m)"
   1.476 +  by (auto simp add: cong_nat_def)
   1.477 +
   1.478 +lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = 
   1.479 +    [a mod m = b mod m] (mod m)"
   1.480 +  by (auto simp add: cong_int_def)
   1.481 +
   1.482 +lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
   1.483 +  by (subst (1 2) cong_altdef_int, auto)
   1.484 +
   1.485 +lemma cong_zero_nat [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
   1.486 +  by (auto simp add: cong_nat_def)
   1.487 +
   1.488 +lemma cong_zero_int [iff]: "[(a::int) = b] (mod 0) = (a = b)"
   1.489 +  by (auto simp add: cong_int_def)
   1.490 +
   1.491 +(*
   1.492 +lemma mod_dvd_mod_int:
   1.493 +    "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
   1.494 +  apply (unfold dvd_def, auto)
   1.495 +  apply (rule mod_mod_cancel)
   1.496 +  apply auto
   1.497 +done
   1.498 +
   1.499 +lemma mod_dvd_mod:
   1.500 +  assumes "0 < (m::nat)" and "m dvd b"
   1.501 +  shows "(a mod b mod m) = (a mod m)"
   1.502 +
   1.503 +  apply (rule mod_dvd_mod_int [transferred])
   1.504 +  using prems apply auto
   1.505 +done
   1.506 +*)
   1.507 +
   1.508 +lemma cong_add_lcancel_nat: 
   1.509 +    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
   1.510 +  by (simp add: cong_iff_lin_nat)
   1.511 +
   1.512 +lemma cong_add_lcancel_int: 
   1.513 +    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
   1.514 +  by (simp add: cong_iff_lin_int)
   1.515 +
   1.516 +lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   1.517 +  by (simp add: cong_iff_lin_nat)
   1.518 +
   1.519 +lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   1.520 +  by (simp add: cong_iff_lin_int)
   1.521 +
   1.522 +lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   1.523 +  by (simp add: cong_iff_lin_nat)
   1.524 +
   1.525 +lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   1.526 +  by (simp add: cong_iff_lin_int)
   1.527 +
   1.528 +lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   1.529 +  by (simp add: cong_iff_lin_nat)
   1.530 +
   1.531 +lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   1.532 +  by (simp add: cong_iff_lin_int)
   1.533 +
   1.534 +lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   1.535 +    [x = y] (mod n)"
   1.536 +  apply (auto simp add: cong_iff_lin_nat dvd_def)
   1.537 +  apply (rule_tac x="k1 * k" in exI)
   1.538 +  apply (rule_tac x="k2 * k" in exI)
   1.539 +  apply (simp add: ring_simps)
   1.540 +done
   1.541 +
   1.542 +lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   1.543 +    [x = y] (mod n)"
   1.544 +  by (auto simp add: cong_altdef_int dvd_def)
   1.545 +
   1.546 +lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   1.547 +  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
   1.548 +
   1.549 +lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   1.550 +  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
   1.551 +
   1.552 +lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
   1.553 +  by (simp add: cong_nat_def)
   1.554 +
   1.555 +lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
   1.556 +  by (simp add: cong_int_def)
   1.557 +
   1.558 +lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
   1.559 +    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   1.560 +  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   1.561 +
   1.562 +lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   1.563 +  apply (simp add: cong_altdef_int)
   1.564 +  apply (subst dvd_minus_iff [symmetric])
   1.565 +  apply (simp add: ring_simps)
   1.566 +done
   1.567 +
   1.568 +lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   1.569 +  by (auto simp add: cong_altdef_int)
   1.570 +
   1.571 +lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
   1.572 +    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   1.573 +  apply (case_tac "b > 0")
   1.574 +  apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   1.575 +  apply (subst (1 2) cong_modulus_neg_int)
   1.576 +  apply (unfold cong_int_def)
   1.577 +  apply (subgoal_tac "a * b = (-a * -b)")
   1.578 +  apply (erule ssubst)
   1.579 +  apply (subst zmod_zmult2_eq)
   1.580 +  apply (auto simp add: mod_add_left_eq) 
   1.581 +done
   1.582 +
   1.583 +lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
   1.584 +  apply (case_tac "a = 0")
   1.585 +  apply force
   1.586 +  apply (subst (asm) cong_altdef_nat)
   1.587 +  apply auto
   1.588 +done
   1.589 +
   1.590 +lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
   1.591 +  by (unfold cong_nat_def, auto)
   1.592 +
   1.593 +lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
   1.594 +  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
   1.595 +
   1.596 +lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
   1.597 +    a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
   1.598 +  apply (case_tac "n = 1")
   1.599 +  apply auto [1]
   1.600 +  apply (drule_tac x = "a - 1" in spec)
   1.601 +  apply force
   1.602 +  apply (case_tac "a = 0")
   1.603 +  apply (auto simp add: cong_0_1_nat) [1]
   1.604 +  apply (rule iffI)
   1.605 +  apply (drule cong_to_1_nat)
   1.606 +  apply (unfold dvd_def)
   1.607 +  apply auto [1]
   1.608 +  apply (rule_tac x = k in exI)
   1.609 +  apply (auto simp add: ring_simps) [1]
   1.610 +  apply (subst cong_altdef_nat)
   1.611 +  apply (auto simp add: dvd_def)
   1.612 +done
   1.613 +
   1.614 +lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   1.615 +  apply (subst cong_altdef_nat)
   1.616 +  apply assumption
   1.617 +  apply (unfold dvd_def, auto simp add: ring_simps)
   1.618 +  apply (rule_tac x = k in exI)
   1.619 +  apply auto
   1.620 +done
   1.621 +
   1.622 +lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   1.623 +  apply (case_tac "n = 0")
   1.624 +  apply force
   1.625 +  apply (frule bezout_nat [of a n], auto)
   1.626 +  apply (rule exI, erule ssubst)
   1.627 +  apply (rule cong_trans_nat)
   1.628 +  apply (rule cong_add_nat)
   1.629 +  apply (subst mult_commute)
   1.630 +  apply (rule cong_mult_self_nat)
   1.631 +  prefer 2
   1.632 +  apply simp
   1.633 +  apply (rule cong_refl_nat)
   1.634 +  apply (rule cong_refl_nat)
   1.635 +done
   1.636 +
   1.637 +lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   1.638 +  apply (case_tac "n = 0")
   1.639 +  apply (case_tac "a \<ge> 0")
   1.640 +  apply auto
   1.641 +  apply (rule_tac x = "-1" in exI)
   1.642 +  apply auto
   1.643 +  apply (insert bezout_int [of a n], auto)
   1.644 +  apply (rule exI)
   1.645 +  apply (erule subst)
   1.646 +  apply (rule cong_trans_int)
   1.647 +  prefer 2
   1.648 +  apply (rule cong_add_int)
   1.649 +  apply (rule cong_refl_int)
   1.650 +  apply (rule cong_sym_int)
   1.651 +  apply (rule cong_mult_self_int)
   1.652 +  apply simp
   1.653 +  apply (subst mult_commute)
   1.654 +  apply (rule cong_refl_int)
   1.655 +done
   1.656 +  
   1.657 +lemma cong_solve_dvd_nat: 
   1.658 +  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
   1.659 +  shows "EX x. [a * x = d] (mod n)"
   1.660 +proof -
   1.661 +  from cong_solve_nat [OF a] obtain x where 
   1.662 +      "[a * x = gcd a n](mod n)"
   1.663 +    by auto
   1.664 +  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
   1.665 +    by (elim cong_scalar2_nat)
   1.666 +  also from b have "(d div gcd a n) * gcd a n = d"
   1.667 +    by (rule dvd_div_mult_self)
   1.668 +  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   1.669 +    by auto
   1.670 +  finally show ?thesis
   1.671 +    by auto
   1.672 +qed
   1.673 +
   1.674 +lemma cong_solve_dvd_int: 
   1.675 +  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
   1.676 +  shows "EX x. [a * x = d] (mod n)"
   1.677 +proof -
   1.678 +  from cong_solve_int [OF a] obtain x where 
   1.679 +      "[a * x = gcd a n](mod n)"
   1.680 +    by auto
   1.681 +  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
   1.682 +    by (elim cong_scalar2_int)
   1.683 +  also from b have "(d div gcd a n) * gcd a n = d"
   1.684 +    by (rule dvd_div_mult_self)
   1.685 +  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   1.686 +    by auto
   1.687 +  finally show ?thesis
   1.688 +    by auto
   1.689 +qed
   1.690 +
   1.691 +lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> 
   1.692 +    EX x. [a * x = 1] (mod n)"
   1.693 +  apply (case_tac "a = 0")
   1.694 +  apply force
   1.695 +  apply (frule cong_solve_nat [of a n])
   1.696 +  apply auto
   1.697 +done
   1.698 +
   1.699 +lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> 
   1.700 +    EX x. [a * x = 1] (mod n)"
   1.701 +  apply (case_tac "a = 0")
   1.702 +  apply auto
   1.703 +  apply (case_tac "n \<ge> 0")
   1.704 +  apply auto
   1.705 +  apply (subst cong_int_def, auto)
   1.706 +  apply (frule cong_solve_int [of a n])
   1.707 +  apply auto
   1.708 +done
   1.709 +
   1.710 +lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = 
   1.711 +    (EX x. [a * x = 1] (mod m))"
   1.712 +  apply (auto intro: cong_solve_coprime_nat)
   1.713 +  apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
   1.714 +done
   1.715 +
   1.716 +lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = 
   1.717 +    (EX x. [a * x = 1] (mod m))"
   1.718 +  apply (auto intro: cong_solve_coprime_int)
   1.719 +  apply (unfold cong_int_def)
   1.720 +  apply (auto intro: invertible_coprime_int)
   1.721 +done
   1.722 +
   1.723 +lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = 
   1.724 +    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
   1.725 +  apply (subst coprime_iff_invertible_int)
   1.726 +  apply auto
   1.727 +  apply (auto simp add: cong_int_def)
   1.728 +  apply (rule_tac x = "x mod m" in exI)
   1.729 +  apply (auto simp add: mod_mult_right_eq [symmetric])
   1.730 +done
   1.731 +
   1.732 +
   1.733 +lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
   1.734 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   1.735 +  apply (case_tac "y \<le> x")
   1.736 +  apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
   1.737 +  apply (rule cong_sym_nat)
   1.738 +  apply (subst (asm) (1 2) cong_sym_eq_nat)
   1.739 +  apply (auto simp add: cong_altdef_nat lcm_least_nat)
   1.740 +done
   1.741 +
   1.742 +lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
   1.743 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   1.744 +  by (auto simp add: cong_altdef_int lcm_least_int) [1]
   1.745 +
   1.746 +lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
   1.747 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
   1.748 +  apply (frule (1) cong_cong_lcm_nat)back
   1.749 +  apply (simp add: lcm_nat_def)
   1.750 +done
   1.751 +
   1.752 +lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
   1.753 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
   1.754 +  apply (frule (1) cong_cong_lcm_int)back
   1.755 +  apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
   1.756 +done
   1.757 +
   1.758 +lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
   1.759 +    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   1.760 +    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   1.761 +      [x = y] (mod (PROD i:A. m i))"
   1.762 +  apply (induct set: finite)
   1.763 +  apply auto
   1.764 +  apply (rule cong_cong_coprime_nat)
   1.765 +  apply (subst gcd_commute_nat)
   1.766 +  apply (rule setprod_coprime_nat)
   1.767 +  apply auto
   1.768 +done
   1.769 +
   1.770 +lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
   1.771 +    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   1.772 +    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
   1.773 +      [x = y] (mod (PROD i:A. m i))"
   1.774 +  apply (induct set: finite)
   1.775 +  apply auto
   1.776 +  apply (rule cong_cong_coprime_int)
   1.777 +  apply (subst gcd_commute_int)
   1.778 +  apply (rule setprod_coprime_int)
   1.779 +  apply auto
   1.780 +done
   1.781 +
   1.782 +lemma binary_chinese_remainder_aux_nat: 
   1.783 +  assumes a: "coprime (m1::nat) m2"
   1.784 +  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   1.785 +    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   1.786 +proof -
   1.787 +  from cong_solve_coprime_nat [OF a]
   1.788 +      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   1.789 +    by auto
   1.790 +  from a have b: "coprime m2 m1" 
   1.791 +    by (subst gcd_commute_nat)
   1.792 +  from cong_solve_coprime_nat [OF b]
   1.793 +      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   1.794 +    by auto
   1.795 +  have "[m1 * x1 = 0] (mod m1)"
   1.796 +    by (subst mult_commute, rule cong_mult_self_nat)
   1.797 +  moreover have "[m2 * x2 = 0] (mod m2)"
   1.798 +    by (subst mult_commute, rule cong_mult_self_nat)
   1.799 +  moreover note one two
   1.800 +  ultimately show ?thesis by blast
   1.801 +qed
   1.802 +
   1.803 +lemma binary_chinese_remainder_aux_int: 
   1.804 +  assumes a: "coprime (m1::int) m2"
   1.805 +  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   1.806 +    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   1.807 +proof -
   1.808 +  from cong_solve_coprime_int [OF a]
   1.809 +      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   1.810 +    by auto
   1.811 +  from a have b: "coprime m2 m1" 
   1.812 +    by (subst gcd_commute_int)
   1.813 +  from cong_solve_coprime_int [OF b]
   1.814 +      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   1.815 +    by auto
   1.816 +  have "[m1 * x1 = 0] (mod m1)"
   1.817 +    by (subst mult_commute, rule cong_mult_self_int)
   1.818 +  moreover have "[m2 * x2 = 0] (mod m2)"
   1.819 +    by (subst mult_commute, rule cong_mult_self_int)
   1.820 +  moreover note one two
   1.821 +  ultimately show ?thesis by blast
   1.822 +qed
   1.823 +
   1.824 +lemma binary_chinese_remainder_nat:
   1.825 +  assumes a: "coprime (m1::nat) m2"
   1.826 +  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   1.827 +proof -
   1.828 +  from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
   1.829 +    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   1.830 +          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   1.831 +    by blast
   1.832 +  let ?x = "u1 * b1 + u2 * b2"
   1.833 +  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   1.834 +    apply (rule cong_add_nat)
   1.835 +    apply (rule cong_scalar2_nat)
   1.836 +    apply (rule `[b1 = 1] (mod m1)`)
   1.837 +    apply (rule cong_scalar2_nat)
   1.838 +    apply (rule `[b2 = 0] (mod m1)`)
   1.839 +    done
   1.840 +  hence "[?x = u1] (mod m1)" by simp
   1.841 +  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   1.842 +    apply (rule cong_add_nat)
   1.843 +    apply (rule cong_scalar2_nat)
   1.844 +    apply (rule `[b1 = 0] (mod m2)`)
   1.845 +    apply (rule cong_scalar2_nat)
   1.846 +    apply (rule `[b2 = 1] (mod m2)`)
   1.847 +    done
   1.848 +  hence "[?x = u2] (mod m2)" by simp
   1.849 +  with `[?x = u1] (mod m1)` show ?thesis by blast
   1.850 +qed
   1.851 +
   1.852 +lemma binary_chinese_remainder_int:
   1.853 +  assumes a: "coprime (m1::int) m2"
   1.854 +  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   1.855 +proof -
   1.856 +  from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
   1.857 +    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   1.858 +          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   1.859 +    by blast
   1.860 +  let ?x = "u1 * b1 + u2 * b2"
   1.861 +  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   1.862 +    apply (rule cong_add_int)
   1.863 +    apply (rule cong_scalar2_int)
   1.864 +    apply (rule `[b1 = 1] (mod m1)`)
   1.865 +    apply (rule cong_scalar2_int)
   1.866 +    apply (rule `[b2 = 0] (mod m1)`)
   1.867 +    done
   1.868 +  hence "[?x = u1] (mod m1)" by simp
   1.869 +  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   1.870 +    apply (rule cong_add_int)
   1.871 +    apply (rule cong_scalar2_int)
   1.872 +    apply (rule `[b1 = 0] (mod m2)`)
   1.873 +    apply (rule cong_scalar2_int)
   1.874 +    apply (rule `[b2 = 1] (mod m2)`)
   1.875 +    done
   1.876 +  hence "[?x = u2] (mod m2)" by simp
   1.877 +  with `[?x = u1] (mod m1)` show ?thesis by blast
   1.878 +qed
   1.879 +
   1.880 +lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
   1.881 +    [x = y] (mod m)"
   1.882 +  apply (case_tac "y \<le> x")
   1.883 +  apply (simp add: cong_altdef_nat)
   1.884 +  apply (erule dvd_mult_left)
   1.885 +  apply (rule cong_sym_nat)
   1.886 +  apply (subst (asm) cong_sym_eq_nat)
   1.887 +  apply (simp add: cong_altdef_nat) 
   1.888 +  apply (erule dvd_mult_left)
   1.889 +done
   1.890 +
   1.891 +lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
   1.892 +    [x = y] (mod m)"
   1.893 +  apply (simp add: cong_altdef_int) 
   1.894 +  apply (erule dvd_mult_left)
   1.895 +done
   1.896 +
   1.897 +lemma cong_less_modulus_unique_nat: 
   1.898 +    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   1.899 +  by (simp add: cong_nat_def)
   1.900 +
   1.901 +lemma binary_chinese_remainder_unique_nat:
   1.902 +  assumes a: "coprime (m1::nat) m2" and
   1.903 +         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   1.904 +  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   1.905 +proof -
   1.906 +  from binary_chinese_remainder_nat [OF a] obtain y where 
   1.907 +      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
   1.908 +    by blast
   1.909 +  let ?x = "y mod (m1 * m2)"
   1.910 +  from nz have less: "?x < m1 * m2"
   1.911 +    by auto   
   1.912 +  have one: "[?x = u1] (mod m1)"
   1.913 +    apply (rule cong_trans_nat)
   1.914 +    prefer 2
   1.915 +    apply (rule `[y = u1] (mod m1)`)
   1.916 +    apply (rule cong_modulus_mult_nat)
   1.917 +    apply (rule cong_mod_nat)
   1.918 +    using nz apply auto
   1.919 +    done
   1.920 +  have two: "[?x = u2] (mod m2)"
   1.921 +    apply (rule cong_trans_nat)
   1.922 +    prefer 2
   1.923 +    apply (rule `[y = u2] (mod m2)`)
   1.924 +    apply (subst mult_commute)
   1.925 +    apply (rule cong_modulus_mult_nat)
   1.926 +    apply (rule cong_mod_nat)
   1.927 +    using nz apply auto
   1.928 +    done
   1.929 +  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
   1.930 +      z = ?x"
   1.931 +  proof (clarify)
   1.932 +    fix z
   1.933 +    assume "z < m1 * m2"
   1.934 +    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
   1.935 +    have "[?x = z] (mod m1)"
   1.936 +      apply (rule cong_trans_nat)
   1.937 +      apply (rule `[?x = u1] (mod m1)`)
   1.938 +      apply (rule cong_sym_nat)
   1.939 +      apply (rule `[z = u1] (mod m1)`)
   1.940 +      done
   1.941 +    moreover have "[?x = z] (mod m2)"
   1.942 +      apply (rule cong_trans_nat)
   1.943 +      apply (rule `[?x = u2] (mod m2)`)
   1.944 +      apply (rule cong_sym_nat)
   1.945 +      apply (rule `[z = u2] (mod m2)`)
   1.946 +      done
   1.947 +    ultimately have "[?x = z] (mod m1 * m2)"
   1.948 +      by (auto intro: coprime_cong_mult_nat a)
   1.949 +    with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
   1.950 +      apply (intro cong_less_modulus_unique_nat)
   1.951 +      apply (auto, erule cong_sym_nat)
   1.952 +      done
   1.953 +  qed  
   1.954 +  with less one two show ?thesis
   1.955 +    by auto
   1.956 + qed
   1.957 +
   1.958 +lemma chinese_remainder_aux_nat:
   1.959 +  fixes A :: "'a set" and
   1.960 +        m :: "'a \<Rightarrow> nat"
   1.961 +  assumes fin: "finite A" and
   1.962 +          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   1.963 +  shows "EX b. (ALL i : A. 
   1.964 +      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
   1.965 +proof (rule finite_set_choice, rule fin, rule ballI)
   1.966 +  fix i
   1.967 +  assume "i : A"
   1.968 +  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
   1.969 +    by (intro setprod_coprime_nat, auto)
   1.970 +  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   1.971 +    by (elim cong_solve_coprime_nat)
   1.972 +  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   1.973 +    by auto
   1.974 +  moreover have "[(PROD j : A - {i}. m j) * x = 0] 
   1.975 +    (mod (PROD j : A - {i}. m j))"
   1.976 +    by (subst mult_commute, rule cong_mult_self_nat)
   1.977 +  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
   1.978 +      (mod setprod m (A - {i}))"
   1.979 +    by blast
   1.980 +qed
   1.981 +
   1.982 +lemma chinese_remainder_nat:
   1.983 +  fixes A :: "'a set" and
   1.984 +        m :: "'a \<Rightarrow> nat" and
   1.985 +        u :: "'a \<Rightarrow> nat"
   1.986 +  assumes 
   1.987 +        fin: "finite A" and
   1.988 +        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   1.989 +  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
   1.990 +proof -
   1.991 +  from chinese_remainder_aux_nat [OF fin cop] obtain b where
   1.992 +    bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
   1.993 +      [b i = 0] (mod (PROD j : A - {i}. m j))"
   1.994 +    by blast
   1.995 +  let ?x = "SUM i:A. (u i) * (b i)"
   1.996 +  show "?thesis"
   1.997 +  proof (rule exI, clarify)
   1.998 +    fix i
   1.999 +    assume a: "i : A"
  1.1000 +    show "[?x = u i] (mod m i)" 
  1.1001 +    proof -
  1.1002 +      from fin a have "?x = (SUM j:{i}. u j * b j) + 
  1.1003 +          (SUM j:A-{i}. u j * b j)"
  1.1004 +        by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
  1.1005 +      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
  1.1006 +        by auto
  1.1007 +      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
  1.1008 +                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
  1.1009 +        apply (rule cong_add_nat)
  1.1010 +        apply (rule cong_scalar2_nat)
  1.1011 +        using bprop a apply blast
  1.1012 +        apply (rule cong_setsum_nat)
  1.1013 +        apply (rule cong_scalar2_nat)
  1.1014 +        using bprop apply auto
  1.1015 +        apply (rule cong_dvd_modulus_nat)
  1.1016 +        apply (drule (1) bspec)
  1.1017 +        apply (erule conjE)
  1.1018 +        apply assumption
  1.1019 +        apply (rule dvd_setprod)
  1.1020 +        using fin a apply auto
  1.1021 +        done
  1.1022 +      finally show ?thesis
  1.1023 +        by simp
  1.1024 +    qed
  1.1025 +  qed
  1.1026 +qed
  1.1027 +
  1.1028 +lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> 
  1.1029 +    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
  1.1030 +      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
  1.1031 +         [x = y] (mod (PROD i:A. m i))" 
  1.1032 +  apply (induct set: finite)
  1.1033 +  apply auto
  1.1034 +  apply (erule (1) coprime_cong_mult_nat)
  1.1035 +  apply (subst gcd_commute_nat)
  1.1036 +  apply (rule setprod_coprime_nat)
  1.1037 +  apply auto
  1.1038 +done
  1.1039 +
  1.1040 +lemma chinese_remainder_unique_nat:
  1.1041 +  fixes A :: "'a set" and
  1.1042 +        m :: "'a \<Rightarrow> nat" and
  1.1043 +        u :: "'a \<Rightarrow> nat"
  1.1044 +  assumes 
  1.1045 +        fin: "finite A" and
  1.1046 +         nz: "ALL i:A. m i \<noteq> 0" and
  1.1047 +        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
  1.1048 +  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
  1.1049 +proof -
  1.1050 +  from chinese_remainder_nat [OF fin cop] obtain y where
  1.1051 +      one: "(ALL i:A. [y = u i] (mod m i))" 
  1.1052 +    by blast
  1.1053 +  let ?x = "y mod (PROD i:A. m i)"
  1.1054 +  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
  1.1055 +    by auto
  1.1056 +  hence less: "?x < (PROD i:A. m i)"
  1.1057 +    by auto
  1.1058 +  have cong: "ALL i:A. [?x = u i] (mod m i)"
  1.1059 +    apply auto
  1.1060 +    apply (rule cong_trans_nat)
  1.1061 +    prefer 2
  1.1062 +    using one apply auto
  1.1063 +    apply (rule cong_dvd_modulus_nat)
  1.1064 +    apply (rule cong_mod_nat)
  1.1065 +    using prodnz apply auto
  1.1066 +    apply (rule dvd_setprod)
  1.1067 +    apply (rule fin)
  1.1068 +    apply assumption
  1.1069 +    done
  1.1070 +  have unique: "ALL z. z < (PROD i:A. m i) \<and> 
  1.1071 +      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
  1.1072 +  proof (clarify)
  1.1073 +    fix z
  1.1074 +    assume zless: "z < (PROD i:A. m i)"
  1.1075 +    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
  1.1076 +    have "ALL i:A. [?x = z] (mod m i)"
  1.1077 +      apply clarify     
  1.1078 +      apply (rule cong_trans_nat)
  1.1079 +      using cong apply (erule bspec)
  1.1080 +      apply (rule cong_sym_nat)
  1.1081 +      using zcong apply auto
  1.1082 +      done
  1.1083 +    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
  1.1084 +      by (intro coprime_cong_prod_nat, auto)
  1.1085 +    with zless less show "z = ?x"
  1.1086 +      apply (intro cong_less_modulus_unique_nat)
  1.1087 +      apply (auto, erule cong_sym_nat)
  1.1088 +      done
  1.1089 +  qed 
  1.1090 +  from less cong unique show ?thesis
  1.1091 +    by blast  
  1.1092 +qed
  1.1093 +
  1.1094 +end