1(* Title: HOL/Number_Theory/Cong.thy 2 Author: Christophe Tabacznyj 3 Author: Lawrence C. Paulson 4 Author: Amine Chaieb 5 Author: Thomas M. Rasmussen 6 Author: Jeremy Avigad 7 8Defines congruence (notation: [x = y] (mod z)) for natural numbers and 9integers. 10 11This file combines and revises a number of prior developments. 12 13The original theories "GCD" and "Primes" were by Christophe Tabacznyj 14and Lawrence C. Paulson, based on @{cite davenport92}. They introduced 15gcd, lcm, and prime for the natural numbers. 16 17The original theory "IntPrimes" was by Thomas M. Rasmussen, and 18extended gcd, lcm, primes to the integers. Amine Chaieb provided 19another extension of the notions to the integers, and added a number 20of results to "Primes" and "GCD". 21 22The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and 23developed the congruence relations on the integers. The notion was 24extended to the natural numbers by Chaieb. Jeremy Avigad combined 25these, revised and tidied them, made the development uniform for the 26natural numbers and the integers, and added a number of new theorems. 27*) 28 29section \<open>Congruence\<close> 30 31theory Cong 32 imports "HOL-Computational_Algebra.Primes" 33begin 34 35subsection \<open>Generic congruences\<close> 36 37context unique_euclidean_semiring 38begin 39 40definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ = _] '(' mod _'))\<close>) 41 where "cong b c a \<longleftrightarrow> b mod a = c mod a" 42 43abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>) 44 where "notcong b c a \<equiv> \<not> cong b c a" 45 46lemma cong_refl [simp]: 47 "[b = b] (mod a)" 48 by (simp add: cong_def) 49 50lemma cong_sym: 51 "[b = c] (mod a) \<Longrightarrow> [c = b] (mod a)" 52 by (simp add: cong_def) 53 54lemma cong_sym_eq: 55 "[b = c] (mod a) \<longleftrightarrow> [c = b] (mod a)" 56 by (auto simp add: cong_def) 57 58lemma cong_trans [trans]: 59 "[b = c] (mod a) \<Longrightarrow> [c = d] (mod a) \<Longrightarrow> [b = d] (mod a)" 60 by (simp add: cong_def) 61 62lemma cong_mult_self_right: 63 "[b * a = 0] (mod a)" 64 by (simp add: cong_def) 65 66lemma cong_mult_self_left: 67 "[a * b = 0] (mod a)" 68 by (simp add: cong_def) 69 70lemma cong_mod_left [simp]: 71 "[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)" 72 by (simp add: cong_def) 73 74lemma cong_mod_right [simp]: 75 "[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)" 76 by (simp add: cong_def) 77 78lemma cong_0 [simp, presburger]: 79 "[b = c] (mod 0) \<longleftrightarrow> b = c" 80 by (simp add: cong_def) 81 82lemma cong_1 [simp, presburger]: 83 "[b = c] (mod 1)" 84 by (simp add: cong_def) 85 86lemma cong_dvd_iff: 87 "a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)" 88 using that by (auto simp: cong_def dvd_eq_mod_eq_0) 89 90lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b" 91 by (simp add: cong_def dvd_eq_mod_eq_0) 92 93lemma cong_add: 94 "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b + d = c + e] (mod a)" 95 by (auto simp add: cong_def intro: mod_add_cong) 96 97lemma cong_mult: 98 "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b * d = c * e] (mod a)" 99 by (auto simp add: cong_def intro: mod_mult_cong) 100 101lemma cong_scalar_right: 102 "[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)" 103 by (simp add: cong_mult) 104 105lemma cong_scalar_left: 106 "[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)" 107 by (simp add: cong_mult) 108 109lemma cong_pow: 110 "[b = c] (mod a) \<Longrightarrow> [b ^ n = c ^ n] (mod a)" 111 by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a]) 112 113lemma cong_sum: 114 "[sum f A = sum g A] (mod a)" if "\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a)" 115 using that by (induct A rule: infinite_finite_induct) (auto intro: cong_add) 116 117lemma cong_prod: 118 "[prod f A = prod g A] (mod a)" if "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a))" 119 using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult) 120 121lemma mod_mult_cong_right: 122 "[c mod (a * b) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)" 123 by (simp add: cong_def mod_mod_cancel mod_add_left_eq) 124 125lemma mod_mult_cong_left: 126 "[c mod (b * a) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)" 127 using mod_mult_cong_right [of c a b d] by (simp add: ac_simps) 128 129end 130 131context unique_euclidean_ring 132begin 133 134lemma cong_diff: 135 "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b - d = c - e] (mod a)" 136 by (auto simp add: cong_def intro: mod_diff_cong) 137 138lemma cong_diff_iff_cong_0: 139 "[b - c = 0] (mod a) \<longleftrightarrow> [b = c] (mod a)" (is "?P \<longleftrightarrow> ?Q") 140proof 141 assume ?P 142 then have "[b - c + c = 0 + c] (mod a)" 143 by (rule cong_add) simp 144 then show ?Q 145 by simp 146next 147 assume ?Q 148 with cong_diff [of b c a c c] show ?P 149 by simp 150qed 151 152lemma cong_minus_minus_iff: 153 "[- b = - c] (mod a) \<longleftrightarrow> [b = c] (mod a)" 154 using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a] 155 by (simp add: cong_0_iff dvd_diff_commute) 156 157lemma cong_modulus_minus_iff [iff]: 158 "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)" 159 using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"] 160 by (simp add: cong_0_iff) 161 162lemma cong_iff_dvd_diff: 163 "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" 164 by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0) 165 166lemma cong_iff_lin: 167 "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" (is "?P \<longleftrightarrow> ?Q") 168proof - 169 have "?P \<longleftrightarrow> m dvd b - a" 170 by (simp add: cong_iff_dvd_diff dvd_diff_commute) 171 also have "\<dots> \<longleftrightarrow> ?Q" 172 by (auto simp add: algebra_simps elim!: dvdE) 173 finally show ?thesis 174 by simp 175qed 176 177lemma cong_add_lcancel: 178 "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 179 by (simp add: cong_iff_lin algebra_simps) 180 181lemma cong_add_rcancel: 182 "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" 183 by (simp add: cong_iff_lin algebra_simps) 184 185lemma cong_add_lcancel_0: 186 "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 187 using cong_add_lcancel [of a x 0 n] by simp 188 189lemma cong_add_rcancel_0: 190 "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 191 using cong_add_rcancel [of x a 0 n] by simp 192 193lemma cong_dvd_modulus: 194 "[x = y] (mod n)" if "[x = y] (mod m)" and "n dvd m" 195 using that by (auto intro: dvd_trans simp add: cong_iff_dvd_diff) 196 197lemma cong_modulus_mult: 198 "[x = y] (mod m)" if "[x = y] (mod m * n)" 199 using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left) 200 201end 202 203lemma cong_abs [simp]: 204 "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)" 205 for x y :: "'a :: {unique_euclidean_ring, linordered_idom}" 206 by (simp add: cong_iff_dvd_diff) 207 208lemma cong_square: 209 "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)" 210 for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}" 211 by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest: prime_dvd_multD) 212 213lemma cong_mult_rcancel: 214 "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" 215 if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}" 216 using that by (auto simp add: cong_iff_dvd_diff left_diff_distrib [symmetric] ac_simps coprime_dvd_mult_right_iff) 217 218lemma cong_mult_lcancel: 219 "[k * a = k * b] (mod m) = [a = b] (mod m)" 220 if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}" 221 using that cong_mult_rcancel [of k m a b] by (simp add: ac_simps) 222 223lemma coprime_cong_mult: 224 "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" 225 for a b :: "'a :: {unique_euclidean_ring, semiring_gcd}" 226 by (simp add: cong_iff_dvd_diff divides_mult) 227 228lemma cong_gcd_eq: 229 "gcd a m = gcd b m" if "[a = b] (mod m)" 230 for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}" 231proof (cases "m = 0") 232 case True 233 with that show ?thesis 234 by simp 235next 236 case False 237 moreover have "gcd (a mod m) m = gcd (b mod m) m" 238 using that by (simp add: cong_def) 239 ultimately show ?thesis 240 by simp 241qed 242 243lemma cong_imp_coprime: 244 "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m" 245 for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}" 246 by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq) 247 248lemma cong_cong_prod_coprime: 249 "[x = y] (mod (\<Prod>i\<in>A. m i))" if 250 "(\<forall>i\<in>A. [x = y] (mod m i))" 251 "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" 252 for x y :: "'a :: {unique_euclidean_ring, semiring_gcd}" 253 using that by (induct A rule: infinite_finite_induct) 254 (auto intro!: coprime_cong_mult prod_coprime_right) 255 256 257subsection \<open>Congruences on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close> 258 259lemma cong_int_iff: 260 "[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)" 261 by (simp add: cong_def of_nat_mod [symmetric]) 262 263lemma cong_Suc_0 [simp, presburger]: 264 "[m = n] (mod Suc 0)" 265 using cong_1 [of m n] by simp 266 267lemma cong_diff_nat: 268 "[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)" 269 and "a \<ge> c" "b \<ge> d" for a b c d m :: nat 270proof - 271 have "[c + (a - c) = d + (b - d)] (mod m)" 272 using that by simp 273 with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)" 274 using mod_add_cong by (auto simp add: cong_def) fastforce 275 then show ?thesis 276 by (simp add: cong_def nat_mod_eq_iff) 277qed 278 279lemma cong_diff_iff_cong_0_nat: 280 "[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat 281 using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma) 282 283lemma cong_diff_iff_cong_0_nat': 284 "[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" 285proof (cases "b \<le> a") 286 case True 287 then show ?thesis 288 by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m]) 289next 290 case False 291 then have "a \<le> b" 292 by simp 293 then show ?thesis 294 by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m]) 295 (auto simp add: cong_def) 296qed 297 298lemma cong_altdef_nat: 299 "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)" 300 for a b :: nat 301 by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat) 302 303lemma cong_altdef_nat': 304 "[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>" 305 using cong_diff_iff_cong_0_nat' [of a b m] 306 by (simp only: cong_0_iff [symmetric]) 307 308lemma cong_mult_rcancel_nat: 309 "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)" 310 if "coprime k m" for a k m :: nat 311proof - 312 have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>" 313 by (simp add: cong_altdef_nat') 314 also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>" 315 by (simp add: algebra_simps) 316 also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k" 317 by (simp add: abs_mult nat_times_as_int) 318 also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>" 319 by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>) 320 also have "\<dots> \<longleftrightarrow> [a = b] (mod m)" 321 by (simp add: cong_altdef_nat') 322 finally show ?thesis . 323qed 324 325lemma cong_mult_lcancel_nat: 326 "[k * a = k * b] (mod m) = [a = b] (mod m)" 327 if "coprime k m" for a k m :: nat 328 using that by (simp add: cong_mult_rcancel_nat ac_simps) 329 330lemma coprime_cong_mult_nat: 331 "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)" 332 for a b :: nat 333 by (simp add: cong_altdef_nat' divides_mult) 334 335lemma cong_less_imp_eq_nat: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" 336 for a b :: nat 337 by (auto simp add: cong_def) 338 339lemma cong_less_imp_eq_int: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b" 340 for a b :: int 341 by (auto simp add: cong_def) 342 343lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 344 for a m :: nat 345 by (auto simp: cong_def) (metis mod_less_divisor mod_mod_trivial) 346 347lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 348 for a m :: int 349 by (auto simp: cong_def) (metis mod_mod_trivial pos_mod_conj) 350 351lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" 352 (is "?lhs = ?rhs") 353 for a b :: nat 354proof 355 assume ?lhs 356 show ?rhs 357 proof (cases "b \<le> a") 358 case True 359 with \<open>?lhs\<close> show ?rhs 360 by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute) 361 next 362 case False 363 with \<open>?lhs\<close> show ?rhs 364 by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma) 365 qed 366next 367 assume ?rhs 368 then show ?lhs 369 by (metis cong_def mult.commute nat_mod_eq_iff) 370qed 371 372lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" 373 for a b :: nat 374 by simp 375 376lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)" 377 for a b :: int 378 by simp 379 380lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 381 for a x y :: nat 382 by (simp add: cong_iff_lin_nat) 383 384lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)" 385 for a x y :: nat 386 by (simp add: cong_iff_lin_nat) 387 388lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 389 for a x :: nat 390 using cong_add_lcancel_nat [of a x 0 n] by simp 391 392lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 393 for a x :: nat 394 using cong_add_rcancel_nat [of x a 0 n] by simp 395 396lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)" 397 for x y :: nat 398 unfolding cong_iff_lin_nat dvd_def 399 by (metis mult.commute mult.left_commute) 400 401lemma cong_to_1_nat: 402 fixes a :: nat 403 assumes "[a = 1] (mod n)" 404 shows "n dvd (a - 1)" 405proof (cases "a = 0") 406 case True 407 then show ?thesis by force 408next 409 case False 410 with assms show ?thesis by (metis cong_altdef_nat leI less_one) 411qed 412 413lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0" 414 by (auto simp: cong_def) 415 416lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1" 417 for n :: nat 418 by (auto simp: cong_def) 419 420lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1" 421 for n :: int 422 by (auto simp: cong_def zmult_eq_1_iff) 423 424lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)" 425 for a :: nat 426 by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat 427 dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if) 428 429lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)" 430 for x y :: nat 431 by (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE) 432 433 434lemma cong_solve_nat: 435 fixes a :: nat 436 shows "\<exists>x. [a * x = gcd a n] (mod n)" 437proof (cases "a = 0 \<or> n = 0") 438 case True 439 then show ?thesis 440 by (force simp add: cong_0_iff cong_sym) 441next 442 case False 443 then show ?thesis 444 using bezout_nat [of a n] 445 by auto (metis cong_add_rcancel_0_nat cong_mult_self_left) 446qed 447 448lemma cong_solve_int: 449 fixes a :: int 450 shows "\<exists>x. [a * x = gcd a n] (mod n)" 451 by (metis bezout_int cong_iff_lin mult.commute) 452 453lemma cong_solve_dvd_nat: 454 fixes a :: nat 455 assumes "gcd a n dvd d" 456 shows "\<exists>x. [a * x = d] (mod n)" 457proof - 458 from cong_solve_nat [of a] obtain x where "[a * x = gcd a n](mod n)" 459 by auto 460 then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 461 using cong_scalar_left by blast 462 also from assms have "(d div gcd a n) * gcd a n = d" 463 by (rule dvd_div_mult_self) 464 also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" 465 by auto 466 finally show ?thesis 467 by auto 468qed 469 470lemma cong_solve_dvd_int: 471 fixes a::int 472 assumes b: "gcd a n dvd d" 473 shows "\<exists>x. [a * x = d] (mod n)" 474proof - 475 from cong_solve_int [of a] obtain x where "[a * x = gcd a n](mod n)" 476 by auto 477 then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 478 using cong_scalar_left by blast 479 also from b have "(d div gcd a n) * gcd a n = d" 480 by (rule dvd_div_mult_self) 481 also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)" 482 by auto 483 finally show ?thesis 484 by auto 485qed 486 487lemma cong_solve_coprime_nat: 488 "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n" 489 using that cong_solve_nat [of a n] by auto 490 491lemma cong_solve_coprime_int: 492 "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int 493 using that cong_solve_int [of a n] by (auto simp add: zabs_def split: if_splits) 494 495lemma coprime_iff_invertible_nat: 496 "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))" (is "?P \<longleftrightarrow> ?Q") 497proof 498 assume ?P then show ?Q 499 by (auto dest!: cong_solve_coprime_nat) 500next 501 assume ?Q 502 then obtain b where "[a * b = Suc 0] (mod m)" 503 by blast 504 with coprime_mod_left_iff [of m "a * b"] show ?P 505 by (cases "m = 0 \<or> m = 1") 506 (unfold cong_def, auto simp add: cong_def) 507qed 508 509lemma coprime_iff_invertible_int: 510 "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))" (is "?P \<longleftrightarrow> ?Q") for m :: int 511proof 512 assume ?P then show ?Q 513 by (auto dest: cong_solve_coprime_int) 514next 515 assume ?Q 516 then obtain b where "[a * b = 1] (mod m)" 517 by blast 518 with coprime_mod_left_iff [of m "a * b"] show ?P 519 by (cases "m = 0 \<or> m = 1") 520 (unfold cong_def, auto simp add: zmult_eq_1_iff) 521qed 522 523lemma coprime_iff_invertible'_nat: 524 assumes "m > 0" 525 shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))" 526proof - 527 have "\<And>b. \<lbrakk>0 < m; [a * b = Suc 0] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = Suc 0] (mod m)" 528 by (metis cong_def mod_less_divisor [OF assms] mod_mult_right_eq) 529 then show ?thesis 530 using assms coprime_iff_invertible_nat by auto 531qed 532 533lemma coprime_iff_invertible'_int: 534 fixes m :: int 535 assumes "m > 0" 536 shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))" 537proof - 538 have "\<And>b. \<lbrakk>0 < m; [a * b = 1] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = 1] (mod m)" 539 by (meson cong_less_unique_int cong_scalar_left cong_sym cong_trans) 540 then show ?thesis 541 by (metis assms coprime_iff_invertible_int cong_def cong_mult_lcancel mod_pos_pos_trivial pos_mod_conj) 542qed 543 544lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" 545 for x y :: nat 546 by (meson cong_altdef_nat' lcm_least) 547 548lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)" 549 for x y :: int 550 by (auto simp add: cong_iff_dvd_diff lcm_least) 551 552lemma cong_cong_prod_coprime_nat: 553 "[x = y] (mod (\<Prod>i\<in>A. m i))" if 554 "(\<forall>i\<in>A. [x = y] (mod m i))" 555 "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))" 556 for x y :: nat 557 using that by (induct A rule: infinite_finite_induct) 558 (auto intro!: coprime_cong_mult_nat prod_coprime_right) 559 560lemma binary_chinese_remainder_nat: 561 fixes m1 m2 :: nat 562 assumes a: "coprime m1 m2" 563 shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" 564proof - 565 have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" 566 proof - 567 from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" 568 by auto 569 from a have b: "coprime m2 m1" 570 by (simp add: ac_simps) 571 from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" 572 by auto 573 have "[m1 * x1 = 0] (mod m1)" 574 by (simp add: cong_mult_self_left) 575 moreover have "[m2 * x2 = 0] (mod m2)" 576 by (simp add: cong_mult_self_left) 577 ultimately show ?thesis 578 using 1 2 by blast 579 qed 580 then obtain b1 b2 581 where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" 582 and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" 583 by blast 584 let ?x = "u1 * b1 + u2 * b2" 585 have "[?x = u1 * 1 + u2 * 0] (mod m1)" 586 using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast 587 then have "[?x = u1] (mod m1)" by simp 588 have "[?x = u1 * 0 + u2 * 1] (mod m2)" 589 using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast 590 then have "[?x = u2] (mod m2)" 591 by simp 592 with \<open>[?x = u1] (mod m1)\<close> show ?thesis 593 by blast 594qed 595 596lemma binary_chinese_remainder_int: 597 fixes m1 m2 :: int 598 assumes a: "coprime m1 m2" 599 shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" 600proof - 601 have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" 602 proof - 603 from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" 604 by auto 605 from a have b: "coprime m2 m1" 606 by (simp add: ac_simps) 607 from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" 608 by auto 609 have "[m1 * x1 = 0] (mod m1)" 610 by (simp add: cong_mult_self_left) 611 moreover have "[m2 * x2 = 0] (mod m2)" 612 by (simp add: cong_mult_self_left) 613 ultimately show ?thesis 614 using 1 2 by blast 615 qed 616 then obtain b1 b2 617 where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" 618 and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" 619 by blast 620 let ?x = "u1 * b1 + u2 * b2" 621 have "[?x = u1 * 1 + u2 * 0] (mod m1)" 622 using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast 623 then have "[?x = u1] (mod m1)" by simp 624 have "[?x = u1 * 0 + u2 * 1] (mod m2)" 625 using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast 626 then have "[?x = u2] (mod m2)" by simp 627 with \<open>[?x = u1] (mod m1)\<close> show ?thesis 628 by blast 629qed 630 631lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)" 632 for x y :: nat 633 by (metis cong_def mod_mult_cong_right) 634 635lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y" 636 for x y :: nat 637 by (simp add: cong_def) 638 639lemma binary_chinese_remainder_unique_nat: 640 fixes m1 m2 :: nat 641 assumes a: "coprime m1 m2" 642 and nz: "m1 \<noteq> 0" "m2 \<noteq> 0" 643 shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)" 644proof - 645 obtain y where y1: "[y = u1] (mod m1)" and y2: "[y = u2] (mod m2)" 646 using binary_chinese_remainder_nat [OF a] by blast 647 let ?x = "y mod (m1 * m2)" 648 from nz have less: "?x < m1 * m2" 649 by auto 650 have 1: "[?x = u1] (mod m1)" 651 using y1 mod_mult_cong_right by blast 652 have 2: "[?x = u2] (mod m2)" 653 using y2 mod_mult_cong_left by blast 654 have "z = ?x" if "z < m1 * m2" "[z = u1] (mod m1)" "[z = u2] (mod m2)" for z 655 proof - 656 have "[?x = z] (mod m1)" 657 by (metis "1" cong_def that(2)) 658 moreover have "[?x = z] (mod m2)" 659 by (metis "2" cong_def that(3)) 660 ultimately have "[?x = z] (mod m1 * m2)" 661 using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right) 662 with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x" 663 by (auto simp add: cong_def) 664 qed 665 with less 1 2 show ?thesis 666 by blast 667 qed 668 669lemma chinese_remainder_nat: 670 fixes A :: "'a set" 671 and m :: "'a \<Rightarrow> nat" 672 and u :: "'a \<Rightarrow> nat" 673 assumes fin: "finite A" 674 and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" 675 shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)" 676proof - 677 have "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))" 678 proof (rule finite_set_choice, rule fin, rule ballI) 679 fix i 680 assume "i \<in> A" 681 with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)" 682 by (intro prod_coprime_left) auto 683 then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)" 684 by (elim cong_solve_coprime_nat) 685 then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)" 686 by auto 687 moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))" 688 by (simp add: cong_0_iff) 689 ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))" 690 by blast 691 qed 692 then obtain b where b: "\<And>i. i \<in> A \<Longrightarrow> [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))" 693 by blast 694 let ?x = "\<Sum>i\<in>A. (u i) * (b i)" 695 show ?thesis 696 proof (rule exI, clarify) 697 fix i 698 assume a: "i \<in> A" 699 show "[?x = u i] (mod m i)" 700 proof - 701 from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) + (\<Sum>j \<in> A - {i}. u j * b j)" 702 by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong) 703 then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)" 704 by auto 705 also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) = 706 u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)" 707 proof (intro cong_add cong_scalar_left cong_sum) 708 show "[b i = 1] (mod m i)" 709 using a b by blast 710 show "[b x = 0] (mod m i)" if "x \<in> A - {i}" for x 711 proof - 712 have "x \<in> A" "x \<noteq> i" 713 using that by auto 714 then show ?thesis 715 using a b [OF \<open>x \<in> A\<close>] cong_dvd_modulus_nat fin by blast 716 qed 717 qed 718 finally show ?thesis 719 by simp 720 qed 721 qed 722qed 723 724lemma coprime_cong_prod_nat: "[x = y] (mod (\<Prod>i\<in>A. m i))" 725 if "\<And>i j. \<lbrakk>i \<in> A; j \<in> A; i \<noteq> j\<rbrakk> \<Longrightarrow> coprime (m i) (m j)" 726 and "\<And>i. i \<in> A \<Longrightarrow> [x = y] (mod m i)" for x y :: nat 727 using that 728proof (induct A rule: infinite_finite_induct) 729 case (insert x A) 730 then show ?case 731 by simp (metis coprime_cong_mult_nat prod_coprime_right) 732qed auto 733 734lemma chinese_remainder_unique_nat: 735 fixes A :: "'a set" 736 and m :: "'a \<Rightarrow> nat" 737 and u :: "'a \<Rightarrow> nat" 738 assumes fin: "finite A" 739 and nz: "\<forall>i\<in>A. m i \<noteq> 0" 740 and cop: "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" 741 shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))" 742proof - 743 from chinese_remainder_nat [OF fin cop] 744 obtain y where one: "(\<forall>i\<in>A. [y = u i] (mod m i))" 745 by blast 746 let ?x = "y mod (\<Prod>i\<in>A. m i)" 747 from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0" 748 by auto 749 then have less: "?x < (\<Prod>i\<in>A. m i)" 750 by auto 751 have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)" 752 using fin one 753 by (auto simp add: cong_def dvd_prod_eqI mod_mod_cancel) 754 have unique: "\<forall>z. z < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = ?x" 755 proof clarify 756 fix z 757 assume zless: "z < (\<Prod>i\<in>A. m i)" 758 assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))" 759 have "\<forall>i\<in>A. [?x = z] (mod m i)" 760 using cong zcong by (auto simp add: cong_def) 761 with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))" 762 by (intro coprime_cong_prod_nat) auto 763 with zless less show "z = ?x" 764 by (auto simp add: cong_def) 765 qed 766 from less cong unique show ?thesis 767 by blast 768qed 769 770end 771