# HG changeset patch
# User haftmann
# Date 1508525875 -7200
# Node ID 930abfdf8727a124ea520371a017fba6b54a93cc
# Parent  72b78ee82f7b4be875f2b669e69397c9d16a9e08
algebraic foundation for congruences

diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -32,236 +32,187 @@
   imports "HOL-Computational_Algebra.Primes"
 begin
 
-subsection \<open>Turn off \<open>One_nat_def\<close>\<close>
-
-lemma power_eq_one_eq_nat [simp]: "x^m = 1 \<longleftrightarrow> m = 0 \<or> x = 1"
-  for x m :: nat
-  by (induct m) auto
-
-declare mod_pos_pos_trivial [simp]
-
-
-subsection \<open>Main definitions\<close>
-
-class cong =
-  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ = _] '(()mod _'))")
+subsection \<open>Generic congruences\<close>
+ 
+context unique_euclidean_semiring
 begin
 
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ = _] '(()mod _'))")
+  where "cong b c a \<longleftrightarrow> b mod a = c mod a"
+  
 abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(()mod _'))")
-  where "notcong x y m \<equiv> \<not> cong x y m"
+  where "notcong b c a \<equiv> \<not> cong b c a"
+
+lemma cong_mod_left [simp]:
+  "[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
+  by (simp add: cong_def)  
+
+lemma cong_mod_right [simp]:
+  "[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)"
+  by (simp add: cong_def)  
+
+lemma cong_dvd_iff:
+  "a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)"
+  using that by (auto simp: cong_def dvd_eq_mod_eq_0)
+
+lemma cong_0 [simp, presburger]:
+  "[b = c] (mod 0) \<longleftrightarrow> b = c"
+  by (simp add: cong_def)
+
+lemma cong_1 [simp, presburger]:
+  "[b = c] (mod 1)"
+  by (simp add: cong_def)
+
+lemma cong_refl [simp]:
+  "[b = b] (mod a)"
+  by (simp add: cong_def)
+
+lemma cong_sym: 
+  "[b = c] (mod a) \<Longrightarrow> [c = b] (mod a)"
+  by (simp add: cong_def)
+
+lemma cong_sym_eq:
+  "[b = c] (mod a) \<longleftrightarrow> [c = b] (mod a)"
+  by (auto simp add: cong_def)
+
+lemma cong_trans [trans]:
+  "[b = c] (mod a) \<Longrightarrow> [c = d] (mod a) \<Longrightarrow> [b = d] (mod a)"
+  by (simp add: cong_def)
+
+lemma cong_add:
+  "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b + d = c + e] (mod a)"
+  by (auto simp add: cong_def intro: mod_add_cong)
+
+lemma cong_mult:
+  "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b * d = c * e] (mod a)"
+  by (auto simp add: cong_def intro: mod_mult_cong)
+
+lemma cong_pow:
+  "[b = c] (mod a) \<Longrightarrow> [b ^ n = c ^ n] (mod a)"
+  by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a])
+
+lemma cong_sum:
+  "[sum f A = sum g A] (mod a)" if "\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a)"
+  using that by (induct A rule: infinite_finite_induct) (auto intro: cong_add)
+
+lemma cong_prod:
+  "[prod f A = prod g A] (mod a)" if "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a))"
+  using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult)
+
+lemma cong_scalar_right:
+  "[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)"
+  by (simp add: cong_mult)
+
+lemma cong_scalar_left:
+  "[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)"
+  by (simp add: cong_mult)
+
+lemma cong_mult_self_right: "[b * a = 0] (mod a)"
+  by (simp add: cong_def)
+
+lemma cong_mult_self_left: "[a * b = 0] (mod a)"
+  by (simp add: cong_def)
+
+lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b"
+  by (simp add: cong_def dvd_eq_mod_eq_0)
+
+lemma mod_mult_cong_right:
+  "[c mod (a * b) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
+  by (simp add: cong_def mod_mod_cancel mod_add_left_eq)
+
+lemma mod_mult_cong_left:
+  "[c mod (b * a) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
+  using mod_mult_cong_right [of c a b d] by (simp add: ac_simps)
+
+end
+
+context unique_euclidean_ring
+begin
+
+lemma cong_diff:
+  "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b - d = c - e] (mod a)"
+  by (auto simp add: cong_def intro: mod_diff_cong)
+
+lemma cong_diff_iff_cong_0:
+  "[b - c = 0] (mod a) \<longleftrightarrow> [b = c] (mod a)" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then have "[b - c + c = 0 + c] (mod a)"
+    by (rule cong_add) simp
+  then show ?Q
+    by simp
+next
+  assume ?Q
+  with cong_diff [of b c a c c] show ?P
+    by simp
+qed
+
+lemma cong_minus_minus_iff:
+  "[- b = - c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
+  using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
+  by (simp add: cong_0_iff dvd_diff_commute)
+
+lemma cong_modulus_minus_iff: "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
+  using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]
+  by (simp add: cong_0_iff)
 
 end
 
 
-subsubsection \<open>Definitions for the natural numbers\<close>
-
-instantiation nat :: cong
-begin
-
-definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "cong_nat x y m \<longleftrightarrow> x mod m = y mod m"
-
-instance ..
-
-end
-
-
-subsubsection \<open>Definitions for the integers\<close>
-
-instantiation int :: cong
-begin
-
-definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
-  where "cong_int x y m \<longleftrightarrow> x mod m = y mod m"
-
-instance ..
-
-end
-
-
-subsection \<open>Set up Transfer\<close>
-
+subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
 
 lemma transfer_nat_int_cong:
   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
   for x y m :: int
-  unfolding cong_int_def cong_nat_def
-  by (metis int_nat_eq nat_mod_distrib zmod_int)
+  by (auto simp add: cong_def nat_mod_distrib [symmetric])
+     (metis eq_nat_nat_iff le_less mod_by_0 pos_mod_conj)
 
 declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
 
-lemma transfer_int_nat_cong: "[int x = int y] (mod (int m)) = [x = y] (mod m)"
-  by (auto simp add: cong_int_def cong_nat_def) (auto simp add: zmod_int [symmetric])
+lemma cong_int_iff:
+  "[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)"
+  by (simp add: cong_def of_nat_mod [symmetric])
+
+lemma transfer_int_nat_cong:
+  "[int x = int y] (mod (int m)) = [x = y] (mod m)"
+  by (fact cong_int_iff)
 
 declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong]
 
