src/HOL/Binomial.thy

 lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"
   by (induct n) simp_all
 
 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)"
   using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp

   with assms show ?thesis
     by (simp add: binomial_altdef_of_nat prod_dividef)
 qed
 
 
-subsection \<open>More on Binomial Coefficients\<close>
-
-lemma choose_one: "n choose 1 = n" for n :: nat
-  by simp
+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 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 -
-  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" .
+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 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"
   shows "card {l::nat list. length l = m \<and> sum_list l = N} =