src/HOL/Big_Operators.thy
changeset 46557 ae926869a311
parent 46554 87d4e4958476
child 46629 8d3442b79f9c
     1.1 --- a/src/HOL/Big_Operators.thy	Mon Feb 20 21:04:00 2012 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Feb 21 08:15:42 2012 +0100
     1.3 @@ -786,13 +786,15 @@
     1.4    by (simp only: card_def setsum_def)
     1.5  
     1.6  lemma card_UN_disjoint:
     1.7 -  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     1.8 -    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
     1.9 -  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
    1.10 -proof -
    1.11 -  have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
    1.12 -  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
    1.13 -qed
    1.14 +  "finite I ==> (ALL i:I. finite (A i)) ==>
    1.15 +   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
    1.16 +   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
    1.17 +apply (simp add: card_eq_setsum del: setsum_constant)
    1.18 +apply (subgoal_tac
    1.19 +         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
    1.20 +apply (simp add: setsum_UN_disjoint del: setsum_constant)
    1.21 +apply simp
    1.22 +done
    1.23  
    1.24  lemma card_Union_disjoint:
    1.25    "finite C ==> (ALL A:C. finite A) ==>