# HG changeset patch
# User huffman
# Date 1234896775 28800
# Node ID a70bc5190534a3d798741afac2e24898059bd448
# Parent  32db776159150f1267910f96f4a6ef03eae97ff0# Parent  cdf12a1cb96389079a11ca3e8b699403957565fc
merged

diff -r cdf12a1cb963 -r a70bc5190534 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Feb 17 18:48:17 2009 +0100
+++ b/src/HOL/IntDiv.thy	Tue Feb 17 10:52:55 2009 -0800
@@ -1147,23 +1147,23 @@
 lemma zdvd_1_left: "1 dvd (m::int)"
   by (rule one_dvd) (* already declared [simp] *)
 
-lemma zdvd_refl [simp]: "m dvd (m::int)"
-  by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
+lemma zdvd_refl: "m dvd (m::int)"
+  by (rule dvd_refl) (* already declared [simp] *)
 
 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
   by (rule dvd_trans)
 
-lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
-  by (rule dvd_minus_iff)
+lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
+  by (rule dvd_minus_iff) (* already declared [simp] *)
 
-lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
-  by (rule minus_dvd_iff)
+lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
+  by (rule minus_dvd_iff) (* already declared [simp] *)
 
-lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
-  by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
+lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
+  by (rule abs_dvd_iff) (* already declared [simp] *)
 
-lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
-  by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
+lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
+  by (rule dvd_abs_iff) (* already declared [simp] *)
 
 lemma zdvd_anti_sym:
     "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
diff -r cdf12a1cb963 -r a70bc5190534 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Feb 17 18:48:17 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Feb 17 10:52:55 2009 -0800
@@ -1100,32 +1100,11 @@
   "sgn a < 0 \<longleftrightarrow> a < 0"
   unfolding sgn_if by auto
 
-(* The int instances are proved, these generic ones are tedious to prove here.
-And not very useful, as int seems to be the only instance.
-If needed, they should be proved later, when metis is available.
-lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
-proof-
-  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
-    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
-  moreover
-  have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
-    by(auto intro!: minus_minus[symmetric]
-         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
-  ultimately show ?thesis by (auto simp: abs_if dvd_def)
-qed
-
-lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
-proof-
-  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
-    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
-  moreover
-  have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
-    by(auto intro!: minus_minus
-         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
-  ultimately show ?thesis
-    by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
-qed
-*)
+lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
+  by (simp add: abs_if)
+
+lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
+  by (simp add: abs_if)
 
 end