-
-subsection \<open>Congruence\<close>
-
-(* was zcong_0, etc. *)
-lemma cong_0_nat [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b"
-  for a b :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_0_int [simp, presburger]: "[a = b] (mod 0) \<longleftrightarrow> a = b"
-  for a b :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_1_nat [simp, presburger]: "[a = b] (mod 1)"
-  for a b :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_Suc_0_nat [simp, presburger]: "[a = b] (mod Suc 0)"
-  for a b :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_1_int [simp, presburger]: "[a = b] (mod 1)"
-  for a b :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_refl_nat [simp]: "[k = k] (mod m)"
-  for k :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_refl_int [simp]: "[k = k] (mod m)"
-  for k :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_sym_nat: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
-  for a b :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_sym_int: "[a = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
-  for a b :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_sym_eq_nat: "[a = b] (mod m) = [b = a] (mod m)"
-  for a b :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_sym_eq_int: "[a = b] (mod m) = [b = a] (mod m)"
-  for a b :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_trans_nat [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
-  for a b c :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_trans_int [trans]: "[a = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
-  for a b c :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_add_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
-  for a b c :: nat
-  unfolding cong_nat_def by (metis mod_add_cong)
-
-lemma cong_add_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
-  for a b c :: int
-  unfolding cong_int_def by (metis mod_add_cong)
-
-lemma cong_diff_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
-  for a b c :: int
-  unfolding cong_int_def by (metis mod_diff_cong)
+lemma cong_Suc_0 [simp, presburger]:
+  "[m = n] (mod Suc 0)"
+  using cong_1 [of m n] by simp
 
 lemma cong_diff_aux_int:
   "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
     a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
   for a b c d :: int
-  by (metis cong_diff_int tsub_eq)
+  by (metis cong_diff tsub_eq)
 
 lemma cong_diff_nat:
-  fixes a b c d :: nat
-  assumes "[a = b] (mod m)" "[c = d] (mod m)" "a \<ge> c" "b \<ge> d"
-  shows "[a - c = b - d] (mod m)"
-  using assms by (rule cong_diff_aux_int [transferred])
-
-lemma cong_mult_nat: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
-  for a b c d :: nat
-  unfolding cong_nat_def  by (metis mod_mult_cong)
-
-lemma cong_mult_int: "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
-  for a b c d :: int
-  unfolding cong_int_def  by (metis mod_mult_cong)
-
-lemma cong_exp_nat: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
-  for x y :: nat
-  by (induct k) (auto simp: cong_mult_nat)
-
-lemma cong_exp_int: "[x = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
-  for x y :: int
-  by (induct k) (auto simp: cong_mult_int)
-
-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)"
-  for f g :: "'a \<Rightarrow> nat"
-  by (induct A rule: infinite_finite_induct) (auto intro: cong_add_nat)
-
-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)"
-  for f g :: "'a \<Rightarrow> int"
-  by (induct A rule: infinite_finite_induct) (auto intro: cong_add_int)
-
-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)"
-  for f g :: "'a \<Rightarrow> nat"
-  by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_nat)
+  "[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
+    and "a \<ge> c" "b \<ge> d" for a b c d m :: nat 
+  using that by (rule cong_diff_aux_int [transferred])
 
-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)"
-  for f g :: "'a \<Rightarrow> int"
-  by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_int)
-
-lemma cong_scalar_nat: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
-  for a b k :: nat
-  by (rule cong_mult_nat) simp_all
-
-lemma cong_scalar_int: "[a = b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
-  for a b k :: int
-  by (rule cong_mult_int) simp_all
-
-lemma cong_scalar2_nat: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
-  for a b k :: nat
-  by (rule cong_mult_nat) simp_all
+lemma cong_diff_iff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [tsub a b = 0] (mod m) = [a = b] (mod m)"
+  for a b :: int
+  by (subst tsub_eq, assumption, rule cong_diff_iff_cong_0)
 
-lemma cong_scalar2_int: "[a = b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
-  for a b k :: int
-  by (rule cong_mult_int) simp_all
-
-lemma cong_mult_self_nat: "[a * m = 0] (mod m)"
-  for a m :: nat
-  by (auto simp: cong_nat_def)
-
-lemma cong_mult_self_int: "[a * m = 0] (mod m)"
-  for a m :: int
-  by (auto simp: cong_int_def)
-
-lemma cong_eq_diff_cong_0_int: "[a = b] (mod m) = [a - b = 0] (mod m)"
-  for a b :: int
-  by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self)
-
-lemma cong_eq_diff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [a = b] (mod m) = [tsub a b = 0] (mod m)"
-  for a b :: int
-  by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
-
-lemma cong_eq_diff_cong_0_nat:
+lemma cong_diff_iff_cong_0_nat:
   fixes a b :: nat
   assumes "a \<ge> b"
-  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
-  using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
-
-lemma cong_diff_cong_0'_nat:
-  "[x = y] (mod n) \<longleftrightarrow> (if x \<le> y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
-  for x y :: nat
-  by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear)
+  shows "[a - b = 0] (mod m) = [a = b] (mod m)"
+  using assms by (rule cong_diff_iff_cong_0_aux_int [transferred])
 
 lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   for a b :: nat
-  apply (subst cong_eq_diff_cong_0_nat, assumption)
-  apply (unfold cong_nat_def)
-  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-  done
+  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
 
 lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   for a b :: int
-  by (metis cong_int_def mod_eq_dvd_iff)
+  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
 
-lemma cong_abs_int: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)"
+lemma cong_abs_int [simp]: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)"
   for x y :: int
   by (simp add: cong_altdef_int)
 
@@ -289,7 +240,6 @@
   for a k m :: int
   by (simp add: mult.commute cong_mult_rcancel_int)
 
-(* was zcong_zgcd_zmult_zmod *)
 lemma coprime_cong_mult_int:
   "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   for a b :: int
@@ -302,19 +252,19 @@
 
 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"
   for a b :: nat
-  by (auto simp add: cong_nat_def)
+  by (auto simp add: cong_def)
 
 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"
   for a b :: int
-  by (auto simp add: cong_int_def)
+  by (auto simp add: cong_def)
 
 lemma cong_less_unique_nat: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   for a m :: nat
-  by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
+  by (auto simp: cong_def) (metis mod_less_divisor mod_mod_trivial)
 
 lemma cong_less_unique_int: "0 < m \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   for a m :: int
-  by (auto simp: cong_int_def)  (metis mod_mod_trivial pos_mod_conj)
+  by (auto simp: cong_def)  (metis mod_mod_trivial pos_mod_conj)
 
 lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
   for a b :: int
@@ -334,20 +284,17 @@
   next
     case False
     with \<open>?lhs\<close> show ?rhs
-      apply (subst (asm) cong_sym_eq_nat)
-      apply (auto simp: cong_altdef_nat)
-      apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
-      done
+      by (metis cong_def mult.commute nat_le_linear nat_mod_eq_lemma)
   qed
 next
   assume ?rhs
   then show ?lhs
-    by (metis cong_nat_def mod_mult_self2 mult.commute)
+    by (metis cong_def mult.commute nat_mod_eq_iff) 
 qed
 
 lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   for a b :: int
-  by (metis cong_int_def gcd_red_int)
+  by (auto simp add: cong_def) (metis gcd_red_int)
 
 lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   for a b :: nat
