src/HOL/Rings.thy

 begin
 
 subsection \<open>Semirings and rings\<close>
 
 class semiring = ab_semigroup_add + semigroup_mult +
-  assumes distrib_right [algebra_simps]: "(a + b) * c = a * c + b * c"
-  assumes distrib_left [algebra_simps]: "a * (b + c) = a * b + a * c"
+  assumes distrib_right [algebra_simps, algebra_split_simps]: "(a + b) * c = a * c + b * c"
+  assumes distrib_left [algebra_simps, algebra_split_simps]: "a * (b + c) = a * b + a * c"
 begin
 
 text \<open>For the \<open>combine_numerals\<close> simproc\<close>
 lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c"
   by (simp add: distrib_right ac_simps)

 
 end
 
 class comm_semiring_1_cancel =
   comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult +
-  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
+  assumes right_diff_distrib' [algebra_simps, algebra_split_simps]:
+    "a * (b - c) = a * b - a * c"
 begin
 
 subclass semiring_1_cancel ..
 subclass comm_semiring_0_cancel ..
 subclass comm_semiring_1 ..
 
-lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a"
+lemma left_diff_distrib' [algebra_simps, algebra_split_simps]:
+  "(b - c) * a = b * a - c * a"
   by (simp add: algebra_simps)
 
 lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
 proof -
   have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")

   by simp
 
 lemma minus_mult_commute: "- a * b = a * - b"
   by simp
 
-lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c"
+lemma right_diff_distrib [algebra_simps, algebra_split_simps]:
+  "a * (b - c) = a * b - a * c"
   using distrib_left [of a b "-c "] by simp
 
-lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c"
+lemma left_diff_distrib [algebra_simps, algebra_split_simps]:
+  "(a - b) * c = a * c - b * c"
   using distrib_right [of a "- b" c] by simp
 
 lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib
 
 lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"

 setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
 
 context semiring
 begin
 
-lemma [field_simps]:
+lemma [field_simps, field_split_simps]:
   shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
     and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
   by (rule distrib_left distrib_right)+
 
 end
 
 context ring
 begin
 
-lemma [field_simps]:
+lemma [field_simps, field_split_simps]:
   shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
     and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
   by (rule left_diff_distrib right_diff_distrib)+
 
 end

   qed
   then show "a * b \<noteq> 0"
     by (simp add: neq_iff)
 qed
 
-lemma zero_less_mult_iff [sign_simps]: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
+lemma zero_less_mult_iff [algebra_split_simps, field_split_simps]:
+  "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
      (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
 
-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"
+lemma zero_le_mult_iff [algebra_split_simps, field_split_simps]:
+  "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
 
-lemma mult_less_0_iff [sign_simps]: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
+lemma mult_less_0_iff [algebra_split_simps, field_split_simps]:
+  "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
   using zero_less_mult_iff [of "- a" b] by auto
 
-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"
+lemma mult_le_0_iff [algebra_split_simps, field_split_simps]:
+  "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   using zero_le_mult_iff [of "- a" b] by auto
 
 text \<open>
   Cancellation laws for \<^term>\<open>c * a < c * b\<close> and \<^term>\<open>a * c < b * c\<close>,
   also with the relations \<open>\<le>\<close> and equality.