--- a/src/HOL/Finite_Set.thy Wed Jan 28 06:03:46 2009 -0800
+++ b/src/HOL/Finite_Set.thy Wed Jan 28 16:57:12 2009 +0100
@@ -989,12 +989,12 @@
lemma setsum_Un_nat: "finite A ==> finite B ==>
(setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
-- {* For the natural numbers, we have subtraction. *}
-by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
+by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
lemma setsum_Un: "finite A ==> finite B ==>
(setsum f (A Un B) :: 'a :: ab_group_add) =
setsum f A + setsum f B - setsum f (A Int B)"
-by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
+by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
(if a:A then setsum f A - f a else setsum f A)"
@@ -1667,7 +1667,7 @@
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
apply (cases "finite A")
apply (erule finite_induct)
-apply (auto simp add: ring_simps)
+apply (auto simp add: algebra_simps)
done
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
@@ -2176,16 +2176,16 @@
thus ?case
proof
assume "a = x" thus ?thesis using insert
- by (simp add: mult_ac_idem)
+ by (simp add: mult_ac)
next
assume "a \<in> F"
hence bel: "fold1 inf F \<le> a" by (rule insert)
have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
- using insert by (simp add: mult_ac_idem)
+ using insert by (simp add: mult_ac)
also have "inf (fold1 inf F) a = fold1 inf F"
using bel by (auto intro: antisym)
also have "inf x \<dots> = fold1 inf (insert x F)"
- using insert by (simp add: mult_ac_idem)
+ using insert by (simp add: mult_ac)
finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
ultimately show ?thesis by simp