--- a/src/HOL/Binomial.thy Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Binomial.thy Sat Sep 09 19:26:08 2023 +0100
@@ -115,6 +115,9 @@
lemma binomial_1 [simp]: "n choose Suc 0 = n"
by (induct n) simp_all
+lemma choose_one: "n choose 1 = n" for n :: nat
+ by simp
+
lemma choose_reduce_nat:
"0 < n \<Longrightarrow> 0 < k \<Longrightarrow>
n choose k = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
@@ -1084,109 +1087,190 @@
qed
-subsection \<open>More on Binomial Coefficients\<close>
+subsection \<open>Inclusion-exclusion principle\<close>
+
+lemma Inter_over_Union:
+ "\<Inter> {\<Union> (\<F> x) |x. x \<in> S} = \<Union> {\<Inter> (G ` S) |G. \<forall>x\<in>S. G x \<in> \<F> x}"
+proof -
+ have "\<And>x. \<forall>s\<in>S. \<exists>X \<in> \<F> s. x \<in> X \<Longrightarrow> \<exists>G. (\<forall>x\<in>S. G x \<in> \<F> x) \<and> (\<forall>s\<in>S. x \<in> G s)"
+ by metis
+ then show ?thesis
+ by (auto simp flip: all_simps ex_simps)
+qed
+
+lemma subset_insert_lemma:
+ "{T. T \<subseteq> (insert a S) \<and> P T} = {T. T \<subseteq> S \<and> P T} \<union> {insert a T |T. T \<subseteq> S \<and> P(insert a T)}" (is "?L=?R")
+proof
+ show "?L \<subseteq> ?R"
+ by (smt (verit) UnI1 UnI2 insert_Diff mem_Collect_eq subsetI subset_insert_iff)
+qed blast
+
+
+text\<open>Versions for additive real functions, where the additivity applies only to some
+ specific subsets (e.g. cardinality of finite sets, measurable sets with bounded measure.
+ (From HOL Light)\<close>
+
+locale Incl_Excl =
+ fixes P :: "'a set \<Rightarrow> bool" and f :: "'a set \<Rightarrow> 'b::ring_1"
+ assumes disj_add: "\<lbrakk>P S; P T; disjnt S T\<rbrakk> \<Longrightarrow> f(S \<union> T) = f S + f T"
+ and empty: "P{}"
+ and Int: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)"
+ and Un: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<union> T)"
+ and Diff: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S - T)"
+
+begin
+
+lemma f_empty [simp]: "f{} = 0"
+ using disj_add empty by fastforce
+
+lemma f_Un_Int: "\<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> f(S \<union> T) + f(S \<inter> T) = f S + f T"
+ by (smt (verit, ccfv_threshold) Groups.add_ac(2) Incl_Excl.Diff Incl_Excl.Int Incl_Excl_axioms Int_Diff_Un Int_Diff_disjoint Int_absorb Un_Diff Un_Int_eq(2) disj_add disjnt_def group_cancel.add2 sup_bot.right_neutral)
-lemma choose_one: "n choose 1 = n" for n :: nat
- by simp
+lemma restricted_indexed:
+ assumes "finite A" and X: "\<And>a. a \<in> A \<Longrightarrow> P(X a)"
+ shows "f(\<Union>(X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+proof -
+ have "\<lbrakk>finite A; card A = n; \<forall>a \<in> A. P (X a)\<rbrakk>
+ \<Longrightarrow> f(\<Union>(X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))" for n X and A :: "'c set"
+ proof (induction n arbitrary: A X rule: less_induct)
+ case (less n0 A0 X)
+ show ?case
+ proof (cases "n0=0")
+ case True
+ with less show ?thesis
+ by fastforce
+ next
+ case False
+ with less.prems obtain A n a where *: "n0 = Suc n" "A0 = insert a A" "a \<notin> A" "card A = n" "finite A"
+ by (metis card_Suc_eq_finite not0_implies_Suc)
+ with less have "P (X a)" by blast
+ have APX: "\<forall>a \<in> A. P (X a)"
+ by (simp add: "*" less.prems)
+ have PUXA: "P (\<Union> (X ` A))"
+ using \<open>finite A\<close> APX
+ by (induction) (auto simp: empty Un)
+ have "f (\<Union> (X ` A0)) = f (X a \<union> \<Union> (X ` A))"
+ by (simp add: *)
+ also have "... = f (X a) + f (\<Union> (X ` A)) - f (X a \<inter> \<Union> (X ` A))"
+ using f_Un_Int add_diff_cancel PUXA \<open>P (X a)\<close> by metis
+ also have "... = f (X a) - (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ card B * f (\<Inter> (X ` B))) +
+ (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B)))"
+ proof -
+ have 1: "f (\<Union>i\<in>A. X a \<inter> X i) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter>b\<in>B. X a \<inter> X b))"
+ using less.IH [of n A "\<lambda>i. X a \<inter> X i"] APX Int \<open>P (X a)\<close> by (simp add: *)
+ have 2: "X a \<inter> \<Union> (X ` A) = (\<Union>i\<in>A. X a \<inter> X i)"
+ by auto
+ have 3: "f (\<Union> (X ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+ using less.IH [of n A X] APX Int \<open>P (X a)\<close> by (simp add: *)
+ show ?thesis
+ unfolding 3 2 1
+ by (simp add: sum_negf)
+ qed
+ also have "... = (\<Sum>B | B \<subseteq> A0 \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> (X ` B)))"
+ proof -
+ have F: "{insert a B |B. B \<subseteq> A} = insert a ` Pow A \<and> {B. B \<subseteq> A \<and> B \<noteq> {}} = Pow A - {{}}"
+ by auto
+ have G: "(\<Sum>B\<in>Pow A. (- 1) ^ card (insert a B) * f (X a \<inter> \<Inter> (X ` B))) = (\<Sum>B\<in>Pow A. - ((- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B))))"
+ proof (rule sum.cong [OF refl])
+ fix B
+ assume B: "B \<in> Pow A"
+ then have "finite B"
+ using \<open>finite A\<close> finite_subset by auto
+ show "(- 1) ^ card (insert a B) * f (X a \<inter> \<Inter> (X ` B)) = - ((- 1) ^ card B * f (X a \<inter> \<Inter> (X ` B)))"
+ using B * by (auto simp add: card_insert_if \<open>finite B\<close>)
+ qed
+ have disj: "{B. B \<subseteq> A \<and> B \<noteq> {}} \<inter> {insert a B |B. B \<subseteq> A} = {}"
+ using * by blast
+ have inj: "inj_on (insert a) (Pow A)"
+ using "*" inj_on_def by fastforce
+ show ?thesis
+ apply (simp add: * subset_insert_lemma sum.union_disjoint disj sum_negf)
+ apply (simp add: F G sum_negf sum.reindex [OF inj] o_def sum_diff *)
+ done
+ qed
+ finally show ?thesis .
+ qed
+ qed
+ then show ?thesis
+ by (meson assms)
+qed
+
+lemma restricted:
+ assumes "finite A" "\<And>a. a \<in> A \<Longrightarrow> P a"
+ shows "f(\<Union> A) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> B))"
+ using restricted_indexed [of A "\<lambda>x. x"] assms by auto
+
+end
+
+subsection\<open>Versions for unrestrictedly additive functions\<close>
+
+lemma Incl_Excl_UN:
+ fixes f :: "'a set \<Rightarrow> 'b::ring_1"
+ assumes "\<And>S T. disjnt S T \<Longrightarrow> f(S \<union> T) = f S + f T" "finite A"
+ shows "f(\<Union>(G ` A)) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (-1) ^ (card B + 1) * f (\<Inter> (G ` B)))"
+proof -
+ interpret Incl_Excl "\<lambda>x. True" f
+ by (simp add: Incl_Excl.intro assms(1))
+ show ?thesis
+ using restricted_indexed assms by blast
+qed
+
+lemma Incl_Excl_Union:
+ fixes f :: "'a set \<Rightarrow> 'b::ring_1"
+ assumes "\<And>S T. disjnt S T \<Longrightarrow> f(S \<union> T) = f S + f T" "finite A"
+ shows "f(\<Union> A) = (\<Sum>B | B \<subseteq> A \<and> B \<noteq> {}. (- 1) ^ (card B + 1) * f (\<Inter> B))"
+ using Incl_Excl_UN[of f A "\<lambda>X. X"] assms by simp
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"
+ assumes "finite A" "\<And>K. K \<in> A \<Longrightarrow> finite K"
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 -
+ interpret Incl_Excl finite "int o card"
+ proof qed (auto simp add: card_Un_disjnt)
+ show ?thesis
+ using restricted assms by auto
+qed
+
+text\<open>A more conventional form\<close>
+lemma inclusion_exclusion:
+ assumes "finite A" "\<And>K. K \<in> A \<Longrightarrow> finite K"
+ shows "int(card(\<Union> A)) =
+ (\<Sum>n=1..card A. (-1) ^ (Suc n) * (\<Sum>B | B \<subseteq> A \<and> card B = n. int (card (\<Inter> B))))" (is "_=?R")
proof -
- have "?rhs = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))"
- by simp
- 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 "\<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)
- also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
- using assms
- by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
- also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
- using assms by (subst sum.Sigma) auto
- also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "sum ?lhs _ = _")
- proof (rule sum.cong[OF refl])
- fix x
- assume x: "x \<in> \<Union>A"
- define K where "K = {X \<in> A. x \<in> X}"
- with \<open>finite A\<close> have K: "finite K"
- by auto
- let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
- have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
- using assms by (auto intro!: inj_onI)
- moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
- using assms
- by (auto intro!: rev_image_eqI[where x="(card a, a)" for a]
- simp add: card_gt_0_iff[folded Suc_le_eq]
- dest: finite_subset intro: card_mono)
- ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
- by (rule sum.reindex_cong [where l = snd]) fastforce
- also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
- using assms by (subst sum.Sigma) auto
- also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
- by (subst sum_distrib_left) simp
- also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))"
- (is "_ = ?rhs")
- proof (rule sum.mono_neutral_cong_right[rule_format])
- show "finite {1..card A}"
- by simp
- show "{1..card K} \<subseteq> {1..card A}"
- using \<open>finite A\<close> by (auto simp add: K_def intro: card_mono)
- next
- fix i
- assume "i \<in> {1..card A} - {1..card K}"
- then have i: "i \<le> card A" "card K < i"
- by auto
- have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
- by (auto simp add: K_def)
- 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 (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)"
- (is "?lhs = ?rhs")
- by (rule sum.cong) (auto simp add: K_def)
- then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs"
- by simp
- qed
- also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}"
- using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset)
- then have "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
- by (subst (2) sum.atLeast_Suc_atMost) simp_all
- also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
- using K by (subst n_subsets[symmetric]) simp_all
- also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
- by (subst sum_distrib_left[symmetric]) simp
- also have "\<dots> = - ((-1 + 1) ^ card K) + 1"
- by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0)
- also have "\<dots> = 1"
- using x K by (auto simp add: K_def card_gt_0_iff)
- finally show "?lhs x = 1" .
+ have fin: "finite {I. I \<subseteq> A \<and> I \<noteq> {}}"
+ by (simp add: assms)
+ have "\<And>k. \<lbrakk>Suc 0 \<le> k; k \<le> card A\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>A. B \<noteq> {} \<and> k = card B"
+ by (metis (mono_tags, lifting) Suc_le_D Zero_neq_Suc card_eq_0_iff obtain_subset_with_card_n)
+ with \<open>finite A\<close> finite_subset
+ have card_eq: "card ` {I. I \<subseteq> A \<and> I \<noteq> {}} = {1..card A}"
+ using not_less_eq_eq card_mono by (fastforce simp: image_iff)
+ have "int(card(\<Union> A))
+ = (\<Sum>y = 1..card A. \<Sum>I\<in>{x. x \<subseteq> A \<and> x \<noteq> {} \<and> card x = y}. - ((- 1) ^ y * int (card (\<Inter> I))))"
+ by (simp add: int_card_UNION assms sum.image_gen [OF fin, where g=card] card_eq)
+ also have "... = ?R"
+ proof -
+ have "{B. B \<subseteq> A \<and> B \<noteq> {} \<and> card B = k} = {B. B \<subseteq> A \<and> card B = k}"
+ if "Suc 0 \<le> k" and "k \<le> card A" for k
+ using that by auto
+ then show ?thesis
+ by (clarsimp simp add: sum_negf simp flip: sum_distrib_left)
qed
- also have "\<dots> = int (card (\<Union>A))"
- by simp
- finally show ?thesis ..
+ finally show ?thesis .
qed
lemma card_UNION:
- assumes "finite A"
- and "\<forall>k \<in> A. finite k"
+ assumes "finite A" and "\<And>K. K \<in> A \<Longrightarrow> 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"
+ assumes "finite A" and "\<And>K. K \<in> A \<Longrightarrow> 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
+subsection \<open>More on Binomial Coefficients\<close>
+
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"