more simplification rules
authorhaftmann
Sat Dec 02 16:50:53 2017 +0000 (7 months ago)
changeset 67118ccab07d1196c
parent 67117 19f627407264
child 67119 acb0807ddb56
more simplification rules
src/HOL/Algebra/IntRing.thy
src/HOL/Computational_Algebra/Primes.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/GCD.thy
src/HOL/Int.thy
src/HOL/Library/Float.thy
src/HOL/Number_Theory/Euler_Criterion.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Number_Theory/Totient.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Word/Word.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Dec 02 16:50:53 2017 +0000
     1.3 @@ -248,10 +248,12 @@
     1.4      by (metis dvd_def mult.commute)
     1.5  next
     1.6    assume "UNIV = {uu. \<exists>x. uu = x * p}"
     1.7 -  then obtain x where "1 = x * p" by best
     1.8 -  then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
     1.9 +  then obtain x where "1 = x * p"
    1.10 +    by best
    1.11 +  then have "\<bar>p * x\<bar> = 1"
    1.12 +    by (simp add: ac_simps)
    1.13    then show False using prime
    1.14 -    by (auto dest!: abs_zmult_eq_1 simp: prime_def)
    1.15 +    by (auto simp add: abs_mult zmult_eq_1_iff)
    1.16  qed
    1.17  
    1.18  
     2.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sat Dec 02 16:50:53 2017 +0000
     2.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sat Dec 02 16:50:53 2017 +0000
     2.3 @@ -115,15 +115,11 @@
     2.4    "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
     2.5    using that by (auto intro!: primeI prime_elemI)
     2.6  
     2.7 -lemma prime_elem_nat_iff:
     2.8 +lemma prime_elem_nat_iff [simp]:
     2.9    "prime_elem n \<longleftrightarrow> prime n" for n :: nat
    2.10    by (simp add: prime_def)
    2.11  
    2.12 -lemma prime_nat_iff_prime_elem:
    2.13 -  "prime n \<longleftrightarrow> prime_elem n" for n :: nat
    2.14 -  by (simp add: prime_elem_nat_iff)
    2.15 -
    2.16 -lemma prime_elem_iff_prime_abs:
    2.17 +lemma prime_elem_iff_prime_abs [simp]:
    2.18    "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
    2.19    by (auto intro: primeI)
    2.20  
    2.21 @@ -137,14 +133,13 @@
    2.22    proof (rule prime_natI)
    2.23      fix r s
    2.24      assume "n dvd r * s"
    2.25 -    then have "int n dvd int (r * s)"
    2.26 -      by (simp add: zdvd_int)
    2.27 -    then have "int n dvd int r * int s"
    2.28 +    with of_nat_dvd_iff [of n "r * s"] have "int n dvd int r * int s"
    2.29        by simp
    2.30      with \<open>?P\<close> have "int n dvd int r \<or> int n dvd int s"
    2.31 -      by (auto dest: prime_dvd_mult_iff)
    2.32 +      using prime_dvd_mult_iff [of "int n" "int r" "int s"]
    2.33 +      by simp
    2.34      then show "n dvd r \<or> n dvd s"
    2.35 -      by (simp add: zdvd_int)
    2.36 +      by simp
    2.37    qed
    2.38  next
    2.39    assume ?Q
    2.40 @@ -155,17 +150,18 @@
    2.41      fix r s
    2.42      assume "int n dvd r * s"
    2.43      then have "n dvd nat \<bar>r * s\<bar>"
    2.44 -      by (simp add: zdvd_int)
    2.45 +      by simp
    2.46      then have "n dvd nat \<bar>r\<bar> * nat \<bar>s\<bar>"
    2.47        by (simp add: nat_abs_mult_distrib)
    2.48      with \<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>"
    2.49 -      by (auto dest: prime_dvd_mult_iff)
    2.50 +      using prime_dvd_mult_iff [of "n" "nat \<bar>r\<bar>" "nat \<bar>s\<bar>"]
    2.51 +      by simp
    2.52      then show "int n dvd r \<or> int n dvd s"
    2.53 -      by (simp add: zdvd_int)
    2.54 +      by simp
    2.55    qed
    2.56  qed
    2.57  
    2.58 -lemma prime_nat_iff_prime:
    2.59 +lemma prime_nat_iff_prime [simp]:
    2.60    "prime (nat k) \<longleftrightarrow> prime k"
    2.61  proof (cases "k \<ge> 0")
    2.62    case True
    2.63 @@ -177,17 +173,9 @@
    2.64      by (auto dest: prime_ge_2_int)
    2.65  qed
    2.66  
    2.67 -lemma prime_elem_int_nat_transfer:
    2.68 -  "prime_elem n \<longleftrightarrow> prime_elem (nat \<bar>n\<bar>)"
    2.69 -  by (simp add: prime_elem_iff_prime_abs prime_elem_nat_iff prime_nat_iff_prime)
    2.70 -
    2.71 -lemma prime_elem_nat_int_transfer [simp]:
    2.72 -  "prime_elem (int n) \<longleftrightarrow> prime_elem n"
    2.73 -  by (simp add: prime_elem_nat_iff prime_elem_iff_prime_abs)
    2.74 -
    2.75  lemma prime_int_nat_transfer:
    2.76    "prime k \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
    2.77 -  by (auto simp add: prime_nat_iff_prime dest: prime_ge_2_int)
    2.78 +  by (auto dest: prime_ge_2_int)
    2.79  
    2.80  lemma prime_nat_naiveI:
    2.81    "prime p" if "p \<ge> 2" and dvd: "\<And>n. n dvd p \<Longrightarrow> n = 1 \<or> n = p" for p :: nat
    2.82 @@ -214,12 +202,12 @@
    2.83      with \<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>"
    2.84        by simp
    2.85      then have "int n dvd p"
    2.86 -      by (simp add: int_dvd_iff)
    2.87 +      by simp
    2.88      with dvd [of "int n"] show "n = 1 \<or> n = nat p"
    2.89        by auto
    2.90    qed
    2.91    then show ?thesis
    2.92 -    by (simp add: prime_nat_iff_prime)
    2.93 +    by simp
    2.94  qed
    2.95  
    2.96  lemma prime_nat_iff:
    2.97 @@ -242,9 +230,9 @@
    2.98    "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
    2.99  proof (intro iffI conjI allI impI; (elim conjE)?)
   2.100    assume *: "prime n"
   2.101 -  hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
   2.102 -  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" 
   2.103 -    by (auto simp: prime_def zabs_def not_less split: if_splits)
   2.104 +  hence irred: "irreducible n" by (auto intro: prime_elem_imp_irreducible)
   2.105 +  from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
   2.106 +    by (auto simp add: prime_ge_0_int)
   2.107    thus "n > 1" by presburger
   2.108    fix m assume "m dvd n" \<open>m \<ge> 0\<close>
   2.109    with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
   2.110 @@ -256,7 +244,10 @@
   2.111    moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
   2.112    proof (intro allI impI)
   2.113      fix m assume "m dvd nat n"
   2.114 -    with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
   2.115 +    with \<open>n > 1\<close> have "m dvd nat \<bar>n\<bar>"
   2.116 +      by simp
   2.117 +    then have "int m dvd n"
   2.118 +      by simp
   2.119      with n(2) have "int m = 1 \<or> int m = n"
   2.120        using of_nat_0_le_iff by blast
   2.121      thus "m = 1 \<or> m = nat n" by auto
   2.122 @@ -280,7 +271,7 @@
   2.123    shows   "\<not>n dvd p"
   2.124  proof
   2.125    assume "n dvd p"
   2.126 -  from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
   2.127 +  from assms(1) have "irreducible p" by (auto intro: prime_elem_imp_irreducible)
   2.128    from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
   2.129      by (auto dest!: zdvd_imp_le)
   2.130  qed
   2.131 @@ -297,10 +288,10 @@
   2.132    unfolding prime_int_iff by blast
   2.133  
   2.134  lemma not_prime_eq_prod_nat:
   2.135 -  assumes "m > 1" "\<not>prime (m::nat)"
   2.136 +  assumes "m > 1" "\<not> prime (m::nat)"
   2.137    shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
   2.138    using assms irreducible_altdef[of m]
   2.139 -  by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
   2.140 +  by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
   2.141  
   2.142      
   2.143  subsection \<open>Largest exponent of a prime factor\<close>
   2.144 @@ -380,15 +371,20 @@
   2.145  qed (auto simp: prime_nat_iff)
   2.146  
   2.147  lemma prime_int_iff':
   2.148 -  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?lhs = ?rhs")
   2.149 -proof
   2.150 -  assume "?lhs"
   2.151 -  thus "?rhs"
   2.152 -      by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_iff')
   2.153 +  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?P \<longleftrightarrow> ?Q")
   2.154 +proof (cases "p \<ge> 0")
   2.155 +  case True
   2.156 +  have "?P \<longleftrightarrow> prime (nat p)"
   2.157 +    by simp
   2.158 +  also have "\<dots> \<longleftrightarrow> p > 1 \<and> (\<forall>n\<in>{2..<nat p}. \<not> n dvd nat \<bar>p\<bar>)"
   2.159 +    using True by (simp add: prime_nat_iff')
   2.160 +  also have "{2..<nat p} = nat ` {2..<p}"
   2.161 +    using True int_eq_iff by fastforce 
   2.162 +  finally show "?P \<longleftrightarrow> ?Q" by simp
   2.163  next
   2.164 -  assume "?rhs"
   2.165 -  thus "?lhs"
   2.166 -    by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_iff')
   2.167 +  case False
   2.168 +  then show ?thesis
   2.169 +    by (auto simp add: prime_ge_0_int) 
   2.170  qed
   2.171  
   2.172  lemma prime_int_numeral_eq [simp]:
   2.173 @@ -415,6 +411,24 @@
   2.174    using prime_divisor_exists[of n]
   2.175    by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
   2.176  
   2.177 +lemma prime_factor_int:
   2.178 +  fixes k :: int
   2.179 +  assumes "\<bar>k\<bar> \<noteq> 1"
   2.180 +  obtains p where "prime p" "p dvd k"
   2.181 +proof (cases "k = 0")
   2.182 +  case True
   2.183 +  then have "prime (2::int)" and "2 dvd k"
   2.184 +    by simp_all
   2.185 +  with that show thesis
   2.186 +    by blast
   2.187 +next
   2.188 +  case False
   2.189 +  with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k"
   2.190 +    by auto
   2.191 +  with that show thesis
   2.192 +    by blast
   2.193 +qed
   2.194 +
   2.195  
   2.196  subsection \<open>Infinitely many primes\<close>
   2.197  
   2.198 @@ -616,7 +630,7 @@
   2.199  
   2.200  lemma prime_factorization_exists_nat:
   2.201    "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
   2.202 -  using prime_factorization_exists[of n] by (auto simp: prime_def)
   2.203 +  using prime_factorization_exists[of n] by auto
   2.204  
   2.205  lemma prod_mset_prime_factorization_nat [simp]: 
   2.206    "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
     3.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 02 16:50:53 2017 +0000
     3.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 02 16:50:53 2017 +0000
     3.3 @@ -303,7 +303,7 @@
     3.4      by (simp add: powr_realpow bheight_size_bound rbt_def)
     3.5    finally have "2 powr (height t / 2) \<le> size1 t" .
     3.6    hence "height t / 2 \<le> log 2 (size1 t)"
     3.7 -    by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
     3.8 +    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
     3.9    thus ?thesis by simp
    3.10  qed
    3.11  
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Dec 02 16:50:53 2017 +0000
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Dec 02 16:50:53 2017 +0000
     4.3 @@ -570,14 +570,15 @@
     4.4      by simp
     4.5  qed simp_all
     4.6  
     4.7 -lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow>
     4.8 -  \<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"
     4.9 -  apply (cases "\<bar>i\<bar> = 0", simp_all add: gcd_int_def)
    4.10 -  apply (cases "\<bar>j\<bar> = 0", simp_all)
    4.11 -  apply (cases "\<bar>i\<bar> = 1", simp_all)
    4.12 -  apply (cases "\<bar>j\<bar> = 1", simp_all)
    4.13 -  apply auto
    4.14 -  done
    4.15 +lemma zgcd_gt1:
    4.16 +  "\<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"
    4.17 +  if "gcd i j > 1" for i j :: int
    4.18 +proof -
    4.19 +  have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
    4.20 +    by auto
    4.21 +  with that show ?thesis
    4.22 +    by (auto simp add: not_less)
    4.23 +qed
    4.24  
    4.25  lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
    4.26    by (induct t rule: numgcdh.induct) auto
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Dec 02 16:50:53 2017 +0000
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Dec 02 16:50:53 2017 +0000
     5.3 @@ -665,14 +665,15 @@
     5.4    from ismaxcoeff_mono[OF H1 thh1] show ?case by simp
     5.5  qed simp_all
     5.6  
     5.7 -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))"
     5.8 -  apply (unfold gcd_int_def)
     5.9 -  apply (cases "i = 0", simp_all)
    5.10 -  apply (cases "j = 0", simp_all)
    5.11 -  apply (cases "\<bar>i\<bar> = 1", simp_all)
    5.12 -  apply (cases "\<bar>j\<bar> = 1", simp_all)
    5.13 -  apply auto
    5.14 -  done
    5.15 +lemma zgcd_gt1:
    5.16 +  "\<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"
    5.17 +  if "gcd i j > 1" for i j :: int
    5.18 +proof -
    5.19 +  have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
    5.20 +    by auto
    5.21 +  with that show ?thesis
    5.22 +    by (auto simp add: not_less)
    5.23 +qed
    5.24  
    5.25  lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
    5.26    by (induct t rule: numgcdh.induct) auto
     6.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 02 16:50:53 2017 +0000
     6.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 02 16:50:53 2017 +0000
     6.3 @@ -61,7 +61,7 @@
     6.4      (* Simp rules for changing (n::int) to int n *)
     6.5      val simpset1 =
     6.6        put_simpset HOL_basic_ss ctxt
     6.7 -      addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
     6.8 +      addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
     6.9          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]}
    6.10        |> Splitter.add_split @{thm zdiff_int_split}
    6.11      (*simp rules for elimination of int n*)
     7.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 02 16:50:53 2017 +0000
     7.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 02 16:50:53 2017 +0000
     7.3 @@ -84,7 +84,7 @@
     7.4              @{thm "split_min"}, @{thm "split_max"}]
     7.5      (* Simp rules for changing (n::int) to int n *)
     7.6      val simpset1 = put_simpset HOL_basic_ss ctxt
     7.7 -      addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @ 
     7.8 +      addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @ 
     7.9            map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}]
    7.10        |> Splitter.add_split @{thm "zdiff_int_split"}
    7.11      (*simp rules for elimination of int n*)
     8.1 --- a/src/HOL/Divides.thy	Sat Dec 02 16:50:53 2017 +0000
     8.2 +++ b/src/HOL/Divides.thy	Sat Dec 02 16:50:53 2017 +0000
     8.3 @@ -384,7 +384,7 @@
     8.4      by (cases l rule: int_cases3)
     8.5        (auto simp del: of_nat_mult of_nat_add
     8.6          simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
     8.7 -        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
     8.8 +        eucl_rel_int_iff divide_int_def modulo_int_def)
     8.9  next
    8.10    case (neg n)
    8.11    then show ?thesis
    8.12 @@ -392,7 +392,7 @@
    8.13      by (cases l rule: int_cases3)
    8.14        (auto simp del: of_nat_mult of_nat_add
    8.15          simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
    8.16 -        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
    8.17 +        eucl_rel_int_iff divide_int_def modulo_int_def)
    8.18  qed
    8.19  
    8.20  lemma divmod_int_unique:
    8.21 @@ -1155,7 +1155,7 @@
    8.22    with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
    8.23      by (simp only: of_nat_mod of_nat_diff)
    8.24    then show ?thesis
    8.25 -    by (simp add: zdvd_int)
    8.26 +    by simp
    8.27  qed
    8.28  
    8.29  lemma mod_eq_nat1E:
     9.1 --- a/src/HOL/Euclidean_Division.thy	Sat Dec 02 16:50:53 2017 +0000
     9.2 +++ b/src/HOL/Euclidean_Division.thy	Sat Dec 02 16:50:53 2017 +0000
     9.3 @@ -1432,7 +1432,7 @@
     9.4        then int (m div n)
     9.5        else - int (m div n + of_bool (\<not> n dvd m)))"
     9.6    by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
     9.7 -    nat_mult_distrib dvd_int_iff)
     9.8 +    nat_mult_distrib)
     9.9  
    9.10  instance proof
    9.11    fix k :: int show "k div 0 = 0"
    9.12 @@ -1460,7 +1460,7 @@
    9.13      fix q
    9.14      assume "q dvd m" "q dvd n"
    9.15      then have "int q dvd int m" "int q dvd int n"
    9.16 -      by (simp_all add: zdvd_int)
    9.17 +      by simp_all
    9.18      with \<open>?P\<close> have "is_unit (int q)"
    9.19        by (rule coprime_common_divisor)
    9.20      then show "is_unit q"
    9.21 @@ -1473,7 +1473,7 @@
    9.22      fix k
    9.23      assume "k dvd int m" "k dvd int n"
    9.24      then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
    9.25 -      by (simp_all add: zdvd_int)
    9.26 +      by simp_all
    9.27      with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
    9.28        by (rule coprime_common_divisor)
    9.29      then show "is_unit k"
    9.30 @@ -1525,7 +1525,7 @@
    9.31        then sgn l * int (m mod n)
    9.32        else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
    9.33    by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
    9.34 -    nat_mult_distrib dvd_int_iff)
    9.35 +    nat_mult_distrib)
    9.36  
    9.37  instance proof
    9.38    fix k l :: int
    9.39 @@ -1574,7 +1574,7 @@
    9.40      by (blast intro: int_sgnE elim: that)
    9.41    with that show ?thesis
    9.42      by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
    9.43 -      sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
    9.44 +      sgn_mult mod_eq_0_iff_dvd)
    9.45  qed
    9.46  
    9.47  instance proof
    10.1 --- a/src/HOL/GCD.thy	Sat Dec 02 16:50:53 2017 +0000
    10.2 +++ b/src/HOL/GCD.thy	Sat Dec 02 16:50:53 2017 +0000
    10.3 @@ -1756,6 +1756,59 @@
    10.4  
    10.5  end
    10.6  
    10.7 +lemma gcd_int_int_eq [simp]:
    10.8 +  "gcd (int m) (int n) = int (gcd m n)"
    10.9 +  by (simp add: gcd_int_def)
   10.10 +
   10.11 +lemma gcd_nat_abs_left_eq [simp]:
   10.12 +  "gcd (nat \<bar>k\<bar>) n = nat (gcd k (int n))"
   10.13 +  by (simp add: gcd_int_def)
   10.14 +
   10.15 +lemma gcd_nat_abs_right_eq [simp]:
   10.16 +  "gcd n (nat \<bar>k\<bar>) = nat (gcd (int n) k)"
   10.17 +  by (simp add: gcd_int_def)
   10.18 +
   10.19 +lemma abs_gcd_int [simp]:
   10.20 +  "\<bar>gcd x y\<bar> = gcd x y"
   10.21 +  for x y :: int
   10.22 +  by (simp only: gcd_int_def)
   10.23 +
   10.24 +lemma gcd_abs1_int [simp]:
   10.25 +  "gcd \<bar>x\<bar> y = gcd x y"
   10.26 +  for x y :: int
   10.27 +  by (simp only: gcd_int_def) simp
   10.28 +
   10.29 +lemma gcd_abs2_int [simp]:
   10.30 +  "gcd x \<bar>y\<bar> = gcd x y"
   10.31 +  for x y :: int
   10.32 +  by (simp only: gcd_int_def) simp
   10.33 +
   10.34 +lemma lcm_int_int_eq [simp]:
   10.35 +  "lcm (int m) (int n) = int (lcm m n)"
   10.36 +  by (simp add: lcm_int_def)
   10.37 +
   10.38 +lemma lcm_nat_abs_left_eq [simp]:
   10.39 +  "lcm (nat \<bar>k\<bar>) n = nat (lcm k (int n))"
   10.40 +  by (simp add: lcm_int_def)
   10.41 +
   10.42 +lemma lcm_nat_abs_right_eq [simp]:
   10.43 +  "lcm n (nat \<bar>k\<bar>) = nat (lcm (int n) k)"
   10.44 +  by (simp add: lcm_int_def)
   10.45 +
   10.46 +lemma lcm_abs1_int [simp]:
   10.47 +  "lcm \<bar>x\<bar> y = lcm x y"
   10.48 +  for x y :: int
   10.49 +  by (simp only: lcm_int_def) simp
   10.50 +
   10.51 +lemma lcm_abs2_int [simp]:
   10.52 +  "lcm x \<bar>y\<bar> = lcm x y"
   10.53 +  for x y :: int
   10.54 +  by (simp only: lcm_int_def) simp
   10.55 +
   10.56 +lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
   10.57 +  for i j :: int
   10.58 +  by (simp only: lcm_int_def)
   10.59 +
   10.60  lemma gcd_nat_induct:
   10.61    fixes m n :: nat
   10.62    assumes "\<And>m. P m 0"
   10.63 @@ -1767,35 +1820,13 @@
   10.64     apply simp_all
   10.65    done
   10.66  
   10.67 -lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   10.68 -  by (simp add: gcd_int_def)
   10.69 -
   10.70 -lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   10.71 -  by (simp add: lcm_int_def)
   10.72 -
   10.73  lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
   10.74    for x y :: int
   10.75 -  by (simp add: gcd_int_def)
   10.76 +  by (simp only: gcd_int_def) simp
   10.77  
   10.78  lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
   10.79    for x y :: int
   10.80 -  by (simp add: gcd_int_def)
   10.81 -
   10.82 -lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
   10.83 -  for x y :: int
   10.84 -  by (simp add: gcd_int_def)
   10.85 -
   10.86 -lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
   10.87 -  for x y :: int
   10.88 -  by (simp add: gcd_int_def)
   10.89 -
   10.90 -lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
   10.91 -  for x y :: int
   10.92 -  by (metis abs_idempotent gcd_abs_int)
   10.93 -
   10.94 -lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
   10.95 -  for x y :: int
   10.96 -  by (metis abs_idempotent gcd_abs_int)
   10.97 +  by (simp only: gcd_int_def) simp
   10.98  
   10.99  lemma gcd_cases_int:
  10.100    fixes x y :: int
  10.101 @@ -1812,27 +1843,11 @@
  10.102  
  10.103  lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
  10.104    for x y :: int
  10.105 -  by (simp add: lcm_int_def)
  10.106 +  by (simp only: lcm_int_def) simp
  10.107  
  10.108  lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
  10.109    for x y :: int
  10.110 -  by (simp add: lcm_int_def)
  10.111 -
  10.112 -lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
  10.113 -  for x y :: int
  10.114 -  by (simp add: lcm_int_def)
  10.115 -
  10.116 -lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
  10.117 -  for i j :: int
  10.118 -  by (simp add:lcm_int_def)
  10.119 -
  10.120 -lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
  10.121 -  for x y :: int
  10.122 -  by (metis abs_idempotent lcm_int_def)
  10.123 -
  10.124 -lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
  10.125 -  for x y :: int
  10.126 -  by (metis abs_idempotent lcm_int_def)
  10.127 +  by (simp only: lcm_int_def) simp
  10.128  
  10.129  lemma lcm_cases_int:
  10.130    fixes x y :: int
  10.131 @@ -1845,7 +1860,7 @@
  10.132  
  10.133  lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
  10.134    for x y :: int
  10.135 -  by (simp add: lcm_int_def)
  10.136 +  by (simp only: lcm_int_def)
  10.137  
  10.138  lemma gcd_0_nat: "gcd x 0 = x"
  10.139    for x :: nat
  10.140 @@ -1861,7 +1876,7 @@
  10.141  
  10.142  lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
  10.143    for x :: int
  10.144 -  by (auto simp:gcd_int_def)
  10.145 +  by (auto simp: gcd_int_def)
  10.146  
  10.147  lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
  10.148    for x y :: nat
  10.149 @@ -1923,9 +1938,20 @@
  10.150  qed (simp_all add: lcm_nat_def)
  10.151  
  10.152  instance int :: ring_gcd
  10.153 -  by standard
  10.154 -    (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
  10.155 -      zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
  10.156 +proof
  10.157 +  fix k l r :: int
  10.158 +  show "gcd k l dvd k" "gcd k l dvd l"
  10.159 +    using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  10.160 +      gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  10.161 +    by simp_all
  10.162 +  show "lcm k l = normalize (k * l) div gcd k l"
  10.163 +    using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  10.164 +    by (simp add: nat_eq_iff of_nat_div abs_mult)
  10.165 +  assume "r dvd k" "r dvd l"
  10.166 +  then show "r dvd gcd k l"
  10.167 +    using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
  10.168 +    by simp
  10.169 +qed simp
  10.170  
  10.171  lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
  10.172    for a b :: nat
  10.173 @@ -1975,7 +2001,7 @@
  10.174  
  10.175  lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
  10.176    for x y :: int
  10.177 -  by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
  10.178 +  by (metis abs_dvd_iff gcd_0_left_int gcd_unique_int)
  10.179  
  10.180  lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
  10.181    for x y :: int
  10.182 @@ -1995,7 +2021,7 @@
  10.183  
  10.184  lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
  10.185    for k m n :: int
  10.186 -  by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
  10.187 +  using gcd_mult_distrib' [of k m n] by simp
  10.188  
  10.189  text \<open>\medskip Addition laws.\<close>
  10.190  
  10.191 @@ -2097,7 +2123,7 @@
  10.192  
  10.193  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>"
  10.194    for k l :: int
  10.195 -  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  10.196 +  using gcd_red_int [of "\<bar>k\<bar>" "\<bar>l\<bar>"] by simp
  10.197  
  10.198  lemma coprime_Suc_left_nat [simp]:
  10.199    "coprime (Suc n) n"
  10.200 @@ -2421,8 +2447,8 @@
  10.201  
  10.202  lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  10.203    for a b :: int
  10.204 -  by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
  10.205 -
  10.206 +  by (simp add: abs_mult lcm_gcd)
  10.207 +  
  10.208  lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
  10.209    for m n :: nat
  10.210    unfolding lcm_nat_def
  10.211 @@ -2439,11 +2465,11 @@
  10.212  
  10.213  lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
  10.214    for m n :: nat
  10.215 -  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  10.216 +  using lcm_eq_0_iff [of m n] by auto
  10.217  
  10.218  lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
  10.219    for m n :: int
  10.220 -  by (simp add: lcm_int_def lcm_pos_nat)
  10.221 +  by (simp add: less_le lcm_eq_0_iff)
  10.222  
  10.223  lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
  10.224    for m n :: nat
  10.225 @@ -2653,33 +2679,83 @@
  10.226  
  10.227  subsubsection \<open>Setwise GCD and LCM for integers\<close>
  10.228  
  10.229 -instantiation int :: semiring_Gcd
  10.230 +instantiation int :: Gcd
  10.231  begin
  10.232  
  10.233 -definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
  10.234 -
  10.235 -definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
  10.236 -
  10.237 -instance
  10.238 -  by standard
  10.239 -    (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
  10.240 -      Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
  10.241 +definition Gcd_int :: "int set \<Rightarrow> int"
  10.242 +  where "Gcd K = int (GCD k\<in>K. (nat \<circ> abs) k)"
  10.243 +
  10.244 +definition Lcm_int :: "int set \<Rightarrow> int"
  10.245 +  where "Lcm K = int (LCM k\<in>K. (nat \<circ> abs) k)"
  10.246 +
  10.247 +instance ..
  10.248  
  10.249  end
  10.250  
  10.251 -lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
  10.252 +lemma Gcd_int_eq [simp]:
  10.253 +  "(GCD n\<in>N. int n) = int (Gcd N)"
  10.254 +  by (simp add: Gcd_int_def image_image)
  10.255 +
  10.256 +lemma Gcd_nat_abs_eq [simp]:
  10.257 +  "(GCD k\<in>K. nat \<bar>k\<bar>) = nat (Gcd K)"
  10.258 +  by (simp add: Gcd_int_def)
  10.259 +
  10.260 +lemma abs_Gcd_eq [simp]:
  10.261 +  "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set"
  10.262 +  by (simp only: Gcd_int_def)
  10.263 +
  10.264 +lemma Gcd_int_greater_eq_0 [simp]:
  10.265 +  "Gcd K \<ge> 0"
  10.266    for K :: "int set"
  10.267 -  using normalize_Gcd [of K] by simp
  10.268 -
  10.269 -lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
  10.270 +  using abs_ge_zero [of "Gcd K"] by simp
  10.271 +
  10.272 +lemma Gcd_abs_eq [simp]:
  10.273 +  "(GCD k\<in>K. \<bar>k\<bar>) = Gcd K"
  10.274    for K :: "int set"
  10.275 -  using normalize_Lcm [of K] by simp
  10.276 -
  10.277 -lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
  10.278 -  by (simp add: Gcd_int_def comp_def image_image)
  10.279 -
  10.280 -lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
  10.281 -  by (simp add: Lcm_int_def comp_def image_image)
  10.282 +  by (simp only: Gcd_int_def image_image) simp
  10.283 +
  10.284 +lemma Lcm_int_eq [simp]:
  10.285 +  "(LCM n\<in>N. int n) = int (Lcm N)"
  10.286 +  by (simp add: Lcm_int_def image_image)
  10.287 +
  10.288 +lemma Lcm_nat_abs_eq [simp]:
  10.289 +  "(LCM k\<in>K. nat \<bar>k\<bar>) = nat (Lcm K)"
  10.290 +  by (simp add: Lcm_int_def)
  10.291 +
  10.292 +lemma abs_Lcm_eq [simp]:
  10.293 +  "\<bar>Lcm K\<bar> = Lcm K" for K :: "int set"
  10.294 +  by (simp only: Lcm_int_def)
  10.295 +
  10.296 +lemma Lcm_int_greater_eq_0 [simp]:
  10.297 +  "Lcm K \<ge> 0"
  10.298 +  for K :: "int set"
  10.299 +  using abs_ge_zero [of "Lcm K"] by simp
  10.300 +
  10.301 +lemma Lcm_abs_eq [simp]:
  10.302 +  "(LCM k\<in>K. \<bar>k\<bar>) = Lcm K"
  10.303 +  for K :: "int set"
  10.304 +  by (simp only: Lcm_int_def image_image) simp
  10.305 +
  10.306 +instance int :: semiring_Gcd
  10.307 +proof
  10.308 +  fix K :: "int set" and k :: int
  10.309 +  show "Gcd K dvd k" and "k dvd Lcm K" if "k \<in> K"
  10.310 +    using that Gcd_dvd [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
  10.311 +      dvd_Lcm [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
  10.312 +    by (simp_all add: comp_def)
  10.313 +  show "k dvd Gcd K" if "\<And>l. l \<in> K \<Longrightarrow> k dvd l"
  10.314 +  proof -
  10.315 +    have "nat \<bar>k\<bar> dvd (GCD k\<in>K. nat \<bar>k\<bar>)"
  10.316 +      by (rule Gcd_greatest) (use that in auto)
  10.317 +    then show ?thesis by simp
  10.318 +  qed
  10.319 +  show "Lcm K dvd k" if "\<And>l. l \<in> K \<Longrightarrow> l dvd k"
  10.320 +  proof -
  10.321 +    have "(LCM k\<in>K. nat \<bar>k\<bar>) dvd nat \<bar>k\<bar>"
  10.322 +      by (rule Lcm_least) (use that in auto)
  10.323 +    then show ?thesis by simp
  10.324 +  qed
  10.325 +qed simp_all
  10.326  
  10.327  
  10.328  subsection \<open>GCD and LCM on @{typ integer}\<close>
    11.1 --- a/src/HOL/Int.thy	Sat Dec 02 16:50:53 2017 +0000
    11.2 +++ b/src/HOL/Int.thy	Sat Dec 02 16:50:53 2017 +0000
    11.3 @@ -1499,43 +1499,64 @@
    11.4    then show ?thesis by simp
    11.5  qed
    11.6  
    11.7 -theorem zdvd_int: "x dvd y \<longleftrightarrow> int x dvd int y"
    11.8 +lemma int_dvd_int_iff [simp]:
    11.9 +  "int m dvd int n \<longleftrightarrow> m dvd n"
   11.10  proof -
   11.11 -  have "x dvd y" if "int y = int x * k" for k
   11.12 +  have "m dvd n" if "int n = int m * k" for k
   11.13    proof (cases k)
   11.14 -    case (nonneg n)
   11.15 -    with that have "y = x * n"
   11.16 +    case (nonneg q)
   11.17 +    with that have "n = m * q"
   11.18        by (simp del: of_nat_mult add: of_nat_mult [symmetric])
   11.19      then show ?thesis ..
   11.20    next
   11.21 -    case (neg n)
   11.22 -    with that have "int y = int x * (- int (Suc n))"
   11.23 +    case (neg q)
   11.24 +    with that have "int n = int m * (- int (Suc q))"
   11.25        by simp
   11.26 -    also have "\<dots> = - (int x * int (Suc n))"
   11.27 +    also have "\<dots> = - (int m * int (Suc q))"
   11.28        by (simp only: mult_minus_right)
   11.29 -    also have "\<dots> = - int (x * Suc n)"
   11.30 +    also have "\<dots> = - int (m * Suc q)"
   11.31        by (simp only: of_nat_mult [symmetric])
   11.32 -    finally have "- int (x * Suc n) = int y" ..
   11.33 +    finally have "- int (m * Suc q) = int n" ..
   11.34      then show ?thesis
   11.35        by (simp only: negative_eq_positive) auto
   11.36    qed
   11.37 -  then show ?thesis
   11.38 -    by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
   11.39 +  then show ?thesis by (auto simp add: dvd_def)
   11.40  qed
   11.41  
   11.42 -lemma zdvd1_eq[simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   11.43 -  (is "?lhs \<longleftrightarrow> ?rhs")
   11.44 +lemma dvd_nat_abs_iff [simp]:
   11.45 +  "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd k"
   11.46 +proof -
   11.47 +  have "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd int (nat \<bar>k\<bar>)"
   11.48 +    by (simp only: int_dvd_int_iff)
   11.49 +  then show ?thesis
   11.50 +    by simp
   11.51 +qed
   11.52 +
   11.53 +lemma nat_abs_dvd_iff [simp]:
   11.54 +  "nat \<bar>k\<bar> dvd n \<longleftrightarrow> k dvd int n"
   11.55 +proof -
   11.56 +  have "nat \<bar>k\<bar> dvd n \<longleftrightarrow> int (nat \<bar>k\<bar>) dvd int n"
   11.57 +    by (simp only: int_dvd_int_iff)
   11.58 +  then show ?thesis
   11.59 +    by simp
   11.60 +qed
   11.61 +
   11.62 +lemma zdvd1_eq [simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" (is "?lhs \<longleftrightarrow> ?rhs")
   11.63    for x :: int
   11.64  proof
   11.65    assume ?lhs
   11.66 -  then have "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   11.67 -  then have "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   11.68 -  then have "nat \<bar>x\<bar> = 1" by simp
   11.69 -  then show ?rhs by (cases "x < 0") auto
   11.70 +  then have "nat \<bar>x\<bar> dvd nat \<bar>1\<bar>"
   11.71 +    by (simp only: nat_abs_dvd_iff) simp
   11.72 +  then have "nat \<bar>x\<bar> = 1"
   11.73 +    by simp
   11.74 +  then show ?rhs
   11.75 +    by (cases "x < 0") simp_all
   11.76  next
   11.77    assume ?rhs
   11.78 -  then have "x = 1 \<or> x = - 1" by auto
   11.79 -  then show ?lhs by (auto intro: dvdI)
   11.80 +  then have "x = 1 \<or> x = - 1"
   11.81 +    by auto
   11.82 +  then show ?lhs
   11.83 +    by (auto intro: dvdI)
   11.84  qed
   11.85  
   11.86  lemma zdvd_mult_cancel1:
   11.87 @@ -1554,17 +1575,8 @@
   11.88      by (simp only: zdvd1_eq)
   11.89  qed
   11.90  
   11.91 -lemma int_dvd_iff: "int m dvd z \<longleftrightarrow> m dvd nat \<bar>z\<bar>"
   11.92 -  by (cases "z \<ge> 0") (simp_all add: zdvd_int)
   11.93 -
   11.94 -lemma dvd_int_iff: "z dvd int m \<longleftrightarrow> nat \<bar>z\<bar> dvd m"
   11.95 -  by (cases "z \<ge> 0") (simp_all add: zdvd_int)
   11.96 -
   11.97 -lemma dvd_int_unfold_dvd_nat: "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
   11.98 -  by (simp add: dvd_int_iff [symmetric])
   11.99 -
  11.100  lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)"
  11.101 -  by (auto simp add: dvd_int_iff)
  11.102 +  using nat_abs_dvd_iff [of z m] by (cases "z \<ge> 0") auto
  11.103  
  11.104  lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
  11.105    by (auto elim: nonneg_int_cases)
  11.106 @@ -1603,7 +1615,7 @@
  11.107  lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
  11.108    for n z :: int
  11.109    apply (cases n)
  11.110 -   apply (auto simp add: dvd_int_iff)
  11.111 +  apply auto
  11.112    apply (cases z)
  11.113     apply (auto simp add: dvd_imp_le)
  11.114    done
    12.1 --- a/src/HOL/Library/Float.thy	Sat Dec 02 16:50:53 2017 +0000
    12.2 +++ b/src/HOL/Library/Float.thy	Sat Dec 02 16:50:53 2017 +0000
    12.3 @@ -1193,6 +1193,7 @@
    12.4          l_def[symmetric, THEN meta_eq_to_obj_eq]
    12.5        apply transfer
    12.6        apply (auto simp add: round_up_def truncate_up_rat_precision)
    12.7 +      apply (metis dvd_triv_left of_nat_dvd_iff)
    12.8        apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
    12.9        done
   12.10     next
   12.11 @@ -1208,6 +1209,7 @@
   12.12          l_def[symmetric, THEN meta_eq_to_obj_eq]
   12.13        apply transfer
   12.14        apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision)
   12.15 +      apply (metis dvd_triv_left of_nat_dvd_iff)
   12.16        apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
   12.17        done
   12.18    qed
    13.1 --- a/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Dec 02 16:50:53 2017 +0000
    13.2 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Dec 02 16:50:53 2017 +0000
    13.3 @@ -17,8 +17,9 @@
    13.4    using p_ge_2 p_prime prime_odd_nat by blast
    13.5  
    13.6  private lemma p_minus_1_int:
    13.7 -  "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
    13.8 -
    13.9 +  "int (p - 1) = int p - 1"
   13.10 +  by (metis of_nat_1 of_nat_diff p_prime prime_ge_1_nat)
   13.11 +  
   13.12  private lemma p_not_eq_Suc_0 [simp]:
   13.13    "p \<noteq> Suc 0"
   13.14    using p_ge_2 by simp
   13.15 @@ -46,8 +47,9 @@
   13.16    proof -
   13.17      have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
   13.18      using p_prime proof (rule fermat_theorem)
   13.19 -      show "\<not> p dvd nat \<bar>b\<bar>"
   13.20 -        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))
   13.21 +      from b p_a_relprime show "\<not> p dvd nat \<bar>b\<bar>"
   13.22 +        by (auto simp add: cong_altdef_int power2_eq_square)
   13.23 +          (metis cong_altdef_int cong_dvd_iff dvd_mult2) 
   13.24      qed
   13.25      then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
   13.26        by (simp add: cong_def)
    14.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sat Dec 02 16:50:53 2017 +0000
    14.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sat Dec 02 16:50:53 2017 +0000
    14.3 @@ -117,7 +117,7 @@
    14.4        by (simp add: cong_altdef_int)
    14.5      with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
    14.6      have "coprime a (int p)"
    14.7 -      by (simp_all add: zdvd_int ac_simps)
    14.8 +      by (simp_all add: ac_simps)
    14.9      with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
   14.10        by simp
   14.11      with cong_less_imp_eq_int [of x y p] p_minus_one_l
   14.12 @@ -152,7 +152,7 @@
   14.13        by (simp add: cong_altdef_int)
   14.14      with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
   14.15      have "coprime a (int p)"
   14.16 -      by (simp_all add: zdvd_int ac_simps)  
   14.17 +      by (simp_all add: ac_simps)  
   14.18      with a' cong_mult_rcancel_int [of a "int p" x y]
   14.19      have "[x = y] (mod p)" by simp
   14.20      with cong_less_imp_eq_int [of x y p] p_minus_one_l
    15.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 02 16:50:53 2017 +0000
    15.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 02 16:50:53 2017 +0000
    15.3 @@ -25,8 +25,8 @@
    15.4    using p_ge_2 p_prime prime_odd_nat by blast
    15.5  
    15.6  lemma p_ge_0: "0 < int p"
    15.7 -  using p_prime not_prime_0[where 'a = nat] by fastforce+
    15.8 -
    15.9 +  by (simp add: p_prime prime_gt_0_nat)
   15.10 +  
   15.11  lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
   15.12    using odd_p by simp
   15.13  
   15.14 @@ -34,7 +34,7 @@
   15.15    using q_ge_2 q_prime prime_odd_nat by blast
   15.16  
   15.17  lemma q_ge_0: "0 < int q"
   15.18 -  using q_prime not_prime_0[where 'a = nat] by fastforce+
   15.19 +  by (simp add: q_prime prime_gt_0_nat)
   15.20  
   15.21  lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1"
   15.22    using odd_q by simp
   15.23 @@ -93,7 +93,7 @@
   15.24  
   15.25  lemma Gpq: "GAUSS p q"
   15.26    using p_prime pq_neq p_ge_2 q_prime
   15.27 -  by (auto simp: GAUSS_def cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq)
   15.28 +  by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq)
   15.29  
   15.30  lemma Gqp: "GAUSS q p"
   15.31    by (simp add: QRqp QR.Gpq)
    16.1 --- a/src/HOL/Number_Theory/Totient.thy	Sat Dec 02 16:50:53 2017 +0000
    16.2 +++ b/src/HOL/Number_Theory/Totient.thy	Sat Dec 02 16:50:53 2017 +0000
    16.3 @@ -78,7 +78,7 @@
    16.4  qed (auto simp: totatives_def)
    16.5  
    16.6  lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}"
    16.7 -  using totatives_prime_power_Suc[of p 0] by fastforce
    16.8 +  using totatives_prime_power_Suc [of p 0] by auto
    16.9  
   16.10  lemma bij_betw_totatives:
   16.11    assumes "m1 > 1" "m2 > 1" "coprime m1 m2"
    17.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 02 16:50:53 2017 +0000
    17.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 02 16:50:53 2017 +0000
    17.3 @@ -811,7 +811,7 @@
    17.4  val ss1 =
    17.5    simpset_of (put_simpset comp_ss @{context}
    17.6      addsimps @{thms simp_thms} @ 
    17.7 -            [@{thm "nat_numeral"} RS sym, @{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] 
    17.8 +            [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] 
    17.9          @ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]
   17.10      |> Splitter.add_split @{thm "zdiff_int_split"})
   17.11  
    18.1 --- a/src/HOL/Word/Word.thy	Sat Dec 02 16:50:53 2017 +0000
    18.2 +++ b/src/HOL/Word/Word.thy	Sat Dec 02 16:50:53 2017 +0000
    18.3 @@ -3997,22 +3997,50 @@
    18.4      done
    18.5  qed
    18.6  
    18.7 -lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
    18.8 -  apply (unfold word_rot_defs)
    18.9 -  apply (cut_tac y="size w" in gt_or_eq_0)
   18.10 -  apply (erule disjE)
   18.11 -   apply simp_all
   18.12 -  apply (safe intro!: abl_cong)
   18.13 -   apply (rule rotater_eqs)
   18.14 -   apply (simp add: word_size nat_mod_distrib)
   18.15 -  apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
   18.16 -  apply (rule rotater_eqs)
   18.17 -  apply (simp add: word_size nat_mod_distrib)
   18.18 -  apply (rule of_nat_eq_0_iff [THEN iffD1])
   18.19 -  apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
   18.20 -  using mod_mod_trivial mod_eq_dvd_iff
   18.21 -  apply blast
   18.22 -  done
   18.23 +lemma word_roti_conv_mod':
   18.24 +  "word_roti n w = word_roti (n mod int (size w)) w"
   18.25 +proof (cases "size w = 0")
   18.26 +  case True
   18.27 +  then show ?thesis
   18.28 +    by simp
   18.29 +next
   18.30 +  case False
   18.31 +  then have [simp]: "l mod int (size w) \<ge> 0" for l
   18.32 +    by simp
   18.33 +  then have *: "word_roti (n mod int (size w)) w = word_rotr (nat (n mod int (size w))) w"
   18.34 +    by (simp add: word_roti_def)
   18.35 +  show ?thesis
   18.36 +  proof (cases "n \<ge> 0")
   18.37 +    case True
   18.38 +    then show ?thesis
   18.39 +      apply (auto simp add: not_le *)
   18.40 +      apply (auto simp add: word_rot_defs)
   18.41 +      apply (safe intro!: abl_cong)
   18.42 +      apply (rule rotater_eqs)
   18.43 +      apply (simp add: word_size nat_mod_distrib)
   18.44 +      done
   18.45 +  next
   18.46 +    case False
   18.47 +    moreover define k where "k = - n"
   18.48 +    ultimately have n: "n = - k"
   18.49 +      by simp_all
   18.50 +    from False show ?thesis
   18.51 +      apply (auto simp add: not_le *)
   18.52 +      apply (auto simp add: word_rot_defs)
   18.53 +      apply (simp add: n)
   18.54 +      apply (safe intro!: abl_cong)
   18.55 +      apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
   18.56 +      apply (rule rotater_eqs)
   18.57 +      apply (simp add: word_size [symmetric, of w])
   18.58 +      apply (rule of_nat_eq_0_iff [THEN iffD1])
   18.59 +      apply (auto simp add: nat_add_distrib [symmetric] mod_eq_0_iff_dvd)
   18.60 +      using dvd_nat_abs_iff [of "size w" "- k mod int (size w) + k"]
   18.61 +      apply (simp add: algebra_simps)
   18.62 +      apply (simp add: word_size)
   18.63 +      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)
   18.64 +      done
   18.65 +  qed
   18.66 +qed
   18.67  
   18.68  lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
   18.69  
    19.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 02 16:50:53 2017 +0000
    19.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sat Dec 02 16:50:53 2017 +0000
    19.3 @@ -86,7 +86,7 @@
    19.4    unfolding rel_fun_def ZN_def by simp
    19.5  
    19.6  lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
    19.7 -  unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
    19.8 +  unfolding rel_fun_def ZN_def by simp
    19.9  
   19.10  lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
   19.11    unfolding rel_fun_def ZN_def by (simp add: zdiv_int)