# HG changeset patch
# User nipkow
# Date 1258146061 -3600
# Node ID 802f5e233e48cacbf0d576ec2664c71795f6da81
# Parent  5241785055bc73117e72dec8cb13f70426480246
moved lemma from Algebra/IntRing to Ring_and_Field

diff -r 5241785055bc -r 802f5e233e48 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 22:01:01 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 5241785055bc -r 802f5e233e48 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Nov 13 22:01:01 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