src/HOL/SetInterval.thy

   apply (simp add: inj_on_def)
   apply (rule image_add_int_atLeastLessThan)
   done
 
 lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)"
-  apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
-  apply (auto simp add: compare_rls)
-  done
+apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym])
+apply (auto simp add: algebra_simps)
+done
 
 lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)"
-  by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
+by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp)
 
 lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))"
-  by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
+by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
 
 lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}"
 proof -
   have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto
   with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset)

 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
 
 lemma setsum_head_upt_Suc:
   "m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
 apply(insert setsum_head_Suc[of m "n - 1" f])
-apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] ring_simps)
+apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
 done
 
 
 lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"

 proof (induct n)
   case 0
   show ?case by simp
 next
   case (Suc n)
-  then show ?case by (simp add: ring_simps)
+  then show ?case by (simp add: algebra_simps)
 qed
 
 theorem arith_series_general:
   "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   of_nat n * (a + (a + of_nat(n - 1)*d))"

     by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   also from ngt1
   have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
     by (simp only: mult_ac gauss_sum [of "n - 1"])
        (simp add:  mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
-  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
+  finally show ?thesis by (simp add: algebra_simps)
 next
   assume "\<not>(n > 1)"
   hence "n = 1 \<or> n = 0" by auto
-  thus ?thesis by (auto simp: mult_ac right_distrib)
+  thus ?thesis by (auto simp: algebra_simps)
 qed
 
 lemma arith_series_nat:
   "Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
 proof -