moved lemma from Algebra/IntRing to Ring_and_Field
authornipkow
Fri Nov 13 22:01:01 2009 +0100 (2009-11-13)
changeset 33676802f5e233e48
parent 33674 5241785055bc
child 33677 ade8e136efb4
moved lemma from Algebra/IntRing to Ring_and_Field
src/HOL/Algebra/IntRing.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Nov 13 19:49:13 2009 +0100
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 22:01:01 2009 +0100
     1.3 @@ -12,32 +12,11 @@
     1.4  
     1.5  subsection {* Some properties of @{typ int} *}
     1.6  
     1.7 -lemma abseq_imp_dvd:
     1.8 -  assumes a_lk: "abs l = abs (k::int)"
     1.9 -  shows "l dvd k"
    1.10 -proof -
    1.11 -  from a_lk
    1.12 -      have "nat (abs l) = nat (abs k)" by simp
    1.13 -  hence "nat (abs l) dvd nat (abs k)" by simp
    1.14 -  hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
    1.15 -  hence "abs l dvd k" by simp
    1.16 -  thus "l dvd k" 
    1.17 -  apply (unfold dvd_def, cases "l<0")
    1.18 -   defer 1 apply clarsimp
    1.19 -  proof (clarsimp)
    1.20 -    fix k
    1.21 -    assume l0: "l < 0"
    1.22 -    have "- (l * k) = l * (-k)" by simp
    1.23 -    thus "\<exists>ka. - (l * k) = l * ka" by fast
    1.24 -  qed
    1.25 -qed
    1.26 -
    1.27  lemma dvds_eq_abseq:
    1.28    "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
    1.29  apply rule
    1.30   apply (simp add: zdvd_antisym_abs)
    1.31 -apply (rule conjI)
    1.32 - apply (simp add: abseq_imp_dvd)+
    1.33 +apply (simp add: dvd_if_abs_eq)
    1.34  done
    1.35  
    1.36  
     2.1 --- a/src/HOL/Ring_and_Field.thy	Fri Nov 13 19:49:13 2009 +0100
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Nov 13 22:01:01 2009 +0100
     2.3 @@ -1301,6 +1301,10 @@
     2.4  lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
     2.5    by (simp add: abs_if)
     2.6  
     2.7 +lemma dvd_if_abs_eq:
     2.8 +  "abs l = abs (k) \<Longrightarrow> l dvd k"
     2.9 +by(subst abs_dvd_iff[symmetric]) simp
    2.10 +
    2.11  end
    2.12  
    2.13  class ordered_field = field + ordered_idom