--- a/src/HOL/Finite_Set.thy Tue Nov 23 08:58:32 2004 +0100
+++ b/src/HOL/Finite_Set.thy Tue Nov 23 09:08:35 2004 +0100
@@ -1025,14 +1025,17 @@
lemma setsum_mult:
fixes f :: "'a => ('b::semiring_0_cancel)"
- assumes fin: "finite A"
shows "r * setsum f A = setsum (%n. r * f n) A"
-using fin
-proof (induct)
- case empty thus ?case by simp
+proof (cases "finite A")
+ case True
+ thus ?thesis
+ proof (induct)
+ case empty thus ?case by simp
+ next
+ case (insert A x) thus ?case by (simp add: right_distrib)
+ qed
next
- case (insert A x)
- thus ?case by (simp add: right_distrib)
+ case False thus ?thesis by (simp add: setsum_def)
qed
lemma setsum_abs: