author paulson Sat, 13 Aug 2022 20:08:24 +0100 changeset 76349 4b507edcf6b5 parent 76348 96e66ba48052 child 76376 86d60f4a10a7
The right way to formulate card_UNION, plus the old version for compatibility
 src/HOL/Binomial.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Binomial.thy	Fri Aug 12 20:21:09 2022 +0200
+++ b/src/HOL/Binomial.thy	Sat Aug 13 20:08:24 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"```