algebraic foundation for congruences
authorhaftmann
Fri Oct 20 20:57:55 2017 +0200 (21 months ago)
changeset 66888930abfdf8727
parent 66887 72b78ee82f7b
child 66889 7fe528893a6c
algebraic foundation for congruences
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Euler_Criterion.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/Totient.thy
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Fri Oct 20 23:29:43 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Fri Oct 20 20:57:55 2017 +0200
     1.3 @@ -32,236 +32,187 @@
     1.4    imports "HOL-Computational_Algebra.Primes"
     1.5  begin
     1.6  
     1.7 -subsection \<open>Turn off \<open>One_nat_def\<close>\<close>
     1.8 -
     1.9 -lemma power_eq_one_eq_nat [simp]: "x^m = 1 \<longleftrightarrow> m = 0 \<or> x = 1"
    1.10 -  for x m :: nat
    1.11 -  by (induct m) auto
    1.12 -
    1.13 -declare mod_pos_pos_trivial [simp]
    1.14 -
    1.15 -
    1.16 -subsection \<open>Main definitions\<close>
    1.17 -
    1.18 -class cong =
    1.19 -  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ = _] '(()mod _'))")
    1.20 +subsection \<open>Generic congruences\<close>
    1.21 + 
    1.22 +context unique_euclidean_semiring
    1.23  begin
    1.24  
    1.25 +definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ = _] '(()mod _'))")
    1.26 +  where "cong b c a \<longleftrightarrow> b mod a = c mod a"
    1.27 +  
    1.28  abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(()mod _'))")
    1.29 -  where "notcong x y m \<equiv> \<not> cong x y m"
    1.30 +  where "notcong b c a \<equiv> \<not> cong b c a"
    1.31 +
    1.32 +lemma cong_mod_left [simp]:
    1.33 +  "[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
    1.34 +  by (simp add: cong_def)  
    1.35 +
    1.36 +lemma cong_mod_right [simp]:
    1.37 +  "[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)"
    1.38 +  by (simp add: cong_def)  
    1.39 +
    1.40 +lemma cong_dvd_iff:
    1.41 +  "a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)"
    1.42 +  using that by (auto simp: cong_def dvd_eq_mod_eq_0)
    1.43 +
    1.44 +lemma cong_0 [simp, presburger]:
    1.45 +  "[b = c] (mod 0) \<longleftrightarrow> b = c"
    1.46 +  by (simp add: cong_def)
    1.47 +
    1.48 +lemma cong_1 [simp, presburger]:
    1.49 +  "[b = c] (mod 1)"
    1.50 +  by (simp add: cong_def)
    1.51 +
    1.52 +lemma cong_refl [simp]:
    1.53 +  "[b = b] (mod a)"
    1.54 +  by (simp add: cong_def)
    1.55 +
    1.56 +lemma cong_sym: 
    1.57 +  "[b = c] (mod a) \<Longrightarrow> [c = b] (mod a)"
    1.58 +  by (simp add: cong_def)
    1.59 +
    1.60 +lemma cong_sym_eq:
    1.61 +  "[b = c] (mod a) \<longleftrightarrow> [c = b] (mod a)"
    1.62 +  by (auto simp add: cong_def)
    1.63 +
    1.64 +lemma cong_trans [trans]:
    1.65 +  "[b = c] (mod a) \<Longrightarrow> [c = d] (mod a) \<Longrightarrow> [b = d] (mod a)"
    1.66 +  by (simp add: cong_def)
    1.67 +
    1.68 +lemma cong_add:
    1.69 +  "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b + d = c + e] (mod a)"
    1.70 +  by (auto simp add: cong_def intro: mod_add_cong)
    1.71 +
    1.72 +lemma cong_mult:
    1.73 +  "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b * d = c * e] (mod a)"
    1.74 +  by (auto simp add: cong_def intro: mod_mult_cong)
    1.75 +
    1.76 +lemma cong_pow:
    1.77 +  "[b = c] (mod a) \<Longrightarrow> [b ^ n = c ^ n] (mod a)"
    1.78 +  by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a])
    1.79 +
    1.80 +lemma cong_sum:
    1.81 +  "[sum f A = sum g A] (mod a)" if "\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a)"
    1.82 +  using that by (induct A rule: infinite_finite_induct) (auto intro: cong_add)
    1.83 +
    1.84 +lemma cong_prod:
    1.85 +  "[prod f A = prod g A] (mod a)" if "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a))"
    1.86 +  using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult)
    1.87 +
    1.88 +lemma cong_scalar_right:
    1.89 +  "[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)"
    1.90 +  by (simp add: cong_mult)
    1.91 +
    1.92 +lemma cong_scalar_left:
    1.93 +  "[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)"
    1.94 +  by (simp add: cong_mult)
    1.95 +
    1.96 +lemma cong_mult_self_right: "[b * a = 0] (mod a)"
    1.97 +  by (simp add: cong_def)
    1.98 +
    1.99 +lemma cong_mult_self_left: "[a * b = 0] (mod a)"
   1.100 +  by (simp add: cong_def)
   1.101 +
   1.102 +lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b"
   1.103 +  by (simp add: cong_def dvd_eq_mod_eq_0)
   1.104 +
   1.105 +lemma mod_mult_cong_right:
   1.106 +  "[c mod (a * b) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
   1.107 +  by (simp add: cong_def mod_mod_cancel mod_add_left_eq)
   1.108 +
   1.109 +lemma mod_mult_cong_left:
   1.110 +  "[c mod (b * a) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
   1.111 +  using mod_mult_cong_right [of c a b d] by (simp add: ac_simps)
   1.112 +
   1.113 +end
   1.114 +
   1.115 +context unique_euclidean_ring
   1.116 +begin
   1.117 +
   1.118 +lemma cong_diff:
   1.119 +  "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b - d = c - e] (mod a)"
   1.120 +  by (auto simp add: cong_def intro: mod_diff_cong)
   1.121 +
   1.122 +lemma cong_diff_iff_cong_0:
   1.123 +  "[b - c = 0] (mod a) \<longleftrightarrow> [b = c] (mod a)" (is "?P \<longleftrightarrow> ?Q")
   1.124 +proof
   1.125 +  assume ?P
   1.126 +  then have "[b - c + c = 0 + c] (mod a)"
   1.127 +    by (rule cong_add) simp
   1.128 +  then show ?Q
   1.129 +    by simp
   1.130 +next
   1.131 +  assume ?Q
   1.132 +  with cong_diff [of b c a c c] show ?P
   1.133 +    by simp
   1.134 +qed
   1.135 +
   1.136 +lemma cong_minus_minus_iff:
   1.137 +  "[- b = - c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
   1.138 +  using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
   1.139 +  by (simp add: cong_0_iff dvd_diff_commute)
   1.140 +
   1.141 +lemma cong_modulus_minus_iff: "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
   1.142 +  using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]
   1.143 +  by (simp add: cong_0_iff)
   1.144  
   1.145  end
   1.146  
   1.147  
   1.148 -subsubsection \<open>Definitions for the natural numbers\<close>
   1.149 -
   1.150 -instantiation nat :: cong
   1.151 -begin
   1.152 -
   1.153 -definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   1.154 -  where "cong_nat x y m \<longleftrightarrow> x mod m = y mod m"
   1.155 -
   1.156 -instance ..
   1.157 -
   1.158 -end
   1.159 -
   1.160 -
   1.161 -subsubsection \<open>Definitions for the integers\<close>
   1.162 -
   1.163 -instantiation int :: cong
   1.164 -begin
   1.165 -
   1.166 -definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
   1.167 -  where "cong_int x y m \<longleftrightarrow> x mod m = y mod m"
   1.168 -
   1.169 -instance ..
   1.170 -
   1.171 -end
   1.172 -
   1.173 -
   1.174 -subsection \<open>Set up Transfer\<close>
   1.175 -
   1.176 +subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
   1.177  
   1.178  lemma transfer_nat_int_cong:
   1.179    "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
   1.180    for x y m :: int
   1.181 -  unfolding cong_int_def cong_nat_def
   1.182 -  by (metis int_nat_eq nat_mod_distrib zmod_int)
   1.183 +  by (auto simp add: cong_def nat_mod_distrib [symmetric])
   1.184 +     (metis eq_nat_nat_iff le_less mod_by_0 pos_mod_conj)
   1.185  
   1.186  declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
   1.187  
   1.188 -lemma transfer_int_nat_cong: "[int x = int y] (mod (int m)) = [x = y] (mod m)"
   1.189 -  by (auto simp add: cong_int_def cong_nat_def) (auto simp add: zmod_int [symmetric])
   1.190 +lemma cong_int_iff:
   1.191 +  "[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)"
   1.192 +  by (simp add: cong_def of_nat_mod [symmetric])
   1.193 +
   1.194 +lemma transfer_int_nat_cong:
   1.195 +  "[int x = int y] (mod (int m)) = [x = y] (mod m)"
   1.196 +  by (fact cong_int_iff)
   1.197  
   1.198  declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong]
   1.199  
   1.200 -
   1.201 -subsection \<open>Congruence\<close>
   1.202 -
   1.203 -(* was zcong_0, etc. *)
   1.204 -lemma cong_0_nat [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b"
   1.205 -  for a b :: nat
   1.206 -  by (auto simp: cong_nat_def)
   1.207 -
   1.208 -lemma cong_0_int [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b"
   1.209 -  for a b :: int
   1.210 -  by (auto simp: cong_int_def)
   1.211 -
   1.212 -lemma cong_1_nat [simp, presburger]: "[a = b] (mod 1)"
   1.213 -  for a b :: nat
   1.214 -  by (auto simp: cong_nat_def)
   1.215 -
   1.216 -lemma cong_Suc_0_nat [simp, presburger]: "[a = b] (mod Suc 0)"
   1.217 -  for a b :: nat
   1.218 -  by (auto simp: cong_nat_def)
   1.219 -
   1.220 -lemma cong_1_int [simp, presburger]: "[a = b] (mod 1)"
   1.221 -  for a b :: int
   1.222 -  by (auto simp: cong_int_def)
   1.223 -
   1.224 -lemma cong_refl_nat [simp]: "[k = k] (mod m)"
   1.225 -  for k :: nat
   1.226 -  by (auto simp: cong_nat_def)
   1.227 -
   1.228 -lemma cong_refl_int [simp]: "[k = k] (mod m)"
   1.229 -  for k :: int
   1.230 -  by (auto simp: cong_int_def)
   1.231 -
   1.232 -lemma cong_sym_nat: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   1.233 -  for a b :: nat
   1.234 -  by (auto simp: cong_nat_def)
   1.235 -
   1.236 -lemma cong_sym_int: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   1.237 -  for a b :: int
   1.238 -  by (auto simp: cong_int_def)
   1.239 -
   1.240 -lemma cong_sym_eq_nat: "[a = b] (mod m) = [b = a] (mod m)"
   1.241 -  for a b :: nat
   1.242 -  by (auto simp: cong_nat_def)
   1.243 -
   1.244 -lemma cong_sym_eq_int: "[a = b] (mod m) = [b = a] (mod m)"
   1.245 -  for a b :: int
   1.246 -  by (auto simp: cong_int_def)
   1.247 -
   1.248 -lemma cong_trans_nat [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   1.249 -  for a b c :: nat
   1.250 -  by (auto simp: cong_nat_def)
   1.251 -
   1.252 -lemma cong_trans_int [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   1.253 -  for a b c :: int
   1.254 -  by (auto simp: cong_int_def)
   1.255 -
   1.256 -lemma cong_add_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   1.257 -  for a b c :: nat
   1.258 -  unfolding cong_nat_def by (metis mod_add_cong)
   1.259 -
   1.260 -lemma cong_add_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   1.261 -  for a b c :: int
   1.262 -  unfolding cong_int_def by (metis mod_add_cong)
   1.263 -
   1.264 -lemma cong_diff_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
   1.265 -  for a b c :: int
   1.266 -  unfolding cong_int_def by (metis mod_diff_cong)
   1.267 +lemma cong_Suc_0 [simp, presburger]:
   1.268 +  "[m = n] (mod Suc 0)"
   1.269 +  using cong_1 [of m n] by simp
   1.270  
   1.271  lemma cong_diff_aux_int:
   1.272    "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
   1.273      a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
   1.274    for a b c d :: int
   1.275 -  by (metis cong_diff_int tsub_eq)
   1.276 +  by (metis cong_diff tsub_eq)
   1.277  
   1.278  lemma cong_diff_nat:
   1.279 -  fixes a b c d :: nat
   1.280 -  assumes "[a = b] (mod m)" "[c = d] (mod m)" "a \<ge> c" "b \<ge> d"
   1.281 -  shows "[a - c = b - d] (mod m)"
   1.282 -  using assms by (rule cong_diff_aux_int [transferred])
   1.283 -
   1.284 -lemma cong_mult_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   1.285 -  for a b c d :: nat
   1.286 -  unfolding cong_nat_def  by (metis mod_mult_cong)
   1.287 -
   1.288 -lemma cong_mult_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   1.289 -  for a b c d :: int
   1.290 -  unfolding cong_int_def  by (metis mod_mult_cong)
   1.291 -
   1.292 -lemma cong_exp_nat: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   1.293 -  for x y :: nat
   1.294 -  by (induct k) (auto simp: cong_mult_nat)
   1.295 -
   1.296 -lemma cong_exp_int: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   1.297 -  for x y :: int
   1.298 -  by (induct k) (auto simp: cong_mult_int)
   1.299 -
   1.300 -lemma cong_sum_nat: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
   1.301 -  for f g :: "'a \<Rightarrow> nat"
   1.302 -  by (induct A rule: infinite_finite_induct) (auto intro: cong_add_nat)
   1.303 -
   1.304 -lemma cong_sum_int: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
   1.305 -  for f g :: "'a \<Rightarrow> int"
   1.306 -  by (induct A rule: infinite_finite_induct) (auto intro: cong_add_int)
   1.307 -
   1.308 -lemma cong_prod_nat: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
   1.309 -  for f g :: "'a \<Rightarrow> nat"
   1.310 -  by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_nat)
   1.311 +  "[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
   1.312 +    and "a \<ge> c" "b \<ge> d" for a b c d m :: nat 
   1.313 +  using that by (rule cong_diff_aux_int [transferred])
   1.314  
   1.315 -lemma cong_prod_int: "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod m)) \<Longrightarrow> [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
   1.316 -  for f g :: "'a \<Rightarrow> int"
   1.317 -  by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_int)
   1.318 -
   1.319 -lemma cong_scalar_nat: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   1.320 -  for a b k :: nat
   1.321 -  by (rule cong_mult_nat) simp_all
   1.322 -
   1.323 -lemma cong_scalar_int: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   1.324 -  for a b k :: int
   1.325 -  by (rule cong_mult_int) simp_all
   1.326 -
   1.327 -lemma cong_scalar2_nat: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   1.328 -  for a b k :: nat
   1.329 -  by (rule cong_mult_nat) simp_all
   1.330 +lemma cong_diff_iff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [tsub a b = 0] (mod m) = [a = b] (mod m)"
   1.331 +  for a b :: int
   1.332 +  by (subst tsub_eq, assumption, rule cong_diff_iff_cong_0)
   1.333  
   1.334 -lemma cong_scalar2_int: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   1.335 -  for a b k :: int
   1.336 -  by (rule cong_mult_int) simp_all
   1.337 -
   1.338 -lemma cong_mult_self_nat: "[a * m = 0] (mod m)"
   1.339 -  for a m :: nat
   1.340 -  by (auto simp: cong_nat_def)
   1.341 -
   1.342 -lemma cong_mult_self_int: "[a * m = 0] (mod m)"
   1.343 -  for a m :: int
   1.344 -  by (auto simp: cong_int_def)
   1.345 -
   1.346 -lemma cong_eq_diff_cong_0_int: "[a = b] (mod m) = [a - b = 0] (mod m)"
   1.347 -  for a b :: int
   1.348 -  by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self)
   1.349 -
   1.350 -lemma cong_eq_diff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [a = b] (mod m) = [tsub a b = 0] (mod m)"
   1.351 -  for a b :: int
   1.352 -  by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
   1.353 -
   1.354 -lemma cong_eq_diff_cong_0_nat:
   1.355 +lemma cong_diff_iff_cong_0_nat:
   1.356    fixes a b :: nat
   1.357    assumes "a \<ge> b"
   1.358 -  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
   1.359 -  using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
   1.360 -
   1.361 -lemma cong_diff_cong_0'_nat:
   1.362 -  "[x = y] (mod n) \<longleftrightarrow> (if x \<le> y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
   1.363 -  for x y :: nat
   1.364 -  by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear)
   1.365 +  shows "[a - b = 0] (mod m) = [a = b] (mod m)"
   1.366 +  using assms by (rule cong_diff_iff_cong_0_aux_int [transferred])
   1.367  
   1.368  lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   1.369    for a b :: nat
   1.370 -  apply (subst cong_eq_diff_cong_0_nat, assumption)
   1.371 -  apply (unfold cong_nat_def)
   1.372 -  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   1.373 -  done
   1.374 +  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
   1.375  
   1.376  lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   1.377    for a b :: int
   1.378 -  by (metis cong_int_def mod_eq_dvd_iff)
   1.379 +  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
   1.380  
   1.381 -lemma cong_abs_int: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)"
   1.382 +lemma cong_abs_int [simp]: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)"
   1.383    for x y :: int
   1.384    by (simp add: cong_altdef_int)
   1.385  
   1.386 @@ -289,7 +240,6 @@
   1.387    for a k m :: int
   1.388    by (simp add: mult.commute cong_mult_rcancel_int)
   1.389  
   1.390 -(* was zcong_zgcd_zmult_zmod *)
   1.391  lemma coprime_cong_mult_int:
   1.392    "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   1.393    for a b :: int
   1.394 @@ -302,19 +252,19 @@
   1.395  
   1.396  lemma 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"
   1.397    for a b :: nat
   1.398 -  by (auto simp add: cong_nat_def)
   1.399 +  by (auto simp add: cong_def)
   1.400  
   1.401  lemma 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"
   1.402    for a b :: int
   1.403 -  by (auto simp add: cong_int_def)
   1.404 +  by (auto simp add: cong_def)
   1.405  
   1.406  lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   1.407    for a m :: nat
   1.408 -  by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
   1.409 +  by (auto simp: cong_def) (metis mod_less_divisor mod_mod_trivial)
   1.410  
   1.411  lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   1.412    for a m :: int
   1.413 -  by (auto simp: cong_int_def)  (metis mod_mod_trivial pos_mod_conj)
   1.414 +  by (auto simp: cong_def)  (metis mod_mod_trivial pos_mod_conj)
   1.415  
   1.416  lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
   1.417    for a b :: int
   1.418 @@ -334,20 +284,17 @@
   1.419    next
   1.420      case False
   1.421      with \<open>?lhs\<close> show ?rhs
   1.422 -      apply (subst (asm) cong_sym_eq_nat)
   1.423 -      apply (auto simp: cong_altdef_nat)
   1.424 -      apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
   1.425 -      done
   1.426 +      by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma)
   1.427    qed
   1.428  next
   1.429    assume ?rhs
   1.430    then show ?lhs
   1.431 -    by (metis cong_nat_def mod_mult_self2 mult.commute)
   1.432 +    by (metis cong_def mult.commute nat_mod_eq_iff) 
   1.433  qed
   1.434  
   1.435  lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   1.436    for a b :: int
   1.437 -  by (metis cong_int_def gcd_red_int)
   1.438 +  by (auto simp add: cong_def) (metis gcd_red_int)
   1.439  
   1.440  lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   1.441    for a b :: nat
   1.442 @@ -363,11 +310,11 @@
   1.443  
   1.444  lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   1.445    for a b :: nat
   1.446 -  by (auto simp add: cong_nat_def)
   1.447 +  by simp
   1.448  
   1.449  lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   1.450    for a b :: int
   1.451 -  by (auto simp add: cong_int_def)
   1.452 +  by simp
   1.453  
   1.454  lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
   1.455    for a b :: int
   1.456 @@ -434,53 +381,6 @@
   1.457    for x y :: int
   1.458    by (auto simp add: cong_altdef_int dvd_def)
   1.459  
   1.460 -lemma cong_dvd_eq_nat: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   1.461 -  for x y :: nat
   1.462 -  by (auto simp: cong_nat_def dvd_eq_mod_eq_0)
   1.463 -
   1.464 -lemma cong_dvd_eq_int: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   1.465 -  for x y :: int
   1.466 -  by (auto simp: cong_int_def dvd_eq_mod_eq_0)
   1.467 -
   1.468 -lemma cong_mod_nat: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
   1.469 -  for a n :: nat
   1.470 -  by (simp add: cong_nat_def)
   1.471 -
   1.472 -lemma cong_mod_int: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
   1.473 -  for a n :: int
   1.474 -  by (simp add: cong_int_def)
   1.475 -
   1.476 -lemma mod_mult_cong_nat: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   1.477 -  for a b :: nat
   1.478 -  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   1.479 -
   1.480 -lemma neg_cong_int: "[a = b] (mod m) \<longleftrightarrow> [- a = - b] (mod m)"
   1.481 -  for a b :: int
   1.482 -  by (metis cong_int_def minus_minus mod_minus_cong)
   1.483 -
   1.484 -lemma cong_modulus_neg_int: "[a = b] (mod m) \<longleftrightarrow> [a = b] (mod - m)"
   1.485 -  for a b :: int
   1.486 -  by (auto simp add: cong_altdef_int)
   1.487 -
   1.488 -lemma mod_mult_cong_int: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   1.489 -  for a b :: int
   1.490 -proof (cases "b > 0")
   1.491 -  case True
   1.492 -  then show ?thesis
   1.493 -    by (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   1.494 -next
   1.495 -  case False
   1.496 -  then show ?thesis
   1.497 -    apply (subst (1 2) cong_modulus_neg_int)
   1.498 -    apply (unfold cong_int_def)
   1.499 -    apply (subgoal_tac "a * b = (- a * - b)")
   1.500 -     apply (erule ssubst)
   1.501 -     apply (subst zmod_zmult2_eq)
   1.502 -      apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
   1.503 -     apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
   1.504 -    done
   1.505 -qed
   1.506 -
   1.507  lemma cong_to_1_nat:
   1.508    fixes a :: nat
   1.509    assumes "[a = 1] (mod n)"
   1.510 @@ -494,15 +394,15 @@
   1.511  qed
   1.512  
   1.513  lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0"
   1.514 -  by (auto simp: cong_nat_def)
   1.515 +  by (auto simp: cong_def)
   1.516  
   1.517  lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1"
   1.518    for n :: nat
   1.519 -  by (auto simp: cong_nat_def)
   1.520 +  by (auto simp: cong_def)
   1.521  
   1.522  lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1"
   1.523    for n :: int
   1.524 -  by (auto simp: cong_int_def zmult_eq_1_iff)
   1.525 +  by (auto simp: cong_def zmult_eq_1_iff)
   1.526  
   1.527  lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
   1.528    for a :: nat
   1.529 @@ -524,7 +424,7 @@
   1.530    case False
   1.531    then show ?thesis
   1.532      using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>]
   1.533 -    by auto (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
   1.534 +    by auto (metis cong_add_rcancel_0_nat cong_mult_self_left)
   1.535  qed
   1.536  
   1.537  lemma cong_solve_int: "a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
   1.538 @@ -546,7 +446,7 @@
   1.539    from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
   1.540      by auto
   1.541    then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
   1.542 -    by (elim cong_scalar2_nat)
   1.543 +    using cong_scalar_left by blast
   1.544    also from b have "(d div gcd a n) * gcd a n = d"
   1.545      by (rule dvd_div_mult_self)
   1.546    also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   1.547 @@ -562,7 +462,7 @@
   1.548    from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
   1.549      by auto
   1.550    then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
   1.551 -    by (elim cong_scalar2_int)
   1.552 +    using cong_scalar_left by blast
   1.553    also from b have "(d div gcd a n) * gcd a n = d"
   1.554      by (rule dvd_div_mult_self)
   1.555    also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   1.556 @@ -577,10 +477,12 @@
   1.557    shows "\<exists>x. [a * x = 1] (mod n)"
   1.558  proof (cases "a = 0")
   1.559    case True
   1.560 -  with assms show ?thesis by force
   1.561 +  with assms show ?thesis
   1.562 +    by (simp add: cong_0_1_nat') 
   1.563  next
   1.564    case False
   1.565 -  with assms show ?thesis by (metis cong_solve_nat)
   1.566 +  with assms show ?thesis
   1.567 +    by (metis cong_solve_nat)
   1.568  qed
   1.569  
   1.570  lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
   1.571 @@ -598,14 +500,14 @@
   1.572  lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   1.573    for m :: int
   1.574    apply (auto intro: cong_solve_coprime_int)
   1.575 -  apply (metis cong_int_def coprime_mul_eq gcd_1_int gcd.commute gcd_red_int)
   1.576 +  using cong_gcd_eq_int coprime_mul_eq' apply fastforce
   1.577    done
   1.578  
   1.579  lemma coprime_iff_invertible'_nat:
   1.580    "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
   1.581    apply (subst coprime_iff_invertible_nat)
   1.582     apply auto
   1.583 -  apply (auto simp add: cong_nat_def)
   1.584 +  apply (auto simp add: cong_def)
   1.585    apply (metis mod_less_divisor mod_mult_right_eq)
   1.586    done
   1.587  
   1.588 @@ -613,35 +515,35 @@
   1.589    "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
   1.590    for m :: int
   1.591    apply (subst coprime_iff_invertible_int)
   1.592 -   apply (auto simp add: cong_int_def)
   1.593 +   apply (auto simp add: cong_def)
   1.594    apply (metis mod_mult_right_eq pos_mod_conj)
   1.595    done
   1.596  
   1.597  lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   1.598    for x y :: nat
   1.599    apply (cases "y \<le> x")
   1.600 -  apply (metis cong_altdef_nat lcm_least)
   1.601 -  apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear)
   1.602 +   apply (simp add: cong_altdef_nat)
   1.603 +  apply (meson cong_altdef_nat cong_sym lcm_least_iff nat_le_linear)
   1.604    done
   1.605  
   1.606  lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   1.607    for x y :: int
   1.608    by (auto simp add: cong_altdef_int lcm_least)
   1.609  
   1.610 -lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
   1.611 -    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   1.612 -    (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   1.613 -      [x = y] (mod (\<Prod>i\<in>A. m i))"
   1.614 -  apply (induct set: finite)
   1.615 -  apply auto
   1.616 +lemma cong_cong_prod_coprime_nat:
   1.617 +  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
   1.618 +    "(\<forall>i\<in>A. [(x::nat) = y] (mod m i))"
   1.619 +    and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   1.620 +  using that apply (induct A rule: infinite_finite_induct)
   1.621 +    apply auto
   1.622    apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   1.623    done
   1.624  
   1.625 -lemma cong_cong_prod_coprime_int [rule_format]: "finite A \<Longrightarrow>
   1.626 -    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   1.627 -    (\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
   1.628 -      [x = y] (mod (\<Prod>i\<in>A. m i))"
   1.629 -  apply (induct set: finite)
   1.630 +lemma cong_cong_prod_coprime_int [rule_format]:
   1.631 +  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
   1.632 +    "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
   1.633 +    "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   1.634 +  using that apply (induct A rule: infinite_finite_induct)
   1.635    apply auto
   1.636    apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
   1.637    done
   1.638 @@ -658,9 +560,9 @@
   1.639    from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
   1.640      by auto
   1.641    have "[m1 * x1 = 0] (mod m1)"
   1.642 -    by (subst mult.commute) (rule cong_mult_self_nat)
   1.643 +    by (simp add: cong_mult_self_left)
   1.644    moreover have "[m2 * x2 = 0] (mod m2)"
   1.645 -    by (subst mult.commute) (rule cong_mult_self_nat)
   1.646 +    by (simp add: cong_mult_self_left)
   1.647    ultimately show ?thesis
   1.648      using 1 2 by blast
   1.649  qed
   1.650 @@ -677,9 +579,9 @@
   1.651    from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
   1.652      by auto
   1.653    have "[m1 * x1 = 0] (mod m1)"
   1.654 -    by (subst mult.commute) (rule cong_mult_self_int)
   1.655 +    by (simp add: cong_mult_self_left)
   1.656    moreover have "[m2 * x2 = 0] (mod m2)"
   1.657 -    by (subst mult.commute) (rule cong_mult_self_int)
   1.658 +    by (simp add: cong_mult_self_left)
   1.659    ultimately show ?thesis
   1.660      using 1 2 by blast
   1.661  qed
   1.662 @@ -695,20 +597,10 @@
   1.663      by blast
   1.664    let ?x = "u1 * b1 + u2 * b2"
   1.665    have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   1.666 -    apply (rule cong_add_nat)
   1.667 -     apply (rule cong_scalar2_nat)
   1.668 -     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
   1.669 -    apply (rule cong_scalar2_nat)
   1.670 -    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
   1.671 -    done
   1.672 +    using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast
   1.673    then have "[?x = u1] (mod m1)" by simp
   1.674    have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   1.675 -    apply (rule cong_add_nat)
   1.676 -     apply (rule cong_scalar2_nat)
   1.677 -     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
   1.678 -    apply (rule cong_scalar2_nat)
   1.679 -    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
   1.680 -    done
   1.681 +    using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast
   1.682    then have "[?x = u2] (mod m2)"
   1.683      by simp
   1.684    with \<open>[?x = u1] (mod m1)\<close> show ?thesis
   1.685 @@ -726,20 +618,10 @@
   1.686      by blast
   1.687    let ?x = "u1 * b1 + u2 * b2"
   1.688    have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   1.689 -    apply (rule cong_add_int)
   1.690 -     apply (rule cong_scalar2_int)
   1.691 -     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
   1.692 -    apply (rule cong_scalar2_int)
   1.693 -    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
   1.694 -    done
   1.695 +    using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast
   1.696    then have "[?x = u1] (mod m1)" by simp
   1.697    have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   1.698 -    apply (rule cong_add_int)
   1.699 -     apply (rule cong_scalar2_int)
   1.700 -     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
   1.701 -    apply (rule cong_scalar2_int)
   1.702 -    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
   1.703 -    done
   1.704 +    using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast
   1.705    then have "[?x = u2] (mod m2)" by simp
   1.706    with \<open>[?x = u1] (mod m1)\<close> show ?thesis
   1.707      by blast
   1.708 @@ -750,8 +632,8 @@
   1.709    apply (cases "y \<le> x")
   1.710     apply (simp add: cong_altdef_nat)
   1.711     apply (erule dvd_mult_left)
   1.712 -  apply (rule cong_sym_nat)
   1.713 -  apply (subst (asm) cong_sym_eq_nat)
   1.714 +  apply (rule cong_sym)
   1.715 +  apply (subst (asm) cong_sym_eq)
   1.716    apply (simp add: cong_altdef_nat)
   1.717    apply (erule dvd_mult_left)
   1.718    done
   1.719 @@ -764,7 +646,7 @@
   1.720  
   1.721  lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   1.722    for x y :: nat
   1.723 -  by (simp add: cong_nat_def)
   1.724 +  by (simp add: cong_def)
   1.725  
   1.726  lemma binary_chinese_remainder_unique_nat:
   1.727    fixes m1 m2 :: nat
   1.728 @@ -779,21 +661,19 @@
   1.729    from nz have less: "?x < m1 * m2"
   1.730      by auto
   1.731    have 1: "[?x = u1] (mod m1)"
   1.732 -    apply (rule cong_trans_nat)
   1.733 +    apply (rule cong_trans)
   1.734       prefer 2
   1.735       apply (rule \<open>[y = u1] (mod m1)\<close>)
   1.736 -    apply (rule cong_modulus_mult_nat)
   1.737 -    apply (rule cong_mod_nat)
   1.738 -    using nz apply auto
   1.739 +    apply (rule cong_modulus_mult_nat [of _ _ _ m2])
   1.740 +    apply simp
   1.741      done
   1.742    have 2: "[?x = u2] (mod m2)"
   1.743 -    apply (rule cong_trans_nat)
   1.744 +    apply (rule cong_trans)
   1.745       prefer 2
   1.746       apply (rule \<open>[y = u2] (mod m2)\<close>)
   1.747      apply (subst mult.commute)
   1.748 -    apply (rule cong_modulus_mult_nat)
   1.749 -    apply (rule cong_mod_nat)
   1.750 -    using nz apply auto
   1.751 +    apply (rule cong_modulus_mult_nat [of _ _ _ m1])
   1.752 +    apply simp
   1.753      done
   1.754    have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
   1.755    proof clarify
   1.756 @@ -801,22 +681,22 @@
   1.757      assume "z < m1 * m2"
   1.758      assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
   1.759      have "[?x = z] (mod m1)"
   1.760 -      apply (rule cong_trans_nat)
   1.761 +      apply (rule cong_trans)
   1.762         apply (rule \<open>[?x = u1] (mod m1)\<close>)
   1.763 -      apply (rule cong_sym_nat)
   1.764 +      apply (rule cong_sym)
   1.765        apply (rule \<open>[z = u1] (mod m1)\<close>)
   1.766        done
   1.767      moreover have "[?x = z] (mod m2)"
   1.768 -      apply (rule cong_trans_nat)
   1.769 +      apply (rule cong_trans)
   1.770         apply (rule \<open>[?x = u2] (mod m2)\<close>)
   1.771 -      apply (rule cong_sym_nat)
   1.772 +      apply (rule cong_sym)
   1.773        apply (rule \<open>[z = u2] (mod m2)\<close>)
   1.774        done
   1.775      ultimately have "[?x = z] (mod m1 * m2)"
   1.776 -      by (auto intro: coprime_cong_mult_nat a)
   1.777 +      using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right)
   1.778      with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
   1.779        apply (intro cong_less_modulus_unique_nat)
   1.780 -        apply (auto, erule cong_sym_nat)
   1.781 +        apply (auto, erule cong_sym)
   1.782        done
   1.783    qed
   1.784    with less 1 2 show ?thesis by auto
   1.785 @@ -838,7 +718,7 @@
   1.786    then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
   1.787      by auto
   1.788    moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   1.789 -    by (subst mult.commute, rule cong_mult_self_nat)
   1.790 +    by (simp add: cong_0_iff)
   1.791    ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
   1.792      by blast
   1.793  qed
   1.794 @@ -867,11 +747,11 @@
   1.795          by auto
   1.796        also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
   1.797                    u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
   1.798 -        apply (rule cong_add_nat)
   1.799 -         apply (rule cong_scalar2_nat)
   1.800 +        apply (rule cong_add)
   1.801 +         apply (rule cong_scalar_left)
   1.802          using b a apply blast
   1.803 -        apply (rule cong_sum_nat)
   1.804 -        apply (rule cong_scalar2_nat)
   1.805 +        apply (rule cong_sum)
   1.806 +        apply (rule cong_scalar_left)
   1.807          using b apply auto
   1.808          apply (rule cong_dvd_modulus_nat)
   1.809           apply (drule (1) bspec)
   1.810 @@ -886,11 +766,11 @@
   1.811    qed
   1.812  qed
   1.813  
   1.814 -lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
   1.815 -    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   1.816 -      (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   1.817 -         [x = y] (mod (\<Prod>i\<in>A. m i))"
   1.818 -  apply (induct set: finite)
   1.819 +lemma coprime_cong_prod_nat:
   1.820 +  "[x = y] (mod (\<Prod>i\<in>A. m i))"
   1.821 +  if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   1.822 +    and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
   1.823 +  using that apply (induct A rule: infinite_finite_induct)
   1.824    apply auto
   1.825    apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   1.826    done
   1.827 @@ -914,15 +794,12 @@
   1.828      by auto
   1.829    have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)"
   1.830      apply auto
   1.831 -    apply (rule cong_trans_nat)
   1.832 +    apply (rule cong_trans)
   1.833       prefer 2
   1.834      using one apply auto
   1.835 -    apply (rule cong_dvd_modulus_nat)
   1.836 -     apply (rule cong_mod_nat)
   1.837 -    using prodnz apply auto
   1.838 -    apply rule
   1.839 -     apply (rule fin)
   1.840 -    apply assumption
   1.841 +    apply (rule cong_dvd_modulus_nat [of _ _ "prod m A"])
   1.842 +     apply simp
   1.843 +    using fin apply auto
   1.844      done
   1.845    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"
   1.846    proof clarify
   1.847 @@ -931,9 +808,9 @@
   1.848      assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))"
   1.849      have "\<forall>i\<in>A. [?x = z] (mod m i)"
   1.850        apply clarify
   1.851 -      apply (rule cong_trans_nat)
   1.852 +      apply (rule cong_trans)
   1.853        using cong apply (erule bspec)
   1.854 -      apply (rule cong_sym_nat)
   1.855 +      apply (rule cong_sym)
   1.856        using zcong apply auto
   1.857        done
   1.858      with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
   1.859 @@ -943,7 +820,7 @@
   1.860      with zless less show "z = ?x"
   1.861        apply (intro cong_less_modulus_unique_nat)
   1.862          apply auto
   1.863 -      apply (erule cong_sym_nat)
   1.864 +      apply (erule cong_sym)
   1.865        done
   1.866    qed
   1.867    from less cong unique show ?thesis
     2.1 --- a/src/HOL/Number_Theory/Euler_Criterion.thy	Fri Oct 20 23:29:43 2017 +0200
     2.2 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Fri Oct 20 20:57:55 2017 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    from assms obtain b where b: "[b ^ 2 = a] (mod int p)"
     2.5      unfolding QuadRes_def by blast
     2.6    then have "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod int p)"
     2.7 -    by (simp add: cong_exp_int cong_sym_int power_mult)
     2.8 +    by (simp add: cong_pow cong_sym power_mult)
     2.9    then have "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod int p)"
    2.10      using odd_p by force
    2.11    moreover have "[b ^ (p - 1) = 1] (mod int p)"
    2.12 @@ -32,19 +32,19 @@
    2.13      have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
    2.14      using p_prime proof (rule fermat_theorem)
    2.15        show "\<not> p dvd nat \<bar>b\<bar>"
    2.16 -        by (metis b cong_altdef_int cong_dvd_eq_int diff_zero int_dvd_iff p_a_relprime p_prime prime_dvd_power_int_iff prime_nat_int_transfer rel_simps(51))
    2.17 +        by (metis b cong_altdef_int cong_dvd_iff diff_zero int_dvd_iff p_a_relprime p_prime prime_dvd_power_int_iff prime_nat_int_transfer rel_simps(51))
    2.18      qed
    2.19      then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
    2.20 -      by (simp add: cong_nat_def)
    2.21 +      by (simp add: cong_def)
    2.22      then have "int (nat \<bar>b\<bar> ^ (p - 1) mod p) = int (1 mod p)"
    2.23        by simp
    2.24      moreover from odd_p have "\<bar>b\<bar> ^ (p - Suc 0) = b ^ (p - Suc 0)"
    2.25        by (simp add: power_even_abs)
    2.26      ultimately show ?thesis
    2.27 -      by (simp add: zmod_int cong_int_def)
    2.28 +      by (simp add: zmod_int cong_def)
    2.29    qed
    2.30    ultimately show ?thesis
    2.31 -    by (auto intro: cong_trans_int)
    2.32 +    by (auto intro: cong_trans)
    2.33  qed
    2.34  
    2.35  private definition S1 :: "int set" where "S1 = {0 <.. int p - 1}"
    2.36 @@ -69,7 +69,7 @@
    2.37    then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
    2.38    moreover define y where "y = y' * a mod p"
    2.39    ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
    2.40 -    cong_scalar_int[of "x * y'"] unfolding cong_int_def mult.assoc by auto
    2.41 +    cong_scalar_right [of "x * y'"] unfolding cong_def mult.assoc by auto
    2.42    moreover have "y \<in> {0 .. int p - 1}" unfolding y_def using p_ge_2 by auto
    2.43    hence "y \<in> S1" using calculation cong_altdef_int p_a_relprime S1_def by auto
    2.44    ultimately have "P x y" unfolding P_def by blast
    2.45 @@ -77,7 +77,7 @@
    2.46      fix y1 y2
    2.47      assume "P x y1" "P x y2"
    2.48      moreover hence "[y1 = y2] (mod p)" unfolding P_def
    2.49 -      using co_xp cong_mult_lcancel_int[of x p y1 y2] cong_sym_int cong_trans_int by blast
    2.50 +      using co_xp cong_mult_lcancel_int[of x p y1 y2] cong_sym cong_trans by blast
    2.51      ultimately have "y1 = y2" unfolding P_def S1_def using cong_less_imp_eq_int by auto
    2.52    }
    2.53    ultimately show ?thesis by blast
    2.54 @@ -144,7 +144,8 @@
    2.55      using x Suc(1)[of S'] Suc(2) Suc(3) by (simp add: card_ge_0_finite)
    2.56    moreover have "prod g S = g x * prod g S'"
    2.57      using x S'_def Suc(2) prod.remove[of S x g] by fastforce
    2.58 -  ultimately show ?case using x Suc(3) cong_mult_int by simp
    2.59 +  ultimately show ?case using x Suc(3) cong_mult
    2.60 +    by simp blast 
    2.61  qed
    2.62  
    2.63  private lemma l11: assumes "~ QuadRes p a"
    2.64 @@ -162,24 +163,31 @@
    2.65    using assms l2 l10 l11 unfolding S2_def by blast
    2.66  
    2.67  private lemma E_2: assumes "~ QuadRes p a"
    2.68 -  shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans_int cong_sym_int assms by blast
    2.69 +  shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans cong_sym assms by blast
    2.70  
    2.71  lemma euler_criterion_aux: "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)"
    2.72 -  using E_1 E_2 Legendre_def cong_sym_int p_a_relprime by presburger
    2.73 +  using p_a_relprime by (auto simp add: Legendre_def
    2.74 +    intro!: cong_sym [of _ 1] cong_sym [of _ "- 1"]
    2.75 +    dest: E_1 E_2)
    2.76  
    2.77  end
    2.78  
    2.79  theorem euler_criterion: assumes "prime p" "2 < p"
    2.80    shows "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)"
    2.81  proof (cases "[a = 0] (mod p)")
    2.82 -case True
    2.83 -  hence "[a ^ ((p - 1) div 2) = 0 ^ ((p - 1) div 2)] (mod p)" using cong_exp_int by blast
    2.84 -  moreover have "(0::int) ^ ((p - 1) div 2) = 0" using zero_power[of "(p - 1) div 2"] assms(2) by simp
    2.85 -  ultimately have "[a ^ ((p - 1) div 2) = 0] (mod p)" using cong_trans_int cong_refl_int by presburger
    2.86 -  thus ?thesis unfolding Legendre_def using True cong_sym_int by presburger
    2.87 +  case True
    2.88 +  then have "[a ^ ((p - 1) div 2) = 0 ^ ((p - 1) div 2)] (mod p)"
    2.89 +    using cong_pow by blast
    2.90 +  moreover have "(0::int) ^ ((p - 1) div 2) = 0"
    2.91 +    using zero_power [of "(p - 1) div 2"] assms(2) by simp
    2.92 +  ultimately have "[a ^ ((p - 1) div 2) = 0] (mod p)"
    2.93 +    using True assms(1) cong_altdef_int prime_dvd_power_int_iff by auto
    2.94 +  then show ?thesis unfolding Legendre_def using True cong_sym
    2.95 +    by auto
    2.96  next
    2.97 -case False
    2.98 -  thus ?thesis using euler_criterion_aux assms by presburger
    2.99 +  case False
   2.100 +  then show ?thesis
   2.101 +    using euler_criterion_aux assms by presburger
   2.102  qed
   2.103  
   2.104  hide_fact euler_criterion_aux
     3.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Oct 20 23:29:43 2017 +0200
     3.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Fri Oct 20 20:57:55 2017 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4      for x y
     3.5    proof -
     3.6      from a have a': "[x * a = y * a](mod p)"
     3.7 -      by (metis cong_int_def)
     3.8 +      using cong_def by blast
     3.9      from p_a_relprime have "\<not>p dvd a"
    3.10        by (simp add: cong_altdef_int)
    3.11      with p_prime have "coprime a (int p)"
    3.12 @@ -173,7 +173,7 @@
    3.13  
    3.14  lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
    3.15    for x :: int
    3.16 -  by (simp add: cong_int_def)
    3.17 +  by (simp add: cong_def)
    3.18  
    3.19  lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
    3.20    by (rule nonzero_mod_p) (auto simp add: A_def)
    3.21 @@ -187,18 +187,21 @@
    3.22  lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
    3.23    using a_nonzero by (auto simp add: B_def A_greater_zero)
    3.24  
    3.25 +lemma B_mod_greater_zero:
    3.26 +  "0 < x mod int p" if "x \<in> B"
    3.27 +proof -
    3.28 +  from that have "x mod int p \<noteq> 0"
    3.29 +    using B_ncong_p cong_def cong_mult_self_left by blast
    3.30 +  moreover from that have "0 < x"
    3.31 +    by (rule B_greater_zero)
    3.32 +  then have "0 \<le> x mod int p"
    3.33 +    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
    3.34 +  ultimately show ?thesis
    3.35 +    by simp
    3.36 +qed
    3.37 +
    3.38  lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
    3.39 -proof (auto simp add: C_def)
    3.40 -  fix x :: int
    3.41 -  assume x: "x \<in> B"
    3.42 -  moreover from x have "x mod int p \<noteq> 0"
    3.43 -    using B_ncong_p cong_int_def by simp
    3.44 -  moreover have "int y = 0 \<or> 0 < int y" for y
    3.45 -    by linarith
    3.46 -  ultimately show "0 < x mod int p"
    3.47 -    using B_greater_zero [of x]
    3.48 -    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
    3.49 -qed
    3.50 +  by (auto simp add: C_def B_mod_greater_zero)
    3.51  
    3.52  lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
    3.53    apply (auto simp add: F_def E_def C_def)
    3.54 @@ -228,7 +231,7 @@
    3.55  subsection \<open>Relationships Between Gauss Sets\<close>
    3.56  
    3.57  lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> inj_on (\<lambda>b. b mod m) X"
    3.58 -  by (auto simp add: ResSet_def inj_on_def cong_int_def)
    3.59 +  by (auto simp add: ResSet_def inj_on_def cong_def)
    3.60  
    3.61  lemma B_card_eq_A: "card B = card A"
    3.62    using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
    3.63 @@ -261,8 +264,8 @@
    3.64    apply (insert finite_B SR_B_inj)
    3.65    apply (drule prod.reindex [of "\<lambda>x. x mod int p" B id])
    3.66    apply auto
    3.67 -  apply (rule cong_prod_int)
    3.68 -  apply (auto simp add: cong_int_def)
    3.69 +  apply (rule cong_prod)
    3.70 +  apply (auto simp add: cong_def)
    3.71    done
    3.72  
    3.73  lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
    3.74 @@ -273,11 +276,11 @@
    3.75    fix y z :: int
    3.76    assume "p - (y * a) mod p = (z * a) mod p"
    3.77    then have "[(y * a) mod p + (z * a) mod p = 0] (mod p)"
    3.78 -    by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
    3.79 +    by (metis add.commute diff_eq_eq dvd_refl cong_def dvd_eq_mod_eq_0 mod_0)
    3.80    moreover have "[y * a = (y * a) mod p] (mod p)"
    3.81 -    by (metis cong_int_def mod_mod_trivial)
    3.82 +    by (metis cong_def mod_mod_trivial)
    3.83    ultimately have "[a * (y + z) = 0] (mod p)"
    3.84 -    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
    3.85 +    by (metis cong_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
    3.86    with p_prime a_nonzero p_a_relprime have a: "[y + z = 0] (mod p)"
    3.87      by (auto dest!: cong_prime_prod_zero_int)
    3.88    assume b: "y \<in> A" and c: "z \<in> A"
    3.89 @@ -314,12 +317,12 @@
    3.90      apply auto
    3.91      done
    3.92    then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
    3.93 -    by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
    3.94 +    by (metis cong_def minus_mod_self1 mod_mod_trivial)
    3.95    then have "[prod ((\<lambda>x. x mod p) o (op - p)) E = prod (uminus) E](mod p)"
    3.96 -    using finite_E p_ge_2 cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
    3.97 +    using finite_E p_ge_2 cong_prod [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
    3.98      by auto
    3.99    then have two: "[prod id F = prod (uminus) E](mod p)"
   3.100 -    by (metis FE cong_cong_mod_int cong_refl_int cong_prod_int minus_mod_self1)
   3.101 +    by (metis FE cong_cong_mod_int cong_refl cong_prod minus_mod_self1)
   3.102    have "prod uminus E = (-1) ^ card E * prod id E"
   3.103      using finite_E by (induct set: finite) auto
   3.104    with two show ?thesis
   3.105 @@ -330,18 +333,18 @@
   3.106  subsection \<open>Gauss' Lemma\<close>
   3.107  
   3.108  lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
   3.109 -  by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
   3.110 +  by auto
   3.111  
   3.112  theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   3.113  proof -
   3.114    have "[prod id A = prod id F * prod id D](mod p)"
   3.115      by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
   3.116    then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
   3.117 -    by (rule cong_trans_int) (metis cong_scalar_int prod_F_zcong)
   3.118 +    by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
   3.119    then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
   3.120 -    by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
   3.121 +    using finite_D finite_E by (auto simp add: ac_simps C_prod_eq_D_times_E C_eq D_E_disj prod.union_disjoint)
   3.122    then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
   3.123 -    by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
   3.124 +    by (rule cong_trans) (metis C_B_zcong_prod cong_scalar_left)
   3.125    then have "[prod id A = ((-1)^(card E) * prod id ((\<lambda>x. x * a) ` A))] (mod p)"
   3.126      by (simp add: B_def)
   3.127    then have "[prod id A = ((-1)^(card E) * prod (\<lambda>x. x * a) A)] (mod p)"
   3.128 @@ -351,20 +354,20 @@
   3.129    ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A * prod id A))] (mod p)"
   3.130      by simp
   3.131    then have "[prod id A = ((-1)^(card E) * a^(card A) * prod id A)](mod p)"
   3.132 -    by (rule cong_trans_int)
   3.133 -      (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
   3.134 +    by (rule cong_trans)
   3.135 +      (simp add: cong_scalar_left cong_scalar_right finite_A prod_constant ac_simps)
   3.136    then have a: "[prod id A * (-1)^(card E) =
   3.137        ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
   3.138 -    by (rule cong_scalar_int)
   3.139 +    by (rule cong_scalar_right)
   3.140    then have "[prod id A * (-1)^(card E) = prod id A *
   3.141        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   3.142 -    by (rule cong_trans_int) (simp add: a mult.commute mult.left_commute)
   3.143 +    by (rule cong_trans) (simp add: a ac_simps)
   3.144    then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
   3.145 -    by (rule cong_trans_int) (simp add: aux cong del: prod.strong_cong)
   3.146 +    by (rule cong_trans) (simp add: aux cong del: prod.strong_cong)
   3.147    with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
   3.148      by (metis cong_mult_lcancel_int)
   3.149    then show ?thesis
   3.150 -    by (simp add: A_card_eq cong_sym_int)
   3.151 +    by (simp add: A_card_eq cong_sym)
   3.152  qed
   3.153  
   3.154  theorem gauss_lemma: "Legendre a p = (-1) ^ (card E)"
   3.155 @@ -376,7 +379,7 @@
   3.156    then have "[a ^ nat (int ((p - 1) div 2)) = a ^ nat ((int p - 1) div 2)] (mod int p)"
   3.157      by force
   3.158    ultimately have "[Legendre a p = (-1) ^ (card E)] (mod p)"
   3.159 -    using pre_gauss_lemma cong_trans_int by blast
   3.160 +    using pre_gauss_lemma cong_trans by blast
   3.161    moreover from p_a_relprime have "Legendre a p = 1 \<or> Legendre a p = -1"
   3.162      by (auto simp add: Legendre_def)
   3.163    moreover have "(-1::int) ^ (card E) = 1 \<or> (-1::int) ^ (card E) = -1"
   3.164 @@ -384,7 +387,7 @@
   3.165    moreover have "[1 \<noteq> - 1] (mod int p)"
   3.166      using cong_altdef_int nonzero_mod_p[of 2] p_odd_int by fastforce
   3.167    ultimately show ?thesis
   3.168 -    by (auto simp add: cong_sym_int)
   3.169 +    by (auto simp add: cong_sym)
   3.170  qed
   3.171  
   3.172  end
     4.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Fri Oct 20 23:29:43 2017 +0200
     4.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Fri Oct 20 20:57:55 2017 +0200
     4.3 @@ -40,7 +40,7 @@
     4.4  proof (cases "a = 0")
     4.5    case True
     4.6    with an show ?thesis
     4.7 -    by (simp add: cong_nat_def)
     4.8 +    by (simp add: cong_def)
     4.9  next
    4.10    case False
    4.11    from bezout_add_strong_nat [OF this]
    4.12 @@ -56,7 +56,7 @@
    4.13    then have "a * (x * b) mod n = b mod n"
    4.14      by (simp add: mod_add_left_eq)
    4.15    then have "[a * (x * b) = b] (mod n)"
    4.16 -    by (simp only: cong_nat_def)
    4.17 +    by (simp only: cong_def)
    4.18    then show ?thesis by blast
    4.19  qed
    4.20  
    4.21 @@ -70,17 +70,17 @@
    4.22    let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
    4.23    let ?x = "x mod n"
    4.24    from x have *: "[a * ?x = b] (mod n)"
    4.25 -    by (simp add: cong_nat_def mod_mult_right_eq[of a x n])
    4.26 +    by (simp add: cong_def mod_mult_right_eq[of a x n])
    4.27    from mod_less_divisor[ of n x] nz * have Px: "?P ?x" by simp
    4.28    have "y = ?x" if Py: "y < n" "[a * y = b] (mod n)" for y
    4.29    proof -
    4.30      from Py(2) * have "[a * y = a * ?x] (mod n)"
    4.31 -      by (simp add: cong_nat_def)
    4.32 +      by (simp add: cong_def)
    4.33      then have "[y = ?x] (mod n)"
    4.34        by (metis an cong_mult_lcancel_nat)
    4.35      with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
    4.36      show ?thesis
    4.37 -      by (simp add: cong_nat_def)
    4.38 +      by (simp add: cong_def)
    4.39    qed
    4.40    with Px show ?thesis by blast
    4.41  qed
    4.42 @@ -103,7 +103,7 @@
    4.43    proof
    4.44      assume "y = 0"
    4.45      with y(2) have "p dvd a"
    4.46 -      by (auto dest: cong_dvd_eq_nat)
    4.47 +      using cong_dvd_iff by auto
    4.48      then show False
    4.49        by (metis gcd_nat.absorb1 not_prime_1 p pa)
    4.50    qed
    4.51 @@ -151,14 +151,14 @@
    4.52    next
    4.53      case 2
    4.54      with am m show ?thesis
    4.55 -      by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)
    4.56 +      by simp
    4.57    next
    4.58      case 3
    4.59      from m obtain m' where m': "m = Suc m'" by (cases m) blast+
    4.60      have "d = 1" if d: "d dvd a" "d dvd n" for d
    4.61      proof -
    4.62        from am mod_less[OF \<open>n > 1\<close>] have am1: "a^m mod n = 1"
    4.63 -        by (simp add: cong_nat_def)
    4.64 +        by (simp add: cong_def)
    4.65        from dvd_mult2[OF d(1), of "a^m'"] have dam: "d dvd a^m"
    4.66          by (simp add: m')
    4.67        from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
    4.68 @@ -234,13 +234,13 @@
    4.69          by (simp add: algebra_simps power_mult)
    4.70        also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
    4.71          using power_mod[of "a^m" n "(n - 1) div m"] by simp
    4.72 -      also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen
    4.73 +      also have "\<dots> = 1" using m(3)[unfolded cong_def onen] onen
    4.74          by (metis power_one)
    4.75        finally have *: "?y mod n = 1"  .
    4.76        have **: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
    4.77 -        using an1[unfolded cong_nat_def onen] onen
    4.78 +        using an1[unfolded cong_def onen] onen
    4.79            div_mult_mod_eq[of "(n - 1)" m, symmetric]
    4.80 -        by (simp add:power_add[symmetric] cong_nat_def * del: One_nat_def)
    4.81 +        by (simp add:power_add[symmetric] cong_def * del: One_nat_def)
    4.82        have "[a ^ ((n - 1) mod m) = 1] (mod n)"
    4.83          by (metis cong_mult_rcancel_nat mult.commute ** yn)
    4.84        with m(4)[rule_format, OF th0] nm1
    4.85 @@ -265,9 +265,9 @@
    4.86      also have "\<dots> = ((a^m mod n)^(r div p)) mod n"
    4.87        using power_mod ..
    4.88      also from m(3) onen have "\<dots> = 1"
    4.89 -      by (simp add: cong_nat_def)
    4.90 +      by (simp add: cong_def)
    4.91      finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
    4.92 -      using onen by (simp add: cong_nat_def)
    4.93 +      using onen by (simp add: cong_def)
    4.94      with pn th show ?thesis by blast
    4.95    qed
    4.96    then have "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
    4.97 @@ -315,7 +315,7 @@
    4.98  text \<open>With the special value \<open>0\<close> for non-coprime case, it's more convenient.\<close>
    4.99  lemma ord_works: "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> \<not> [a^ m = 1] (mod n))"
   4.100    for n :: nat
   4.101 -  by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_nat_def\<close>)
   4.102 +  by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_def\<close>)
   4.103  
   4.104  lemma ord: "[a^(ord n a) = 1] (mod n)"
   4.105    for n :: nat
   4.106 @@ -341,10 +341,10 @@
   4.107    then obtain k where "d = ord n a * k"
   4.108      unfolding dvd_def by blast
   4.109    then have "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
   4.110 -    by (simp add : cong_nat_def power_mult power_mod)
   4.111 +    by (simp add : cong_def power_mult power_mod)
   4.112    also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
   4.113 -    using ord[of a n, unfolded cong_nat_def]
   4.114 -    by (simp add: cong_nat_def power_mod)
   4.115 +    using ord[of a n, unfolded cong_def]
   4.116 +    by (simp add: cong_def power_mod)
   4.117    finally show ?lhs .
   4.118  next
   4.119    assume ?lhs
   4.120 @@ -355,7 +355,7 @@
   4.121      show ?thesis
   4.122      proof (cases d)
   4.123        case 0
   4.124 -      with o prem show ?thesis by (simp add: cong_nat_def)
   4.125 +      with o prem show ?thesis by (simp add: cong_def)
   4.126      next
   4.127        case (Suc d')
   4.128        then have d0: "d \<noteq> 0" by simp
   4.129 @@ -374,17 +374,17 @@
   4.130      let ?q = "d div ord n a"
   4.131      let ?r = "d mod ord n a"
   4.132      have eqo: "[(a^?o)^?q = 1] (mod n)"
   4.133 -      by (metis cong_exp_nat ord power_one)
   4.134 +      using cong_pow ord_works by fastforce
   4.135      from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
   4.136      then have op: "?o > 0" by simp
   4.137      from div_mult_mod_eq[of d "ord n a"] \<open>?lhs\<close>
   4.138      have "[a^(?o*?q + ?r) = 1] (mod n)"
   4.139 -      by (simp add: cong_nat_def mult.commute)
   4.140 +      by (simp add: cong_def mult.commute)
   4.141      then have "[(a^?o)^?q * (a^?r) = 1] (mod n)"
   4.142 -      by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
   4.143 +      by (simp add: cong_def power_mult[symmetric] power_add[symmetric])
   4.144      then have th: "[a^?r = 1] (mod n)"
   4.145        using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
   4.146 -      by (simp add: cong_nat_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
   4.147 +      by (simp add: cong_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
   4.148      show ?thesis
   4.149      proof (cases "?r = 0")
   4.150        case True
   4.151 @@ -425,8 +425,7 @@
   4.152      also have "\<dots> \<longleftrightarrow> ord n a dvd c"
   4.153        by (simp only: ord_divides)
   4.154      also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
   4.155 -      using cong_add_lcancel_nat
   4.156 -      by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1)
   4.157 +      by (auto simp add: cong_altdef_nat)
   4.158      finally show ?thesis
   4.159        using c by simp
   4.160    qed
   4.161 @@ -438,7 +437,7 @@
   4.162    next
   4.163      case 2
   4.164      from th[OF na this] show ?thesis
   4.165 -      by (metis cong_sym_nat)
   4.166 +      by (metis cong_sym)
   4.167    qed
   4.168  qed
   4.169  
   4.170 @@ -583,7 +582,7 @@
   4.171      with n have "a^ (n - 1) = 0"
   4.172        by (simp add: power_0_left)
   4.173      with n an mod_less[of 1 n] show False
   4.174 -      by (simp add: power_0_left cong_nat_def)
   4.175 +      by (simp add: power_0_left cong_def)
   4.176    qed
   4.177    with n nqr have aqr0: "a ^ (q * r) \<noteq> 0"
   4.178      by simp
   4.179 @@ -616,7 +615,7 @@
   4.180      then have exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
   4.181        by (simp only: power_mult)
   4.182      then have "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
   4.183 -      by (metis cong_exp_nat ord power_one)
   4.184 +      by (metis cong_pow ord power_one)
   4.185      then have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
   4.186        by (metis cong_to_1_nat exps)
   4.187      from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
   4.188 @@ -694,7 +693,7 @@
   4.189        from n an have "[0 = 1] (mod n)"
   4.190          unfolding a0 power_0_left by auto
   4.191        then show False
   4.192 -        using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])
   4.193 +        using n by (simp add: cong_def dvd_eq_mod_eq_0[symmetric])
   4.194      qed
   4.195      then have a1: "a \<ge> 1" by arith
   4.196      from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
   4.197 @@ -712,11 +711,11 @@
   4.198        then have pS: "Suc (p - 1) = p" by arith
   4.199        from b have d: "n dvd a^((n - 1) div p)"
   4.200          unfolding b0 by auto
   4.201 -      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n show False
   4.202 +      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_iff [OF an] n show False
   4.203          by simp
   4.204      qed
   4.205      then have b1: "b \<ge> 1" by arith
   4.206 -    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]]
   4.207 +    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym [OF b(1)] cong_refl [of 1] b1]]
   4.208        ath b1 b nqr
   4.209      have "coprime (a ^ ((n - 1) div p) - 1) n"
   4.210        by simp
   4.211 @@ -820,7 +819,7 @@
   4.212    from div_mult_mod_eq[of "a^(n - 1)" n]
   4.213      mod_less_divisor[OF n0, of "a^(n - 1)"]
   4.214    have an1: "[a ^ (n - 1) = 1] (mod n)"
   4.215 -    by (metis bqn cong_nat_def mod_mod_trivial)
   4.216 +    by (metis bqn cong_def mod_mod_trivial)
   4.217    have "coprime (a ^ ((n - 1) div p) - 1) n" if p: "prime p" "p dvd q" for p
   4.218    proof -
   4.219      from psp psq have pfpsq: "primefact ps q"
   4.220 @@ -853,10 +852,10 @@
   4.221      }
   4.222      then have *: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
   4.223      have "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
   4.224 -      by (simp add: cong_nat_def)
   4.225 +      by (simp add: cong_def)
   4.226      with ath[OF mod_less_eq_dividend *]
   4.227      have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
   4.228 -      by (metis cong_diff_nat cong_refl_nat)
   4.229 +      by (simp add: cong_diff_nat)
   4.230      then show ?thesis
   4.231        by (metis cong_imp_coprime_nat eq1 p')
   4.232    qed
     5.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Oct 20 23:29:43 2017 +0200
     5.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Oct 20 20:57:55 2017 +0200
     5.3 @@ -146,9 +146,10 @@
     5.4      then have "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q"
     5.5        by (simp add: algebra_simps)
     5.6      then have "kx mod q = ky mod q"
     5.7 -      using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] by (auto simp: cong_int_def)
     5.8 +      using p_inv mod_mult_cong[of "p * p_inv" "q" "1"]
     5.9 +      by (auto simp: cong_def)
    5.10      then have "[kx = ky] (mod q)"
    5.11 -      unfolding cong_int_def by blast
    5.12 +      unfolding cong_def by blast
    5.13      ultimately show ?thesis
    5.14        using cong_less_imp_eq_int k by blast
    5.15    qed
    5.16 @@ -184,12 +185,21 @@
    5.17  proof -
    5.18    obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q"
    5.19      using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
    5.20 -  have *: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
    5.21 -    using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp
    5.22 -    using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp
    5.23 -  have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
    5.24 -    using *(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
    5.25 -    using *(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
    5.26 +  have "fst res = int (y - k1 * p)"
    5.27 +    using \<open>0 \<le> fst res\<close> yk(1) by simp
    5.28 +  moreover have "snd res = int (y - k2 * q)"
    5.29 +    using \<open>0 \<le> snd res\<close> yk(2) by simp
    5.30 +  ultimately have res: "res = (int (y - k1 * p), int (y - k2 * q))"
    5.31 +    by (simp add: prod_eq_iff)
    5.32 +  have y: "k1 * p \<le> y" "k2 * q \<le> y"
    5.33 +    using yk by simp_all
    5.34 +  from y have *: "[y = nat (fst res)] (mod p)" "[y = nat (snd res)] (mod q)"
    5.35 +    by (auto simp add: res cong_le_nat intro: exI [of _ k1] exI [of _ k2])
    5.36 +  from * have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
    5.37 +    using y apply (auto simp add: res of_nat_mult [symmetric] of_nat_mod [symmetric] mod_mod_cancel simp del: of_nat_mult)
    5.38 +     apply (metis \<open>fst res = int (y - k1 * p)\<close> assms(1) assms(2) cong_def mod_pos_pos_trivial nat_int of_nat_mod)
    5.39 +    apply (metis \<open>snd res = int (y - k2 * q)\<close> assms(3) assms(4) cong_def mod_pos_pos_trivial nat_int of_nat_mod)
    5.40 +    done
    5.41    then obtain x where "P_1 res x"
    5.42      unfolding P_1_def
    5.43      using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
    5.44 @@ -320,7 +330,7 @@
    5.45  lemma QR_lemma_08:
    5.46      "f_2 x mod p \<in> Res_l p \<longleftrightarrow> x mod p \<in> Res_h p"
    5.47      "f_2 x mod p \<in> Res_h p \<longleftrightarrow> x mod p \<in> Res_l p"
    5.48 -  using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
    5.49 +  using f_2_lemma_2[of x] cong_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
    5.50      zmod_zminus1_eq_if[of x p] p_eq2
    5.51    by auto
    5.52  
    5.53 @@ -381,7 +391,7 @@
    5.54        from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x"
    5.55          by force
    5.56        from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
    5.57 -        by (auto simp: div_pos_pos_trivial)
    5.58 +        by auto
    5.59        with * show "f_3 (g_3 x) = x"
    5.60          by (simp add: f_3_def g_3_def)
    5.61      qed
     6.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Oct 20 23:29:43 2017 +0200
     6.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Oct 20 20:57:55 2017 +0200
     6.3 @@ -112,7 +112,7 @@
     6.4       apply auto
     6.5     apply (metis invertible_coprime_int)
     6.6    apply (subst (asm) coprime_iff_invertible'_int)
     6.7 -   apply (auto simp add: cong_int_def mult.commute)
     6.8 +   apply (auto simp add: cong_def mult.commute)
     6.9    done
    6.10  
    6.11  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
    6.12 @@ -186,7 +186,7 @@
    6.13  qed
    6.14  
    6.15  lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
    6.16 -  by (auto simp: cong_int_def)
    6.17 +  by (auto simp: cong_def)
    6.18  
    6.19  
    6.20  text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
    6.21 @@ -364,7 +364,7 @@
    6.22      done
    6.23    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
    6.24    then show ?thesis
    6.25 -    by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int)
    6.26 +    by (simp add: cong_def res_neg_eq res_one_eq zmod_int)
    6.27  qed
    6.28  
    6.29  lemma wilson_theorem:
    6.30 @@ -373,7 +373,7 @@
    6.31  proof (cases "p = 2")
    6.32    case True
    6.33    then show ?thesis
    6.34 -    by (simp add: cong_int_def fact_prod)
    6.35 +    by (simp add: cong_def fact_prod)
    6.36  next
    6.37    case False
    6.38    then show ?thesis
     7.1 --- a/src/HOL/Number_Theory/Totient.thy	Fri Oct 20 23:29:43 2017 +0200
     7.2 +++ b/src/HOL/Number_Theory/Totient.thy	Fri Oct 20 20:57:55 2017 +0200
     7.3 @@ -93,7 +93,7 @@
     7.4        by (rule binary_chinese_remainder_unique_nat) (insert assms, simp_all)
     7.5      have "x < m1 * m2 \<and> [x = x] (mod m1) \<and> [x = x] (mod m2)"
     7.6           "y < m1 * m2 \<and> [y = x] (mod m1) \<and> [y = x] (mod m2)"
     7.7 -      using xy assms by (simp_all add: totatives_less one_less_mult cong_nat_def)
     7.8 +      using xy assms by (simp_all add: totatives_less one_less_mult cong_def)
     7.9      from this[THEN the1_equality[OF ex]] show "x = y" by simp
    7.10    qed
    7.11  next
    7.12 @@ -106,7 +106,7 @@
    7.13      fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
    7.14      with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
    7.15      with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
    7.16 -      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_nat_def)
    7.17 +      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
    7.18      from x ab assms(3) have "x \<in> totatives (m1 * m2)"
    7.19        by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
    7.20      with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast