1.1 --- a/src/HOL/Number_Theory/Binomial.thy	Wed Feb 27 13:44:19 2013 +0100
     1.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Wed Feb 27 13:48:15 2013 +0100
     1.3 @@ -362,28 +362,14 @@
     1.4   finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -
     1.8 -lemma finite_SigmaI2:
     1.9 -  assumes "finite {x\<in>A. B x \<noteq> {}}"
    1.10 -  and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
    1.11 -  shows "finite (Sigma A B)"
    1.12 -proof -
    1.13 -  from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)"
    1.14 -    by(rule finite_SigmaI) simp
    1.15 -  also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" by auto
    1.16 -  finally show ?thesis .
    1.17 -qed
    1.18 -
    1.19  lemma card_UNION:
    1.20 -  fixes A :: "'a set set"
    1.21 -  assumes "finite A"
    1.22 -  and "\<forall>k \<in> A. finite k"
    1.23 +  assumes "finite A" and "\<forall>k \<in> A. finite k"
    1.24    shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
    1.25    (is "?lhs = ?rhs")
    1.26  proof -
    1.27    have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
    1.28    also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
    1.29 -    by(subst setsum_linear[symmetric]) simp
    1.30 +    by(subst setsum_right_distrib) simp
    1.31    also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
    1.32      using assms by(subst setsum_Sigma)(auto)
    1.33    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))"
    1.34 @@ -409,7 +395,7 @@
    1.35      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)))"
    1.36        using assms by(subst setsum_Sigma) auto
    1.37      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))"
    1.38 -      by(subst setsum_linear[symmetric]) simp
    1.39 +      by(subst setsum_right_distrib) simp
    1.40      also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
    1.41      proof(rule setsum_mono_zero_cong_right[rule_format])
    1.42        show "{1..card K} \<subseteq> {1..card A}" using `finite A`
    1.43 @@ -438,7 +424,7 @@
    1.44      also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
    1.45        using K by(subst card_subsets_nat[symmetric]) simp_all
    1.46      also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
    1.47 -      by(subst setsum_linear) simp
    1.48 +      by(subst setsum_right_distrib[symmetric]) simp
    1.49      also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
    1.50        by(subst binomial)(simp add: mult_ac)
    1.51      also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)