# HG changeset patch
# User huffman
# Date 1234882773 28800
# Node ID 20a506b8256d84333f2e2d0623a3e329c641b9a2
# Parent  0a51765d2084067b97deb094ce10881988d52c55
lemmas abs_dvd_iff, dvd_abs_iff

diff -r 0a51765d2084 -r 20a506b8256d src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Tue Feb 17 06:59:33 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