# HG changeset patch
# User nipkow
# Date 1258146080 -3600
# Node ID ade8e136efb4efc8cc597e7f017a9d6a818822ad
# Parent  2582cc24bc2a94e4ae8f885d883fb10b084ef23c# Parent  802f5e233e48cacbf0d576ec2664c71795f6da81
merged

diff -r 2582cc24bc2a -r ade8e136efb4 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Nov 13 21:26:09 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 22:01:20 2009 +0100
@@ -12,32 +12,11 @@
 
 subsection {* Some properties of @{typ int} *}
 
-lemma abseq_imp_dvd:
-  assumes a_lk: "abs l = abs (k::int)"
-  shows "l dvd k"
-proof -
-  from a_lk
-      have "nat (abs l) = nat (abs k)" by simp
-  hence "nat (abs l) dvd nat (abs k)" by simp
-  hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
-  hence "abs l dvd k" by simp
-  thus "l dvd k" 
-  apply (unfold dvd_def, cases "l<0")
-   defer 1 apply clarsimp
-  proof (clarsimp)
-    fix k
-    assume l0: "l < 0"
-    have "- (l * k) = l * (-k)" by simp
-    thus "\<exists>ka. - (l * k) = l * ka" by fast
-  qed
-qed
-
 lemma dvds_eq_abseq:
   "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
 apply rule
  apply (simp add: zdvd_antisym_abs)
-apply (rule conjI)
- apply (simp add: abseq_imp_dvd)+
+apply (simp add: dvd_if_abs_eq)
 done
 
 
diff -r 2582cc24bc2a -r ade8e136efb4 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Nov 13 21:26:09 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Nov 13 22:01:20 2009 +0100
@@ -1301,6 +1301,10 @@
 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)
 
+lemma dvd_if_abs_eq:
+  "abs l = abs (k) \<Longrightarrow> l dvd k"
+by(subst abs_dvd_iff[symmetric]) simp
+
 end
 
 class ordered_field = field + ordered_idom