# HG changeset patch
# User haftmann
# Date 1512233453 0
# Node ID ccab07d1196c8c91a9d08a94a3d6cc596122ceae
# Parent  19f6274072643f85d646f78b48e4ffdb6f494a7b
more simplification rules

diff -r 19f627407264 -r ccab07d1196c src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Algebra/IntRing.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -248,10 +248,12 @@
     by (metis dvd_def mult.commute)
 next
   assume "UNIV = {uu. \<exists>x. uu = x * p}"
-  then obtain x where "1 = x * p" by best
-  then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
+  then obtain x where "1 = x * p"
+    by best
+  then have "\<bar>p * x\<bar> = 1"
+    by (simp add: ac_simps)
   then show False using prime
-    by (auto dest!: abs_zmult_eq_1 simp: prime_def)
+    by (auto simp add: abs_mult zmult_eq_1_iff)
 qed
 
 
diff -r 19f627407264 -r ccab07d1196c src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Computational_Algebra/Primes.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -115,15 +115,11 @@
   "prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: int
   using that by (auto intro!: primeI prime_elemI)
 
-lemma prime_elem_nat_iff:
+lemma prime_elem_nat_iff [simp]:
   "prime_elem n \<longleftrightarrow> prime n" for n :: nat
   by (simp add: prime_def)
 
-lemma prime_nat_iff_prime_elem:
-  "prime n \<longleftrightarrow> prime_elem n" for n :: nat
-  by (simp add: prime_elem_nat_iff)
-
-lemma prime_elem_iff_prime_abs:
+lemma prime_elem_iff_prime_abs [simp]:
   "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
   by (auto intro: primeI)
 
@@ -137,14 +133,13 @@
   proof (rule prime_natI)
     fix r s
     assume "n dvd r * s"
-    then have "int n dvd int (r * s)"
-      by (simp add: zdvd_int)
-    then have "int n dvd int r * int s"
+    with of_nat_dvd_iff [of n "r * s"] have "int n dvd int r * int s"
       by simp
     with \<open>?P\<close> have "int n dvd int r \<or> int n dvd int s"
-      by (auto dest: prime_dvd_mult_iff)
+      using prime_dvd_mult_iff [of "int n" "int r" "int s"]
+      by simp
     then show "n dvd r \<or> n dvd s"
-      by (simp add: zdvd_int)
+      by simp
   qed
 next
   assume ?Q
@@ -155,17 +150,18 @@
     fix r s
     assume "int n dvd r * s"
     then have "n dvd nat \<bar>r * s\<bar>"
-      by (simp add: zdvd_int)
+      by simp
     then have "n dvd nat \<bar>r\<bar> * nat \<bar>s\<bar>"
       by (simp add: nat_abs_mult_distrib)
     with \<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>"
-      by (auto dest: prime_dvd_mult_iff)
+      using prime_dvd_mult_iff [of "n" "nat \<bar>r\<bar>" "nat \<bar>s\<bar>"]
+      by simp
     then show "int n dvd r \<or> int n dvd s"
-      by (simp add: zdvd_int)
+      by simp
   qed
 qed
 
-lemma prime_nat_iff_prime:
+lemma prime_nat_iff_prime [simp]:
   "prime (nat k) \<longleftrightarrow> prime k"
 proof (cases "k \<ge> 0")
   case True
@@ -177,17 +173,9 @@
     by (auto dest: prime_ge_2_int)
 qed
 
-lemma prime_elem_int_nat_transfer:
-  "prime_elem n \<longleftrightarrow> prime_elem (nat \<bar>n\<bar>)"
-  by (simp add: prime_elem_iff_prime_abs prime_elem_nat_iff prime_nat_iff_prime)
-
-lemma prime_elem_nat_int_transfer [simp]:
-  "prime_elem (int n) \<longleftrightarrow> prime_elem n"
-  by (simp add: prime_elem_nat_iff prime_elem_iff_prime_abs)
-
 lemma prime_int_nat_transfer:
   "prime k \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
-  by (auto simp add: prime_nat_iff_prime dest: prime_ge_2_int)
+  by (auto dest: prime_ge_2_int)
 
 lemma prime_nat_naiveI:
   "prime p" if "p \<ge> 2" and dvd: "\<And>n. n dvd p \<Longrightarrow> n = 1 \<or> n = p" for p :: nat
