--- a/src/HOL/Divides.thy Tue Nov 21 17:18:10 2017 +0100
+++ b/src/HOL/Divides.thy Thu Nov 23 13:00:00 2017 +0000
@@ -904,11 +904,11 @@
subsubsection \<open>Quotients of Signs\<close>
-lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
-by (simp add: divide_int_def)
+lemma div_eq_minus1: "0 < b \<Longrightarrow> - 1 div b = - 1" for b :: int
+ by (simp add: divide_int_def)
-lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
-by (simp add: modulo_int_def)
+lemma zmod_minus1: "0 < b \<Longrightarrow> - 1 mod b = b - 1" for b :: int
+ by (auto simp add: modulo_int_def)
lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
apply (subgoal_tac "a div b \<le> -1", force)
--- a/src/HOL/Euclidean_Division.thy Tue Nov 21 17:18:10 2017 +0100
+++ b/src/HOL/Euclidean_Division.thy Thu Nov 23 13:00:00 2017 +0000
@@ -1084,6 +1084,10 @@
and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
+lemma Suc_0_mod_eq [simp]:
+ "Suc 0 mod n = of_bool (n \<noteq> Suc 0)"
+ by (cases n) simp_all
+
context
fixes m n q :: nat
begin
--- a/src/HOL/Number_Theory/Euler_Criterion.thy Tue Nov 21 17:18:10 2017 +0100
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy Thu Nov 23 13:00:00 2017 +0000
@@ -13,9 +13,24 @@
assumes p_a_relprime: "[a \<noteq> 0](mod p)"
begin
-private lemma odd_p: "odd p" using p_ge_2 p_prime prime_odd_nat by blast
+private lemma odd_p: "odd p"
+ using p_ge_2 p_prime prime_odd_nat by blast
+
+private lemma p_minus_1_int:
+ "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
-private lemma p_minus_1_int: "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
+private lemma p_not_eq_Suc_0 [simp]:
+ "p \<noteq> Suc 0"
+ using p_ge_2 by simp
+
+private lemma one_mod_int_p_eq [simp]:
+ "1 mod int p = 1"
+proof -
+ from p_ge_2 have "int 1 mod int p = int 1"
+ by simp
+ then show ?thesis
+ by simp
+qed
private lemma E_1:
assumes "QuadRes (int p) a"
@@ -41,7 +56,7 @@
moreover from odd_p have "\<bar>b\<bar> ^ (p - Suc 0) = b ^ (p - Suc 0)"
by (simp add: power_even_abs)
ultimately show ?thesis
- by (simp add: zmod_int cong_def)
+ by (auto simp add: cong_def zmod_int)
qed
ultimately show ?thesis
by (auto intro: cong_trans)
@@ -68,8 +83,10 @@
by (simp add: ac_simps)
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_right [of "x * y'"] unfolding cong_def mult.assoc by auto
+ ultimately have "[x * y = a] (mod p)"
+ using mod_mult_right_eq [of x "y' * a" p]
+ 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
ultimately have "P x y" unfolding P_def by blast
--- a/src/HOL/Parity.thy Tue Nov 21 17:18:10 2017 +0100
+++ b/src/HOL/Parity.thy Thu Nov 23 13:00:00 2017 +0000
@@ -191,12 +191,11 @@
lemma one_mod_2_pow_eq [simp]:
"1 mod (2 ^ n) = of_bool (n > 0)"
proof -
- have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
- by (induct n) (simp_all add: mod_mult2_eq)
- then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
+ have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
+ using of_nat_mod [of 1 "2 ^ n"] by simp
+ also have "\<dots> = of_bool (n > 0)"
by simp
- then show ?thesis
- by (simp add: of_nat_mod)
+ finally show ?thesis .
qed
lemma even_of_nat [simp]: