diff -r 0929d6d08dd3 -r a52309ac4a4d src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Tue Jan 22 23:06:58 2008 +0100 +++ b/src/HOL/IntDiv.thy Tue Jan 22 23:07:21 2008 +0100 @@ -712,6 +712,7 @@ apply (erule subst, simp_all) done + subsection{*More Algebraic Laws for div and mod*} text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} @@ -746,6 +747,9 @@ lemma zdiv_zmult_self1 [simp]: "b \ (0::int) ==> (a*b) div b = a" by (simp add: zdiv_zmult1_eq) +instance int :: semiring_div + by intro_classes auto + lemma zdiv_zmult_self2 [simp]: "b \ (0::int) ==> (b*a) div b = a" by (subst mult_commute, erule zdiv_zmult_self1) @@ -1053,7 +1057,6 @@ simp) done - (*Not clear why this must be proved separately; probably number_of causes simplification problems*) lemma not_0_le_lemma: "~ 0 \ x ==> x \ (0::int)" @@ -1152,9 +1155,6 @@ lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" by (simp add: dvd_def zmod_eq_0_iff) -instance int :: dvd_mod - by default (simp add: zdvd_iff_zmod_eq_0) - lemmas zdvd_iff_zmod_eq_0_number_of [simp] = zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]