generalized more lemmas
authorhaftmann
Sat Dec 02 16:50:53 2017 +0000 (7 weeks ago)
changeset 671152977773a481c
parent 67114 3d8626cbaff8
child 67116 7397a6df81d8
generalized more lemmas
src/HOL/Number_Theory/Cong.thy
     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