@@ -363,11 +310,11 @@
 
 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: nat
-  by (auto simp add: cong_nat_def)
+  by simp
 
 lemma cong_cong_mod_int: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: int
-  by (auto simp add: cong_int_def)
+  by simp
 
 lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
   for a b :: int
@@ -434,53 +381,6 @@
   for x y :: int
   by (auto simp add: cong_altdef_int dvd_def)
 
-lemma cong_dvd_eq_nat: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
-  for x y :: nat
-  by (auto simp: cong_nat_def dvd_eq_mod_eq_0)
-
-lemma cong_dvd_eq_int: "[x = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
-  for x y :: int
-  by (auto simp: cong_int_def dvd_eq_mod_eq_0)
-
-lemma cong_mod_nat: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
-  for a n :: nat
-  by (simp add: cong_nat_def)
-
-lemma cong_mod_int: "n \<noteq> 0 \<Longrightarrow> [a mod n = a] (mod n)"
-  for a n :: int
-  by (simp add: cong_int_def)
-
-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)"
-  for a b :: nat
-  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
-
-lemma neg_cong_int: "[a = b] (mod m) \<longleftrightarrow> [- a = - b] (mod m)"
-  for a b :: int
-  by (metis cong_int_def minus_minus mod_minus_cong)
-
-lemma cong_modulus_neg_int: "[a = b] (mod m) \<longleftrightarrow> [a = b] (mod - m)"
-  for a b :: int
-  by (auto simp add: cong_altdef_int)
-
-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)"
-  for a b :: int
-proof (cases "b > 0")
-  case True
-  then show ?thesis
-    by (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
-next
-  case False
-  then show ?thesis
-    apply (subst (1 2) cong_modulus_neg_int)
-    apply (unfold cong_int_def)
-    apply (subgoal_tac "a * b = (- a * - b)")
-     apply (erule ssubst)
-     apply (subst zmod_zmult2_eq)
-      apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
-     apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
-    done
-qed
-
 lemma cong_to_1_nat:
   fixes a :: nat
   assumes "[a = 1] (mod n)"
@@ -494,15 +394,15 @@
 qed
 
 lemma cong_0_1_nat': "[0 = Suc 0] (mod n) \<longleftrightarrow> n = Suc 0"
-  by (auto simp: cong_nat_def)
+  by (auto simp: cong_def)
 
 lemma cong_0_1_nat: "[0 = 1] (mod n) \<longleftrightarrow> n = 1"
   for n :: nat
-  by (auto simp: cong_nat_def)
+  by (auto simp: cong_def)
 
 lemma cong_0_1_int: "[0 = 1] (mod n) \<longleftrightarrow> n = 1 \<or> n = - 1"
   for n :: int
-  by (auto simp: cong_int_def zmult_eq_1_iff)
+  by (auto simp: cong_def zmult_eq_1_iff)
 
 lemma cong_to_1'_nat: "[a = 1] (mod n) \<longleftrightarrow> a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
   for a :: nat
@@ -524,7 +424,7 @@
   case False
   then show ?thesis
     using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>]
