Removed subsumed lemmas
authornipkow
Sat Feb 21 20:52:30 2009 +0100 (2009-02-21)
changeset 3004231039ee583fa
parent 30035 7f4d475a6c50
child 30043 9925ee6a5c59
Removed subsumed lemmas
src/HOL/Algebra/Exponent.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Groebner_Basis.thy
src/HOL/Hoare/Arith2.thy
src/HOL/IntDiv.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Pocklington.thy
src/HOL/Library/Primes.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Euler.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/Residues.thy
src/HOL/NumberTheory/WilsonBij.thy
src/HOL/NumberTheory/WilsonRuss.thy
src/HOL/RealDef.thy
src/HOL/Ring_and_Field.thy
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Word/Num_Lemmas.thy
src/HOL/Word/WordShift.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Sat Feb 21 09:58:45 2009 +0100
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Sat Feb 21 20:52:30 2009 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4   prefer 2 apply (blast intro: dvd_mult2)
     1.5  apply (drule dvd_diffD1)
     1.6    apply assumption
     1.7 - prefer 2 apply (blast intro: dvd_diff)
     1.8 + prefer 2 apply (blast intro: nat_dvd_diff)
     1.9  apply (drule gr0_implies_Suc, auto)
    1.10  done
    1.11  
    1.12 @@ -231,7 +231,7 @@
    1.13   prefer 2 apply (blast intro: dvd_mult2)
    1.14  apply (drule dvd_diffD1)
    1.15    apply assumption
    1.16 - prefer 2 apply (blast intro: dvd_diff)
    1.17 + prefer 2 apply (blast intro: nat_dvd_diff)
    1.18  apply (drule less_imp_Suc_add, auto)
    1.19  done
    1.20  
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sat Feb 21 09:58:45 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Feb 21 20:52:30 2009 +0100
     2.3 @@ -620,7 +620,7 @@
     2.4    {assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
     2.5    moreover 
     2.6    {assume i1: "abs i = 1"
     2.7 -      from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
     2.8 +      from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
     2.9        have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
    2.10  	by (cases "i > 0", simp_all)}
    2.11    moreover   
    2.12 @@ -640,7 +640,7 @@
    2.13    {assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
    2.14    moreover 
    2.15    {assume i1: "abs i = 1"
    2.16 -      from zdvd_1_left[where m = "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
    2.17 +      from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
    2.18        have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
    2.19        apply (cases "i > 0", simp_all) done}
    2.20    moreover   
    2.21 @@ -990,7 +990,7 @@
    2.22    have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
    2.23    moreover
    2.24    {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
    2.25 -    hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
    2.26 +    hence ?case using prems by (simp del: zlfm.simps)}
    2.27    moreover
    2.28    {assume "?c=0" and "j\<noteq>0" hence ?case 
    2.29        using zsplit0_I[OF spl, where x="i" and bs="bs"]
    2.30 @@ -1005,7 +1005,7 @@
    2.31    moreover
    2.32    {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    2.33        by (simp add: nb Let_def split_def)
    2.34 -    hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
    2.35 +    hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
    2.36        by (simp add: Let_def split_def) }
    2.37    ultimately show ?case by blast
    2.38  next
    2.39 @@ -1019,7 +1019,7 @@
    2.40    have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
    2.41    moreover
    2.42    {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
    2.43 -    hence ?case using prems by (simp del: zlfm.simps add: zdvd_0_left)}
    2.44 +    hence ?case using prems by (simp del: zlfm.simps)}
    2.45    moreover
    2.46    {assume "?c=0" and "j\<noteq>0" hence ?case 
    2.47        using zsplit0_I[OF spl, where x="i" and bs="bs"]
    2.48 @@ -1034,7 +1034,7 @@
    2.49    moreover
    2.50    {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    2.51        by (simp add: nb Let_def split_def)
    2.52 -    hence ?case using Ia cn jnz zdvd_zminus_iff[where m="abs j" and n="?c*i + ?N ?r" ]
    2.53 +    hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
    2.54        by (simp add: Let_def split_def)}
    2.55    ultimately show ?case by blast
    2.56  qed auto
    2.57 @@ -1092,10 +1092,10 @@
    2.58    using lin ad d
    2.59  proof(induct p rule: iszlfm.induct)
    2.60    case (9 i c e)  thus ?case using d
    2.61 -    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
    2.62 +    by (simp add: dvd_trans[of "i" "d" "d'"])
    2.63  next
    2.64    case (10 i c e) thus ?case using d
    2.65 -    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
    2.66 +    by (simp add: dvd_trans[of "i" "d" "d'"])
    2.67  qed simp_all
    2.68  
    2.69  lemma \<delta> : assumes lin:"iszlfm p"
    2.70 @@ -1354,7 +1354,7 @@
    2.71    case (9 j c e) hence nb: "numbound0 e" by simp
    2.72    have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
    2.73      also have "\<dots> = (j dvd (- (c*x - ?e)))"
    2.74 -    by (simp only: zdvd_zminus_iff)
    2.75 +    by (simp only: dvd_minus_iff)
    2.76    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
    2.77      apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
    2.78      by (simp add: algebra_simps)
    2.79 @@ -1366,7 +1366,7 @@
    2.80      case (10 j c e) hence nb: "numbound0 e" by simp
    2.81    have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
    2.82      also have "\<dots> = (j dvd (- (c*x - ?e)))"
    2.83 -    by (simp only: zdvd_zminus_iff)
    2.84 +    by (simp only: dvd_minus_iff)
    2.85    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
    2.86      apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
    2.87      by (simp add: algebra_simps)
    2.88 @@ -1392,7 +1392,7 @@
    2.89    and dr: "d\<beta> p l"
    2.90    and d: "l dvd l'"
    2.91    shows "d\<beta> p l'"
    2.92 -using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
    2.93 +using dr linp dvd_trans[of _ "l" "l'", simplified d]
    2.94  by (induct p rule: iszlfm.induct) simp_all
    2.95  
    2.96  lemma \<alpha>_l: assumes lp: "iszlfm p"
    2.97 @@ -1431,7 +1431,7 @@
    2.98        by (simp add: zdiv_mono1[OF clel cp])
    2.99      then have ldcp:"0 < l div c" 
   2.100        by (simp add: zdiv_self[OF cnz])
   2.101 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.102 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.103      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.104        by simp
   2.105      hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
   2.106 @@ -1449,7 +1449,7 @@
   2.107        by (simp add: zdiv_mono1[OF clel cp])
   2.108      then have ldcp:"0 < l div c" 
   2.109        by (simp add: zdiv_self[OF cnz])
   2.110 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.111 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.112      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.113        by simp
   2.114      hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
   2.115 @@ -1467,7 +1467,7 @@
   2.116        by (simp add: zdiv_mono1[OF clel cp])
   2.117      then have ldcp:"0 < l div c" 
   2.118        by (simp add: zdiv_self[OF cnz])
   2.119 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.120 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.121      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.122        by simp
   2.123      hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
   2.124 @@ -1485,7 +1485,7 @@
   2.125        by (simp add: zdiv_mono1[OF clel cp])
   2.126      then have ldcp:"0 < l div c" 
   2.127        by (simp add: zdiv_self[OF cnz])
   2.128 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.129 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.130      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.131        by simp
   2.132      hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
   2.133 @@ -1505,7 +1505,7 @@
   2.134        by (simp add: zdiv_mono1[OF clel cp])
   2.135      then have ldcp:"0 < l div c" 
   2.136        by (simp add: zdiv_self[OF cnz])
   2.137 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.138 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.139      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.140        by simp
   2.141      hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
   2.142 @@ -1523,7 +1523,7 @@
   2.143        by (simp add: zdiv_mono1[OF clel cp])
   2.144      then have ldcp:"0 < l div c" 
   2.145        by (simp add: zdiv_self[OF cnz])
   2.146 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.147 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.148      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.149        by simp
   2.150      hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
   2.151 @@ -1541,7 +1541,7 @@
   2.152        by (simp add: zdiv_mono1[OF clel cp])
   2.153      then have ldcp:"0 < l div c" 
   2.154        by (simp add: zdiv_self[OF cnz])
   2.155 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.156 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.157      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.158        by simp
   2.159      hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
   2.160 @@ -1558,7 +1558,7 @@
   2.161        by (simp add: zdiv_mono1[OF clel cp])
   2.162      then have ldcp:"0 < l div c" 
   2.163        by (simp add: zdiv_self[OF cnz])
   2.164 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   2.165 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   2.166      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   2.167        by simp
   2.168      hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Feb 21 09:58:45 2009 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Feb 21 20:52:30 2009 +0100
     3.3 @@ -501,9 +501,9 @@
     3.4    assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
     3.5    shows "dvdnumcoeff t g"
     3.6    using dgt' gdg 
     3.7 -  by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
     3.8 +  by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
     3.9  
    3.10 -declare zdvd_trans [trans add]
    3.11 +declare dvd_trans [trans add]
    3.12  
    3.13  lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
    3.14  by arith
     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Feb 21 09:58:45 2009 +0100
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Feb 21 20:52:30 2009 +0100
     4.3 @@ -132,13 +132,13 @@
     4.4    assume d: "real d rdvd t"
     4.5    from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" by auto
     4.6  
     4.7 -  from iffD2[OF zdvd_abs1] d2 have "(abs d) dvd (floor t)" by blast
     4.8 +  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast
     4.9    with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast 
    4.10    thus "abs (real d) rdvd t" by simp
    4.11  next
    4.12    assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp
    4.13    with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" by auto
    4.14 -  from iffD1[OF zdvd_abs1] d2 have "d dvd floor t" by blast
    4.15 +  from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast
    4.16    with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast
    4.17  qed
    4.18  
    4.19 @@ -675,9 +675,9 @@
    4.20    assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
    4.21    shows "dvdnumcoeff t g"
    4.22    using dgt' gdg 
    4.23 -  by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
    4.24 -
    4.25 -declare zdvd_trans [trans add]
    4.26 +  by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
    4.27 +
    4.28 +declare dvd_trans [trans add]
    4.29  
    4.30  lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
    4.31  by arith
    4.32 @@ -2114,10 +2114,10 @@
    4.33    using lin ad d
    4.34  proof(induct p rule: iszlfm.induct)
    4.35    case (9 i c e)  thus ?case using d
    4.36 -    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
    4.37 +    by (simp add: dvd_trans[of "i" "d" "d'"])
    4.38  next
    4.39    case (10 i c e) thus ?case using d
    4.40 -    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
    4.41 +    by (simp add: dvd_trans[of "i" "d" "d'"])
    4.42  qed simp_all
    4.43  
    4.44  lemma \<delta> : assumes lin:"iszlfm p bs"
    4.45 @@ -2496,7 +2496,7 @@
    4.46    and dr: "d\<beta> p l"
    4.47    and d: "l dvd l'"
    4.48    shows "d\<beta> p l'"
    4.49 -using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
    4.50 +using dr linp dvd_trans[of _ "l" "l'", simplified d]
    4.51  by (induct p rule: iszlfm.induct) simp_all
    4.52  
    4.53  lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)"
    4.54 @@ -2535,7 +2535,7 @@
    4.55        by (simp add: zdiv_mono1[OF clel cp])
    4.56      then have ldcp:"0 < l div c" 
    4.57        by (simp add: zdiv_self[OF cnz])
    4.58 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
    4.59 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.60      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.61        by simp
    4.62      hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =
    4.63 @@ -2553,7 +2553,7 @@
    4.64        by (simp add: zdiv_mono1[OF clel cp])
    4.65      then have ldcp:"0 < l div c" 
    4.66        by (simp add: zdiv_self[OF cnz])
    4.67 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
    4.68 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.69      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.70        by simp
    4.71      hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =
    4.72 @@ -2571,7 +2571,7 @@
    4.73        by (simp add: zdiv_mono1[OF clel cp])
    4.74      then have ldcp:"0 < l div c" 
    4.75        by (simp add: zdiv_self[OF cnz])
    4.76 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
    4.77 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.78      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.79        by simp
    4.80      hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =
    4.81 @@ -2589,7 +2589,7 @@
    4.82        by (simp add: zdiv_mono1[OF clel cp])
    4.83      then have ldcp:"0 < l div c" 
    4.84        by (simp add: zdiv_self[OF cnz])
    4.85 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
    4.86 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.87      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.88        by simp
    4.89      hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =
    4.90 @@ -2607,7 +2607,7 @@
    4.91        by (simp add: zdiv_mono1[OF clel cp])
    4.92      then have ldcp:"0 < l div c" 
    4.93        by (simp add: zdiv_self[OF cnz])
    4.94 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
    4.95 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.96      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.97        by simp
    4.98      hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =
    4.99 @@ -2625,7 +2625,7 @@
   4.100        by (simp add: zdiv_mono1[OF clel cp])
   4.101      then have ldcp:"0 < l div c" 
   4.102        by (simp add: zdiv_self[OF cnz])
   4.103 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   4.104 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   4.105      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   4.106        by simp
   4.107      hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =
   4.108 @@ -2643,7 +2643,7 @@
   4.109        by (simp add: zdiv_mono1[OF clel cp])
   4.110      then have ldcp:"0 < l div c" 
   4.111        by (simp add: zdiv_self[OF cnz])
   4.112 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   4.113 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   4.114      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   4.115        by simp
   4.116      hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
   4.117 @@ -2660,7 +2660,7 @@
   4.118        by (simp add: zdiv_mono1[OF clel cp])
   4.119      then have ldcp:"0 < l div c" 
   4.120        by (simp add: zdiv_self[OF cnz])
   4.121 -    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
   4.122 +    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   4.123      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
   4.124        by simp
   4.125      hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
     5.1 --- a/src/HOL/Divides.thy	Sat Feb 21 09:58:45 2009 +0100
     5.2 +++ b/src/HOL/Divides.thy	Sat Feb 21 20:52:30 2009 +0100
     5.3 @@ -813,9 +813,9 @@
     5.4  interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
     5.5    proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
     5.6  
     5.7 -lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
     5.8 -  unfolding dvd_def
     5.9 -  by (blast intro: diff_mult_distrib2 [symmetric])
    5.10 +lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
    5.11 +unfolding dvd_def
    5.12 +by (blast intro: diff_mult_distrib2 [symmetric])
    5.13  
    5.14  lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
    5.15    apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    5.16 @@ -823,7 +823,7 @@
    5.17    done
    5.18  
    5.19  lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
    5.20 -by (drule_tac m = m in dvd_diff, auto)
    5.21 +by (drule_tac m = m in nat_dvd_diff, auto)
    5.22  
    5.23  lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    5.24    apply (rule iffI)
    5.25 @@ -832,7 +832,7 @@
    5.26    apply (subgoal_tac "n = (n+k) -k")
    5.27     prefer 2 apply simp
    5.28    apply (erule ssubst)
    5.29 -  apply (erule dvd_diff)
    5.30 +  apply (erule nat_dvd_diff)
    5.31    apply (rule dvd_refl)
    5.32    done
    5.33  
     6.1 --- a/src/HOL/GCD.thy	Sat Feb 21 09:58:45 2009 +0100
     6.2 +++ b/src/HOL/GCD.thy	Sat Feb 21 20:52:30 2009 +0100
     6.3 @@ -156,7 +156,6 @@
     6.4       apply (simp add: gcd_assoc)
     6.5       apply (simp add: gcd_commute)
     6.6      apply (simp_all add: mult_commute)
     6.7 -  apply (blast intro: dvd_mult)
     6.8    done
     6.9  
    6.10  
    6.11 @@ -404,7 +403,7 @@
    6.12    {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
    6.13      have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
    6.14        using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
    6.15 -    from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
    6.16 +    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
    6.17      have ?rhs by auto}
    6.18    ultimately show ?thesis by blast
    6.19  qed
    6.20 @@ -597,8 +596,8 @@
    6.21    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
    6.22    then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
    6.23    then show ?thesis
    6.24 -    apply (subst zdvd_abs1 [symmetric])
    6.25 -    apply (subst zdvd_abs2 [symmetric])
    6.26 +    apply (subst abs_dvd_iff [symmetric])
    6.27 +    apply (subst dvd_abs_iff [symmetric])
    6.28      apply (unfold dvd_def)
    6.29      apply (rule_tac x = "int h'" in exI, simp)
    6.30      done
    6.31 @@ -614,11 +613,11 @@
    6.32    let ?m' = "nat \<bar>m\<bar>"
    6.33    let ?n' = "nat \<bar>n\<bar>"
    6.34    from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
    6.35 -    unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
    6.36 +    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
    6.37    from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
    6.38      unfolding zgcd_def by (simp only: zdvd_int)
    6.39    then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
    6.40 -  then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
    6.41 +  then show "k dvd zgcd m n" by simp
    6.42  qed
    6.43  
    6.44  lemma div_zgcd_relprime:
    6.45 @@ -721,7 +720,7 @@
    6.46    assumes "k dvd i" shows "k dvd (zlcm i j)"
    6.47  proof -
    6.48    have "nat(abs k) dvd nat(abs i)" using `k dvd i`
    6.49 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
    6.50 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
    6.51    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
    6.52  qed
    6.53  
    6.54 @@ -729,7 +728,7 @@
    6.55    assumes "k dvd j" shows "k dvd (zlcm i j)"
    6.56  proof -
    6.57    have "nat(abs k) dvd nat(abs j)" using `k dvd j`
    6.58 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
    6.59 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
    6.60    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
    6.61  qed
    6.62  
     7.1 --- a/src/HOL/Groebner_Basis.thy	Sat Feb 21 09:58:45 2009 +0100
     7.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Feb 21 20:52:30 2009 +0100
     7.3 @@ -457,7 +457,7 @@
     7.4  declare mod_mult_self2_is_0[algebra]
     7.5  declare mod_mult_self1_is_0[algebra]
     7.6  declare zmod_eq_0_iff[algebra]
     7.7 -declare zdvd_0_left[algebra]
     7.8 +declare dvd_0_left_iff[algebra]
     7.9  declare zdvd1_eq[algebra]
    7.10  declare zmod_eq_dvd_iff[algebra]
    7.11  declare nat_mod_eq_iff[algebra]
     8.1 --- a/src/HOL/Hoare/Arith2.thy	Sat Feb 21 09:58:45 2009 +0100
     8.2 +++ b/src/HOL/Hoare/Arith2.thy	Sat Feb 21 20:52:30 2009 +0100
     8.3 @@ -42,12 +42,12 @@
     8.4  
     8.5  lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
     8.6    apply (unfold cd_def)
     8.7 -  apply (blast intro: dvd_diff dest: dvd_diffD)
     8.8 +  apply (fastsimp dest: dvd_diffD)
     8.9    done
    8.10  
    8.11  lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
    8.12    apply (unfold cd_def)
    8.13 -  apply (blast intro: dvd_diff dest: dvd_diffD)
    8.14 +  apply (fastsimp dest: dvd_diffD)
    8.15    done
    8.16  
    8.17  
     9.1 --- a/src/HOL/IntDiv.thy	Sat Feb 21 09:58:45 2009 +0100
     9.2 +++ b/src/HOL/IntDiv.thy	Sat Feb 21 20:52:30 2009 +0100
     9.3 @@ -836,13 +836,6 @@
     9.4    "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
     9.5  by (simp add:zdiv_zmult_zmult1)
     9.6  
     9.7 -(*
     9.8 -lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
     9.9 -apply (drule zdiv_zmult_zmult1)
    9.10 -apply (auto simp add: mult_commute)
    9.11 -done
    9.12 -*)
    9.13 -
    9.14  
    9.15  subsection{*Distribution of Factors over mod*}
    9.16  
    9.17 @@ -1001,7 +994,7 @@
    9.18  apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = 
    9.19                      1 + 2* ((-b - 1) mod (-a))")
    9.20  apply (rule_tac [2] pos_zmod_mult_2)
    9.21 -apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)
    9.22 +apply (auto simp add: right_diff_distrib)
    9.23  apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
    9.24   prefer 2 apply simp 
    9.25  apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])
    9.26 @@ -1063,38 +1056,8 @@
    9.27  
    9.28  subsection {* The Divides Relation *}
    9.29  
    9.30 -lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
    9.31 -  by (rule dvd_eq_mod_eq_0)
    9.32 -
    9.33  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    9.34 -  zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
    9.35 -
    9.36 -lemma zdvd_0_right: "(m::int) dvd 0"
    9.37 -  by (rule dvd_0_right) (* already declared [iff] *)
    9.38 -
    9.39 -lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
    9.40 -  by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
    9.41 -
    9.42 -lemma zdvd_1_left: "1 dvd (m::int)"
    9.43 -  by (rule one_dvd) (* already declared [simp] *)
    9.44 -
    9.45 -lemma zdvd_refl: "m dvd (m::int)"
    9.46 -  by (rule dvd_refl) (* already declared [simp] *)
    9.47 -
    9.48 -lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
    9.49 -  by (rule dvd_trans)
    9.50 -
    9.51 -lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
    9.52 -  by (rule dvd_minus_iff) (* already declared [simp] *)
    9.53 -
    9.54 -lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    9.55 -  by (rule minus_dvd_iff) (* already declared [simp] *)
    9.56 -
    9.57 -lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
    9.58 -  by (rule abs_dvd_iff) (* already declared [simp] *)
    9.59 -
    9.60 -lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
    9.61 -  by (rule dvd_abs_iff) (* already declared [simp] *)
    9.62 +  dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
    9.63  
    9.64  lemma zdvd_anti_sym:
    9.65      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
    9.66 @@ -1102,58 +1065,32 @@
    9.67    apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
    9.68    done
    9.69  
    9.70 -lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
    9.71 -  by (rule dvd_add)
    9.72 -
    9.73 -lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 
    9.74 +lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
    9.75    shows "\<bar>a\<bar> = \<bar>b\<bar>"
    9.76  proof-
    9.77 -  from ab obtain k where k:"b = a*k" unfolding dvd_def by blast 
    9.78 -  from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
    9.79 +  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
    9.80 +  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
    9.81    from k k' have "a = a*k*k'" by simp
    9.82    with mult_cancel_left1[where c="a" and b="k*k'"]
    9.83 -  have kk':"k*k' = 1" using anz by (simp add: mult_assoc)
    9.84 +  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
    9.85    hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
    9.86    thus ?thesis using k k' by auto
    9.87  qed
    9.88  
    9.89 -lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
    9.90 -  by (rule Ring_and_Field.dvd_diff)
    9.91 -
    9.92  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
    9.93    apply (subgoal_tac "m = n + (m - n)")
    9.94     apply (erule ssubst)
    9.95 -   apply (blast intro: zdvd_zadd, simp)
    9.96 +   apply (blast intro: dvd_add, simp)
    9.97    done
    9.98  
    9.99 -lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
   9.100 -  by (rule dvd_mult)
   9.101 -
   9.102 -lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
   9.103 -  by (rule dvd_mult2)
   9.104 -
   9.105 -lemma zdvd_triv_right: "(k::int) dvd m * k"
   9.106 -  by (rule dvd_triv_right) (* already declared [simp] *)
   9.107 -
   9.108 -lemma zdvd_triv_left: "(k::int) dvd k * m"
   9.109 -  by (rule dvd_triv_left) (* already declared [simp] *)
   9.110 -
   9.111 -lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   9.112 -  by (rule dvd_mult_left)
   9.113 -
   9.114 -lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   9.115 -  by (rule dvd_mult_right)
   9.116 -
   9.117 -lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   9.118 -  by (rule mult_dvd_mono)
   9.119 -
   9.120  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
   9.121 -  apply (rule iffI)
   9.122 -   apply (erule_tac [2] zdvd_zadd)
   9.123 -   apply (subgoal_tac "n = (n + k * m) - k * m")
   9.124 -    apply (erule ssubst)
   9.125 -    apply (erule zdvd_zdiff, simp_all)
   9.126 -  done
   9.127 +apply (rule iffI)
   9.128 + apply (erule_tac [2] dvd_add)
   9.129 + apply (subgoal_tac "n = (n + k * m) - k * m")
   9.130 +  apply (erule ssubst)
   9.131 +  apply (erule dvd_diff)
   9.132 +  apply(simp_all)
   9.133 +done
   9.134  
   9.135  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   9.136    apply (simp add: dvd_def)
   9.137 @@ -1163,7 +1100,7 @@
   9.138  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   9.139    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
   9.140     apply (simp add: zmod_zdiv_equality [symmetric])
   9.141 -  apply (simp only: zdvd_zadd zdvd_zmult2)
   9.142 +  apply (simp only: dvd_add dvd_mult2)
   9.143    done
   9.144  
   9.145  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   9.146 @@ -1183,7 +1120,7 @@
   9.147  lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
   9.148  apply (subgoal_tac "m mod n = 0")
   9.149   apply (simp add: zmult_div_cancel)
   9.150 -apply (simp only: zdvd_iff_zmod_eq_0)
   9.151 +apply (simp only: dvd_eq_mod_eq_0)
   9.152  done
   9.153  
   9.154  lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
   9.155 @@ -1196,10 +1133,6 @@
   9.156    thus ?thesis by simp
   9.157  qed
   9.158  
   9.159 -lemma zdvd_zmult_cancel_disj:
   9.160 -  "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
   9.161 -by (rule dvd_mult_cancel_left) (* already declared [simp] *)
   9.162 -
   9.163  
   9.164  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   9.165  apply (simp split add: split_nat)
   9.166 @@ -1231,44 +1164,38 @@
   9.167        then show ?thesis by (simp only: negative_eq_positive) auto
   9.168      qed
   9.169    qed
   9.170 -  then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
   9.171 +  then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
   9.172  qed
   9.173  
   9.174  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   9.175  proof
   9.176 -  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
   9.177 +  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   9.178    hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   9.179    hence "nat \<bar>x\<bar> = 1"  by simp
   9.180    thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
   9.181  next
   9.182    assume "\<bar>x\<bar>=1" thus "x dvd 1" 
   9.183 -    by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)
   9.184 +    by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
   9.185  qed
   9.186  lemma zdvd_mult_cancel1: 
   9.187    assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   9.188  proof
   9.189    assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   9.190 -    by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)
   9.191 +    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
   9.192  next
   9.193    assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   9.194    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
   9.195  qed
   9.196  
   9.197  lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   9.198 -  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus_iff)
   9.199 +  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   9.200  
   9.201  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   9.202 -  unfolding zdvd_int by (cases "z \<ge> 0") (simp_all add: zdvd_zminus2_iff)
   9.203 +  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   9.204  
   9.205  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   9.206    by (auto simp add: dvd_int_iff)
   9.207  
   9.208 -lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   9.209 -  by (rule minus_dvd_iff)
   9.210 -
   9.211 -lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   9.212 -  by (rule dvd_minus_iff)
   9.213 -
   9.214  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   9.215    apply (rule_tac z=n in int_cases)
   9.216    apply (auto simp add: dvd_int_iff)
   9.217 @@ -1395,7 +1322,7 @@
   9.218    hence "x mod n - y mod n = 0" by simp
   9.219    hence "(x mod n - y mod n) mod n = 0" by simp 
   9.220    hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   9.221 -  thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
   9.222 +  thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
   9.223  next
   9.224    assume H: "n dvd x - y"
   9.225    then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
    10.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sat Feb 21 09:58:45 2009 +0100
    10.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Feb 21 20:52:30 2009 +0100
    10.3 @@ -247,7 +247,7 @@
    10.4      (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
    10.5    apply (frule of_int_div_aux [of d n, where ?'a = 'a])
    10.6    apply simp
    10.7 -  apply (simp add: zdvd_iff_zmod_eq_0)
    10.8 +  apply (simp add: dvd_eq_mod_eq_0)
    10.9  done
   10.10  
   10.11  
    11.1 --- a/src/HOL/Library/Pocklington.thy	Sat Feb 21 09:58:45 2009 +0100
    11.2 +++ b/src/HOL/Library/Pocklington.thy	Sat Feb 21 20:52:30 2009 +0100
    11.3 @@ -873,7 +873,7 @@
    11.4        from lh[unfolded nat_mod] 
    11.5        obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
    11.6        hence "a ^ d + n * q1 - n * q2 = 1" by simp
    11.7 -      with dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp 
    11.8 +      with nat_dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
    11.9        with p(3) have False by simp
   11.10        hence ?rhs ..}
   11.11      ultimately have ?rhs by blast}
    12.1 --- a/src/HOL/Library/Primes.thy	Sat Feb 21 09:58:45 2009 +0100
    12.2 +++ b/src/HOL/Library/Primes.thy	Sat Feb 21 20:52:30 2009 +0100
    12.3 @@ -307,8 +307,8 @@
    12.4    {fix e assume H: "e dvd a^n" "e dvd b^n"
    12.5      from bezout_gcd_pow[of a n b] obtain x y 
    12.6        where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
    12.7 -    from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
    12.8 -      dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
    12.9 +    from nat_dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
   12.10 +      nat_dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
   12.11      have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
   12.12    hence th:  "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
   12.13    from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
    13.1 --- a/src/HOL/NumberTheory/Chinese.thy	Sat Feb 21 09:58:45 2009 +0100
    13.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Sat Feb 21 20:52:30 2009 +0100
    13.3 @@ -90,10 +90,8 @@
    13.4      "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
    13.5    apply (induct l)
    13.6     apply auto
    13.7 -    apply (rule_tac [1] zdvd_zmult2)
    13.8 -    apply (rule_tac [2] zdvd_zmult)
    13.9 -    apply (subgoal_tac "i = Suc (k + l)")
   13.10 -    apply (simp_all (no_asm_simp))
   13.11 +  apply (subgoal_tac "i = Suc (k + l)")
   13.12 +   apply (simp_all (no_asm_simp))
   13.13    done
   13.14  
   13.15  lemma funsum_mod:
   13.16 @@ -196,8 +194,8 @@
   13.17     apply (case_tac [2] "i = n")
   13.18      apply (simp_all (no_asm_simp))
   13.19      apply (case_tac [3] "j < i")
   13.20 -     apply (rule_tac [3] zdvd_zmult2)
   13.21 -     apply (rule_tac [4] zdvd_zmult)
   13.22 +     apply (rule_tac [3] dvd_mult2)
   13.23 +     apply (rule_tac [4] dvd_mult)
   13.24       apply (rule_tac [!] funprod_zdvd)
   13.25       apply arith
   13.26       apply arith
   13.27 @@ -217,8 +215,8 @@
   13.28    apply (subst funsum_mod)
   13.29    apply (subst funsum_oneelem)
   13.30       apply auto
   13.31 -  apply (subst zdvd_iff_zmod_eq_0 [symmetric])
   13.32 -  apply (rule zdvd_zmult)
   13.33 +  apply (subst dvd_eq_mod_eq_0 [symmetric])
   13.34 +  apply (rule dvd_mult)
   13.35    apply (rule x_sol_lin_aux)
   13.36    apply auto
   13.37    done
    14.1 --- a/src/HOL/NumberTheory/Euler.thy	Sat Feb 21 09:58:45 2009 +0100
    14.2 +++ b/src/HOL/NumberTheory/Euler.thy	Sat Feb 21 20:52:30 2009 +0100
    14.3 @@ -272,7 +272,7 @@
    14.4  text {* \medskip Prove the final part of Euler's Criterion: *}
    14.5  
    14.6  lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
    14.7 -  by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div zdvd_trans)
    14.8 +  by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
    14.9  
   14.10  lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
   14.11    by (auto simp add: nat_mult_distrib)
    15.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Sat Feb 21 09:58:45 2009 +0100
    15.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Sat Feb 21 20:52:30 2009 +0100
    15.3 @@ -155,7 +155,7 @@
    15.4      prefer 2
    15.5      apply (subst zdvd_iff_zgcd [symmetric])
    15.6       apply (rule_tac [4] zgcd_zcong_zgcd)
    15.7 -       apply (simp_all add: zdvd_zminus_iff zcong_sym)
    15.8 +       apply (simp_all add: zcong_sym)
    15.9    done
   15.10  
   15.11  
    16.1 --- a/src/HOL/NumberTheory/Int2.thy	Sat Feb 21 09:58:45 2009 +0100
    16.2 +++ b/src/HOL/NumberTheory/Int2.thy	Sat Feb 21 20:52:30 2009 +0100
    16.3 @@ -18,7 +18,7 @@
    16.4  
    16.5  lemma zpower_zdvd_prop1:
    16.6    "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
    16.7 -  by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
    16.8 +  by (induct n) (auto simp add: dvd_mult2 [of p y])
    16.9  
   16.10  lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m"
   16.11  proof -
   16.12 @@ -42,7 +42,7 @@
   16.13     apply simp
   16.14    apply (frule zprime_zdvd_zmult_better)
   16.15     apply simp
   16.16 -  apply force
   16.17 +  apply (force simp del:dvd_mult)
   16.18    done
   16.19  
   16.20  lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
   16.21 @@ -86,7 +86,7 @@
   16.22    by (auto simp add: zcong_def)
   16.23  
   16.24  lemma zcong_id: "[m = 0] (mod m)"
   16.25 -  by (auto simp add: zcong_def zdvd_0_right)
   16.26 +  by (auto simp add: zcong_def)
   16.27  
   16.28  lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
   16.29    by (auto simp add: zcong_refl zcong_zadd)
    17.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Sat Feb 21 09:58:45 2009 +0100
    17.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Sat Feb 21 20:52:30 2009 +0100
    17.3 @@ -50,7 +50,7 @@
    17.4  
    17.5  lemma zrelprime_zdvd_zmult_aux:
    17.6       "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
    17.7 -    by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
    17.8 +    by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
    17.9  
   17.10  lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
   17.11    apply (case_tac "0 \<le> m")
   17.12 @@ -73,7 +73,7 @@
   17.13  lemma zprime_imp_zrelprime:
   17.14      "zprime p ==> \<not> p dvd n ==> zgcd n p = 1"
   17.15    apply (auto simp add: zprime_def)
   17.16 -  apply (metis zgcd_commute zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
   17.17 +  apply (metis zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
   17.18    done
   17.19  
   17.20  lemma zless_zprime_imp_zrelprime:
   17.21 @@ -93,9 +93,7 @@
   17.22    done
   17.23  
   17.24  lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
   17.25 -  apply (simp add: zgcd_greatest_iff)
   17.26 -  apply (blast intro: zdvd_trans dvd_triv_right)
   17.27 -  done
   17.28 +by (simp add: zgcd_greatest_iff)
   17.29  
   17.30  lemma zgcd_zmult_zdvd_zgcd:
   17.31      "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
   17.32 @@ -127,20 +125,20 @@
   17.33    by (unfold zcong_def, auto)
   17.34  
   17.35  lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)"
   17.36 -  unfolding zcong_def minus_diff_eq [of a, symmetric] zdvd_zminus_iff ..
   17.37 +  unfolding zcong_def minus_diff_eq [of a, symmetric] dvd_minus_iff ..
   17.38  
   17.39  lemma zcong_zadd:
   17.40      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)"
   17.41    apply (unfold zcong_def)
   17.42    apply (rule_tac s = "(a - b) + (c - d)" in subst)
   17.43 -   apply (rule_tac [2] zdvd_zadd, auto)
   17.44 +   apply (rule_tac [2] dvd_add, auto)
   17.45    done
   17.46  
   17.47  lemma zcong_zdiff:
   17.48      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a - c = b - d] (mod m)"
   17.49    apply (unfold zcong_def)
   17.50    apply (rule_tac s = "(a - b) - (c - d)" in subst)
   17.51 -   apply (rule_tac [2] zdvd_zdiff, auto)
   17.52 +   apply (rule_tac [2] dvd_diff, auto)
   17.53    done
   17.54  
   17.55  lemma zcong_trans:
   17.56 @@ -151,8 +149,8 @@
   17.57      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
   17.58    apply (rule_tac b = "b * c" in zcong_trans)
   17.59     apply (unfold zcong_def)
   17.60 -  apply (metis zdiff_zmult_distrib2 zdvd_zmult zmult_commute)
   17.61 -  apply (metis zdiff_zmult_distrib2 zdvd_zmult)
   17.62 +  apply (metis zdiff_zmult_distrib2 dvd_mult zmult_commute)
   17.63 +  apply (metis zdiff_zmult_distrib2 dvd_mult)
   17.64    done
   17.65  
   17.66  lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
   17.67 @@ -163,7 +161,7 @@
   17.68  
   17.69  lemma zcong_zmult_self: "[a * m = b * m] (mod m)"
   17.70    apply (unfold zcong_def)
   17.71 -  apply (rule zdvd_zdiff, simp_all)
   17.72 +  apply (rule dvd_diff, simp_all)
   17.73    done
   17.74  
   17.75  lemma zcong_square:
   17.76 @@ -191,7 +189,7 @@
   17.77       apply (simp_all add: zdiff_zmult_distrib)
   17.78    apply (subgoal_tac "m dvd (-(a * k - b * k))")
   17.79     apply simp
   17.80 -  apply (subst zdvd_zminus_iff, assumption)
   17.81 +  apply (subst dvd_minus_iff, assumption)
   17.82    done
   17.83  
   17.84  lemma zcong_cancel2:
   17.85 @@ -206,10 +204,10 @@
   17.86    apply (subgoal_tac "m dvd n * ka")
   17.87     apply (subgoal_tac "m dvd ka")
   17.88      apply (case_tac [2] "0 \<le> ka")
   17.89 -  apply (metis zdvd_mult_div_cancel zdvd_refl zdvd_zminus2_iff zdvd_zmultD2 zgcd_zminus zmult_commute zmult_zminus zrelprime_zdvd_zmult)
   17.90 -  apply (metis IntDiv.zdvd_abs1 abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
   17.91 -  apply (metis abs_eq_0 int_0_neq_1 mult_le_0_iff  zdvd_mono zdvd_mult_cancel zdvd_mult_cancel1 zdvd_refl zdvd_triv_left zdvd_zmult2 zero_le_mult_iff zgcd_greatest_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
   17.92 -  apply (metis zdvd_triv_left)
   17.93 +  apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
   17.94 +  apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
   17.95 +  apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
   17.96 +  apply (metis dvd_triv_left)
   17.97    done
   17.98  
   17.99  lemma zcong_zless_imp_eq:
  17.100 @@ -237,7 +235,7 @@
  17.101  lemma zcong_zless_0:
  17.102      "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
  17.103    apply (unfold zcong_def dvd_def, auto)
  17.104 -  apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id zle_refl zle_trans)
  17.105 +  apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
  17.106    done
  17.107  
  17.108  lemma zcong_zless_unique:
  17.109 @@ -403,7 +401,7 @@
  17.110     prefer 2
  17.111     apply simp
  17.112    apply (unfold zcong_def)
  17.113 -  apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff)
  17.114 +  apply (simp (no_asm) add: zmult_commute)
  17.115    done
  17.116  
  17.117  lemma zcong_lineq_unique:
    18.1 --- a/src/HOL/NumberTheory/Residues.thy	Sat Feb 21 09:58:45 2009 +0100
    18.2 +++ b/src/HOL/NumberTheory/Residues.thy	Sat Feb 21 20:52:30 2009 +0100
    18.3 @@ -48,7 +48,7 @@
    18.4    by (auto simp add: StandardRes_def zcong_zmod_eq)
    18.5  
    18.6  lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"
    18.7 -  by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
    18.8 +  by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_eq_0)
    18.9  
   18.10  lemma StandardRes_prop4: "2 < m 
   18.11       ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
    19.1 --- a/src/HOL/NumberTheory/WilsonBij.thy	Sat Feb 21 09:58:45 2009 +0100
    19.2 +++ b/src/HOL/NumberTheory/WilsonBij.thy	Sat Feb 21 20:52:30 2009 +0100
    19.3 @@ -57,7 +57,7 @@
    19.4     apply (rule_tac [2] zdvd_not_zless)
    19.5      apply (subgoal_tac "p dvd 1")
    19.6       prefer 2
    19.7 -     apply (subst zdvd_zminus_iff [symmetric])
    19.8 +     apply (subst dvd_minus_iff [symmetric])
    19.9       apply auto
   19.10    done
   19.11  
   19.12 @@ -79,7 +79,7 @@
   19.13    apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
   19.14    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   19.15     apply (simp add: mult_commute)
   19.16 -  apply (subst zdvd_zminus_iff)
   19.17 +  apply (subst dvd_minus_iff)
   19.18    apply (subst zdvd_reduce)
   19.19    apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
   19.20     apply (subst zdvd_reduce)
    20.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Sat Feb 21 09:58:45 2009 +0100
    20.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Sat Feb 21 20:52:30 2009 +0100
    20.3 @@ -68,7 +68,7 @@
    20.4     apply (rule_tac [2] zdvd_not_zless)
    20.5      apply (subgoal_tac "p dvd 1")
    20.6       prefer 2
    20.7 -     apply (subst zdvd_zminus_iff [symmetric], auto)
    20.8 +     apply (subst dvd_minus_iff [symmetric], auto)
    20.9    done
   20.10  
   20.11  lemma inv_not_1:
   20.12 @@ -87,7 +87,7 @@
   20.13    apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
   20.14    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   20.15     apply (simp add: mult_commute)
   20.16 -  apply (subst zdvd_zminus_iff)
   20.17 +  apply (subst dvd_minus_iff)
   20.18    apply (subst zdvd_reduce)
   20.19    apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
   20.20     apply (subst zdvd_reduce, auto)
    21.1 --- a/src/HOL/RealDef.thy	Sat Feb 21 09:58:45 2009 +0100
    21.2 +++ b/src/HOL/RealDef.thy	Sat Feb 21 20:52:30 2009 +0100
    21.3 @@ -655,7 +655,7 @@
    21.4      real(n div d) = real n / real d"
    21.5    apply (frule real_of_int_div_aux [of d n])
    21.6    apply simp
    21.7 -  apply (simp add: zdvd_iff_zmod_eq_0)
    21.8 +  apply (simp add: dvd_eq_mod_eq_0)
    21.9  done
   21.10  
   21.11  lemma real_of_int_div2:
    22.1 --- a/src/HOL/Ring_and_Field.thy	Sat Feb 21 09:58:45 2009 +0100
    22.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Feb 21 20:52:30 2009 +0100
    22.3 @@ -147,10 +147,10 @@
    22.4  lemma one_dvd [simp]: "1 dvd a"
    22.5  by (auto intro!: dvdI)
    22.6  
    22.7 -lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
    22.8 +lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
    22.9  by (auto intro!: mult_left_commute dvdI elim!: dvdE)
   22.10  
   22.11 -lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
   22.12 +lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   22.13    apply (subst mult_commute)
   22.14    apply (erule dvd_mult)
   22.15    done
   22.16 @@ -162,12 +162,12 @@
   22.17  by (rule dvd_mult2) (rule dvd_refl)
   22.18  
   22.19  lemma mult_dvd_mono:
   22.20 -  assumes ab: "a dvd b"
   22.21 -    and "cd": "c dvd d"
   22.22 +  assumes "a dvd b"
   22.23 +    and "c dvd d"
   22.24    shows "a * c dvd b * d"
   22.25  proof -
   22.26 -  from ab obtain b' where "b = a * b'" ..
   22.27 -  moreover from "cd" obtain d' where "d = c * d'" ..
   22.28 +  from `a dvd b` obtain b' where "b = a * b'" ..
   22.29 +  moreover from `c dvd d` obtain d' where "d = c * d'" ..
   22.30    ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   22.31    then show ?thesis ..
   22.32  qed
   22.33 @@ -310,8 +310,8 @@
   22.34    then show "- x dvd y" ..
   22.35  qed
   22.36  
   22.37 -lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   22.38 -by (simp add: diff_minus dvd_add dvd_minus_iff)
   22.39 +lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   22.40 +by (simp add: diff_minus dvd_minus_iff)
   22.41  
   22.42  end
   22.43  
    23.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Sat Feb 21 09:58:45 2009 +0100
    23.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sat Feb 21 20:52:30 2009 +0100
    23.3 @@ -122,7 +122,7 @@
    23.4    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    23.5  val div_mod_ss = HOL_basic_ss addsimps simp_thms 
    23.6    @ map (symmetric o mk_meta_eq) 
    23.7 -    [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, 
    23.8 +    [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add1_eq"}, 
    23.9       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
   23.10       @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   23.11    @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
    24.1 --- a/src/HOL/Word/Num_Lemmas.thy	Sat Feb 21 09:58:45 2009 +0100
    24.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Sat Feb 21 20:52:30 2009 +0100
    24.3 @@ -314,7 +314,7 @@
    24.4    "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
    24.5    apply clarsimp
    24.6    apply safe
    24.7 -   apply (simp add: zdvd_iff_zmod_eq_0 [symmetric])
    24.8 +   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
    24.9     apply (drule le_iff_add [THEN iffD1])
   24.10     apply (force simp: zpower_zadd_distrib)
   24.11    apply (rule mod_pos_pos_trivial)
    25.1 --- a/src/HOL/Word/WordShift.thy	Sat Feb 21 09:58:45 2009 +0100
    25.2 +++ b/src/HOL/Word/WordShift.thy	Sat Feb 21 20:52:30 2009 +0100
    25.3 @@ -530,7 +530,7 @@
    25.4    done
    25.5  
    25.6  lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
    25.7 -  apply (simp add: zdvd_iff_zmod_eq_0 and_mask_mod_2p)
    25.8 +  apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
    25.9    apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
   25.10    apply (subst word_uint.norm_Rep [symmetric])
   25.11    apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)