# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1532901862 -3600
# Node ID 5b269897df9dfad47fb84b4f8a6f92ea1fa8e8ec
# Parent  f3763989d589e0c9dee3761da938f1d45b3b295a
de-applying and removal of obsolete aliases

diff -r f3763989d589 -r 5b269897df9d src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sun Jul 29 18:24:47 2018 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Sun Jul 29 23:04:22 2018 +0100
@@ -395,11 +395,8 @@
 
 lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   for x y :: nat
-  apply (auto simp add: cong_iff_lin_nat dvd_def)
-  apply (rule_tac x= "k1 * k" in exI)
-  apply (rule_tac x= "k2 * k" in exI)
-  apply (simp add: field_simps)
-  done
+  unfolding cong_iff_lin_nat dvd_def
+  by (metis mult.commute mult.left_commute)
 
 lemma cong_to_1_nat:
   fixes a :: nat
@@ -433,41 +430,36 @@
   for x y :: nat
   by (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE)
 
+
 lemma cong_solve_nat:
   fixes a :: nat
-  assumes "a \<noteq> 0"
   shows "\<exists>x. [a * x = gcd a n] (mod n)"
-proof (cases "n = 0")
+proof (cases "a = 0 \<or> n = 0")
   case True
-  then show ?thesis by force
+  then show ?thesis
+    by (force simp add: cong_0_iff cong_sym)
 next
   case False
   then show ?thesis
-    using bezout_nat [of a n, OF \<open>a \<noteq> 0\<close>]
+    using bezout_nat [of a n]
     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)"
-  for a :: int
-  apply (cases "n = 0")
-   apply (cases "a \<ge> 0")
-    apply auto
-   apply (rule_tac x = "-1" in exI)
-   apply auto
-  apply (insert bezout_int [of a n], auto)
-  apply (metis cong_iff_lin mult.commute)
-  done
+lemma cong_solve_int:
+  fixes a :: int
+  shows "\<exists>x. [a * x = gcd a n] (mod n)"
+    by (metis bezout_int cong_iff_lin mult.commute)
 
 lemma cong_solve_dvd_nat:
   fixes a :: nat
-  assumes a: "a \<noteq> 0" and b: "gcd a n dvd d"
+  assumes "gcd a n dvd d"
   shows "\<exists>x. [a * x = d] (mod n)"
 proof -
-  from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
+  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)"
     using cong_scalar_left by blast
-  also from b have "(d div gcd a n) * gcd a n = d"
+  also from assms 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)"
     by auto
@@ -476,10 +468,11 @@
 qed
 
 lemma cong_solve_dvd_int:
-  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
+  fixes a::int
+  assumes b: "gcd a n dvd d"
   shows "\<exists>x. [a * x = d] (mod n)"
 proof -
-  from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
+  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)"
     using cong_scalar_left by blast
@@ -493,12 +486,11 @@
 
 lemma cong_solve_coprime_nat:
   "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
-  using that cong_solve_nat [of a n] by (cases "a = 0") simp_all
+  using that cong_solve_nat [of a n] by auto
 
 lemma cong_solve_coprime_int:
   "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
-  using that cong_solve_int [of a n] by (cases "a = 0")
-    (auto simp add: zabs_def split: if_splits)
+  using that cong_solve_int [of a n] by (auto simp add: zabs_def split: if_splits)
 
 lemma coprime_iff_invertible_nat:
   "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))" (is "?P \<longleftrightarrow> ?Q")
@@ -529,27 +521,29 @@
 qed
 
 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_def)
-  apply (metis mod_less_divisor mod_mult_right_eq)
-  done
+  assumes "m > 0"
+  shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
+proof -
+  have "\<And>b. \<lbrakk>0 < m; [a * b = Suc 0] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = Suc 0] (mod m)"
+    by (metis cong_def mod_less_divisor [OF assms] mod_mult_right_eq)
+  then show ?thesis
+    using assms coprime_iff_invertible_nat by auto
+qed
 
 lemma coprime_iff_invertible'_int:
-  "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_def)
-  apply (metis mod_mult_right_eq pos_mod_conj)
-  done
+  fixes m :: int
+  assumes "m > 0"
+  shows "coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = 1] (mod m))"
+proof -
+  have "\<And>b. \<lbrakk>0 < m; [a * b = 1] (mod m)\<rbrakk> \<Longrightarrow> \<exists>b'<m. [a * b' = 1] (mod m)"
+    by (meson cong_less_unique_int cong_scalar_left cong_sym cong_trans)
+  then show ?thesis
+    by (metis assms coprime_iff_invertible_int cong_def cong_mult_lcancel mod_pos_pos_trivial pos_mod_conj)
+qed
 
 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 (simp add: cong_altdef_nat)
