Theory Binomial_Lemmas

(*  Title:      Binomial_Lemmas.thy
    Author:     Ata Keskin, TU München
*)

section ‹Lemmas involving the binomial coefficient›

text ‹In this section, we prove lemmas that use the term for the binomial coefficient @{term choose}.›

theory Binomial_Lemmas
  imports Main
begin

lemma choose_mono:
  assumes "x ≤ y"
  shows "x choose n ≤ y choose n"
proof -
  have "finite {0..<y}" by blast
  with finite_Pow_iff[of "{0..<y}"] have finiteness: "finite {K ∈ Pow {0..<y}. card K = n}" by simp
  from assms have "Pow {0..<x} ⊆ Pow {0..<y}" by force
  then have "{K ∈ Pow {0..<x}. card K = n} ⊆ {K ∈ Pow {0..<y}. card K = n}" by blast
  from card_mono[OF finiteness this] show ?thesis unfolding binomial_def .
qed

lemma choose_row_sum_set:
  assumes "finite (⋃F)"
  shows "card {S. S ⊆ ⋃F ∧ card S ≤ k} = (∑i≤k. card (⋃ F) choose i)"
proof (induction k)
  case 0
  from rev_finite_subset[OF assms] have "S ⊆ ⋃F ∧ card S ≤ 0 ⟷ S = {}" for S by fastforce
  then show ?case by simp
next
  case (Suc k)
  let ?FS = "{S. S ⊆ ⋃ F ∧ card S ≤ Suc k}"
  and ?F_Asm = "{S. S ⊆ ⋃ F ∧ card S ≤ k}" 
  and ?F_Step = "{S. S ⊆ ⋃ F ∧ card S = Suc k}"

  from finite_Pow_iff[of "⋃F"] assms have finite_Pow_Un_F: "finite (Pow (⋃ F))" ..
  have "?F_Asm ⊆ Pow (⋃ F)" and "?F_Step ⊆ Pow (⋃ F)" by fast+
  with rev_finite_subset[OF finite_Pow_Un_F] have finite_F_Asm: "finite ?F_Asm" and finite_F_Step: "finite ?F_Step" by presburger+

  have F_Un: "?FS = ?F_Asm ∪ ?F_Step"  and F_disjoint: "?F_Asm ∩ ?F_Step = {}" by fastforce+
  from card_Un_disjoint[OF finite_F_Asm finite_F_Step F_disjoint] F_Un have "card ?FS = card ?F_Asm + card ?F_Step" by argo
  also from Suc have "... = (∑i≤k. card (⋃ F) choose i) + card ?F_Step" by argo
  also from n_subsets[OF assms, of "Suc k"] have "... = (∑i≤Suc k. card (⋃ F) choose i)" by force
  finally show ?case by blast
qed

end