@@ -214,12 +202,12 @@
     with \<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>"
       by simp
     then have "int n dvd p"
-      by (simp add: int_dvd_iff)
+      by simp
     with dvd [of "int n"] show "n = 1 \<or> n = nat p"
       by auto
   qed
   then show ?thesis
-    by (simp add: prime_nat_iff_prime)
+    by simp
 qed
 
 lemma prime_nat_iff:
@@ -242,9 +230,9 @@
   "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
 proof (intro iffI conjI allI impI; (elim conjE)?)
   assume *: "prime n"
-  hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
-  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
-    by (auto simp: prime_def zabs_def not_less split: if_splits)
+  hence irred: "irreducible n" by (auto intro: prime_elem_imp_irreducible)
+  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
+    by (auto simp add: prime_ge_0_int)
   thus "n > 1" by presburger
   fix m assume "m dvd n" \<open>m \<ge> 0\<close>
   with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
@@ -256,7 +244,10 @@
   moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
   proof (intro allI impI)
     fix m assume "m dvd nat n"
-    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
+    with \<open>n > 1\<close> have "m dvd nat \<bar>n\<bar>"
+      by simp
+    then have "int m dvd n"
+      by simp
     with n(2) have "int m = 1 \<or> int m = n"
       using of_nat_0_le_iff by blast
     thus "m = 1 \<or> m = nat n" by auto
@@ -280,7 +271,7 @@
   shows   "\<not>n dvd p"
 proof
   assume "n dvd p"
-  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
+  from assms(1) have "irreducible p" by (auto intro: prime_elem_imp_irreducible)
   from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
     by (auto dest!: zdvd_imp_le)
 qed
@@ -297,10 +288,10 @@
   unfolding prime_int_iff by blast
 
 lemma not_prime_eq_prod_nat:
-  assumes "m > 1" "\<not>prime (m::nat)"
+  assumes "m > 1" "\<not> prime (m::nat)"
   shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
   using assms irreducible_altdef[of m]
-  by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
+  by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
 
     
 subsection \<open>Largest exponent of a prime factor\<close>
@@ -380,15 +371,20 @@
 qed (auto simp: prime_nat_iff)
 
 lemma prime_int_iff':
-  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?lhs = ?rhs")
-proof
-  assume "?lhs"
-  thus "?rhs"
-      by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_iff')
+  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?P \<longleftrightarrow> ?Q")
+proof (cases "p \<ge> 0")
+  case True
+  have "?P \<longleftrightarrow> prime (nat p)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> p > 1 \<and> (\<forall>n\<in>{2..<nat p}. \<not> n dvd nat \<bar>p\<bar>)"
+    using True by (simp add: prime_nat_iff')
+  also have "{2..<nat p} = nat ` {2..<p}"
+    using True int_eq_iff by fastforce 
+  finally show "?P \<longleftrightarrow> ?Q" by simp
 next
-  assume "?rhs"
-  thus "?lhs"
-    by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_iff')
+  case False
+  then show ?thesis
+    by (auto simp add: prime_ge_0_int) 
 qed
 
 lemma prime_int_numeral_eq [simp]:
@@ -415,6 +411,24 @@
   using prime_divisor_exists[of n]
   by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
 
+lemma prime_factor_int:
+  fixes k :: int
+  assumes "\<bar>k\<bar> \<noteq> 1"
+  obtains p where "prime p" "p dvd k"
+proof (cases "k = 0")
+  case True
+  then have "prime (2::int)" and "2 dvd k"
+    by simp_all
+  with that show thesis
+    by blast
+next
+  case False
+  with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k"
+    by auto
+  with that show thesis
+    by blast
+qed
+
 
 subsection \<open>Infinitely many primes\<close>
 
@@ -616,7 +630,7 @@
 
 lemma prime_factorization_exists_nat:
   "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
-  using prime_factorization_exists[of n] by (auto simp: prime_def)
+  using prime_factorization_exists[of n] by auto
 
 lemma prod_mset_prime_factorization_nat [simp]: 
   "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
diff -r 19f627407264 -r ccab07d1196c src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -303,7 +303,7 @@
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
   hence "height t / 2 \<le> log 2 (size1 t)"
-    by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
+    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
   thus ?thesis by simp
 qed
 
diff -r 19f627407264 -r ccab07d1196c src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -570,14 +570,15 @@
     by simp
 qed simp_all
 
-lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow>
-  \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
-  apply (cases "\<bar>i\<bar> = 0", simp_all add: gcd_int_def)
-  apply (cases "\<bar>j\<bar> = 0", simp_all)
-  apply (cases "\<bar>i\<bar> = 1", simp_all)
-  apply (cases "\<bar>j\<bar> = 1", simp_all)
-  apply auto
-  done
+lemma zgcd_gt1:
+  "\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
+  if "gcd i j > 1" for i j :: int
+proof -
+  have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
+    by auto
+  with that show ?thesis
+    by (auto simp add: not_less)
+qed
 
 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
   by (induct t rule: numgcdh.induct) auto
diff -r 19f627407264 -r ccab07d1196c src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -665,14 +665,15 @@
   from ismaxcoeff_mono[OF H1 thh1] show ?case by simp
 qed simp_all
 
-lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0))"
-  apply (unfold gcd_int_def)
-  apply (cases "i = 0", simp_all)
-  apply (cases "j = 0", simp_all)
-  apply (cases "\<bar>i\<bar> = 1", simp_all)
-  apply (cases "\<bar>j\<bar> = 1", simp_all)
-  apply auto
-  done
+lemma zgcd_gt1:
+  "\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
+  if "gcd i j > 1" for i j :: int
+proof -
+  have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
+    by auto
+  with that show ?thesis
+    by (auto simp add: not_less)
+qed
 
 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
   by (induct t rule: numgcdh.induct) auto
