diff -r 555e5358b8c9 -r a4179bf442d1 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Thu Nov 12 14:32:21 2009 -0800 +++ b/src/HOL/Algebra/IntRing.thy Fri Nov 13 14:14:04 2009 +0100 @@ -12,26 +12,6 @@ subsection {* Some properties of @{typ int} *} -lemma dvds_imp_abseq: - "\l dvd k; k dvd l\ \ abs l = abs (k::int)" -apply (subst abs_split, rule conjI) - apply (clarsimp, subst abs_split, rule conjI) - apply (clarsimp) - apply (cases "k=0", simp) - apply (cases "l=0", simp) - apply (simp add: zdvd_anti_sym) - apply clarsimp - apply (cases "k=0", simp) - apply (simp add: zdvd_anti_sym) -apply (clarsimp, subst abs_split, rule conjI) - apply (clarsimp) - apply (cases "l=0", simp) - apply (simp add: zdvd_anti_sym) -apply (clarsimp) -apply (subgoal_tac "-l = -k", simp) -apply (intro zdvd_anti_sym, simp+) -done - lemma abseq_imp_dvd: assumes a_lk: "abs l = abs (k::int)" shows "l dvd k" @@ -55,7 +35,7 @@ lemma dvds_eq_abseq: "(l dvd k \ k dvd l) = (abs l = abs (k::int))" apply rule - apply (simp add: dvds_imp_abseq) + apply (simp add: zdvd_antisym_abs) apply (rule conjI) apply (simp add: abseq_imp_dvd)+ done