src/HOL/Rings.thy
changeset 36348 89c54f51f55a
parent 36304 6984744e6b34
child 36622 e393a91f86df
     1.1 --- a/src/HOL/Rings.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Apr 26 11:34:15 2010 +0200
     1.3 @@ -14,8 +14,8 @@
     1.4  begin
     1.5  
     1.6  class semiring = ab_semigroup_add + semigroup_mult +
     1.7 -  assumes left_distrib[algebra_simps]: "(a + b) * c = a * c + b * c"
     1.8 -  assumes right_distrib[algebra_simps]: "a * (b + c) = a * b + a * c"
     1.9 +  assumes left_distrib[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
    1.10 +  assumes right_distrib[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
    1.11  begin
    1.12  
    1.13  text{*For the @{text combine_numerals} simproc*}
    1.14 @@ -230,18 +230,15 @@
    1.15  lemma minus_mult_commute: "- a * b = a * - b"
    1.16  by simp
    1.17  
    1.18 -lemma right_diff_distrib[algebra_simps]: "a * (b - c) = a * b - a * c"
    1.19 +lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
    1.20  by (simp add: right_distrib diff_minus)
    1.21  
    1.22 -lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
    1.23 +lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
    1.24  by (simp add: left_distrib diff_minus)
    1.25  
    1.26  lemmas ring_distribs[no_atp] =
    1.27    right_distrib left_distrib left_diff_distrib right_diff_distrib
    1.28  
    1.29 -text{*Legacy - use @{text algebra_simps} *}
    1.30 -lemmas ring_simps[no_atp] = algebra_simps
    1.31 -
    1.32  lemma eq_add_iff1:
    1.33    "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
    1.34  by (simp add: algebra_simps)
    1.35 @@ -536,7 +533,7 @@
    1.36  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    1.37    by (simp add: diff_minus add_divide_distrib)
    1.38  
    1.39 -lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
    1.40 +lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
    1.41  proof -
    1.42    assume [simp]: "c \<noteq> 0"
    1.43    have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
    1.44 @@ -544,7 +541,7 @@
    1.45    finally show ?thesis .
    1.46  qed
    1.47  
    1.48 -lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
    1.49 +lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
    1.50  proof -
    1.51    assume [simp]: "c \<noteq> 0"
    1.52    have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
    1.53 @@ -560,7 +557,7 @@
    1.54  
    1.55  end
    1.56  
    1.57 -class division_by_zero = division_ring +
    1.58 +class division_ring_inverse_zero = division_ring +
    1.59    assumes inverse_zero [simp]: "inverse 0 = 0"
    1.60  begin
    1.61  
    1.62 @@ -861,9 +858,6 @@
    1.63  
    1.64  subclass ordered_ab_group_add ..
    1.65  
    1.66 -text{*Legacy - use @{text algebra_simps} *}
    1.67 -lemmas ring_simps[no_atp] = algebra_simps
    1.68 -
    1.69  lemma less_add_iff1:
    1.70    "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
    1.71  by (simp add: algebra_simps)
    1.72 @@ -1068,9 +1062,6 @@
    1.73  
    1.74  end
    1.75  
    1.76 -text{*Legacy - use @{text algebra_simps} *}
    1.77 -lemmas ring_simps[no_atp] = algebra_simps
    1.78 -
    1.79  lemmas mult_sign_intros =
    1.80    mult_nonneg_nonneg mult_nonneg_nonpos
    1.81    mult_nonpos_nonneg mult_nonpos_nonpos