src/HOL/Algebra/IntRing.thy
changeset 33657 a4179bf442d1
parent 32480 6c19da8e661a
child 33676 802f5e233e48
--- 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:
-  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> 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 \<and> 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