src/HOL/IntDiv.thy
changeset 25942 a52309ac4a4d
parent 25919 8b1c0d434824
child 25961 ec39d7e40554
     1.1 --- a/src/HOL/IntDiv.thy	Tue Jan 22 23:06:58 2008 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Jan 22 23:07:21 2008 +0100
     1.3 @@ -712,6 +712,7 @@
     1.4  apply (erule subst, simp_all)
     1.5  done
     1.6  
     1.7 +
     1.8  subsection{*More Algebraic Laws for div and mod*}
     1.9  
    1.10  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
    1.11 @@ -746,6 +747,9 @@
    1.12  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
    1.13  by (simp add: zdiv_zmult1_eq)
    1.14  
    1.15 +instance int :: semiring_div
    1.16 +  by intro_classes auto
    1.17 +
    1.18  lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
    1.19  by (subst mult_commute, erule zdiv_zmult_self1)
    1.20  
    1.21 @@ -1053,7 +1057,6 @@
    1.22         simp) 
    1.23  done
    1.24  
    1.25 -
    1.26  (*Not clear why this must be proved separately; probably number_of causes
    1.27    simplification problems*)
    1.28  lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
    1.29 @@ -1152,9 +1155,6 @@
    1.30  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
    1.31    by (simp add: dvd_def zmod_eq_0_iff)
    1.32  
    1.33 -instance int :: dvd_mod
    1.34 -  by default (simp add: zdvd_iff_zmod_eq_0)
    1.35 -
    1.36  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    1.37    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
    1.38