1.1 --- a/src/HOL/Number_Theory/Cong.thy Fri Dec 01 20:49:42 2017 +0100
1.2 +++ b/src/HOL/Number_Theory/Cong.thy Sat Dec 02 16:50:53 2017 +0000
1.3 @@ -154,7 +154,7 @@
1.4 using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
1.5 by (simp add: cong_0_iff dvd_diff_commute)
1.6
1.7 -lemma cong_modulus_minus_iff:
1.8 +lemma cong_modulus_minus_iff [iff]:
1.9 "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
1.10 using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]
1.11 by (simp add: cong_0_iff)
1.12 @@ -174,8 +174,85 @@
1.13 by simp
1.14 qed
1.15
1.16 +lemma cong_add_lcancel:
1.17 + "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.18 + by (simp add: cong_iff_lin algebra_simps)
1.19 +
1.20 +lemma cong_add_rcancel:
1.21 + "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.22 + by (simp add: cong_iff_lin algebra_simps)
1.23 +
1.24 +lemma cong_add_lcancel_0:
1.25 + "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.26 + using cong_add_lcancel [of a x 0 n] by simp
1.27 +
1.28 +lemma cong_add_rcancel_0:
1.29 + "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.30 + using cong_add_rcancel [of x a 0 n] by simp
1.31 +
1.32 +lemma cong_dvd_modulus:
1.33 + "[x = y] (mod n)" if "[x = y] (mod m)" and "n dvd m"
1.34 + using that by (auto intro: dvd_trans simp add: cong_iff_dvd_diff)
1.35 +
1.36 +lemma cong_modulus_mult:
1.37 + "[x = y] (mod m)" if "[x = y] (mod m * n)"
1.38 + using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left)
1.39 +
1.40 end
1.41
1.42 +lemma cong_abs [simp]:
1.43 + "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
1.44 + for x y :: "'a :: {unique_euclidean_ring, linordered_idom}"
1.45 + by (simp add: cong_iff_dvd_diff)
1.46 +
1.47 +lemma cong_square:
1.48 + "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
1.49 + for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}"
1.50 + by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest: prime_dvd_multD)
1.51 +
1.52 +lemma cong_mult_rcancel:
1.53 + "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
1.54 + if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
1.55 + using that by (auto simp add: cong_iff_dvd_diff left_diff_distrib [symmetric] ac_simps coprime_dvd_mult_right_iff)
1.56 +
1.57 +lemma cong_mult_lcancel:
1.58 + "[k * a = k * b] (mod m) = [a = b] (mod m)"
1.59 + if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
1.60 + using that cong_mult_rcancel [of k m a b] by (simp add: ac_simps)
1.61 +
1.62 +lemma coprime_cong_mult:
1.63 + "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
1.64 + for a b :: "'a :: {unique_euclidean_ring, semiring_gcd}"
1.65 + by (simp add: cong_iff_dvd_diff divides_mult)
1.66 +
1.67 +lemma cong_gcd_eq:
1.68 + "gcd a m = gcd b m" if "[a = b] (mod m)"
1.69 + for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
1.70 +proof (cases "m = 0")
1.71 + case True
1.72 + with that show ?thesis
1.73 + by simp
1.74 +next
1.75 + case False
1.76 + moreover have "gcd (a mod m) m = gcd (b mod m) m"
1.77 + using that by (simp add: cong_def)
1.78 + ultimately show ?thesis
1.79 + by simp
1.80 +qed
1.81 +
1.82 +lemma cong_imp_coprime:
1.83 + "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.84 + for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
1.85 + by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq)
1.86 +
1.87 +lemma cong_cong_prod_coprime:
1.88 + "[x = y] (mod (\<Prod>i\<in>A. m i))" if
1.89 + "(\<forall>i\<in>A. [x = y] (mod m i))"
1.90 + "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
1.91 + for x y :: "'a :: {unique_euclidean_ring, semiring_gcd}"
1.92 + using that by (induct A rule: infinite_finite_induct)
1.93 + (auto intro!: coprime_cong_mult prod_coprime_right)
1.94 +
1.95
1.96 subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
1.97
1.98 @@ -228,29 +305,6 @@
1.99 using cong_diff_iff_cong_0_nat' [of a b m]
1.100 by (simp only: cong_0_iff [symmetric])
1.101
1.102 -lemma cong_altdef_int:
1.103 - "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
1.104 - for a b :: int
1.105 - by (fact cong_iff_dvd_diff)
1.106 -
1.107 -lemma cong_abs_int [simp]: "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
1.108 - for x y :: int
1.109 - by (simp add: cong_iff_dvd_diff)
1.110 -
1.111 -lemma cong_square_int:
1.112 - "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
1.113 - for a :: int
1.114 - apply (simp only: cong_iff_dvd_diff)
1.115 - apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
1.116 - apply (auto simp add: field_simps)
1.117 - done
1.118 -
1.119 -lemma cong_mult_rcancel_int:
1.120 - "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
1.121 - if "coprime k m" for a k m :: int
1.122 - using that by (simp add: cong_altdef_int)
1.123 - (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib')
1.124 -
1.125 lemma cong_mult_rcancel_nat:
1.126 "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
1.127 if "coprime k m" for a k m :: nat
1.128 @@ -268,21 +322,11 @@
1.129 finally show ?thesis .
1.130 qed
1.131
1.132 -lemma cong_mult_lcancel_int:
1.133 - "[k * a = k * b] (mod m) = [a = b] (mod m)"
1.134 - if "coprime k m" for a k m :: int
1.135 - using that by (simp add: cong_mult_rcancel_int ac_simps)
1.136 -
1.137 lemma cong_mult_lcancel_nat:
1.138 "[k * a = k * b] (mod m) = [a = b] (mod m)"
1.139 if "coprime k m" for a k m :: nat
1.140 using that by (simp add: cong_mult_rcancel_nat ac_simps)
1.141
1.142 -lemma coprime_cong_mult_int:
1.143 - "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
1.144 - for a b :: int
1.145 - by (simp add: cong_altdef_int divides_mult)
1.146 -
1.147 lemma coprime_cong_mult_nat:
1.148 "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
1.149 for a b :: nat
1.150 @@ -304,10 +348,6 @@
1.151 for a m :: int
1.152 by (auto simp: cong_def) (metis mod_mod_trivial pos_mod_conj)
1.153
1.154 -lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
1.155 - for a b :: int
1.156 - by (fact cong_iff_lin)
1.157 -
1.158 lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
1.159 (is "?lhs = ?rhs")
1.160 for a b :: nat
1.161 @@ -329,22 +369,6 @@
1.162 by (metis cong_def mult.commute nat_mod_eq_iff)
1.163 qed
1.164
1.165 -lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.166 - for a b :: nat
1.167 - by (auto simp add: cong_def) (metis gcd_red_nat)
1.168 -
1.169 -lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.170 - for a b :: int
1.171 - by (auto simp add: cong_def) (metis gcd_red_int)
1.172 -
1.173 -lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.174 - for a b :: nat
1.175 - by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_nat)
1.176 -
1.177 -lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.178 - for a b :: int
1.179 - by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_int)
1.180 -
1.181 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
1.182 for a b :: nat
1.183 by simp
1.184 @@ -353,42 +377,22 @@
1.185 for a b :: int
1.186 by simp
1.187
1.188 -lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
1.189 - for a b :: int
1.190 - by (fact cong_modulus_minus_iff)
1.191 -
1.192 lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.193 for a x y :: nat
1.194 by (simp add: cong_iff_lin_nat)
1.195
1.196 -lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.197 - for a x y :: int
1.198 - by (simp add: cong_iff_lin_int)
1.199 -
1.200 lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.201 for a x y :: nat
1.202 by (simp add: cong_iff_lin_nat)
1.203
1.204 -lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.205 - for a x y :: int
1.206 - by (simp add: cong_iff_lin_int)
1.207 -
1.208 lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.209 for a x :: nat
1.210 using cong_add_lcancel_nat [of a x 0 n] by simp
1.211
1.212 -lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.213 - for a x :: int
1.214 - using cong_add_lcancel_int [of a x 0 n] by simp
1.215 -
1.216 lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.217 for a x :: nat
1.218 using cong_add_rcancel_nat [of x a 0 n] by simp
1.219
1.220 -lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.221 - for a x :: int
1.222 - using cong_add_rcancel_int [of x a 0 n] by simp
1.223 -
1.224 lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
1.225 for x y :: nat
1.226 apply (auto simp add: cong_iff_lin_nat dvd_def)
1.227 @@ -397,10 +401,6 @@
1.228 apply (simp add: field_simps)
1.229 done
1.230
1.231 -lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
1.232 - for x y :: int
1.233 - by (auto simp add: cong_altdef_int dvd_def)
1.234 -
1.235 lemma cong_to_1_nat:
1.236 fixes a :: nat
1.237 assumes "[a = 1] (mod n)"
1.238 @@ -455,7 +455,7 @@
1.239 apply (rule_tac x = "-1" in exI)
1.240 apply auto
1.241 apply (insert bezout_int [of a n], auto)
1.242 - apply (metis cong_iff_lin_int mult.commute)
1.243 + apply (metis cong_iff_lin mult.commute)
1.244 done
1.245
1.246 lemma cong_solve_dvd_nat:
1.247 @@ -553,25 +553,15 @@
1.248
1.249 lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
1.250 for x y :: int
1.251 - by (auto simp add: cong_altdef_int lcm_least)
1.252 + by (auto simp add: cong_iff_dvd_diff lcm_least)
1.253
1.254 lemma cong_cong_prod_coprime_nat:
1.255 "[x = y] (mod (\<Prod>i\<in>A. m i))" if
1.256 - "(\<forall>i\<in>A. [(x::nat) = y] (mod m i))"
1.257 - and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
1.258 - using that apply (induct A rule: infinite_finite_induct)
1.259 - apply auto
1.260 - apply (metis coprime_cong_mult_nat prod_coprime_right)
1.261 - done
1.262 -
1.263 -lemma cong_cong_prod_coprime_int:
1.264 - "[x = y] (mod (\<Prod>i\<in>A. m i))" if
1.265 - "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
1.266 + "(\<forall>i\<in>A. [x = y] (mod m i))"
1.267 "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
1.268 - using that apply (induct A rule: infinite_finite_induct)
1.269 - apply auto
1.270 - apply (metis coprime_cong_mult_int prod_coprime_right)
1.271 - done
1.272 + for x y :: nat
1.273 + using that by (induct A rule: infinite_finite_induct)
1.274 + (auto intro!: coprime_cong_mult_nat prod_coprime_right)
1.275
1.276 lemma binary_chinese_remainder_nat:
1.277 fixes m1 m2 :: nat
1.278 @@ -651,12 +641,6 @@
1.279 apply (metis cong_def mod_mult_cong_right)
1.280 done
1.281
1.282 -lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
1.283 - for x y :: int
1.284 - apply (simp add: cong_altdef_int)
1.285 - apply (erule dvd_mult_left)
1.286 - done
1.287 -
1.288 lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
1.289 for x y :: nat
1.290 by (simp add: cong_def)
1.291 @@ -811,4 +795,94 @@
1.292 by blast
1.293 qed
1.294
1.295 +
1.296 +subsection \<open>Aliasses\<close>
1.297 +
1.298 +lemma cong_altdef_int:
1.299 + "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
1.300 + for a b :: int
1.301 + by (fact cong_iff_dvd_diff)
1.302 +
1.303 +lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
1.304 + for a b :: int
1.305 + by (fact cong_iff_lin)
1.306 +
1.307 +lemma cong_minus_int: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
1.308 + for a b :: int
1.309 + by (fact cong_modulus_minus_iff)
1.310 +
1.311 +lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.312 + for a x y :: int
1.313 + by (fact cong_add_lcancel)
1.314 +
1.315 +lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
1.316 + for a x y :: int
1.317 + by (fact cong_add_rcancel)
1.318 +
1.319 +lemma cong_add_lcancel_0_int:
1.320 + "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.321 + for a x :: int
1.322 + by (fact cong_add_lcancel_0)
1.323 +
1.324 +lemma cong_add_rcancel_0_int:
1.325 + "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
1.326 + for a x :: int
1.327 + by (fact cong_add_rcancel_0)
1.328 +
1.329 +lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
1.330 + for x y :: int
1.331 + by (fact cong_dvd_modulus)
1.332 +
1.333 +lemma cong_abs_int:
1.334 + "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
1.335 + for x y :: int
1.336 + by (fact cong_abs)
1.337 +
1.338 +lemma cong_square_int:
1.339 + "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
1.340 + for a :: int
1.341 + by (fact cong_square)
1.342 +
1.343 +lemma cong_mult_rcancel_int:
1.344 + "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
1.345 + if "coprime k m" for a k m :: int
1.346 + using that by (fact cong_mult_rcancel)
1.347 +
1.348 +lemma cong_mult_lcancel_int:
1.349 + "[k * a = k * b] (mod m) = [a = b] (mod m)"
1.350 + if "coprime k m" for a k m :: int
1.351 + using that by (fact cong_mult_lcancel)
1.352 +
1.353 +lemma coprime_cong_mult_int:
1.354 + "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
1.355 + for a b :: int
1.356 + by (fact coprime_cong_mult)
1.357 +
1.358 +lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.359 + for a b :: nat
1.360 + by (fact cong_gcd_eq)
1.361 +
1.362 +lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
1.363 + for a b :: int
1.364 + by (fact cong_gcd_eq)
1.365 +
1.366 +lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.367 + for a b :: nat
1.368 + by (fact cong_imp_coprime)
1.369 +
1.370 +lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.371 + for a b :: int
1.372 + by (fact cong_imp_coprime)
1.373 +
1.374 +lemma cong_cong_prod_coprime_int:
1.375 + "[x = y] (mod (\<Prod>i\<in>A. m i))" if
1.376 + "(\<forall>i\<in>A. [x = y] (mod m i))"
1.377 + "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
1.378 + for x y :: int
1.379 + using that by (fact cong_cong_prod_coprime)
1.380 +
1.381 +lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
1.382 + for x y :: int
1.383 + by (fact cong_modulus_mult)
1.384 +
1.385 end