-  apply (meson cong_altdef_nat cong_sym lcm_least_iff nat_le_linear)
-  done
+  by (meson cong_altdef_nat' lcm_least)
 
 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
@@ -636,10 +630,7 @@
 
 lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
   for x y :: nat
-  apply (cases "y \<le> x")
-   apply (auto simp add: cong_altdef_nat elim: dvd_mult_left)
-  apply (metis cong_def mod_mult_cong_right)
-  done
+  by (metis cong_def mod_mult_cong_right)
 
 lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   for x y :: nat
@@ -651,50 +642,28 @@
     and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
-  from binary_chinese_remainder_nat [OF a] obtain y
-    where "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
-    by blast
+  obtain y where y1: "[y = u1] (mod m1)" and y2: "[y = u2] (mod m2)"
+    using binary_chinese_remainder_nat [OF a] by blast
   let ?x = "y mod (m1 * m2)"
   from nz have less: "?x < m1 * m2"
     by auto
   have 1: "[?x = u1] (mod m1)"
-    apply (rule cong_trans)
-     prefer 2
-     apply (rule \<open>[y = u1] (mod m1)\<close>)
-    apply (rule cong_modulus_mult_nat [of _ _ _ m2])
-    apply simp
-    done
+    using y1 mod_mult_cong_right by blast
   have 2: "[?x = u2] (mod m2)"
-    apply (rule cong_trans)
-     prefer 2
-     apply (rule \<open>[y = u2] (mod m2)\<close>)
-    apply (subst mult.commute)
-    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
-    fix z
-    assume "z < m1 * m2"
-    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
+    using y2 mod_mult_cong_left by blast
+  have "z = ?x" if "z < m1 * m2" "[z = u1] (mod m1)"  "[z = u2] (mod m2)" for z
+  proof -
     have "[?x = z] (mod m1)"
-      apply (rule cong_trans)
-       apply (rule \<open>[?x = u1] (mod m1)\<close>)
-      apply (rule cong_sym)
-      apply (rule \<open>[z = u1] (mod m1)\<close>)
-      done
+      by (metis "1" cong_def that(2))
     moreover have "[?x = z] (mod m2)"
-      apply (rule cong_trans)
-       apply (rule \<open>[?x = u2] (mod m2)\<close>)
-      apply (rule cong_sym)
-      apply (rule \<open>[z = u2] (mod m2)\<close>)
-      done
+      by (metis "2" cong_def that(3))
     ultimately have "[?x = z] (mod m1 * m2)"
       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"
       by (auto simp add: cong_def)
   qed
-  with less 1 2 show ?thesis by auto
+  with less 1 2 show ?thesis
+    by blast
  qed
 
 lemma chinese_remainder_nat:
@@ -720,7 +689,7 @@
     ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
       by blast
   qed
-  then obtain b where b: "\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
+  then obtain b where b: "\<And>i. i \<in> A \<Longrightarrow> [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
     by blast
   let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
   show ?thesis
@@ -735,29 +704,32 @@
         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)
-         apply (rule cong_scalar_left)
-        using b a apply blast
-        apply (rule cong_sum)
-        apply (rule cong_scalar_left)
-        using b apply (auto simp add: mod_eq_0_iff_dvd cong_def)
-        apply (rule dvd_trans [of _ "prod m (A - {x})" "b x" for x])
-        using a fin apply auto
-        done
+      proof (intro cong_add cong_scalar_left cong_sum)
+        show "[b i = 1] (mod m i)"
+          using a b by blast
+        show "[b x = 0] (mod m i)" if "x \<in> A - {i}" for x
+        proof -
+          have "x \<in> A" "x \<noteq> i"
+            using that by auto
+          then show ?thesis
+            using a b [OF \<open>x \<in> A\<close>] cong_dvd_modulus_nat fin by blast
+        qed
+      qed
       finally show ?thesis
         by simp
     qed
   qed
 qed
 
-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 coprime_cong_mult_nat prod_coprime_right)
-  done
+lemma coprime_cong_prod_nat: "[x = y] (mod (\<Prod>i\<in>A. m i))"
+  if "\<And>i j. \<lbrakk>i \<in> A; j \<in> A; i \<noteq> j\<rbrakk> \<Longrightarrow> coprime (m i) (m j)"
+    and "\<And>i. i \<in> A \<Longrightarrow> [x = y] (mod m i)" for x y :: nat
+  using that 
+proof (induct A rule: infinite_finite_induct)
+  case (insert x A)
+  then show ?case
+    by simp (metis coprime_cong_mult_nat prod_coprime_right)
+qed auto
 
 lemma chinese_remainder_unique_nat:
   fixes A :: "'a set"
