# 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 "\ka. - (l * k) = l * ka" by fast - qed -qed - lemma dvds_eq_abseq: "(l dvd k \ 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) \ m dvd k" by (simp add: abs_if) +lemma dvd_if_abs_eq: + "abs l = abs (k) \ l dvd k" +by(subst abs_dvd_iff[symmetric]) simp + end class ordered_field = field + ordered_idom