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

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 .

lemma choose_row_sum_set:
  assumes "finite (F)"
  shows "card {S. S  F  card S  k} = (ik. 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
  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 "... = (ik. card ( F) choose i) + card ?F_Step" by argo
  also from n_subsets[OF assms, of "Suc k"] have "... = (iSuc k. card ( F) choose i)" by force
  finally show ?case by blast