diff -r 19f627407264 -r ccab07d1196c src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 02 16:50:53 2017 +0000
@@ -61,7 +61,7 @@
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 =
       put_simpset HOL_basic_ss ctxt
-      addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
+      addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
         map (fn r => r RS sym) @{thms of_nat_numeral [where ?'a = int] int_int_eq zle_int of_nat_less_iff [where ?'a = int]}
       |> Splitter.add_split @{thm zdiff_int_split}
     (*simp rules for elimination of int n*)
diff -r 19f627407264 -r ccab07d1196c src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 02 16:50:53 2017 +0000
@@ -84,7 +84,7 @@
             @{thm "split_min"}, @{thm "split_max"}]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = put_simpset HOL_basic_ss ctxt
-      addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ 
+      addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @ 
           map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}]
       |> Splitter.add_split @{thm "zdiff_int_split"}
     (*simp rules for elimination of int n*)
diff -r 19f627407264 -r ccab07d1196c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Divides.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -384,7 +384,7 @@
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
+        eucl_rel_int_iff divide_int_def modulo_int_def)
 next
   case (neg n)
   then show ?thesis
@@ -392,7 +392,7 @@
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
+        eucl_rel_int_iff divide_int_def modulo_int_def)
 qed
 
 lemma divmod_int_unique:
@@ -1155,7 +1155,7 @@
   with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
     by (simp only: of_nat_mod of_nat_diff)
   then show ?thesis
-    by (simp add: zdvd_int)
+    by simp
 qed
 
 lemma mod_eq_nat1E:
diff -r 19f627407264 -r ccab07d1196c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -1432,7 +1432,7 @@
       then int (m div n)
       else - int (m div n + of_bool (\<not> n dvd m)))"
   by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib dvd_int_iff)
+    nat_mult_distrib)
 
 instance proof
   fix k :: int show "k div 0 = 0"
@@ -1460,7 +1460,7 @@
     fix q
     assume "q dvd m" "q dvd n"
     then have "int q dvd int m" "int q dvd int n"
-      by (simp_all add: zdvd_int)
+      by simp_all
     with \<open>?P\<close> have "is_unit (int q)"
       by (rule coprime_common_divisor)
     then show "is_unit q"
@@ -1473,7 +1473,7 @@
     fix k
     assume "k dvd int m" "k dvd int n"
     then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
-      by (simp_all add: zdvd_int)
+      by simp_all
     with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
       by (rule coprime_common_divisor)
     then show "is_unit k"
@@ -1525,7 +1525,7 @@
       then sgn l * int (m mod n)
       else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
   by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib dvd_int_iff)
