--- a/src/HOL/Big_Operators.thy Wed Aug 15 12:18:30 2012 +0200
+++ b/src/HOL/Big_Operators.thy Wed Aug 15 12:56:54 2012 +0200
@@ -39,12 +39,6 @@
then show ?thesis unfolding `A = B` by simp
qed
-lemma F_unit[simp]: "F (%i. 1) A = 1"
-by (cases "finite A") (erule finite_induct, auto)
-
-lemma F_unit': "ALL a:A. g a = 1 ==> F g A = 1"
-by (simp add:F_cong)
-
lemma If_cases:
fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
assumes fA: "finite A"
@@ -208,8 +202,11 @@
==> setsum h B = setsum g A"
by (simp add: setsum_reindex)
-lemmas setsum_0 = setsum.F_unit
-lemmas setsum_0' = setsum.F_unit'
+lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
+ by (cases "finite A") (erule finite_induct, auto)
+
+lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
+ by (simp add:setsum_cong)
lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
@@ -945,9 +942,16 @@
using I0 by auto
-lemmas setprod_1 = setprod.F_unit
-lemmas setprod_1' = setprod.F_unit'
+lemma setprod_1: "setprod (%i. 1) A = 1"
+apply (case_tac "finite A")
+apply (erule finite_induct, auto simp add: mult_ac)
+done
+lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
+apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
+apply (erule ssubst, rule setprod_1)
+apply (rule setprod_cong, auto)
+done
lemma setprod_Un_Int: "finite A ==> finite B
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"