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.33    "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
1.35 @@ -536,7 +533,7 @@
1.36  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
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.65
1.66 -text{*Legacy - use @{text algebra_simps} *}
1.67 -lemmas ring_simps[no_atp] = algebra_simps
1.68 -