+    nat_mult_distrib)
 
 instance proof
   fix k l :: int
@@ -1574,7 +1574,7 @@
     by (blast intro: int_sgnE elim: that)
   with that show ?thesis
     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
-      sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
+      sgn_mult mod_eq_0_iff_dvd)
 qed
 
 instance proof
diff -r 19f627407264 -r ccab07d1196c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/GCD.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -1756,6 +1756,59 @@
 
 end
 
+lemma gcd_int_int_eq [simp]:
+  "gcd (int m) (int n) = int (gcd m n)"
+  by (simp add: gcd_int_def)
+
+lemma gcd_nat_abs_left_eq [simp]:
+  "gcd (nat \<bar>k\<bar>) n = nat (gcd k (int n))"
+  by (simp add: gcd_int_def)
+
+lemma gcd_nat_abs_right_eq [simp]:
+  "gcd n (nat \<bar>k\<bar>) = nat (gcd (int n) k)"
+  by (simp add: gcd_int_def)
+
+lemma abs_gcd_int [simp]:
+  "\<bar>gcd x y\<bar> = gcd x y"
+  for x y :: int
+  by (simp only: gcd_int_def)
+
+lemma gcd_abs1_int [simp]:
+  "gcd \<bar>x\<bar> y = gcd x y"
+  for x y :: int
+  by (simp only: gcd_int_def) simp
+
+lemma gcd_abs2_int [simp]:
+  "gcd x \<bar>y\<bar> = gcd x y"
+  for x y :: int
+  by (simp only: gcd_int_def) simp
+
+lemma lcm_int_int_eq [simp]:
+  "lcm (int m) (int n) = int (lcm m n)"
+  by (simp add: lcm_int_def)
+
+lemma lcm_nat_abs_left_eq [simp]:
+  "lcm (nat \<bar>k\<bar>) n = nat (lcm k (int n))"
+  by (simp add: lcm_int_def)
+
+lemma lcm_nat_abs_right_eq [simp]:
+  "lcm n (nat \<bar>k\<bar>) = nat (lcm (int n) k)"
+  by (simp add: lcm_int_def)
+
+lemma lcm_abs1_int [simp]:
+  "lcm \<bar>x\<bar> y = lcm x y"
+  for x y :: int
+  by (simp only: lcm_int_def) simp
+
+lemma lcm_abs2_int [simp]:
+  "lcm x \<bar>y\<bar> = lcm x y"
+  for x y :: int
+  by (simp only: lcm_int_def) simp
+
+lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
+  for i j :: int
+  by (simp only: lcm_int_def)
+
 lemma gcd_nat_induct:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
@@ -1767,35 +1820,13 @@
    apply simp_all
   done
 
-lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
-  by (simp add: gcd_int_def)
-
-lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
-  by (simp add: lcm_int_def)
-
 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
   for x y :: int
-  by (simp add: gcd_int_def)
+  by (simp only: gcd_int_def) simp
 
 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
   for x y :: int
-  by (simp add: gcd_int_def)
-
-lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
-  for x y :: int
-  by (simp add: gcd_int_def)
-
-lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
-  for x y :: int
-  by (simp add: gcd_int_def)
-
-lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
-  for x y :: int
-  by (metis abs_idempotent gcd_abs_int)
-
-lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
-  for x y :: int
-  by (metis abs_idempotent gcd_abs_int)
+  by (simp only: gcd_int_def) simp
 
 lemma gcd_cases_int:
   fixes x y :: int
@@ -1812,27 +1843,11 @@
 
 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
   for x y :: int
-  by (simp add: lcm_int_def)
+  by (simp only: lcm_int_def) simp
 
 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
   for x y :: int
-  by (simp add: lcm_int_def)
-
-lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
-  for x y :: int
-  by (simp add: lcm_int_def)
-
-lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
-  for i j :: int
-  by (simp add:lcm_int_def)
-
-lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
-  for x y :: int
-  by (metis abs_idempotent lcm_int_def)
-
-lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
-  for x y :: int
-  by (metis abs_idempotent lcm_int_def)
+  by (simp only: lcm_int_def) simp
 
 lemma lcm_cases_int:
   fixes x y :: int
@@ -1845,7 +1860,7 @@
 
 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
   for x y :: int