-    by auto (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
+    by auto (metis cong_add_rcancel_0_nat cong_mult_self_left)
 qed
 
 lemma cong_solve_int: "a \<noteq> 0 \<Longrightarrow> \<exists>x. [a * x = gcd a n] (mod n)"
@@ -546,7 +446,7 @@
   from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
     by auto
   then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
-    by (elim cong_scalar2_nat)
+    using cong_scalar_left by blast
   also from b have "(d div gcd a n) * gcd a n = d"
     by (rule dvd_div_mult_self)
   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
@@ -562,7 +462,7 @@
   from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
     by auto
   then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
-    by (elim cong_scalar2_int)
+    using cong_scalar_left by blast
   also from b have "(d div gcd a n) * gcd a n = d"
     by (rule dvd_div_mult_self)
   also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
@@ -577,10 +477,12 @@
   shows "\<exists>x. [a * x = 1] (mod n)"
 proof (cases "a = 0")
   case True
-  with assms show ?thesis by force
+  with assms show ?thesis
+    by (simp add: cong_0_1_nat') 
 next
   case False
-  with assms show ?thesis by (metis cong_solve_nat)
+  with assms show ?thesis
+    by (metis cong_solve_nat)
 qed
 
 lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
@@ -598,14 +500,14 @@
 lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   for m :: int
   apply (auto intro: cong_solve_coprime_int)
-  apply (metis cong_int_def coprime_mul_eq gcd_1_int gcd.commute gcd_red_int)
+  using cong_gcd_eq_int coprime_mul_eq' apply fastforce
   done
 
 lemma coprime_iff_invertible'_nat:
   "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
   apply (subst coprime_iff_invertible_nat)
    apply auto
-  apply (auto simp add: cong_nat_def)
+  apply (auto simp add: cong_def)
   apply (metis mod_less_divisor mod_mult_right_eq)
   done
 
@@ -613,35 +515,35 @@
   "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
   for m :: int
   apply (subst coprime_iff_invertible_int)
-   apply (auto simp add: cong_int_def)
+   apply (auto simp add: cong_def)
   apply (metis mod_mult_right_eq pos_mod_conj)
   done
 
 lemma cong_cong_lcm_nat: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   for x y :: nat
   apply (cases "y \<le> x")
-  apply (metis cong_altdef_nat lcm_least)
-  apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear)
+   apply (simp add: cong_altdef_nat)
+  apply (meson cong_altdef_nat cong_sym lcm_least_iff nat_le_linear)
   done
 
 lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   for x y :: int
   by (auto simp add: cong_altdef_int lcm_least)
 
-lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
-    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
-    (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
-      [x = y] (mod (\<Prod>i\<in>A. m i))"
-  apply (induct set: finite)
-  apply auto
+lemma cong_cong_prod_coprime_nat:
+  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
+    "(\<forall>i\<in>A. [(x::nat) = y] (mod m i))"
+    and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
+  using that apply (induct A rule: infinite_finite_induct)
+    apply auto
   apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   done
 
-lemma cong_cong_prod_coprime_int [rule_format]: "finite A \<Longrightarrow>
-    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
-    (\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
-      [x = y] (mod (\<Prod>i\<in>A. m i))"
-  apply (induct set: finite)
+lemma cong_cong_prod_coprime_int [rule_format]:
+  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
+    "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
+    "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
+  using that apply (induct A rule: infinite_finite_induct)
   apply auto
   apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
   done
@@ -658,9 +560,9 @@
   from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
-    by (subst mult.commute) (rule cong_mult_self_nat)
+    by (simp add: cong_mult_self_left)
   moreover have "[m2 * x2 = 0] (mod m2)"
-    by (subst mult.commute) (rule cong_mult_self_nat)
+    by (simp add: cong_mult_self_left)
   ultimately show ?thesis
     using 1 2 by blast
 qed
@@ -677,9 +579,9 @@
   from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
-    by (subst mult.commute) (rule cong_mult_self_int)
+    by (simp add: cong_mult_self_left)
   moreover have "[m2 * x2 = 0] (mod m2)"
-    by (subst mult.commute) (rule cong_mult_self_int)
+    by (simp add: cong_mult_self_left)
   ultimately show ?thesis
     using 1 2 by blast
 qed
@@ -695,20 +597,10 @@
     by blast
   let ?x = "u1 * b1 + u2 * b2"
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
-    apply (rule cong_add_nat)
-     apply (rule cong_scalar2_nat)
-     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
-    apply (rule cong_scalar2_nat)
-    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
-    done
+    using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
-    apply (rule cong_add_nat)
-     apply (rule cong_scalar2_nat)
-     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
-    apply (rule cong_scalar2_nat)
-    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
-    done
+    using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u2] (mod m2)"
     by simp
   with \<open>[?x = u1] (mod m1)\<close> show ?thesis
@@ -726,20 +618,10 @@
     by blast
   let ?x = "u1 * b1 + u2 * b2"
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
-    apply (rule cong_add_int)
-     apply (rule cong_scalar2_int)
-     apply (rule \<open>[b1 = 1] (mod m1)\<close>)
-    apply (rule cong_scalar2_int)
-    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
-    done
+    using \<open>[b1 = 1] (mod m1)\<close> \<open>[b2 = 0] (mod m1)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
-    apply (rule cong_add_int)
-     apply (rule cong_scalar2_int)
-     apply (rule \<open>[b1 = 0] (mod m2)\<close>)
-    apply (rule cong_scalar2_int)
-    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
-    done
+    using \<open>[b1 = 0] (mod m2)\<close> \<open>[b2 = 1] (mod m2)\<close> cong_add cong_scalar_left by blast
   then have "[?x = u2] (mod m2)" by simp
   with \<open>[?x = u1] (mod m1)\<close> show ?thesis
     by blast
@@ -750,8 +632,8 @@
   apply (cases "y \<le> x")
    apply (simp add: cong_altdef_nat)
    apply (erule dvd_mult_left)
-  apply (rule cong_sym_nat)
-  apply (subst (asm) cong_sym_eq_nat)
+  apply (rule cong_sym)
+  apply (subst (asm) cong_sym_eq)
   apply (simp add: cong_altdef_nat)
   apply (erule dvd_mult_left)
   done
@@ -764,7 +646,7 @@
 
 lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   for x y :: nat
-  by (simp add: cong_nat_def)
+  by (simp add: cong_def)
 
 lemma binary_chinese_remainder_unique_nat:
   fixes m1 m2 :: nat
@@ -779,21 +661,19 @@
   from nz have less: "?x < m1 * m2"
     by auto
   have 1: "[?x = u1] (mod m1)"
-    apply (rule cong_trans_nat)
+    apply (rule cong_trans)
      prefer 2
      apply (rule \<open>[y = u1] (mod m1)\<close>)
-    apply (rule cong_modulus_mult_nat)
-    apply (rule cong_mod_nat)
-    using nz apply auto
+    apply (rule cong_modulus_mult_nat [of _ _ _ m2])
+    apply simp
     done
   have 2: "[?x = u2] (mod m2)"
-    apply (rule cong_trans_nat)
+    apply (rule cong_trans)
      prefer 2
      apply (rule \<open>[y = u2] (mod m2)\<close>)
     apply (subst mult.commute)
-    apply (rule cong_modulus_mult_nat)
-    apply (rule cong_mod_nat)
-    using nz apply auto
+    apply (rule cong_modulus_mult_nat [of _ _ _ m1])
+    apply simp
     done
   have "\<forall>z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
   proof clarify
@@ -801,22 +681,22 @@
     assume "z < m1 * m2"
     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
     have "[?x = z] (mod m1)"
-      apply (rule cong_trans_nat)
+      apply (rule cong_trans)
        apply (rule \<open>[?x = u1] (mod m1)\<close>)
-      apply (rule cong_sym_nat)
+      apply (rule cong_sym)
       apply (rule \<open>[z = u1] (mod m1)\<close>)
       done
     moreover have "[?x = z] (mod m2)"
-      apply (rule cong_trans_nat)
+      apply (rule cong_trans)
        apply (rule \<open>[?x = u2] (mod m2)\<close>)
-      apply (rule cong_sym_nat)
+      apply (rule cong_sym)
       apply (rule \<open>[z = u2] (mod m2)\<close>)
       done
     ultimately have "[?x = z] (mod m1 * m2)"
-      by (auto intro: coprime_cong_mult_nat a)
+      using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right)
     with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
       apply (intro cong_less_modulus_unique_nat)
-        apply (auto, erule cong_sym_nat)
+        apply (auto, erule cong_sym)
       done
   qed
   with less 1 2 show ?thesis by auto
@@ -838,7 +718,7 @@
   then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
     by auto
   moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
-    by (subst mult.commute, rule cong_mult_self_nat)
+    by (simp add: cong_0_iff)
   ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
     by blast
 qed
@@ -867,11 +747,11 @@
         by auto
       also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
                   u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
-        apply (rule cong_add_nat)
-         apply (rule cong_scalar2_nat)
+        apply (rule cong_add)
+         apply (rule cong_scalar_left)
         using b a apply blast
-        apply (rule cong_sum_nat)
-        apply (rule cong_scalar2_nat)
+        apply (rule cong_sum)
+        apply (rule cong_scalar_left)
         using b apply auto
         apply (rule cong_dvd_modulus_nat)
          apply (drule (1) bspec)
@@ -886,11 +766,11 @@
   qed
 qed
 
-lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
-    (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
-      (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
-         [x = y] (mod (\<Prod>i\<in>A. m i))"
-  apply (induct set: finite)
+lemma coprime_cong_prod_nat:
+  "[x = y] (mod (\<Prod>i\<in>A. m i))"
+  if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+    and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
+  using that apply (induct A rule: infinite_finite_induct)
   apply auto
   apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   done
@@ -914,15 +794,12 @@
     by auto
   have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)"
     apply auto
-    apply (rule cong_trans_nat)
+    apply (rule cong_trans)
      prefer 2
     using one apply auto
-    apply (rule cong_dvd_modulus_nat)
-     apply (rule cong_mod_nat)
-    using prodnz apply auto
-    apply rule
-     apply (rule fin)
-    apply assumption
+    apply (rule cong_dvd_modulus_nat [of _ _ "prod m A"])
+     apply simp
+    using fin apply auto
     done
   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"
   proof clarify
@@ -931,9 +808,9 @@
     assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))"
     have "\<forall>i\<in>A. [?x = z] (mod m i)"
       apply clarify
-      apply (rule cong_trans_nat)
+      apply (rule cong_trans)
       using cong apply (erule bspec)
-      apply (rule cong_sym_nat)
+      apply (rule cong_sym)
       using zcong apply auto
       done
     with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
