1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jan 30 13:41:45 2009 +0000
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jan 31 09:04:16 2009 +0100
     1.3 @@ -1053,26 +1053,53 @@
     1.4  
     1.5  lemma sgn_sgn [simp]:
     1.6    "sgn (sgn a) = sgn a"
     1.7 -  unfolding sgn_if by simp
     1.8 +unfolding sgn_if by simp
     1.9  
    1.10  lemma sgn_0_0:
    1.11    "sgn a = 0 \<longleftrightarrow> a = 0"
    1.12 -  unfolding sgn_if by simp
    1.13 +unfolding sgn_if by simp
    1.14  
    1.15  lemma sgn_1_pos:
    1.16    "sgn a = 1 \<longleftrightarrow> a > 0"
    1.17 -  unfolding sgn_if by (simp add: neg_equal_zero)
    1.18 +unfolding sgn_if by (simp add: neg_equal_zero)
    1.19  
    1.20  lemma sgn_1_neg:
    1.21    "sgn a = - 1 \<longleftrightarrow> a < 0"
    1.22 -  unfolding sgn_if by (auto simp add: equal_neg_zero)
    1.23 +unfolding sgn_if by (auto simp add: equal_neg_zero)
    1.24  
    1.25  lemma sgn_times:
    1.26    "sgn (a * b) = sgn a * sgn b"
    1.27  by (auto simp add: sgn_if zero_less_mult_iff)
    1.28  
    1.29  lemma abs_sgn: "abs k = k * sgn k"
    1.30 -  unfolding sgn_if abs_if by auto
    1.31 +unfolding sgn_if abs_if by auto
    1.32 +
    1.33 +(* The int instances are proved, these generic ones are tedious to prove here.
    1.34 +And not very useful, as int seems to be the only instance.
    1.35 +If needed, they should be proved later, when metis is available.
    1.36 +lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
    1.37 +proof-
    1.38 +  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
    1.39 +    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
    1.40 +  moreover
    1.41 +  have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
    1.42 +    by(auto intro!: minus_minus[symmetric]
    1.43 +         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
    1.44 +  ultimately show ?thesis by (auto simp: abs_if dvd_def)
    1.45 +qed
    1.46 +
    1.47 +lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
    1.48 +proof-
    1.49 +  have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
    1.50 +    by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
    1.51 +  moreover
    1.52 +  have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
    1.53 +    by(auto intro!: minus_minus
    1.54 +         simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
    1.55 +  ultimately show ?thesis
    1.56 +    by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
    1.57 +qed
    1.58 +*)
    1.59  
    1.60  end
    1.61