-  by (simp add: lcm_int_def)
+  by (simp only: lcm_int_def)
 
 lemma gcd_0_nat: "gcd x 0 = x"
   for x :: nat
@@ -1861,7 +1876,7 @@
 
 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
   for x :: int
-  by (auto simp:gcd_int_def)
+  by (auto simp: gcd_int_def)
 
 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
   for x y :: nat
@@ -1923,9 +1938,20 @@
 qed (simp_all add: lcm_nat_def)
 
 instance int :: ring_gcd
-  by standard
-    (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
-      zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
+proof
+  fix k l r :: int
+  show "gcd k l dvd k" "gcd k l dvd l"
+    using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+      gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+    by simp_all
+  show "lcm k l = normalize (k * l) div gcd k l"
+    using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+    by (simp add: nat_eq_iff of_nat_div abs_mult)
+  assume "r dvd k" "r dvd l"
+  then show "r dvd gcd k l"
+    using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+    by simp
+qed simp
 
 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
   for a b :: nat
@@ -1975,7 +2001,7 @@
 
 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
   for x y :: int
-  by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
+  by (metis abs_dvd_iff gcd_0_left_int gcd_unique_int)
 
 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
   for x y :: int
@@ -1995,7 +2021,7 @@
 
 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
   for k m n :: int
-  by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
+  using gcd_mult_distrib' [of k m n] by simp
 
 text \<open>\medskip Addition laws.\<close>
 
@@ -2097,7 +2123,7 @@
 
 lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   for k l :: int
-  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
+  using gcd_red_int [of "\<bar>k\<bar>" "\<bar>l\<bar>"] by simp
 
 lemma coprime_Suc_left_nat [simp]:
   "coprime (Suc n) n"
@@ -2421,8 +2447,8 @@
 
 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   for a b :: int
-  by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
-
+  by (simp add: abs_mult lcm_gcd)
+  
 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
   for m n :: nat
   unfolding lcm_nat_def
@@ -2439,11 +2465,11 @@
 
 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
   for m n :: nat
-  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
+  using lcm_eq_0_iff [of m n] by auto
 
 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
   for m n :: int
-  by (simp add: lcm_int_def lcm_pos_nat)
+  by (simp add: less_le lcm_eq_0_iff)
 
 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
   for m n :: nat
@@ -2653,33 +2679,83 @@
 
 subsubsection \<open>Setwise GCD and LCM for integers\<close>
 
-instantiation int :: semiring_Gcd
+instantiation int :: Gcd
 begin
 
-definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
-
-definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
-
-instance
-  by standard
-    (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
-      Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
+definition Gcd_int :: "int set \<Rightarrow> int"
+  where "Gcd K = int (GCD k\<in>K. (nat \<circ> abs) k)"
+
+definition Lcm_int :: "int set \<Rightarrow> int"
+  where "Lcm K = int (LCM k\<in>K. (nat \<circ> abs) k)"
+
+instance ..
 
 end
 
-lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
+lemma Gcd_int_eq [simp]:
+  "(GCD n\<in>N. int n) = int (Gcd N)"
+  by (simp add: Gcd_int_def image_image)
+
+lemma Gcd_nat_abs_eq [simp]:
+  "(GCD k\<in>K. nat \<bar>k\<bar>) = nat (Gcd K)"
+  by (simp add: Gcd_int_def)
+
+lemma abs_Gcd_eq [simp]:
+  "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set"
+  by (simp only: Gcd_int_def)
+
+lemma Gcd_int_greater_eq_0 [simp]:
+  "Gcd K \<ge> 0"
   for K :: "int set"
-  using normalize_Gcd [of K] by simp
-
-lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
+  using abs_ge_zero [of "Gcd K"] by simp
+
+lemma Gcd_abs_eq [simp]:
+  "(GCD k\<in>K. \<bar>k\<bar>) = Gcd K"
   for K :: "int set"
-  using normalize_Lcm [of K] by simp
-
-lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
-  by (simp add: Gcd_int_def comp_def image_image)
-
-lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
-  by (simp add: Lcm_int_def comp_def image_image)
+  by (simp only: Gcd_int_def image_image) simp
+
+lemma Lcm_int_eq [simp]:
+  "(LCM n\<in>N. int n) = int (Lcm N)"
+  by (simp add: Lcm_int_def image_image)
+
+lemma Lcm_nat_abs_eq [simp]:
+  "(LCM k\<in>K. nat \<bar>k\<bar>) = nat (Lcm K)"
+  by (simp add: Lcm_int_def)
+
+lemma abs_Lcm_eq [simp]:
+  "\<bar>Lcm K\<bar> = Lcm K" for K :: "int set"
+  by (simp only: Lcm_int_def)
+
+lemma Lcm_int_greater_eq_0 [simp]:
+  "Lcm K \<ge> 0"
+  for K :: "int set"
+  using abs_ge_zero [of "Lcm K"] by simp
+
+lemma Lcm_abs_eq [simp]:
+  "(LCM k\<in>K. \<bar>k\<bar>) = Lcm K"
+  for K :: "int set"
+  by (simp only: Lcm_int_def image_image) simp
+
+instance int :: semiring_Gcd
+proof
+  fix K :: "int set" and k :: int
+  show "Gcd K dvd k" and "k dvd Lcm K" if "k \<in> K"
+    using that Gcd_dvd [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
+      dvd_Lcm [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
+    by (simp_all add: comp_def)
+  show "k dvd Gcd K" if "\<And>l. l \<in> K \<Longrightarrow> k dvd l"
+  proof -
+    have "nat \<bar>k\<bar> dvd (GCD k\<in>K. nat \<bar>k\<bar>)"
+      by (rule Gcd_greatest) (use that in auto)
+    then show ?thesis by simp
+  qed
+  show "Lcm K dvd k" if "\<And>l. l \<in> K \<Longrightarrow> l dvd k"
+  proof -
+    have "(LCM k\<in>K. nat \<bar>k\<bar>) dvd nat \<bar>k\<bar>"
+      by (rule Lcm_least) (use that in auto)
+    then show ?thesis by simp
+  qed
+qed simp_all
 
 
 subsection \<open>GCD and LCM on @{typ integer}\<close>
diff -r 19f627407264 -r ccab07d1196c src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Int.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -1499,43 +1499,64 @@
   then show ?thesis by simp
 qed
 
-theorem zdvd_int: "x dvd y \<longleftrightarrow> int x dvd int y"
+lemma int_dvd_int_iff [simp]:
+  "int m dvd int n \<longleftrightarrow> m dvd n"
 proof -
-  have "x dvd y" if "int y = int x * k" for k
+  have "m dvd n" if "int n = int m * k" for k
   proof (cases k)
-    case (nonneg n)
-    with that have "y = x * n"
+    case (nonneg q)
+    with that have "n = m * q"
       by (simp del: of_nat_mult add: of_nat_mult [symmetric])
     then show ?thesis ..
   next
-    case (neg n)
-    with that have "int y = int x * (- int (Suc n))"
+    case (neg q)
+    with that have "int n = int m * (- int (Suc q))"
       by simp
-    also have "\<dots> = - (int x * int (Suc n))"
+    also have "\<dots> = - (int m * int (Suc q))"
       by (simp only: mult_minus_right)
-    also have "\<dots> = - int (x * Suc n)"
+    also have "\<dots> = - int (m * Suc q)"
       by (simp only: of_nat_mult [symmetric])
-    finally have "- int (x * Suc n) = int y" ..
+    finally have "- int (m * Suc q) = int n" ..
     then show ?thesis
       by (simp only: negative_eq_positive) auto
   qed
-  then show ?thesis
-    by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
+  then show ?thesis by (auto simp add: dvd_def)
 qed
 
-lemma zdvd1_eq[simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
-  (is "?lhs \<longleftrightarrow> ?rhs")
+lemma dvd_nat_abs_iff [simp]:
+  "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd k"
+proof -
+  have "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd int (nat \<bar>k\<bar>)"
+    by (simp only: int_dvd_int_iff)
+  then show ?thesis
+    by simp
+qed
+
+lemma nat_abs_dvd_iff [simp]:
+  "nat \<bar>k\<bar> dvd n \<longleftrightarrow> k dvd int n"
+proof -
+  have "nat \<bar>k\<bar> dvd n \<longleftrightarrow> int (nat \<bar>k\<bar>) dvd int n"
+    by (simp only: int_dvd_int_iff)
+  then show ?thesis
+    by simp
+qed
+
+lemma zdvd1_eq [simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" (is "?lhs \<longleftrightarrow> ?rhs")
   for x :: int
 proof
   assume ?lhs
-  then have "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
-  then have "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
-  then have "nat \<bar>x\<bar> = 1" by simp
-  then show ?rhs by (cases "x < 0") auto
+  then have "nat \<bar>x\<bar> dvd nat \<bar>1\<bar>"
+    by (simp only: nat_abs_dvd_iff) simp
+  then have "nat \<bar>x\<bar> = 1"
+    by simp
+  then show ?rhs
+    by (cases "x < 0") simp_all
 next
   assume ?rhs
-  then have "x = 1 \<or> x = - 1" by auto
-  then show ?lhs by (auto intro: dvdI)
+  then have "x = 1 \<or> x = - 1"
+    by auto
+  then show ?lhs
+    by (auto intro: dvdI)
 qed
 
 lemma zdvd_mult_cancel1:
@@ -1554,17 +1575,8 @@
     by (simp only: zdvd1_eq)
 qed
 
-lemma int_dvd_iff: "int m dvd z \<longleftrightarrow> m dvd nat \<bar>z\<bar>"
-  by (cases "z \<ge> 0") (simp_all add: zdvd_int)
-
-lemma dvd_int_iff: "z dvd int m \<longleftrightarrow> nat \<bar>z\<bar> dvd m"
-  by (cases "z \<ge> 0") (simp_all add: zdvd_int)
-
-lemma dvd_int_unfold_dvd_nat: "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
-  by (simp add: dvd_int_iff [symmetric])
-
 lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)"
-  by (auto simp add: dvd_int_iff)
+  using nat_abs_dvd_iff [of z m] by (cases "z \<ge> 0") auto
 
 lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
   by (auto elim: nonneg_int_cases)
@@ -1603,7 +1615,7 @@
 lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
   for n z :: int
   apply (cases n)
-   apply (auto simp add: dvd_int_iff)
+  apply auto
   apply (cases z)
    apply (auto simp add: dvd_imp_le)
   done
diff -r 19f627407264 -r ccab07d1196c src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Library/Float.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -1193,6 +1193,7 @@
         l_def[symmetric, THEN meta_eq_to_obj_eq]
       apply transfer
       apply (auto simp add: round_up_def truncate_up_rat_precision)
+      apply (metis dvd_triv_left of_nat_dvd_iff)
       apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
       done
    next
@@ -1208,6 +1209,7 @@
         l_def[symmetric, THEN meta_eq_to_obj_eq]
       apply transfer
       apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision)
+      apply (metis dvd_triv_left of_nat_dvd_iff)
       apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
       done
   qed
diff -r 19f627407264 -r ccab07d1196c src/HOL/Number_Theory/Euler_Criterion.thy
--- a/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -17,8 +17,9 @@
   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
-
+  "int (p - 1) = int p - 1"
+  by (metis of_nat_1 of_nat_diff p_prime prime_ge_1_nat)
+  
 private lemma p_not_eq_Suc_0 [simp]:
   "p \<noteq> Suc 0"
   using p_ge_2 by simp
@@ -46,8 +47,9 @@
   proof -
     have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
     using p_prime proof (rule fermat_theorem)
-      show "\<not> p dvd nat \<bar>b\<bar>"
-        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))
+      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) 
     qed
     then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
       by (simp add: cong_def)
diff -r 19f627407264 -r ccab07d1196c src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -117,7 +117,7 @@
       by (simp add: cong_altdef_int)
     with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
     have "coprime a (int p)"
-      by (simp_all add: zdvd_int ac_simps)
+      by (simp_all add: ac_simps)
     with a cong_mult_rcancel_int [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
@@ -152,7 +152,7 @@
       by (simp add: cong_altdef_int)
     with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
     have "coprime a (int p)"
-      by (simp_all add: zdvd_int ac_simps)  
+      by (simp_all add: ac_simps)  
     with a' cong_mult_rcancel_int [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
diff -r 19f627407264 -r ccab07d1196c src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -25,8 +25,8 @@
   using p_ge_2 p_prime prime_odd_nat by blast
 
 lemma p_ge_0: "0 < int p"
-  using p_prime not_prime_0[where 'a = nat] by fastforce+
-
+  by (simp add: p_prime prime_gt_0_nat)
+  
 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
   using odd_p by simp
 
@@ -34,7 +34,7 @@
   using q_ge_2 q_prime prime_odd_nat by blast
 
 lemma q_ge_0: "0 < int q"
-  using q_prime not_prime_0[where 'a = nat] by fastforce+
+  by (simp add: q_prime prime_gt_0_nat)
 
 lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1"
   using odd_q by simp
@@ -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 zdvd_int [symmetric] dest: primes_dvd_imp_eq)
+  by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq)
 
 lemma Gqp: "GAUSS q p"
   by (simp add: QRqp QR.Gpq)
diff -r 19f627407264 -r ccab07d1196c src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Totient.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -78,7 +78,7 @@
 qed (auto simp: totatives_def)
 
 lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}"
-  using totatives_prime_power_Suc[of p 0] by fastforce
+  using totatives_prime_power_Suc [of p 0] by auto
 
 lemma bij_betw_totatives:
   assumes "m1 > 1" "m2 > 1" "coprime m1 m2"
diff -r 19f627407264 -r ccab07d1196c src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 02 16:50:53 2017 +0000
@@ -811,7 +811,7 @@
 val ss1 =
   simpset_of (put_simpset comp_ss @{context}
     addsimps @{thms simp_thms} @ 
-            [@{thm "nat_numeral"} RS sym, @{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] 
+            [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] 
         @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]
     |> Splitter.add_split @{thm "zdiff_int_split"})
 
diff -r 19f627407264 -r ccab07d1196c src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Word/Word.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -3997,22 +3997,50 @@
     done
 qed
 
-lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
-  apply (unfold word_rot_defs)
-  apply (cut_tac y="size w" in gt_or_eq_0)
-  apply (erule disjE)
-   apply simp_all
-  apply (safe intro!: abl_cong)
-   apply (rule rotater_eqs)
-   apply (simp add: word_size nat_mod_distrib)
-  apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
-  apply (rule rotater_eqs)
-  apply (simp add: word_size nat_mod_distrib)
-  apply (rule of_nat_eq_0_iff [THEN iffD1])
-  apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
-  using mod_mod_trivial mod_eq_dvd_iff
-  apply blast
-  done
+lemma word_roti_conv_mod':
+  "word_roti n w = word_roti (n mod int (size w)) w"
+proof (cases "size w = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have [simp]: "l mod int (size w) \<ge> 0" for l
+    by simp
+  then have *: "word_roti (n mod int (size w)) w = word_rotr (nat (n mod int (size w))) w"
+    by (simp add: word_roti_def)
+  show ?thesis
+  proof (cases "n \<ge> 0")
+    case True
+    then show ?thesis
+      apply (auto simp add: not_le *)
+      apply (auto simp add: word_rot_defs)
+      apply (safe intro!: abl_cong)
+      apply (rule rotater_eqs)
+      apply (simp add: word_size nat_mod_distrib)
+      done
+  next
+    case False
+    moreover define k where "k = - n"
+    ultimately have n: "n = - k"
+      by simp_all
+    from False show ?thesis
+      apply (auto simp add: not_le *)
+      apply (auto simp add: word_rot_defs)
+      apply (simp add: n)
+      apply (safe intro!: abl_cong)
+      apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
+      apply (rule rotater_eqs)
+      apply (simp add: word_size [symmetric, of w])
+      apply (rule of_nat_eq_0_iff [THEN iffD1])
+      apply (auto simp add: nat_add_distrib [symmetric] mod_eq_0_iff_dvd)
+      using dvd_nat_abs_iff [of "size w" "- k mod int (size w) + k"]
+      apply (simp add: algebra_simps)
+      apply (simp add: word_size)
+      apply (metis (no_types, hide_lams) add.right_inverse dvd_0_right dvd_mod_imp_dvd dvd_refl minus_dvd_iff minus_equation_iff mod_0 mod_add_eq mod_minus_eq)
+      done
+  qed
+qed
 
 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
 
diff -r 19f627407264 -r ccab07d1196c src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -86,7 +86,7 @@
   unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
-  unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
   unfolding rel_fun_def ZN_def by (simp add: zdiv_int)