src/HOL/Rings.thy
changeset 70347 e5cd5471c18a
parent 70176 330382e284a4
     1.1 --- a/src/HOL/Rings.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Rings.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -16,8 +16,8 @@
     1.4  subsection \<open>Semirings and rings\<close>
     1.5  
     1.6  class semiring = ab_semigroup_add + semigroup_mult +
     1.7 -  assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
     1.8 -  assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
     1.9 +  assumes distrib_right [algebra_simps]: "(a + b) * c = a * c + b * c"
    1.10 +  assumes distrib_left [algebra_simps]: "a * (b + c) = a * b + a * c"
    1.11  begin
    1.12  
    1.13  text \<open>For the \<open>combine_numerals\<close> simproc\<close>
    1.14 @@ -2176,17 +2176,17 @@
    1.15      by (simp add: neq_iff)
    1.16  qed
    1.17  
    1.18 -lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    1.19 +lemma zero_less_mult_iff [sign_simps]: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    1.20    by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
    1.21       (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
    1.22  
    1.23 -lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
    1.24 +lemma zero_le_mult_iff [sign_simps]: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
    1.25    by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
    1.26  
    1.27 -lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
    1.28 +lemma mult_less_0_iff [sign_simps]: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
    1.29    using zero_less_mult_iff [of "- a" b] by auto
    1.30  
    1.31 -lemma mult_le_0_iff: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
    1.32 +lemma mult_le_0_iff [sign_simps]: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
    1.33    using zero_le_mult_iff [of "- a" b] by auto
    1.34  
    1.35  text \<open>