# 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 \Turn off \One_nat_def\\ - -lemma power_eq_one_eq_nat [simp]: "x^m = 1 \ m = 0 \ x = 1" - for x m :: nat - by (induct m) auto - -declare mod_pos_pos_trivial [simp] - - -subsection \Main definitions\ - -class cong = - fixes cong :: "'a \ 'a \ 'a \ bool" ("(1[_ = _] '(()mod _'))") +subsection \Generic congruences\ + +context unique_euclidean_semiring begin +definition cong :: "'a \ 'a \ 'a \ bool" ("(1[_ = _] '(()mod _'))") + where "cong b c a \ b mod a = c mod a" + abbreviation notcong :: "'a \ 'a \ 'a \ bool" ("(1[_ \ _] '(()mod _'))") - where "notcong x y m \ \ cong x y m" + where "notcong b c a \ \ cong b c a" + +lemma cong_mod_left [simp]: + "[b mod a = c] (mod a) \ [b = c] (mod a)" + by (simp add: cong_def) + +lemma cong_mod_right [simp]: + "[b = c mod a] (mod a) \ [b = c] (mod a)" + by (simp add: cong_def) + +lemma cong_dvd_iff: + "a dvd b \ 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) \ 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) \ [c = b] (mod a)" + by (simp add: cong_def) + +lemma cong_sym_eq: + "[b = c] (mod a) \ [c = b] (mod a)" + by (auto simp add: cong_def) + +lemma cong_trans [trans]: + "[b = c] (mod a) \ [c = d] (mod a) \ [b = d] (mod a)" + by (simp add: cong_def) + +lemma cong_add: + "[b = c] (mod a) \ [d = e] (mod a) \ [b + d = c + e] (mod a)" + by (auto simp add: cong_def intro: mod_add_cong) + +lemma cong_mult: + "[b = c] (mod a) \ [d = e] (mod a) \ [b * d = c * e] (mod a)" + by (auto simp add: cong_def intro: mod_mult_cong) + +lemma cong_pow: + "[b = c] (mod a) \ [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 "\x. x \ A \ [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 "(\x. x \ A \ [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) \ [b * d = c * d] (mod a)" + by (simp add: cong_mult) + +lemma cong_scalar_left: + "[b = c] (mod a) \ [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) \ 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) \ [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) \ [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) \ [d = e] (mod a) \ [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) \ [b = c] (mod a)" (is "?P \ ?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) \ [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) \ [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 \Definitions for the natural numbers\ - -instantiation nat :: cong -begin - -definition cong_nat :: "nat \ nat \ nat \ bool" - where "cong_nat x y m \ x mod m = y mod m" - -instance .. - -end - - -subsubsection \Definitions for the integers\ - -instantiation int :: cong -begin - -definition cong_int :: "int \ int \ int \ bool" - where "cong_int x y m \ x mod m = y mod m" - -instance .. - -end - - -subsection \Set up Transfer\ - +subsection \Congruences on @{typ nat} and @{typ int}\ lemma transfer_nat_int_cong: "x \ 0 \ y \ 0 \ m \ 0 \ [nat x = nat y] (mod (nat m)) \ [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) \ [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 \Congruence\ - -(* was zcong_0, etc. *) -lemma cong_0_nat [simp, presburger]: "[a = b] (mod 0) \ a = b" - for a b :: nat - by (auto simp: cong_nat_def) - -lemma cong_0_int [simp, presburger]: "[a = b] (mod 0) \ 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) \ [b = a] (mod m)" - for a b :: nat - by (auto simp: cong_nat_def) - -lemma cong_sym_int: "[a = b] (mod m) \ [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) \ [b = c] (mod m) \ [a = c] (mod m)" - for a b c :: nat - by (auto simp: cong_nat_def) - -lemma cong_trans_int [trans]: "[a = b] (mod m) \ [b = c] (mod m) \ [a = c] (mod m)" - for a b c :: int - by (auto simp: cong_int_def) - -lemma cong_add_nat: "[a = b] (mod m) \ [c = d] (mod m) \ [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) \ [c = d] (mod m) \ [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) \ [c = d] (mod m) \ [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) \ [c = d] (mod m) \ a \ c \ b \ d \ [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 \ c" "b \ 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) \ [c = d] (mod m) \ [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) \ [c = d] (mod m) \ [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) \ [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) \ [x^k = y^k] (mod n)" - for x y :: int - by (induct k) (auto simp: cong_mult_int) - -lemma cong_sum_nat: "(\x. x \ A \ [f x = g x] (mod m)) \ [(\x\A. f x) = (\x\A. g x)] (mod m)" - for f g :: "'a \ nat" - by (induct A rule: infinite_finite_induct) (auto intro: cong_add_nat) - -lemma cong_sum_int: "(\x. x \ A \ [f x = g x] (mod m)) \ [(\x\A. f x) = (\x\A. g x)] (mod m)" - for f g :: "'a \ int" - by (induct A rule: infinite_finite_induct) (auto intro: cong_add_int) - -lemma cong_prod_nat: "(\x. x \ A \ [f x = g x] (mod m)) \ [(\x\A. f x) = (\x\A. g x)] (mod m)" - for f g :: "'a \ 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 \ c" "b \ d" for a b c d m :: nat + using that by (rule cong_diff_aux_int [transferred]) -lemma cong_prod_int: "(\x. x \ A \ [f x = g x] (mod m)) \ [(\x\A. f x) = (\x\A. g x)] (mod m)" - for f g :: "'a \ int" - by (induct A rule: infinite_finite_induct) (auto intro: cong_mult_int) - -lemma cong_scalar_nat: "[a = b] (mod m) \ [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) \ [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) \ [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 \ b \ [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) \ [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 \ b \ [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 \ 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) \ (if x \ 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 \ b \ [a = b] (mod m) \ 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) \ 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) \ [x = y] (mod m)" +lemma cong_abs_int [simp]: "[x = y] (mod abs m) \ [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) \ [a = b] (mod n) \ coprime m n \ [a = b] (mod m * n)" for a b :: int @@ -302,19 +252,19 @@ lemma cong_less_imp_eq_nat: "0 \ a \ a < m \ 0 \ b \ b < m \ [a = b] (mod m) \ 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 \ a \ a < m \ 0 \ b \ b < m \ [a = b] (mod m) \ 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 \ (\!b. 0 \ b \ b < m \ [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 \ (\!b. 0 \ b \ b < m \ [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) \ (\k. b = a + m * k)" for a b :: int @@ -334,20 +284,17 @@ next case False with \?lhs\ 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) \ 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) \ gcd a m = gcd b m" for a b :: nat @@ -363,11 +310,11 @@ lemma cong_cong_mod_nat: "[a = b] (mod m) \ [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) \ [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) \ [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) \ n dvd x \ 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) \ n dvd x \ n dvd y" - for x y :: int - by (auto simp: cong_int_def dvd_eq_mod_eq_0) - -lemma cong_mod_nat: "n \ 0 \ [a mod n = a] (mod n)" - for a n :: nat - by (simp add: cong_nat_def) - -lemma cong_mod_int: "n \ 0 \ [a mod n = a] (mod n)" - for a n :: int - by (simp add: cong_int_def) - -lemma mod_mult_cong_nat: "a \ 0 \ b \ 0 \ [x mod (a * b) = y] (mod a) \ [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) \ [- 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) \ [a = b] (mod - m)" - for a b :: int - by (auto simp add: cong_altdef_int) - -lemma mod_mult_cong_int: "a \ 0 \ b \ 0 \ [x mod (a * b) = y] (mod a) \ [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) \ n = Suc 0" - by (auto simp: cong_nat_def) + by (auto simp: cong_def) lemma cong_0_1_nat: "[0 = 1] (mod n) \ 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) \ n = 1 \ 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) \ a = 0 \ n = 1 \ (\m. a = 1 + m * n)" for a :: nat @@ -524,7 +424,7 @@ case False then show ?thesis using bezout_nat [of a n, OF \a \ 0\] - 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 \ 0 \ \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 "\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 \ \x. [a * x = 1] (mod n)" @@ -598,14 +500,14 @@ lemma coprime_iff_invertible_int: "m > 0 \ coprime a m \ (\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 \ coprime a m \ (\x. 0 \ x \ x < m \ [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 \ coprime a m \ (\x. 0 \ x \ x < m \ [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) \ [x = y] (mod b) \ [x = y] (mod lcm a b)" for x y :: nat apply (cases "y \ 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) \ [x = y] (mod b) \ [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 \ - (\i\A. (\j\A. i \ j \ coprime (m i) (m j))) \ - (\i\A. [(x::nat) = y] (mod m i)) \ - [x = y] (mod (\i\A. m i))" - apply (induct set: finite) - apply auto +lemma cong_cong_prod_coprime_nat: + "[x = y] (mod (\i\A. m i))" if + "(\i\A. [(x::nat) = y] (mod m i))" + and "(\i\A. (\j\A. i \ j \ 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 \ - (\i\A. (\j\A. i \ j \ coprime (m i) (m j))) \ - (\i\A. [(x::int) = y] (mod m i)) \ - [x = y] (mod (\i\A. m i))" - apply (induct set: finite) +lemma cong_cong_prod_coprime_int [rule_format]: + "[x = y] (mod (\i\A. m i))" if + "(\i\A. [(x::int) = y] (mod m i))" + "(\i\A. (\j\A. i \ j \ 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 \[b1 = 1] (mod m1)\) - apply (rule cong_scalar2_nat) - apply (rule \[b2 = 0] (mod m1)\) - done + using \[b1 = 1] (mod m1)\ \[b2 = 0] (mod m1)\ 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 \[b1 = 0] (mod m2)\) - apply (rule cong_scalar2_nat) - apply (rule \[b2 = 1] (mod m2)\) - done + using \[b1 = 0] (mod m2)\ \[b2 = 1] (mod m2)\ cong_add cong_scalar_left by blast then have "[?x = u2] (mod m2)" by simp with \[?x = u1] (mod m1)\ 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 \[b1 = 1] (mod m1)\) - apply (rule cong_scalar2_int) - apply (rule \[b2 = 0] (mod m1)\) - done + using \[b1 = 1] (mod m1)\ \[b2 = 0] (mod m1)\ 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 \[b1 = 0] (mod m2)\) - apply (rule cong_scalar2_int) - apply (rule \[b2 = 1] (mod m2)\) - done + using \[b1 = 0] (mod m2)\ \[b2 = 1] (mod m2)\ cong_add cong_scalar_left by blast then have "[?x = u2] (mod m2)" by simp with \[?x = u1] (mod m1)\ show ?thesis by blast @@ -750,8 +632,8 @@ apply (cases "y \ 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) \ x < m \ y < m \ 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 \[y = u1] (mod m1)\) - 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 \[y = u2] (mod m2)\) 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 "\z. z < m1 * m2 \ [z = u1] (mod m1) \ [z = u2] (mod m2) \ 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 \[?x = u1] (mod m1)\) - apply (rule cong_sym_nat) + apply (rule cong_sym) apply (rule \[z = u1] (mod m1)\) done moreover have "[?x = z] (mod m2)" - apply (rule cong_trans_nat) + apply (rule cong_trans) apply (rule \[?x = u2] (mod m2)\) - apply (rule cong_sym_nat) + apply (rule cong_sym) apply (rule \[z = u2] (mod m2)\) 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 \z < m1 * m2\ \?x < m1 * m2\ 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 "[(\j \ A - {i}. m j) * x = 1] (mod m i)" by auto moreover have "[(\j \ A - {i}. m j) * x = 0] (mod (\j \ A - {i}. m j))" - by (subst mult.commute, rule cong_mult_self_nat) + by (simp add: cong_0_iff) ultimately show "\a. [a = 1] (mod m i) \ [a = 0] (mod prod m (A - {i}))" by blast qed @@ -867,11 +747,11 @@ by auto also have "[u i * b i + (\j \ A - {i}. u j * b j) = u i * 1 + (\j \ 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 \ - (\i\A. (\j\A. i \ j \ coprime (m i) (m j))) \ - (\i\A. [(x::nat) = y] (mod m i)) \ - [x = y] (mod (\i\A. m i))" - apply (induct set: finite) +lemma coprime_cong_prod_nat: + "[x = y] (mod (\i\A. m i))" + if "\i\A. (\j\A. i \ j \ coprime (m i) (m j))" + and "\i\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: "\i\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: "\z. z < (\i\A. m i) \ (\i\A. [z = u i] (mod m i)) \ z = ?x" proof clarify @@ -931,9 +808,9 @@ assume zcong: "(\i\A. [z = u i] (mod m i))" have "\i\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 (\i\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 \b\ ^ (p - 1) = 1] (mod p)" using p_prime proof (rule fermat_theorem) show "\ p dvd nat \b\" - 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 \b\ ^ (p - 1) mod p = 1 mod p" - by (simp add: cong_nat_def) + by (simp add: cong_def) then have "int (nat \b\ ^ (p - 1) mod p) = int (1 mod p)" by simp moreover from odd_p have "\b\ ^ (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 \ {0 .. int p - 1}" unfolding y_def using p_ge_2 by auto hence "y \ 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 "\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 \ x < int p \ [x \ 0](mod p)" for x :: int - by (simp add: cong_int_def) + by (simp add: cong_def) lemma A_ncong_p: "x \ A \ [x \ 0](mod p)" by (rule nonzero_mod_p) (auto simp add: A_def) @@ -187,18 +187,21 @@ lemma B_greater_zero: "x \ B \ 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 \ B" +proof - + from that have "x mod int p \ 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 \ 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 \ C \ 0 < y" -proof (auto simp add: C_def) - fix x :: int - assume x: "x \ B" - moreover from x have "x mod int p \ 0" - using B_ncong_p cong_int_def by simp - moreover have "int y = 0 \ 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 \ {x. 0 < x \ x \ ((int p - 1) div 2)}" apply (auto simp add: F_def E_def C_def) @@ -228,7 +231,7 @@ subsection \Relationships Between Gauss Sets\ lemma StandardRes_inj_on_ResSet: "ResSet m X \ inj_on (\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 "\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 \ D) \ 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 \ A" and c: "z \ A" @@ -314,12 +317,12 @@ apply auto done then have "\x \ 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 ((\x. x mod p) o (op - p)) E = prod (uminus) E](mod p)" - using finite_E p_ge_2 cong_prod_int [of E "(\x. x mod p) o (op - p)" uminus p] + using finite_E p_ge_2 cong_prod [of E "(\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 \Gauss' Lemma\ 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 ((\x. x * a) ` A))] (mod p)" by (simp add: B_def) then have "[prod id A = ((-1)^(card E) * prod (\x. x * a) A)] (mod p)" @@ -351,20 +354,20 @@ ultimately have "[prod id A = ((-1)^(card E) * (prod (\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 \ Legendre a p = -1" by (auto simp add: Legendre_def) moreover have "(-1::int) ^ (card E) = 1 \ (-1::int) ^ (card E) = -1" @@ -384,7 +387,7 @@ moreover have "[1 \ - 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 = "\x. x < n \ [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 \n > 1\] 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 "\ = (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 "\ = 1" using m(3)[unfolded cong_nat_def onen] onen + also have "\ = 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 "\ = ((a^m mod n)^(r div p)) mod n" using power_mod .. also from m(3) onen have "\ = 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 "\m. 0 < m \ m < n - 1 \ \ [a ^ m = 1] (mod n)" @@ -315,7 +315,7 @@ text \With the special value \0\ for non-coprime case, it's more convenient.\ lemma ord_works: "[a ^ (ord n a) = 1] (mod n) \ (\m. 0 < m \ m < ord n a \ \ [a^ m = 1] (mod n))" for n :: nat - by (cases "coprime n a") (use coprime_ord[of n a] in \auto simp add: ord_def cong_nat_def\) + by (cases "coprime n a") (use coprime_ord[of n a] in \auto simp add: ord_def cong_def\) 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 \ 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 \ 0" by (simp add: ord_eq_0) then have op: "?o > 0" by simp from div_mult_mod_eq[of d "ord n a"] \?lhs\ 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 "\ \ ord n a dvd c" by (simp only: ord_divides) also have "\ \ [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) \ 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 \ 1" by arith from one_le_power[OF a1] have ath: "1 \ 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 \ 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 \ 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 \0 \ fst res\ yk(1) by simp + moreover have "snd res = int (y - k2 * q)" + using \0 \ snd res\ 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 \ y" "k2 * q \ 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 \fst res = int (y - k1 * p)\ assms(1) assms(2) cong_def mod_pos_pos_trivial nat_int of_nat_mod) + apply (metis \snd res = int (y - k2 * q)\ 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 \ Res_l p \ x mod p \ Res_h p" "f_2 x mod p \ Res_h p \ x mod p \ 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: "\ x = (- x) mod m" @@ -186,7 +186,7 @@ qed lemma res_eq_to_cong: "(a mod m) = (b mod m) \ [a = b] (mod m)" - by (auto simp: cong_int_def) + by (auto simp: cong_def) text \Simplifying with these will translate a ring equation in R to a congruence.\ @@ -364,7 +364,7 @@ done finally have "fact (p - 1) mod p = \ \" . 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 \ [x = x] (mod m1) \ [x = x] (mod m2)" "y < m1 * m2 \ [y = x] (mod m1) \ [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 \ totatives m1" "b \ 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 \ totatives (m1 * m2)" by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I) with x show "(a, b) \ (\x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast