# HG changeset patch
# User haftmann
# Date 1511442000 0
# Node ID 6b2c0681ef2853041243b25239cec8c841b6a02e
# Parent  4e4bea76e5595c97abc8f553b0dc5809b729ee66
new simp rule

diff -r 4e4bea76e559 -r 6b2c0681ef28 src/HOL/Divides.thy
--- 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)
diff -r 4e4bea76e559 -r 6b2c0681ef28 src/HOL/Euclidean_Division.thy
--- 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
diff -r 4e4bea76e559 -r 6b2c0681ef28 src/HOL/Number_Theory/Euler_Criterion.thy
--- 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
diff -r 4e4bea76e559 -r 6b2c0681ef28 src/HOL/Parity.thy
--- 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]: