author Andreas Lochbihler Wed, 27 Feb 2013 13:48:15 +0100 changeset 51292 8a635bf2c86c parent 51291 c2b452628afa child 51296 77e71d54efda
use lemma from Big_Operators
```--- 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"