@@ -795,94 +767,4 @@
     by blast
 qed
 
-
-subsection \<open>Aliasses\<close>
-
-lemma cong_altdef_int:
-  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
-  for a b :: int
-  by (fact cong_iff_dvd_diff)
-
-lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
-  for a b :: int
-  by (fact cong_iff_lin)
-
-lemma cong_minus_int: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
-  for a b :: int
-  by (fact cong_modulus_minus_iff)
-
-lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
-  for a x y :: int
-  by (fact cong_add_lcancel)
-
-lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
-  for a x y :: int
-  by (fact cong_add_rcancel)
-
-lemma cong_add_lcancel_0_int:
-  "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
-  for a x :: int
-  by (fact cong_add_lcancel_0)
-
-lemma cong_add_rcancel_0_int:
-  "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
-  for a x :: int
-  by (fact cong_add_rcancel_0) 
-
-lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
-  for x y :: int
-  by (fact cong_dvd_modulus)
-
-lemma cong_abs_int:
-  "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
-  for x y :: int
-  by (fact cong_abs)
-
-lemma cong_square_int:
-  "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
-  for a :: int
-  by (fact cong_square)
-
-lemma cong_mult_rcancel_int:
-  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
-  if "coprime k m" for a k m :: int
-  using that by (fact cong_mult_rcancel)
-
-lemma cong_mult_lcancel_int:
-  "[k * a = k * b] (mod m) = [a = b] (mod m)"
-  if "coprime k m" for a k m :: int
-  using that by (fact cong_mult_lcancel)
-
-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
-  by (fact coprime_cong_mult)
-
-lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
-  for a b :: nat
-  by (fact cong_gcd_eq)
-
-lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
-  for a b :: int
-  by (fact cong_gcd_eq)
-
-lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
-  for a b :: nat
-  by (fact cong_imp_coprime)
-
-lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
-  for a b :: int
-  by (fact cong_imp_coprime)
-
-lemma cong_cong_prod_coprime_int:
-  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
-    "(\<forall>i\<in>A. [x = y] (mod m i))"
-    "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
-  for x y :: int
-  using that by (fact cong_cong_prod_coprime)
-
-lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
-  for x y :: int
-  by (fact cong_modulus_mult)
-
 end
diff -r f3763989d589 -r 5b269897df9d src/HOL/Number_Theory/Euler_Criterion.thy
--- a/src/HOL/Number_Theory/Euler_Criterion.thy	Sun Jul 29 18:24:47 2018 +0200
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Sun Jul 29 23:04:22 2018 +0100
@@ -48,8 +48,8 @@
     have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
     using p_prime proof (rule fermat_theorem)
       from b p_a_relprime show "\<not> p dvd nat \<bar>b\<bar>"
-        by (auto simp add: cong_altdef_int power2_eq_square)
-          (metis cong_altdef_int cong_dvd_iff dvd_mult2) 
+        by (auto simp add: cong_iff_dvd_diff power2_eq_square)
+          (metis cong_iff_dvd_diff cong_dvd_iff dvd_mult2) 
     qed
     then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
       by (simp add: cong_def)
@@ -90,13 +90,13 @@
     cong_scalar_right [of "x * y'" 1 "int p" a]
     by (auto simp add: cong_def ac_simps)
   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