@@ -943,7 +820,7 @@
     with zless less show "z = ?x"
       apply (intro cong_less_modulus_unique_nat)
         apply auto
-      apply (erule cong_sym_nat)
+      apply (erule cong_sym)
       done
   qed
   from less cong unique show ?thesis
diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Euler_Criterion.thy
--- a/src/HOL/Number_Theory/Euler_Criterion.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -24,7 +24,7 @@
   from assms obtain b where b: "[b ^ 2 = a] (mod int p)"
     unfolding QuadRes_def by blast
   then have "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod int p)"
-    by (simp add: cong_exp_int cong_sym_int power_mult)
+    by (simp add: cong_pow cong_sym power_mult)
   then have "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod int p)"
     using odd_p by force
   moreover have "[b ^ (p - 1) = 1] (mod int p)"
@@ -32,19 +32,19 @@
     have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
     using p_prime proof (rule fermat_theorem)
       show "\<not> p dvd nat \<bar>b\<bar>"
-        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))
+        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))
     qed
     then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
-      by (simp add: cong_nat_def)
+      by (simp add: cong_def)
     then have "int (nat \<bar>b\<bar> ^ (p - 1) mod p) = int (1 mod p)"
       by simp
     moreover from odd_p have "\<bar>b\<bar> ^ (p - Suc 0) = b ^ (p - Suc 0)"
       by (simp add: power_even_abs)
     ultimately show ?thesis
-      by (simp add: zmod_int cong_int_def)
+      by (simp add: zmod_int cong_def)
   qed
   ultimately show ?thesis
-    by (auto intro: cong_trans_int)
+    by (auto intro: cong_trans)
 qed
 
 private definition S1 :: "int set" where "S1 = {0 <.. int p - 1}"
@@ -69,7 +69,7 @@
   then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
   moreover define y where "y = y' * a mod p"
   ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
-    cong_scalar_int[of "x * y'"] unfolding cong_int_def mult.assoc by auto
+    cong_scalar_right [of "x * y'"] unfolding cong_def mult.assoc by auto
   moreover have "y \<in> {0 .. int p - 1}" unfolding y_def using p_ge_2 by auto
   hence "y \<in> S1" using calculation cong_altdef_int p_a_relprime S1_def by auto
   ultimately have "P x y" unfolding P_def by blast
@@ -77,7 +77,7 @@
     fix y1 y2
     assume "P x y1" "P x y2"
     moreover hence "[y1 = y2] (mod p)" unfolding P_def
-      using co_xp cong_mult_lcancel_int[of x p y1 y2] cong_sym_int cong_trans_int by blast
+      using co_xp cong_mult_lcancel_int[of x p y1 y2] cong_sym cong_trans by blast
     ultimately have "y1 = y2" unfolding P_def S1_def using cong_less_imp_eq_int by auto
   }
   ultimately show ?thesis by blast
@@ -144,7 +144,8 @@
     using x Suc(1)[of S'] Suc(2) Suc(3) by (simp add: card_ge_0_finite)
   moreover have "prod g S = g x * prod g S'"
     using x S'_def Suc(2) prod.remove[of S x g] by fastforce
-  ultimately show ?case using x Suc(3) cong_mult_int by simp
+  ultimately show ?case using x Suc(3) cong_mult
+    by simp blast 
 qed
 
 private lemma l11: assumes "~ QuadRes p a"
@@ -162,24 +163,31 @@
   using assms l2 l10 l11 unfolding S2_def by blast
 
 private lemma E_2: assumes "~ QuadRes p a"
-  shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans_int cong_sym_int assms by blast
+  shows "[a ^ ((p - 1) div 2) = -1] (mod p)" using l9 l12 cong_trans cong_sym assms by blast
 
 lemma euler_criterion_aux: "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)"
-  using E_1 E_2 Legendre_def cong_sym_int p_a_relprime by presburger
+  using p_a_relprime by (auto simp add: Legendre_def
+    intro!: cong_sym [of _ 1] cong_sym [of _ "- 1"]
+    dest: E_1 E_2)
 
 end
 
 theorem euler_criterion: assumes "prime p" "2 < p"
   shows "[(Legendre a p) = a ^ ((p - 1) div 2)] (mod p)"
 proof (cases "[a = 0] (mod p)")
-case True
-  hence "[a ^ ((p - 1) div 2) = 0 ^ ((p - 1) div 2)] (mod p)" using cong_exp_int by blast
-  moreover have "(0::int) ^ ((p - 1) div 2) = 0" using zero_power[of "(p - 1) div 2"] assms(2) by simp
-  ultimately have "[a ^ ((p - 1) div 2) = 0] (mod p)" using cong_trans_int cong_refl_int by presburger
-  thus ?thesis unfolding Legendre_def using True cong_sym_int by presburger
+  case True
+  then have "[a ^ ((p - 1) div 2) = 0 ^ ((p - 1) div 2)] (mod p)"
+    using cong_pow by blast
+  moreover have "(0::int) ^ ((p - 1) div 2) = 0"
+    using zero_power [of "(p - 1) div 2"] assms(2) by simp
+  ultimately have "[a ^ ((p - 1) div 2) = 0] (mod p)"
+    using True assms(1) cong_altdef_int prime_dvd_power_int_iff by auto
+  then show ?thesis unfolding Legendre_def using True cong_sym
+    by auto
 next
-case False
-  thus ?thesis using euler_criterion_aux assms by presburger
+  case False
+  then show ?thesis
+    using euler_criterion_aux assms by presburger
 qed
 
 hide_fact euler_criterion_aux
diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -146,7 +146,7 @@
     for x y
   proof -
     from a have a': "[x * a = y * a](mod p)"
-      by (metis cong_int_def)
+      using cong_def by blast
     from p_a_relprime have "\<not>p dvd a"
       by (simp add: cong_altdef_int)
     with p_prime have "coprime a (int p)"
@@ -173,7 +173,7 @@
 
 lemma nonzero_mod_p: "0 < x \<Longrightarrow> x < int p \<Longrightarrow> [x \<noteq> 0](mod p)"
   for x :: int
-  by (simp add: cong_int_def)
+  by (simp add: cong_def)
 
 lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
   by (rule nonzero_mod_p) (auto simp add: A_def)
@@ -187,18 +187,21 @@
 lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
   using a_nonzero by (auto simp add: B_def A_greater_zero)
 
+lemma B_mod_greater_zero:
+  "0 < x mod int p" if "x \<in> B"
+proof -
+  from that have "x mod int p \<noteq> 0"
+    using B_ncong_p cong_def cong_mult_self_left by blast
+  moreover from that have "0 < x"
+    by (rule B_greater_zero)
+  then have "0 \<le> x mod int p"
+    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
+  ultimately show ?thesis
+    by simp
+qed
+
 lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
-proof (auto simp add: C_def)
-  fix x :: int
-  assume x: "x \<in> B"
-  moreover from x have "x mod int p \<noteq> 0"
-    using B_ncong_p cong_int_def by simp
-  moreover have "int y = 0 \<or> 0 < int y" for y
-    by linarith
-  ultimately show "0 < x mod int p"
-    using B_greater_zero [of x]
-    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
-qed
+  by (auto simp add: C_def B_mod_greater_zero)
 
 lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
   apply (auto simp add: F_def E_def C_def)
@@ -228,7 +231,7 @@
 subsection \<open>Relationships Between Gauss Sets\<close>
 
 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> inj_on (\<lambda>b. b mod m) X"
-  by (auto simp add: ResSet_def inj_on_def cong_int_def)
+  by (auto simp add: ResSet_def inj_on_def cong_def)
 
 lemma B_card_eq_A: "card B = card A"
   using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
@@ -261,8 +264,8 @@
   apply (insert finite_B SR_B_inj)
   apply (drule prod.reindex [of "\<lambda>x. x mod int p" B id])
   apply auto
-  apply (rule cong_prod_int)
-  apply (auto simp add: cong_int_def)
+  apply (rule cong_prod)
+  apply (auto simp add: cong_def)
   done
 
 lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
@@ -273,11 +276,11 @@
   fix y z :: int
   assume "p - (y * a) mod p = (z * a) mod p"
   then have "[(y * a) mod p + (z * a) mod p = 0] (mod p)"
-    by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
+    by (metis add.commute diff_eq_eq dvd_refl cong_def dvd_eq_mod_eq_0 mod_0)
   moreover have "[y * a = (y * a) mod p] (mod p)"
-    by (metis cong_int_def mod_mod_trivial)
+    by (metis cong_def mod_mod_trivial)
   ultimately have "[a * (y + z) = 0] (mod p)"
-    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
+    by (metis cong_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
   with p_prime a_nonzero p_a_relprime have a: "[y + z = 0] (mod p)"
     by (auto dest!: cong_prime_prod_zero_int)
   assume b: "y \<in> A" and c: "z \<in> A"
@@ -314,12 +317,12 @@
     apply auto
     done
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
-    by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
+    by (metis cong_def minus_mod_self1 mod_mod_trivial)
   then have "[prod ((\<lambda>x. x mod p) o (op - p)) E = prod (uminus) E](mod p)"
-    using finite_E p_ge_2 cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
+    using finite_E p_ge_2 cong_prod [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
     by auto
   then have two: "[prod id F = prod (uminus) E](mod p)"
-    by (metis FE cong_cong_mod_int cong_refl_int cong_prod_int minus_mod_self1)
+    by (metis FE cong_cong_mod_int cong_refl cong_prod minus_mod_self1)
   have "prod uminus E = (-1) ^ card E * prod id E"
     using finite_E by (induct set: finite) auto
   with two show ?thesis
@@ -330,18 +333,18 @@
 subsection \<open>Gauss' Lemma\<close>
 
 lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
-  by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
+  by auto
 
 theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
   have "[prod id A = prod id F * prod id D](mod p)"
     by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
   then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
-    by (rule cong_trans_int) (metis cong_scalar_int prod_F_zcong)
+    by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
   then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
-    by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
+    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)
   then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
-    by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
+    by (rule cong_trans) (metis C_B_zcong_prod cong_scalar_left)
   then have "[prod id A = ((-1)^(card E) * prod id ((\<lambda>x. x * a) ` A))] (mod p)"
     by (simp add: B_def)
   then have "[prod id A = ((-1)^(card E) * prod (\<lambda>x. x * a) A)] (mod p)"
@@ -351,20 +354,20 @@
   ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A * prod id A))] (mod p)"
     by simp
   then have "[prod id A = ((-1)^(card E) * a^(card A) * prod id A)](mod p)"
