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) ==>
```