Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
authornipkow
Mon Nov 19 13:40:04 2018 +0100 (12 months ago)
changeset 69316248696d0a05f
parent 69313 b021008c5397
child 69317 e8dea06456b4
Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
NEWS
src/HOL/Groups_Big.thy
     1.1 --- a/NEWS	Sun Nov 18 18:07:51 2018 +0000
     1.2 +++ b/NEWS	Mon Nov 19 13:40:04 2018 +0100
     1.3 @@ -54,6 +54,8 @@
     1.4  * Theory "HOL-Library.Multiset": the <Union># operator now has the same
     1.5  precedence as any other prefix function symbol.
     1.6  
     1.7 +* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
     1.8 +
     1.9  * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
    1.10  and prod_mset.swap, similarly to sum.swap and prod.swap.
    1.11  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Groups_Big.thy	Sun Nov 18 18:07:51 2018 +0000
     2.2 +++ b/src/HOL/Groups_Big.thy	Mon Nov 19 13:40:04 2018 +0100
     2.3 @@ -1089,22 +1089,6 @@
     2.4    qed
     2.5  qed simp
     2.6  
     2.7 -lemma card_Union_image:
     2.8 -  assumes "finite S"
     2.9 -  assumes "\<And>s. s \<in> S \<Longrightarrow> finite (f s)"
    2.10 -  assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) S"
    2.11 -  shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S"
    2.12 -proof -
    2.13 -  have "pairwise disjnt (f ` S)"
    2.14 -    using assms(3)
    2.15 -    by (metis pairwiseD pairwise_imageI) 
    2.16 -  then have "card (\<Union>(f ` S)) = sum card (f ` S)"
    2.17 -    by (subst card_Union_disjoint) (use assms in auto)
    2.18 -  also have "... = sum (\<lambda>x. card (f x)) S"
    2.19 -    by (metis (mono_tags, lifting) assms(1) assms(3) sum_card_image)
    2.20 -  finally show ?thesis .
    2.21 -qed
    2.22 -
    2.23  
    2.24  subsubsection \<open>Cardinality of products\<close>
    2.25