-    by (rule cong_trans_int)
-      (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
+    by (rule cong_trans)
+      (simp add: cong_scalar_left cong_scalar_right finite_A prod_constant ac_simps)
   then have a: "[prod id A * (-1)^(card E) =
       ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
-    by (rule cong_scalar_int)
+    by (rule cong_scalar_right)
   then have "[prod id A * (-1)^(card E) = prod id A *
       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
-    by (rule cong_trans_int) (simp add: a mult.commute mult.left_commute)
+    by (rule cong_trans) (simp add: a ac_simps)
   then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
-    by (rule cong_trans_int) (simp add: aux cong del: prod.strong_cong)
+    by (rule cong_trans) (simp add: aux cong del: prod.strong_cong)
   with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
     by (metis cong_mult_lcancel_int)
   then show ?thesis
-    by (simp add: A_card_eq cong_sym_int)
+    by (simp add: A_card_eq cong_sym)
 qed
 
 theorem gauss_lemma: "Legendre a p = (-1) ^ (card E)"
@@ -376,7 +379,7 @@
   then have "[a ^ nat (int ((p - 1) div 2)) = a ^ nat ((int p - 1) div 2)] (mod int p)"
     by force
   ultimately have "[Legendre a p = (-1) ^ (card E)] (mod p)"
-    using pre_gauss_lemma cong_trans_int by blast
+    using pre_gauss_lemma cong_trans by blast
   moreover from p_a_relprime have "Legendre a p = 1 \<or> Legendre a p = -1"
     by (auto simp add: Legendre_def)
   moreover have "(-1::int) ^ (card E) = 1 \<or> (-1::int) ^ (card E) = -1"
@@ -384,7 +387,7 @@
   moreover have "[1 \<noteq> - 1] (mod int p)"
     using cong_altdef_int nonzero_mod_p[of 2] p_odd_int by fastforce
   ultimately show ?thesis
-    by (auto simp add: cong_sym_int)
+    by (auto simp add: cong_sym)
 qed
 
 end
diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -40,7 +40,7 @@
 proof (cases "a = 0")
   case True
   with an show ?thesis
-    by (simp add: cong_nat_def)
+    by (simp add: cong_def)
 next
   case False
   from bezout_add_strong_nat [OF this]
@@ -56,7 +56,7 @@
   then have "a * (x * b) mod n = b mod n"
     by (simp add: mod_add_left_eq)
   then have "[a * (x * b) = b] (mod n)"
-    by (simp only: cong_nat_def)
+    by (simp only: cong_def)
   then show ?thesis by blast
 qed
 
@@ -70,17 +70,17 @@
   let ?P = "\<lambda>x. x < n \<and> [a * x = b] (mod n)"
   let ?x = "x mod n"
   from x have *: "[a * ?x = b] (mod n)"
-    by (simp add: cong_nat_def mod_mult_right_eq[of a x n])
+    by (simp add: cong_def mod_mult_right_eq[of a x n])
   from mod_less_divisor[ of n x] nz * have Px: "?P ?x" by simp
   have "y = ?x" if Py: "y < n" "[a * y = b] (mod n)" for y
   proof -
     from Py(2) * have "[a * y = a * ?x] (mod n)"
-      by (simp add: cong_nat_def)
+      by (simp add: cong_def)
     then have "[y = ?x] (mod n)"
       by (metis an cong_mult_lcancel_nat)
     with mod_less[OF Py(1)] mod_less_divisor[ of n x] nz
     show ?thesis
-      by (simp add: cong_nat_def)
+      by (simp add: cong_def)
   qed
   with Px show ?thesis by blast
 qed
@@ -103,7 +103,7 @@
   proof
     assume "y = 0"
     with y(2) have "p dvd a"
-      by (auto dest: cong_dvd_eq_nat)
+      using cong_dvd_iff by auto
     then show False
       by (metis gcd_nat.absorb1 not_prime_1 p pa)
   qed
@@ -151,14 +151,14 @@
   next
     case 2
     with am m show ?thesis
-      by (metis am cong_0_nat gcd_nat.right_neutral power_eq_one_eq_nat)
+      by simp
   next
     case 3
     from m obtain m' where m': "m = Suc m'" by (cases m) blast+
     have "d = 1" if d: "d dvd a" "d dvd n" for d
     proof -
       from am mod_less[OF \<open>n > 1\<close>] have am1: "a^m mod n = 1"
-        by (simp add: cong_nat_def)
+        by (simp add: cong_def)
       from dvd_mult2[OF d(1), of "a^m'"] have dam: "d dvd a^m"
         by (simp add: m')
       from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
@@ -234,13 +234,13 @@
         by (simp add: algebra_simps power_mult)
       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
         using power_mod[of "a^m" n "(n - 1) div m"] by simp
-      also have "\<dots> = 1" using m(3)[unfolded cong_nat_def onen] onen
+      also have "\<dots> = 1" using m(3)[unfolded cong_def onen] onen
         by (metis power_one)
       finally have *: "?y mod n = 1"  .
       have **: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
-        using an1[unfolded cong_nat_def onen] onen
+        using an1[unfolded cong_def onen] onen
           div_mult_mod_eq[of "(n - 1)" m, symmetric]
-        by (simp add:power_add[symmetric] cong_nat_def * del: One_nat_def)
+        by (simp add:power_add[symmetric] cong_def * del: One_nat_def)
       have "[a ^ ((n - 1) mod m) = 1] (mod n)"
         by (metis cong_mult_rcancel_nat mult.commute ** yn)
       with m(4)[rule_format, OF th0] nm1
@@ -265,9 +265,9 @@
     also have "\<dots> = ((a^m mod n)^(r div p)) mod n"
       using power_mod ..
     also from m(3) onen have "\<dots> = 1"
-      by (simp add: cong_nat_def)
+      by (simp add: cong_def)
     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
-      using onen by (simp add: cong_nat_def)
+      using onen by (simp add: cong_def)
     with pn th show ?thesis by blast
   qed
   then have "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
@@ -315,7 +315,7 @@
 text \<open>With the special value \<open>0\<close> for non-coprime case, it's more convenient.\<close>
 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))"
   for n :: nat
