src/HOL/Algebra/IntRing.thy
changeset 33657 a4179bf442d1
parent 32480 6c19da8e661a
child 33676 802f5e233e48
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 14:14:04 2009 +0100
     1.3 @@ -12,26 +12,6 @@
     1.4  
     1.5  subsection {* Some properties of @{typ int} *}
     1.6  
     1.7 -lemma dvds_imp_abseq:
     1.8 -  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
     1.9 -apply (subst abs_split, rule conjI)
    1.10 - apply (clarsimp, subst abs_split, rule conjI)
    1.11 -  apply (clarsimp)
    1.12 -  apply (cases "k=0", simp)
    1.13 -  apply (cases "l=0", simp)
    1.14 -  apply (simp add: zdvd_anti_sym)
    1.15 - apply clarsimp
    1.16 - apply (cases "k=0", simp)
    1.17 - apply (simp add: zdvd_anti_sym)
    1.18 -apply (clarsimp, subst abs_split, rule conjI)
    1.19 - apply (clarsimp)
    1.20 - apply (cases "l=0", simp)
    1.21 - apply (simp add: zdvd_anti_sym)
    1.22 -apply (clarsimp)
    1.23 -apply (subgoal_tac "-l = -k", simp)
    1.24 -apply (intro zdvd_anti_sym, simp+)
    1.25 -done
    1.26 -
    1.27  lemma abseq_imp_dvd:
    1.28    assumes a_lk: "abs l = abs (k::int)"
    1.29    shows "l dvd k"
    1.30 @@ -55,7 +35,7 @@
    1.31  lemma dvds_eq_abseq:
    1.32    "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
    1.33  apply rule
    1.34 - apply (simp add: dvds_imp_abseq)
    1.35 + apply (simp add: zdvd_antisym_abs)
    1.36  apply (rule conjI)
    1.37   apply (simp add: abseq_imp_dvd)+
    1.38  done