# HG changeset patch
# User haftmann
# Date 1330024549 -3600
# Node ID 8d3442b79f9c747ce13b8c7242e1f4c0030093ba
# Parent  08cb66dc7d2cb81f08b4a84ac6f7e81eb23eba71
tuned proof

diff -r 08cb66dc7d2c -r 8d3442b79f9c src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Feb 23 17:27:37 2012 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Feb 23 20:15:49 2012 +0100
@@ -786,15 +786,13 @@
   by (simp only: card_def setsum_def)
 
 lemma card_UN_disjoint:
-  "finite I ==> (ALL i:I. finite (A i)) ==>
-   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
-   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
-apply (simp add: card_eq_setsum del: setsum_constant)
-apply (subgoal_tac
-         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
-apply (simp add: setsum_UN_disjoint del: setsum_constant)
-apply simp
-done
+  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
+    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
+  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
+proof -
+  have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
+  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
+qed
 
 lemma card_Union_disjoint:
   "finite C ==> (ALL A:C. finite A) ==>