# HG changeset patch
# User Andreas Lochbihler
# Date 1361969295 -3600
# Node ID 8a635bf2c86c76ce4be5c6ee32cce75b9d23f792
# Parent  c2b452628afa87ca8ed1ba5aa4235deda7c41551
use lemma from Big_Operators

diff -r c2b452628afa -r 8a635bf2c86c src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Wed Feb 27 13:44:19 2013 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Wed Feb 27 13:48:15 2013 +0100
@@ -362,28 +362,14 @@
  finally show ?thesis .
 qed
 
-
-lemma finite_SigmaI2:
-  assumes "finite {x\<in>A. B x \<noteq> {}}"
-  and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
-  shows "finite (Sigma A B)"
-proof -
-  from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)"
-    by(rule finite_SigmaI) simp
-  also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" by auto
-  finally show ?thesis .
-qed
-
 lemma card_UNION:
-  fixes A :: "'a set set"
-  assumes "finite A"
-  and "\<forall>k \<in> A. finite k"
+  assumes "finite A" and "\<forall>k \<in> A. finite k"
   shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
   (is "?lhs = ?rhs")
 proof -
   have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
   also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
-    by(subst setsum_linear[symmetric]) simp
+    by(subst setsum_right_distrib) simp
   also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
     using assms by(subst setsum_Sigma)(auto)
   also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
@@ -409,7 +395,7 @@
     also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
       using assms by(subst setsum_Sigma) auto
     also have "\<dots> = (\<Sum>i=1..card A. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
-      by(subst setsum_linear[symmetric]) simp
+      by(subst setsum_right_distrib) simp
     also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
     proof(rule setsum_mono_zero_cong_right[rule_format])
       show "{1..card K} \<subseteq> {1..card A}" using `finite A`
@@ -438,7 +424,7 @@
     also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
       using K by(subst card_subsets_nat[symmetric]) simp_all
     also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
-      by(subst setsum_linear) simp
+      by(subst setsum_right_distrib[symmetric]) simp
     also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
       by(subst binomial)(simp add: mult_ac)
     also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)