--- 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
--- 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
--- 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
--- 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
--- 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