--- a/src/HOL/Finite_Set.thy Fri Jan 26 21:16:03 2018 +0100
+++ b/src/HOL/Finite_Set.thy Sat Jan 27 10:27:57 2018 +0100
@@ -485,6 +485,12 @@
lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A"
by (blast intro: finite_subset [OF subset_Pow_Union])
+lemma finite_bind:
+ assumes "finite S"
+ assumes "\<forall>x \<in> S. finite (f x)"
+ shows "finite (Set.bind S f)"
+using assms by (simp add: bind_UNION)
+
lemma finite_set_of_finite_funs:
assumes "finite A" "finite B"
shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")
--- a/src/HOL/Groups_Big.thy Fri Jan 26 21:16:03 2018 +0100
+++ b/src/HOL/Groups_Big.thy Sat Jan 27 10:27:57 2018 +0100
@@ -1027,6 +1027,43 @@
finally show ?thesis by auto
qed
+lemma sum_card_image:
+ assumes "finite A"
+ assumes "\<forall>s\<in>A. \<forall>t\<in>A. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}"
+ shows "sum card (f ` A) = sum (\<lambda>a. card (f a)) A"
+using assms
+proof (induct A)
+ case empty
+ from this show ?case by simp
+next
+ case (insert a A)
+ show ?case
+ proof cases
+ assume "f a = {}"
+ from this insert show ?case
+ by (subst sum.mono_neutral_right[where S="f ` A"]) auto
+ next
+ assume "f a \<noteq> {}"
+ from this have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)"
+ using insert by (subst sum.insert) auto
+ from this insert show ?case by simp
+ qed
+qed
+
+lemma card_Union_image:
+ assumes "finite S"
+ assumes "\<forall>s\<in>f ` S. finite s"
+ assumes "\<forall>s\<in>S. \<forall>t\<in>S. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}"
+ shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S"
+proof -
+ have "\<forall>A\<in>f ` S. \<forall>B\<in>f ` S. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
+ using assms(3) by (metis image_iff)
+ from this have "card (\<Union>(f ` S)) = sum card (f ` S)"
+ using assms(1, 2) by (subst card_Union_disjoint) auto
+ also have "... = sum (\<lambda>x. card (f x)) S"
+ using assms(1, 3) by (auto simp add: sum_card_image)
+ finally show ?thesis .
+qed
subsubsection \<open>Cardinality of products\<close>