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.35      by (simp add: algebra_simps)
    1.36    then show "a = b \<or> a = - b"
    1.37 -    by (simp add: right_minus_eq eq_neg_iff_add_eq_0)
    1.38 +    by (simp add: eq_neg_iff_add_eq_0)
    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.63 -    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric]
    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.68 +    (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
    1.69 +     auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
    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 ==>