src/HOL/Rings.thy
 changeset 35216 7641e8d831d2 parent 35097 4554bb2abfa3 child 35302 4bc6b4d70e08
```     1.1 --- a/src/HOL/Rings.thy	Thu Feb 18 13:29:59 2010 -0800
1.2 +++ b/src/HOL/Rings.thy	Thu Feb 18 14:21:44 2010 -0800
1.3 @@ -315,7 +315,7 @@
1.4  qed
1.5
1.6  lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
1.7 -by (simp add: diff_minus dvd_minus_iff)
1.8 +by (simp only: diff_minus dvd_add dvd_minus_iff)
1.9
1.10  end
1.11
1.12 @@ -336,16 +336,16 @@
1.13    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
1.14  proof -
1.15    have "(a * c = b * c) = ((a - b) * c = 0)"
1.16 -    by (simp add: algebra_simps right_minus_eq)
1.17 -  thus ?thesis by (simp add: disj_commute right_minus_eq)
1.18 +    by (simp add: algebra_simps)
1.19 +  thus ?thesis by (simp add: disj_commute)
1.20  qed
1.21
1.22  lemma mult_cancel_left [simp, noatp]:
1.23    "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
1.24  proof -
1.25    have "(c * a = c * b) = (c * (a - b) = 0)"
1.26 -    by (simp add: algebra_simps right_minus_eq)
1.27 -  thus ?thesis by (simp add: right_minus_eq)
1.28 +    by (simp add: algebra_simps)
1.29 +  thus ?thesis by simp
1.30  qed
1.31
1.32  end
1.33 @@ -382,7 +382,7 @@
1.34    then have "(a - b) * (a + b) = 0"
1.36    then show "a = b \<or> a = - b"
1.39  next
1.40    assume "a = b \<or> a = - b"
1.41    then show "a * a = b * b" by auto
1.42 @@ -764,13 +764,13 @@
1.43  lemma mult_left_mono_neg:
1.44    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
1.45    apply (drule mult_left_mono [of _ _ "uminus c"])
1.46 -  apply (simp_all add: minus_mult_left [symmetric])
1.47 +  apply simp_all
1.48    done
1.49
1.50  lemma mult_right_mono_neg:
1.51    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
1.52    apply (drule mult_right_mono [of _ _ "uminus c"])
1.53 -  apply (simp_all add: minus_mult_right [symmetric])
1.54 +  apply simp_all
1.55    done
1.56
1.57  lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
1.58 @@ -791,11 +791,10 @@
1.59  proof
1.60    fix a b
1.61    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1.62 -    by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
1.64 -     neg_less_eq_nonneg less_eq_neg_nonpos, auto intro: add_nonneg_nonneg,
1.65 -      auto intro!: less_imp_le add_neg_neg)
1.66 -qed (auto simp add: abs_if less_eq_neg_nonpos neg_equal_zero)
1.67 +    by (auto simp add: abs_if not_less)
1.70 +qed (auto simp add: abs_if)
1.71
1.72  end
1.73
1.74 @@ -864,14 +863,14 @@
1.75
1.76  lemma mult_less_0_iff:
1.77    "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
1.78 -  apply (insert zero_less_mult_iff [of "-a" b])
1.79 -  apply (force simp add: minus_mult_left[symmetric])
1.80 +  apply (insert zero_less_mult_iff [of "-a" b])
1.81 +  apply force
1.82    done
1.83
1.84  lemma mult_le_0_iff:
1.85    "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
1.86    apply (insert zero_le_mult_iff [of "-a" b])
1.87 -  apply (force simp add: minus_mult_left[symmetric])
1.88 +  apply force
1.89    done
1.90
1.91  lemma zero_le_square [simp]: "0 \<le> a * a"
1.92 @@ -1056,11 +1055,11 @@
1.93
1.94  lemma sgn_1_pos:
1.95    "sgn a = 1 \<longleftrightarrow> a > 0"
1.96 -unfolding sgn_if by (simp add: neg_equal_zero)
1.97 +unfolding sgn_if by simp
1.98
1.99  lemma sgn_1_neg:
1.100    "sgn a = - 1 \<longleftrightarrow> a < 0"
1.101 -unfolding sgn_if by (auto simp add: equal_neg_zero)
1.102 +unfolding sgn_if by auto
1.103
1.104  lemma sgn_pos [simp]:
1.105    "0 < a \<Longrightarrow> sgn a = 1"
1.106 @@ -1116,11 +1115,11 @@
1.107
1.108  lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
1.109      ==> x * y <= x"
1.110 -by (auto simp add: mult_compare_simps)
1.111 +by (auto simp add: mult_le_cancel_left2)
1.112
1.113  lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
1.114      ==> y * x <= x"
1.115 -by (auto simp add: mult_compare_simps)
1.116 +by (auto simp add: mult_le_cancel_right2)
1.117
1.118  context linordered_semidom
1.119  begin
1.120 @@ -1159,7 +1158,7 @@
1.121  begin
1.122
1.123  subclass ordered_ring_abs proof
1.124 -qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
1.125 +qed (auto simp add: abs_if not_less mult_less_0_iff)
1.126
1.127  lemma abs_mult:
1.128    "abs (a * b) = abs a * abs b"
1.129 @@ -1187,7 +1186,7 @@
1.130
1.131  lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))"
1.132  apply (simp add: order_less_le abs_le_iff)
1.133 -apply (auto simp add: abs_if neg_less_eq_nonneg less_eq_neg_nonpos)
1.134 +apply (auto simp add: abs_if)
1.135  done
1.136
1.137  lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==>
```