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.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
```