# HG changeset patch
# User paulson
# Date 1660471871 -3600
# Node ID 86d60f4a10a76c992881d85e4891619fce1d5f46
# Parent  9ce4cb8e3f77a44c63a0a74f2a94861a72401869# Parent  4b507edcf6b51dbc38206dabcfb6773f40c23464
merged

diff -r 9ce4cb8e3f77 -r 86d60f4a10a7 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sat Aug 13 23:47:08 2022 +0200
+++ b/src/HOL/Binomial.thy	Sun Aug 14 11:11:11 2022 +0100
@@ -1074,18 +1074,18 @@
 lemma choose_one: "n choose 1 = n" for n :: nat
   by simp
 
-lemma card_UNION:
+text \<open>The famous inclusion-exclusion formula for the cardinality of a union\<close>
+lemma int_card_UNION:
   assumes "finite A"
     and "\<forall>k \<in> A. finite k"
-  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
+  shows "int (card (\<Union>A)) = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
   (is "?lhs = ?rhs")
 proof -
-  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))"
+  have "?rhs = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))"
     by simp
-  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))"
-    (is "_ = nat ?rhs")
+  also have "\<dots> = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))"
     by (subst sum_distrib_left) simp
-  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
+  also have "\<dots> = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
     using assms by (subst sum.Sigma) auto
   also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
     by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI)
@@ -1132,7 +1132,7 @@
       also have "\<dots> = {}"
         using \<open>finite A\<close> i by (auto simp add: K_def dest: card_mono[rotated 1])
       finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
-        by (simp only:) simp
+        by (metis mult_zero_right sum.empty)
     next
       fix i
       have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
@@ -1155,11 +1155,23 @@
       using x K by (auto simp add: K_def card_gt_0_iff)
     finally show "?lhs x = 1" .
   qed
-  also have "nat \<dots> = card (\<Union>A)"
+  also have "\<dots> = int (card (\<Union>A))"
     by simp
   finally show ?thesis ..
 qed
 
+lemma card_UNION:
+  assumes "finite A"
+    and "\<forall>k \<in> A. finite k"
+  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
+  by (simp only: flip: int_card_UNION [OF assms])
+
+lemma card_UNION_nonneg:
+  assumes "finite A"
+    and "\<forall>k \<in> A. finite k"
+  shows "(\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I))) \<ge> 0"
+  using int_card_UNION [OF assms] by presburger
+
 text \<open>The number of nat lists of length \<open>m\<close> summing to \<open>N\<close> is \<^term>\<open>(N + m - 1) choose N\<close>:\<close>
 lemma card_length_sum_list_rec:
   assumes "m \<ge> 1"