Theory Falling_Factorial_Sum_Combinatorics

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Proving Falling Factorial of a Sum with Combinatorics›

theory Falling_Factorial_Sum_Combinatorics
imports
  Discrete_Summation.Factorials
  Card_Partitions.Injectivity_Solver
begin

subsection ‹Preliminaries›

subsubsection ‹Addition to Factorials Theory›

lemma card_lists_distinct_length_eq:
  assumes "finite A"
  shows "card {xs. length xs = n  distinct xs  set xs  A} = ffact n (card A)"
proof cases
  assume "n  card A"
  have "card {xs. length xs = n  distinct xs  set xs  A} = {card A - n + 1..card A}"
    using finite A n  card A by (rule card_lists_distinct_length_eq)
  also have " = ffact n (card A)"
    using n  card A by (simp add: prod_rev_ffact_nat'[symmetric])
  finally show ?thesis .
next
  assume "¬ n  card A"
  from this finite A have "xs. length xs = n  distinct xs  set xs  A  False"
    by (metis card_mono distinct_card)
  from this have eq_empty: "{xs. length xs = n  distinct xs  set xs  A} = {}"
    using finite A by auto
  from ¬ n  card A show ?thesis
    by (simp add: ffact_nat_triv eq_empty)
qed

subsection ‹Interleavings of Two Lists›

inductive interleavings :: "'a list  'a list  'a list  bool"
where
  "interleavings [] ys ys"
| "interleavings xs [] xs"
| "interleavings xs ys zs  interleavings (x#xs) ys (x#zs)"
| "interleavings xs ys zs  interleavings xs (y#ys) (y#zs)"

lemma interleaving_Nil_implies_eq1:
  assumes "interleavings xs ys zs"
  assumes "xs = []"
  shows "ys = zs"
using assms by (induct rule: interleavings.induct) auto

lemma interleaving_Nil_iff1:
  "interleavings [] ys zs  (ys = zs)"
using interleaving_Nil_implies_eq1
by (auto simp add: interleavings.intros(1))

lemma interleaving_Nil_implies_eq2:
  assumes "interleavings xs ys zs"
  assumes "ys = []"
  shows "xs = zs"
using assms by (induct rule: interleavings.induct) auto

lemma interleaving_Nil_iff2:
  "interleavings xs [] zs  (xs = zs)"
using interleaving_Nil_implies_eq2
by (auto simp add: interleavings.intros(2))

lemma interleavings_Cons:
  "{zs. interleavings (x#xs) (y#ys) zs} =
    {x#zs|zs. interleavings xs (y#ys) zs}  {y#zs|zs. interleavings (x#xs) ys zs}"
  (is "?S = ?expr")
proof
  show "?S  ?expr"
    by (auto elim: interleavings.cases)
next
  show "?expr  ?S"
    by (auto intro: interleavings.intros)
qed

lemma interleavings_filter:
  assumes "X  Y = {}" "set zs  X  Y"
  shows "interleavings [zzs . z  X] [zzs . z  Y] zs"
using assms by (induct zs) (auto intro: interleavings.intros)

lemma interleavings_filter_eq1:
  assumes "interleavings xs ys zs"
  assumes "(xset xs. P x)  (yset ys. ¬ P y)"
  shows "filter P zs = xs"
using assms by (induct rule: interleavings.induct) auto

lemma interleavings_filter_eq2:
  assumes "interleavings xs ys zs"
  assumes "(xset xs. ¬ P x)  (yset ys. P y)"
  shows "filter P zs = ys"
using assms by (induct rule: interleavings.induct) auto

lemma interleavings_length:
  assumes "interleavings xs ys zs"
  shows "length xs + length ys = length zs"
using assms by (induct xs ys zs rule: interleavings.induct) auto

lemma interleavings_set:
  assumes "interleavings xs ys zs"
  shows "set xs  set ys = set zs"
using assms by (induct xs ys zs rule: interleavings.induct) auto

lemma interleavings_distinct:
  assumes "interleavings xs ys zs"
  shows "distinct xs  distinct ys  set xs  set ys = {}  distinct zs"
using assms interleavings_set by (induct xs ys zs rule: interleavings.induct) fastforce+

lemma two_mutual_lists_induction:
  assumes "ys. P [] ys"
  assumes "xs. P xs []"
  assumes "x xs y ys. P xs (y#ys)  P (x#xs) ys  P (x#xs) (y#ys)"
  shows "P xs ys"
using assms by (induction_schema) (pat_completeness, lexicographic_order)

lemma finite_interleavings:
  "finite {zs. interleavings xs ys zs}"
proof (induct xs ys rule: two_mutual_lists_induction)
  case (1 ys)
  show ?case by (simp add: interleaving_Nil_iff1)
next
  case (2 xs)
  then show ?case by (simp add: interleaving_Nil_iff2)
next
  case (3 x xs y ys)
  then show ?case by (simp add: interleavings_Cons)
qed

lemma card_interleavings:
  assumes "set xs  set ys = {}"
  shows "card {zs. interleavings xs ys zs} = (length xs + length ys choose (length xs))"
using assms
proof (induct xs ys rule: two_mutual_lists_induction)
  case (1 ys)
  have "card {zs. interleavings [] ys zs} = card {ys}"
    by (simp add: interleaving_Nil_iff1)
  also have " = (length [] + length ys choose (length []))" by simp
  finally show ?case .
next
  case (2 xs)
  have "card {zs. interleavings xs [] zs} = card {xs}"
    by (simp add: interleaving_Nil_iff2)
  also have " = (length xs + length [] choose (length xs))" by simp
  finally show ?case .
next
  case (3 x xs y ys)
  have "card {zs. interleavings (x # xs) (y # ys) zs} =
    card ({x#zs|zs. interleavings xs (y#ys) zs}  {y#zs|zs. interleavings (x#xs) ys zs})"
    by (simp add: interleavings_Cons)
  also have " = card {x#zs|zs. interleavings xs (y#ys) zs} + card {y#zs|zs. interleavings (x#xs) ys zs}"
  proof -
    have "finite {x # zs |zs. interleavings xs (y # ys) zs}"
      by (simp add: finite_interleavings)
    moreover have "finite {y # zs |zs. interleavings (x # xs) ys zs}"
      by (simp add: finite_interleavings)
    moreover have "{x # zs |zs. interleavings xs (y # ys) zs}  {y # zs |zs. interleavings (x # xs) ys zs} = {}"
      using set (x # xs)  set (y # ys) = {} by auto
    ultimately show ?thesis by (simp add: card_Un_disjoint)
  qed
  also have " = card ((λzs. x # zs) ` {zs. interleavings xs (y # ys) zs}) +
    card ((λzs. y # zs) ` {zs. interleavings (x#xs) ys zs})"
    by (simp add: setcompr_eq_image)
  also have " = card {zs. interleavings xs (y # ys) zs} + card {zs. interleavings (x#xs) ys zs}"
    by (simp add: card_image)
  also have " = (length xs + length (y # ys) choose length xs) + (length (x # xs) + length ys choose length (x # xs))"
    using 3 by simp
  also have " = length (x # xs) + length (y # ys) choose length (x # xs)" by simp
  finally show ?case .
qed

subsection ‹Cardinality of Distinct Fixed-Length Lists from a Union of Two Sets›

lemma lists_distinct_union_by_interleavings:
  assumes "X  Y = {}"
  shows "{zs. length zs = n  distinct zs  set zs  X  Y} = do {
    k  {0..n};
    xs  {xs. length xs = k  distinct xs  set xs  X};
    ys  {ys. length ys = n - k  distinct ys  set ys  Y};
    {zs. interleavings xs ys zs}
  }" (is "?S = ?expr")
proof
  show "?S  ?expr"
  proof
    fix zs
    assume "zs  ?S"
    from this have "length zs = n" and "distinct zs" and "set zs  X  Y" by auto
    define xs where "xs = filter (λz. z  X) zs"
    define ys where "ys = filter (λz. z  Y) zs"
    have eq: "[zzs . z  Y] = [zzs . z  X]"
      using set zs  X  Y X  Y = {}
      by (auto intro: filter_cong)
    have "length xs  n  distinct xs  set xs  X"
      using length zs = n distinct zs unfolding xs_def by auto
    moreover have "length ys = n - length xs"
      using set zs  X  Y length zs = n
      unfolding xs_def ys_def eq
      by (metis diff_add_inverse sum_length_filter_compl)
    moreover have "distinct ys  set ys  Y"
      using distinct zs unfolding ys_def by auto
    moreover have "interleavings xs ys zs"
      using xs_def ys_def X  Y = {} set zs  X  Y
      by (simp add: interleavings_filter)
    ultimately show "zs  ?expr" by force
  qed
next
  show "?expr  ?S"
  proof
    fix zs
    assume "zs  ?expr"
    from this obtain xs ys where "length xs  n" "distinct xs" "set xs  X"
      and "length ys = n - length xs" "distinct ys" "set ys  Y" "interleavings xs ys zs" by auto
    have "length zs = n"
      using length xs  n length ys = n - length xs interleavings xs ys zs
      using interleavings_length by force
    moreover have "distinct zs"
      using distinct xs distinct ys interleavings xs ys zs set xs  X set ys  Y
      using X  Y = {} interleavings_distinct by fastforce
    moreover have "set zs  X  Y"
      using interleavings xs ys zs set xs  X set ys  Y interleavings_set by blast
    ultimately show "zs  ?S" by blast
  qed
qed

lemma interleavings_inject:
  assumes "(set xs  set xs')  (set ys  set ys') = {}"
  assumes "interleavings xs ys zs" "interleavings xs' ys' zs'"
  assumes "zs = zs'"
  shows "xs = xs'" and "ys = ys'"
proof -
  have "xs = filter (λz. z  set xs  set xs') zs"
    using (set xs  set xs')  (set ys  set ys') = {} interleavings xs ys zs
    by (auto intro: interleavings_filter_eq1[symmetric])
  also have " = filter (λz. z  set xs  set xs') zs'"
    using zs = zs' by simp
  also have " = xs'"
    using (set xs  set xs')  (set ys  set ys') = {} interleavings xs' ys' zs'
    by (auto intro: interleavings_filter_eq1)
  finally show "xs = xs'" by simp
  have "ys = filter (λz. z  set ys  set ys') zs"
    using (set xs  set xs')  (set ys  set ys') = {} interleavings xs ys zs
    by (auto intro: interleavings_filter_eq2[symmetric])
  also have " = filter (λz. z  set ys  set ys') zs'"
    using zs = zs' by simp
  also have " = ys'"
    using (set xs  set xs')  (set ys  set ys') = {} interleavings xs' ys' zs'
    by (auto intro: interleavings_filter_eq2)
  finally show "ys = ys'" .
qed

lemma injectivity:
  assumes "X  Y = {}"
  assumes "k  {0..n}  k'  {0..n}"
  assumes "(length xs = k  distinct xs  set xs  X)  (length xs' = k'  distinct xs'  set xs'  X)"
  assumes "(length ys = n - k  distinct ys  set ys  Y)  (length ys' = n - k'  distinct ys'  set ys'  Y)"
  assumes "interleavings xs ys zs  interleavings xs' ys' zs'"
  assumes "zs = zs'"
  shows "k = k'" and "xs = xs'" and "ys = ys'"
proof -
  from assms(1,3,4) have "(set xs  set xs')  (set ys  set ys') = {}" by blast
  from this assms(5) zs = zs' show "xs = xs'" and "ys = ys'"
    using interleavings_inject by fastforce+
  from this assms(3) show "k = k'" by auto
qed

lemma finite_length_distinct: "finite X   finite {xs. length xs = k  distinct xs  set xs  X}"
by(fast elim: rev_finite_subset[OF finite_subset_distinct])

lemma card_lists_distinct_length_eq_union:
  assumes "finite X" "finite Y" "X  Y = {}"
  shows "card {zs. length zs = n  distinct zs  set zs  X  Y} =
    (k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
  (is "card ?S = _")
proof -
  let ?expr = "do {
    k  {0..n};
    xs  {xs. length xs = k  distinct xs  set xs  X};
    ys  {ys. length ys = n - k  distinct ys  set ys  Y};
    {zs. interleavings xs ys zs}
  }"
  from X  Y = {} have "card ?S = card ?expr"
    by (simp add: lists_distinct_union_by_interleavings)
  let "?S  ?comp" = "?expr"
  {
    fix k
    assume "k  ?S"
    let "?expr" = "?comp k"
    let "?S  ?comp" = "?expr"
    from finite X have "finite ?S" by(rule finite_length_distinct)
    moreover {
      fix xs
      assume xs: "xs  ?S"
      let ?expr = "?comp xs"
      let "?S  ?comp" = ?expr
      from finite Y have "finite ?S" by(rule finite_length_distinct)
      moreover {
        fix ys
        assume ys: "ys  ?S"
        let ?expr = "?comp ys"
        have "finite ?expr"
          by (simp add: finite_interleavings)
        moreover have "card ?expr = (n choose k)"
          using xs ys X  Y = {} k  _
          by (subst card_interleavings) auto
        ultimately have "finite ?expr  card ?expr = (n choose k)" ..
      }
      moreover have "disjoint_family_on ?comp ?S"
        using k  {0..n} xs  {xs. length xs = k  distinct xs  set xs  X}
        by (injectivity_solver rule: injectivity(3)[OF X  Y = {}])
      moreover have "card ?S = ffact (n - k) (card Y)"
        using finite Y by (simp add: card_lists_distinct_length_eq)
      ultimately have "card ?expr = (n choose k) * ffact (n - k) (card Y)"
        by (subst card_bind_constant) auto
      moreover have "finite ?expr"
        using finite ?S by (auto intro!: finite_bind finite_interleavings)
      ultimately have "finite ?expr  card ?expr = (n choose k) * ffact (n - k) (card Y)"
        by blast
    }
    moreover have "disjoint_family_on ?comp ?S"
      using k  {0..n}
      by (injectivity_solver rule: injectivity(2)[OF X  Y = {}])
    moreover have "card ?S = ffact k (card X)"
      using finite X by (simp add: card_lists_distinct_length_eq)
    ultimately have "card ?expr = (n choose k) * ffact k (card X) * ffact (n - k) (card Y)"
      by (subst card_bind_constant) auto
    moreover have "finite ?expr"
      using finite ?S finite Y by (auto intro!: finite_bind finite_interleavings finite_length_distinct)
    ultimately have "finite ?expr  card ?expr = (n choose k) * ffact k (card X) * ffact (n - k) (card Y)"
      by blast
  }
  moreover have "disjoint_family_on ?comp ?S"
    by (injectivity_solver rule: injectivity(1)[OF X  Y = {}])
  ultimately have "card ?expr = (k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
    by (auto simp add: card_bind)
  from card _ = card ?expr this show ?thesis by simp
qed

lemma
  "ffact n (x + y) = (k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
proof -
  define X where "X = {..<x}"
  define Y where "Y = {x..<x+y}"
  have "finite X" and "card X = x" unfolding X_def by auto
  have "finite Y" and "card Y = y" unfolding Y_def by auto
  have "X  Y = {}" unfolding X_def Y_def by auto
  have "ffact n (x + y) = ffact n (card X + card Y)"
    using card X = x card Y = y by simp
  also have " = ffact n (card (X  Y))"
    using X  Y = {} finite X finite Y by (simp add: card_Un_disjoint)
  also have " = card {xs. length xs = n  distinct xs  set xs  X  Y}"
   using finite X finite Y by (simp add: card_lists_distinct_length_eq)
  also have " = (k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
    using X  Y = {} finite X finite Y by (simp add: card_lists_distinct_length_eq_union)
  also have " = (k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
    using card X = x card Y = y by simp
  finally show ?thesis .
qed

end