-  by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_nat_def\<close>)
+  by (cases "coprime n a") (use coprime_ord[of n a] in \<open>auto simp add: ord_def cong_def\<close>)
 
 lemma ord: "[a^(ord n a) = 1] (mod n)"
   for n :: nat
@@ -341,10 +341,10 @@
   then obtain k where "d = ord n a * k"
     unfolding dvd_def by blast
   then have "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
-    by (simp add : cong_nat_def power_mult power_mod)
+    by (simp add : cong_def power_mult power_mod)
   also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)"
-    using ord[of a n, unfolded cong_nat_def]
-    by (simp add: cong_nat_def power_mod)
+    using ord[of a n, unfolded cong_def]
+    by (simp add: cong_def power_mod)
   finally show ?lhs .
 next
   assume ?lhs
@@ -355,7 +355,7 @@
     show ?thesis
     proof (cases d)
       case 0
-      with o prem show ?thesis by (simp add: cong_nat_def)
+      with o prem show ?thesis by (simp add: cong_def)
     next
       case (Suc d')
       then have d0: "d \<noteq> 0" by simp
@@ -374,17 +374,17 @@
     let ?q = "d div ord n a"
     let ?r = "d mod ord n a"
     have eqo: "[(a^?o)^?q = 1] (mod n)"
-      by (metis cong_exp_nat ord power_one)
+      using cong_pow ord_works by fastforce
     from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
     then have op: "?o > 0" by simp
     from div_mult_mod_eq[of d "ord n a"] \<open>?lhs\<close>
     have "[a^(?o*?q + ?r) = 1] (mod n)"
-      by (simp add: cong_nat_def mult.commute)
+      by (simp add: cong_def mult.commute)
     then have "[(a^?o)^?q * (a^?r) = 1] (mod n)"
-      by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
+      by (simp add: cong_def power_mult[symmetric] power_add[symmetric])
     then have th: "[a^?r = 1] (mod n)"
       using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
-      by (simp add: cong_nat_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
+      by (simp add: cong_def del: One_nat_def) (metis mod_mult_left_eq nat_mult_1)
     show ?thesis
     proof (cases "?r = 0")
       case True
@@ -425,8 +425,7 @@
     also have "\<dots> \<longleftrightarrow> ord n a dvd c"
       by (simp only: ord_divides)
     also have "\<dots> \<longleftrightarrow> [e + c = e + 0] (mod ord n a)"
-      using cong_add_lcancel_nat
-      by (metis cong_dvd_eq_nat dvd_0_right cong_dvd_modulus_nat cong_mult_self_nat nat_mult_1)
+      by (auto simp add: cong_altdef_nat)
     finally show ?thesis
       using c by simp
   qed
@@ -438,7 +437,7 @@
   next
     case 2
     from th[OF na this] show ?thesis
-      by (metis cong_sym_nat)
+      by (metis cong_sym)
   qed
 qed
 
@@ -583,7 +582,7 @@
     with n have "a^ (n - 1) = 0"
       by (simp add: power_0_left)
     with n an mod_less[of 1 n] show False
-      by (simp add: power_0_left cong_nat_def)
+      by (simp add: power_0_left cong_def)
   qed
   with n nqr have aqr0: "a ^ (q * r) \<noteq> 0"
     by simp
@@ -616,7 +615,7 @@
     then have exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
       by (simp only: power_mult)
     then have "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
-      by (metis cong_exp_nat ord power_one)
+      by (metis cong_pow ord power_one)
     then have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
       by (metis cong_to_1_nat exps)
     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
@@ -694,7 +693,7 @@
       from n an have "[0 = 1] (mod n)"
         unfolding a0 power_0_left by auto
       then show False
-        using n by (simp add: cong_nat_def dvd_eq_mod_eq_0[symmetric])
+        using n by (simp add: cong_def dvd_eq_mod_eq_0[symmetric])
     qed
     then have a1: "a \<ge> 1" by arith
     from one_le_power[OF a1] have ath: "1 \<le> a ^ ((n - 1) div p)" .
@@ -712,11 +711,11 @@
       then have pS: "Suc (p - 1) = p" by arith
       from b have d: "n dvd a^((n - 1) div p)"
         unfolding b0 by auto
-      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n show False
+      from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_iff [OF an] n show False
         by simp
     qed
     then have b1: "b \<ge> 1" by arith
-    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]]
+    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym [OF b(1)] cong_refl [of 1] b1]]
       ath b1 b nqr
     have "coprime (a ^ ((n - 1) div p) - 1) n"
       by simp