+  hence "y \<in> S1" using calculation cong_iff_dvd_diff p_a_relprime S1_def cong_dvd_iff by fastforce
   ultimately have "P x y" unfolding P_def by blast
   moreover {
     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 cong_trans by blast
+      using co_xp cong_mult_lcancel[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
@@ -200,7 +200,8 @@
   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
+    using True assms(1) prime_dvd_power_int_iff
+    by (simp add: cong_iff_dvd_diff)
   then show ?thesis unfolding Legendre_def using True cong_sym
     by auto
 next
diff -r f3763989d589 -r 5b269897df9d src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Jul 29 18:24:47 2018 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Sun Jul 29 23:04:22 2018 +0100
@@ -18,7 +18,7 @@
 lemma cong_prime_prod_zero_int:
   "[a * b = 0] (mod p) \<Longrightarrow> prime p \<Longrightarrow> [a = 0] (mod p) \<or> [b = 0] (mod p)"
   for a :: int
-  by (auto simp add: cong_altdef_int prime_dvd_mult_iff)
+  by (simp add: cong_0_iff prime_dvd_mult_iff)
 
 
 locale GAUSS =
@@ -114,11 +114,11 @@
     for x y
   proof -
     from p_a_relprime have "\<not> p dvd a"
-      by (simp add: cong_altdef_int)
+      by (simp add: cong_0_iff)
     with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
     have "coprime a (int p)"
       by (simp_all add: ac_simps)
-    with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
+    with a cong_mult_rcancel [of a "int p" x y] have "[x = y] (mod p)"
       by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
       order_le_less_trans [of x "(int p - 1) div 2" p]
@@ -127,12 +127,8 @@
       by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
   qed
   show ?thesis
-    apply (insert p_ge_2 p_a_relprime p_minus_one_l)
-    apply (auto simp add: B_def)
-    apply (rule ResSet_image)
-      apply (auto simp add: A_res)
-    apply (auto simp add: A_def *)
-    done
+    using p_ge_2 p_a_relprime p_minus_one_l
+    by (metis "*" A_def A_res B_def GAUSS.ResSet_image GAUSS_axioms greaterThanAtMost_iff odd_p odd_pos of_nat_0_less_iff)
 qed
 
 lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
@@ -149,11 +145,11 @@
     from a have a': "[x * a = y * a](mod p)"
       using cong_def by blast
     from p_a_relprime have "\<not>p dvd a"
-      by (simp add: cong_altdef_int)
+      by (simp add: cong_0_iff)
     with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
     have "coprime a (int p)"
       by (simp_all add: ac_simps)  
-    with a' cong_mult_rcancel_int [of a "int p" x y]
+    with a' cong_mult_rcancel [of a "int p" x y]
     have "[x = y] (mod p)" by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
       order_le_less_trans [of x "(int p - 1) div 2" p]
@@ -224,7 +220,7 @@
   "coprime x p" if "x \<in> A"
 proof -
   from A_ncong_p [OF that] have "\<not> int p dvd x"
-    by (simp add: cong_altdef_int)
+    by (simp add: cong_0_iff)
   with p_prime show ?thesis
     by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer)
 qed
@@ -370,7 +366,7 @@
   then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
     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)
+    by (metis cong_mult_lcancel)
   then show ?thesis
     by (simp add: A_card_eq cong_sym)
 qed
@@ -390,7 +386,8 @@
   moreover have "(-1::int) ^ (card E) = 1 \<or> (-1::int) ^ (card E) = -1"
     using neg_one_even_power neg_one_odd_power by blast
   moreover have "[1 \<noteq> - 1] (mod int p)"
-    using cong_altdef_int nonzero_mod_p[of 2] p_odd_int by fastforce
+    using cong_iff_dvd_diff [where 'a=int] nonzero_mod_p[of 2] p_odd_int   
+    by fastforce
   ultimately show ?thesis
     by (auto simp add: cong_sym)
 qed
diff -r f3763989d589 -r 5b269897df9d src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Sun Jul 29 18:24:47 2018 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sun Jul 29 23:04:22 2018 +0100
@@ -121,7 +121,7 @@
   obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
     by blast
   from ma nb x have "coprime x a" "coprime x b"
-    using cong_imp_coprime_nat cong_sym by blast+
+    using cong_imp_coprime cong_sym by blast+
   then have "coprime x (a*b)"
     by simp
   with x show ?thesis
@@ -209,7 +209,7 @@
     by arith+
   from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
     by simp
-  from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
+  from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime an1
   have an: "coprime a n" "coprime (a ^ (n - 1)) n"
     using \<open>n \<ge> 2\<close> by simp_all
   have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "\<exists>m. ?P m")
@@ -716,7 +716,7 @@
         by simp
     qed
     then have b1: "b \<ge> 1" by arith
-    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym [OF b(1)] cong_refl [of 1] b1]]
+    from cong_imp_coprime[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
@@ -858,7 +858,7 @@
     have "[a ^ ((n - 1) div p) mod n - 1 = a ^ ((n - 1) div p) - 1] (mod n)"
       by (simp add: cong_diff_nat)
     then show ?thesis
-      by (metis cong_imp_coprime_nat eq1 p')
+      by (metis cong_imp_coprime eq1 p')
   qed
   with pocklington[OF n qrn[symmetric] nq2 an1] show ?thesis
     by blast
diff -r f3763989d589 -r 5b269897df9d src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Jul 29 18:24:47 2018 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Jul 29 23:04:22 2018 +0100
@@ -93,7 +93,7 @@
 
 lemma Gpq: "GAUSS p q"
   using p_prime pq_neq p_ge_2 q_prime
-  by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq)
+  by (auto simp: GAUSS_def cong_iff_dvd_diff dest: primes_dvd_imp_eq)
 
 lemma Gqp: "GAUSS q p"
   by (simp add: QRqp QR.Gpq)
@@ -304,7 +304,7 @@
   by (simp add: f_2_def)
 
 lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)"
-  by (simp add: f_2_def cong_altdef_int)
+  by (simp add: f_2_def cong_iff_dvd_diff)
 
 lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S"
   using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger