# HG changeset patch
# User nipkow
# Date 1542631204 -3600
# Node ID 248696d0a05f08ea74f2330bdc2e9ee40a32e057
# Parent  b021008c5397c4def58be3da5d2023ae9e846199
Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.

diff -r b021008c5397 -r 248696d0a05f NEWS
--- a/NEWS	Sun Nov 18 18:07:51 2018 +0000
+++ b/NEWS	Mon Nov 19 13:40:04 2018 +0100
@@ -54,6 +54,8 @@
 * Theory "HOL-Library.Multiset": the <Union># operator now has the same
 precedence as any other prefix function symbol.
 
+* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
+
 * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
 and prod_mset.swap, similarly to sum.swap and prod.swap.
 INCOMPATIBILITY.
diff -r b021008c5397 -r 248696d0a05f src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Nov 18 18:07:51 2018 +0000
+++ b/src/HOL/Groups_Big.thy	Mon Nov 19 13:40:04 2018 +0100
@@ -1089,22 +1089,6 @@
   qed
 qed simp
 
-lemma card_Union_image:
-  assumes "finite S"
-  assumes "\<And>s. s \<in> S \<Longrightarrow> finite (f s)"
-  assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) S"
-  shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S"
-proof -
-  have "pairwise disjnt (f ` S)"
-    using assms(3)
-    by (metis pairwiseD pairwise_imageI) 
-  then have "card (\<Union>(f ` S)) = sum card (f ` S)"
-    by (subst card_Union_disjoint) (use assms in auto)
-  also have "... = sum (\<lambda>x. card (f x)) S"
-    by (metis (mono_tags, lifting) assms(1) assms(3) sum_card_image)
-  finally show ?thesis .
-qed
-
 
 subsubsection \<open>Cardinality of products\<close>