lemmas abs_dvd_iff, dvd_abs_iff
authorhuffman
Tue Feb 17 06:59:33 2009 -0800 (2009-02-17)
changeset 2994920a506b8256d
parent 29947 0a51765d2084
child 29950 32db77615915
lemmas abs_dvd_iff, dvd_abs_iff
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Feb 16 19:35:52 2009 -0800
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Feb 17 06:59:33 2009 -0800
     1.3 @@ -1100,32 +1100,11 @@
     1.4    "sgn a < 0 \<longleftrightarrow> a < 0"
     1.5    unfolding sgn_if by auto
     1.6  
     1.7 -(* The int instances are proved, these generic ones are tedious to prove here.
     1.8 -And not very useful, as int seems to be the only instance.
     1.9 -If needed, they should be proved later, when metis is available.
    1.10 -lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
    1.11 -proof-
    1.12 -  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
    1.13 -    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
    1.14 -  moreover
    1.15 -  have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
    1.16 -    by(auto intro!: minus_minus[symmetric]
    1.17 -         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
    1.18 -  ultimately show ?thesis by (auto simp: abs_if dvd_def)
    1.19 -qed
    1.20 -
    1.21 -lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
    1.22 -proof-
    1.23 -  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
    1.24 -    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
    1.25 -  moreover
    1.26 -  have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
    1.27 -    by(auto intro!: minus_minus
    1.28 -         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
    1.29 -  ultimately show ?thesis
    1.30 -    by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
    1.31 -qed
    1.32 -*)
    1.33 +lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
    1.34 +  by (simp add: abs_if)
    1.35 +
    1.36 +lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
    1.37 +  by (simp add: abs_if)
    1.38  
    1.39  end
    1.40