src/HOL/Rings.thy
changeset 35828 46cfc4b8112e
parent 35631 0b8a5fd339ab
child 36301 72f4d079ebf8
     1.1 --- a/src/HOL/Rings.thy	Wed Mar 17 19:37:44 2010 +0100
     1.2 +++ b/src/HOL/Rings.thy	Thu Mar 18 12:58:52 2010 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4    then show ?thesis ..
     1.5  qed
     1.6  
     1.7 -lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
     1.8 +lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
     1.9  by (auto intro: dvd_refl elim!: dvdE)
    1.10  
    1.11  lemma dvd_0_right [iff]: "a dvd 0"
    1.12 @@ -221,8 +221,8 @@
    1.13  by (rule minus_unique) (simp add: right_distrib [symmetric]) 
    1.14  
    1.15  text{*Extract signs from products*}
    1.16 -lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
    1.17 -lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
    1.18 +lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
    1.19 +lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
    1.20  
    1.21  lemma minus_mult_minus [simp]: "- a * - b = a * b"
    1.22  by simp
    1.23 @@ -236,11 +236,11 @@
    1.24  lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
    1.25  by (simp add: left_distrib diff_minus)
    1.26  
    1.27 -lemmas ring_distribs[noatp] =
    1.28 +lemmas ring_distribs[no_atp] =
    1.29    right_distrib left_distrib left_diff_distrib right_diff_distrib
    1.30  
    1.31  text{*Legacy - use @{text algebra_simps} *}
    1.32 -lemmas ring_simps[noatp] = algebra_simps
    1.33 +lemmas ring_simps[no_atp] = algebra_simps
    1.34  
    1.35  lemma eq_add_iff1:
    1.36    "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
    1.37 @@ -252,7 +252,7 @@
    1.38  
    1.39  end
    1.40  
    1.41 -lemmas ring_distribs[noatp] =
    1.42 +lemmas ring_distribs[no_atp] =
    1.43    right_distrib left_distrib left_diff_distrib right_diff_distrib
    1.44  
    1.45  class comm_ring = comm_semiring + ab_group_add
    1.46 @@ -319,7 +319,7 @@
    1.47  qed
    1.48  
    1.49  text{*Cancellation of equalities with a common factor*}
    1.50 -lemma mult_cancel_right [simp, noatp]:
    1.51 +lemma mult_cancel_right [simp, no_atp]:
    1.52    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
    1.53  proof -
    1.54    have "(a * c = b * c) = ((a - b) * c = 0)"
    1.55 @@ -327,7 +327,7 @@
    1.56    thus ?thesis by (simp add: disj_commute)
    1.57  qed
    1.58  
    1.59 -lemma mult_cancel_left [simp, noatp]:
    1.60 +lemma mult_cancel_left [simp, no_atp]:
    1.61    "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
    1.62  proof -
    1.63    have "(c * a = c * b) = (c * (a - b) = 0)"
    1.64 @@ -743,7 +743,7 @@
    1.65  subclass ordered_ab_group_add ..
    1.66  
    1.67  text{*Legacy - use @{text algebra_simps} *}
    1.68 -lemmas ring_simps[noatp] = algebra_simps
    1.69 +lemmas ring_simps[no_atp] = algebra_simps
    1.70  
    1.71  lemma less_add_iff1:
    1.72    "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
    1.73 @@ -950,7 +950,7 @@
    1.74  end
    1.75  
    1.76  text{*Legacy - use @{text algebra_simps} *}
    1.77 -lemmas ring_simps[noatp] = algebra_simps
    1.78 +lemmas ring_simps[no_atp] = algebra_simps
    1.79  
    1.80  lemmas mult_sign_intros =
    1.81    mult_nonneg_nonneg mult_nonneg_nonpos
    1.82 @@ -1099,7 +1099,7 @@
    1.83  
    1.84  text {* Simprules for comparisons where common factors can be cancelled. *}
    1.85  
    1.86 -lemmas mult_compare_simps[noatp] =
    1.87 +lemmas mult_compare_simps[no_atp] =
    1.88      mult_le_cancel_right mult_le_cancel_left
    1.89      mult_le_cancel_right1 mult_le_cancel_right2
    1.90      mult_le_cancel_left1 mult_le_cancel_left2
    1.91 @@ -1180,7 +1180,7 @@
    1.92    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
    1.93  qed
    1.94  
    1.95 -lemmas eq_minus_self_iff[noatp] = equal_neg_zero
    1.96 +lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
    1.97  
    1.98  lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
    1.99    unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..