src/HOL/Int.thy

   show "- i + i = 0"
     by (cases i) (simp add: Zero_int_def minus add)
   show "i - j = i + - j"
     by (simp add: diff_int_def)
   show "(i * j) * k = i * (j * k)"
-    by (cases i, cases j, cases k) (simp add: mult ring_simps)
+    by (cases i, cases j, cases k) (simp add: mult algebra_simps)
   show "i * j = j * i"
-    by (cases i, cases j) (simp add: mult ring_simps)
+    by (cases i, cases j) (simp add: mult algebra_simps)
   show "1 * i = i"
     by (cases i) (simp add: One_int_def mult)
   show "(i + j) * k = i * k + j * k"
-    by (cases i, cases j, cases k) (simp add: add mult ring_simps)
+    by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
   show "0 \<noteq> (1::int)"
     by (simp add: Zero_int_def One_int_def)
 qed
 
 lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"

   [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
-    by (simp add: congruent_def compare_rls of_nat_add [symmetric]
+    by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
             del: of_nat_add) 
   thus ?thesis
     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
 qed
 
 lemma of_int_0 [simp]: "of_int 0 = 0"
-  by (simp add: of_int Zero_int_def)
+by (simp add: of_int Zero_int_def)
 
 lemma of_int_1 [simp]: "of_int 1 = 1"
-  by (simp add: of_int One_int_def)
+by (simp add: of_int One_int_def)
 
 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
-  by (cases w, cases z, simp add: compare_rls of_int OrderedGroup.compare_rls add)
+by (cases w, cases z, simp add: algebra_simps of_int add)
 
 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
-  by (cases z, simp add: compare_rls of_int minus)
+by (cases z, simp add: algebra_simps of_int minus)
 
 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
-  by (simp add: OrderedGroup.diff_minus diff_minus)
+by (simp add: OrderedGroup.diff_minus diff_minus)
 
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
 apply (cases w, cases z)
-apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
-                 mult add_ac of_nat_mult)
+apply (simp add: algebra_simps of_int mult of_nat_mult)
 done
 
 text{*Collapse nested embeddings*}
 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
-  by (induct n) auto
+by (induct n) auto
 
 end
 
 context ordered_idom
 begin
 
 lemma of_int_le_iff [simp]:
   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
-  by (cases w, cases z, simp add: of_int le minus compare_rls of_nat_add [symmetric] del: of_nat_add)
+by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
 
 text{*Special cases where either operand is zero*}
 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified]
 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified]
 

   have "(w \<le> z) = (0 \<le> z - w)"
     by (simp only: le_diff_eq add_0_left)
   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
     by (auto elim: zero_le_imp_eq_int)
   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
-    by (simp only: group_simps)
+    by (simp only: algebra_simps)
   finally show ?thesis .
 qed
 
 lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
 by simp

   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
                              le_imp_0_less [THEN order_less_imp_le])  
 next
   case (neg n)
   thus ?thesis by (simp del: of_nat_Suc of_nat_add
-    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
+    add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
 lemma bin_less_0_simps:
   "Pls < 0 \<longleftrightarrow> False"
   "Min < 0 \<longleftrightarrow> True"

 by (simp add: iszero_def eq_commute)
 
 lemma eq_number_of_eq:
   "((number_of x::'a::number_ring) = number_of y) =
    iszero (number_of (x + uminus y) :: 'a)"
-  unfolding iszero_def number_of_add number_of_minus
-  by (simp add: compare_rls)
+unfolding iszero_def number_of_add number_of_minus
+by (simp add: algebra_simps)
 
 lemma iszero_number_of_Pls:
   "iszero ((number_of Pls)::'a::number_ring)"
-  unfolding iszero_def numeral_0_eq_0 ..
+unfolding iszero_def numeral_0_eq_0 ..
 
 lemma nonzero_number_of_Min:
   "~ iszero ((number_of Min)::'a::number_ring)"
-  unfolding iszero_def numeral_m1_eq_minus_1 by simp
+unfolding iszero_def numeral_m1_eq_minus_1 by simp
 
 
 subsubsection {* Comparisons, for Ordered Rings *}
 
 lemmas double_eq_0_iff = double_zero

   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
                              le_imp_0_less [THEN order_less_imp_le])  
 next
   case (neg n)
   thus ?thesis by (simp del: of_nat_Suc of_nat_add
-    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
+    add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
 text {* Less-Than or Equals *}
 
 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}

   by (simp add: diff_minus add_number_of_left)
 
 lemma add_number_of_diff2 [simp]:
   "number_of v + (c - number_of w) =
    number_of (v + uminus w) + (c::'a::number_ring)"
-apply (subst diff_number_of_eq [symmetric])
-apply (simp only: compare_rls)
-done
+by (simp add: algebra_simps diff_number_of_eq [symmetric])
 
 
 subsection {* The Set of Integers *}
 
 context ring_1