@@ -820,7 +819,7 @@
   from div_mult_mod_eq[of "a^(n - 1)" n]
     mod_less_divisor[OF n0, of "a^(n - 1)"]
   have an1: "[a ^ (n - 1) = 1] (mod n)"
-    by (metis bqn cong_nat_def mod_mod_trivial)
+    by (metis bqn cong_def mod_mod_trivial)
   have "coprime (a ^ ((n - 1) div p) - 1) n" if p: "prime p" "p dvd q" for p
   proof -
     from psp psq have pfpsq: "primefact ps q"
@@ -853,10 +852,10 @@
     }
     then have *: "a ^ ((n - 1) div p) mod n \<noteq> 0" by auto
     have "[a ^ ((n - 1) div p) mod n = a ^ ((n - 1) div p)] (mod n)"
-      by (simp add: cong_nat_def)
+      by (simp add: cong_def)
     with ath[OF mod_less_eq_dividend *]
     have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
-      by (metis cong_diff_nat cong_refl_nat)
+      by (simp add: cong_diff_nat)
     then show ?thesis
       by (metis cong_imp_coprime_nat eq1 p')
   qed
diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -146,9 +146,10 @@
     then have "(p * p_inv * kx) mod q = (p * p_inv * ky) mod q"
       by (simp add: algebra_simps)
     then have "kx mod q = ky mod q"
-      using p_inv mod_mult_cong[of "p * p_inv" "q" "1"] by (auto simp: cong_int_def)
+      using p_inv mod_mult_cong[of "p * p_inv" "q" "1"]
+      by (auto simp: cong_def)
     then have "[kx = ky] (mod q)"
-      unfolding cong_int_def by blast
+      unfolding cong_def by blast
     ultimately show ?thesis
       using cong_less_imp_eq_int k by blast
   qed
@@ -184,12 +185,21 @@
 proof -
   obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q"
     using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce
-  have *: "[y = fst res] (mod p)" "[y = snd res] (mod q)"
-    using yk(1) assms(1) cong_iff_lin_int[of "fst res"] cong_sym_int apply simp
-    using yk(2) assms(3) cong_iff_lin_int[of "snd res"] cong_sym_int by simp
-  have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
-    using *(1) mod_mod_cancel[of "int p"] assms(1) assms(2) cong_int_def apply simp
-    using *(2) mod_mod_cancel[of "int q"] assms(3) assms(4) cong_int_def by simp
+  have "fst res = int (y - k1 * p)"
+    using \<open>0 \<le> fst res\<close> yk(1) by simp
+  moreover have "snd res = int (y - k2 * q)"
+    using \<open>0 \<le> snd res\<close> yk(2) by simp
+  ultimately have res: "res = (int (y - k1 * p), int (y - k2 * q))"
+    by (simp add: prod_eq_iff)
+  have y: "k1 * p \<le> y" "k2 * q \<le> y"
+    using yk by simp_all
+  from y have *: "[y = nat (fst res)] (mod p)" "[y = nat (snd res)] (mod q)"
+    by (auto simp add: res cong_le_nat intro: exI [of _ k1] exI [of _ k2])
+  from * have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res"
+    using y apply (auto simp add: res of_nat_mult [symmetric] of_nat_mod [symmetric] mod_mod_cancel simp del: of_nat_mult)
+     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)
+    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)
+    done
   then obtain x where "P_1 res x"
     unfolding P_1_def
     using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce
@@ -320,7 +330,7 @@
 lemma QR_lemma_08:
     "f_2 x mod p \<in> Res_l p \<longleftrightarrow> x mod p \<in> Res_h p"
     "f_2 x mod p \<in> Res_h p \<longleftrightarrow> x mod p \<in> Res_l p"
-  using f_2_lemma_2[of x] cong_int_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
+  using f_2_lemma_2[of x] cong_def[of "f_2 x" "p - x" p] minus_mod_self2[of x p]
     zmod_zminus1_eq_if[of x p] p_eq2
   by auto
 
@@ -381,7 +391,7 @@
       from that have *: "(fst x + (snd x - 1) * int p) mod int p = fst x"
         by force
       from that have "(fst x + (snd x - 1) * int p) div int p + 1 = snd x"
-        by (auto simp: div_pos_pos_trivial)
+        by auto
       with * show "f_3 (g_3 x) = x"
         by (simp add: f_3_def g_3_def)
     qed
diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -112,7 +112,7 @@
      apply auto
    apply (metis invertible_coprime_int)
   apply (subst (asm) coprime_iff_invertible'_int)
-   apply (auto simp add: cong_int_def mult.commute)
+   apply (auto simp add: cong_def mult.commute)
   done
 
 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
@@ -186,7 +186,7 @@
 qed
 
 lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
-  by (auto simp: cong_int_def)
+  by (auto simp: cong_def)
 
 
 text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
@@ -364,7 +364,7 @@
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>" .
   then show ?thesis
-    by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int)
+    by (simp add: cong_def res_neg_eq res_one_eq zmod_int)
 qed
 
 lemma wilson_theorem:
@@ -373,7 +373,7 @@
 proof (cases "p = 2")
   case True
   then show ?thesis
-    by (simp add: cong_int_def fact_prod)
+    by (simp add: cong_def fact_prod)
 next
   case False
   then show ?thesis
diff -r 72b78ee82f7b -r 930abfdf8727 src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Fri Oct 20 23:29:43 2017 +0200
+++ b/src/HOL/Number_Theory/Totient.thy	Fri Oct 20 20:57:55 2017 +0200
@@ -93,7 +93,7 @@
       by (rule binary_chinese_remainder_unique_nat) (insert assms, simp_all)
     have "x < m1 * m2 \<and> [x = x] (mod m1) \<and> [x = x] (mod m2)"
          "y < m1 * m2 \<and> [y = x] (mod m1) \<and> [y = x] (mod m2)"
-      using xy assms by (simp_all add: totatives_less one_less_mult cong_nat_def)
+      using xy assms by (simp_all add: totatives_less one_less_mult cong_def)
     from this[THEN the1_equality[OF ex]] show "x = y" by simp
   qed
 next
@@ -106,7 +106,7 @@
     fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
     with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
     with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
-      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_nat_def)
+      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
     from x ab assms(3) have "x \<in> totatives (m1 * m2)"
       by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
     with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast