Session Falling_Factorial_Sum

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 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 auto
    moreover {
      fix xs
      assume xs: "xs  ?S"
      let ?expr = "?comp xs"
      let "?S  ?comp" = ?expr
      from ‹finite Y have "finite ?S" by auto
      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)
    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

Theory Falling_Factorial_Sum_Induction

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

section ‹Proving Falling Factorial of a Sum with Induction›

theory Falling_Factorial_Sum_Induction
imports
  Discrete_Summation.Factorials
begin

text ‹Note the potentially special copyright license condition of the following proof.›

lemma ffact_add_nat:
  "ffact n (x + y) = (k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  let ?s = "λk. (n choose k) * ffact k x * ffact (n - k) y"
  let ?t = "λk. ffact k x * ffact (Suc n - k) y"
  let ?u = "λk. ffact (Suc k) x * ffact (n - k) y"
  have "ffact (Suc n) (x + y) = (x + y - n) * ffact n (x + y)"
    by (simp add: ffact_Suc_rev_nat)
  also have " = (x + y - n) * (k = 0..n. (n choose k) * ffact k x * ffact (n - k) y)"
    using Suc.hyps by simp
  also have " = (k = 0..n. ?s k * (x + y - n))"
    by (simp add: mult.commute sum_distrib_left)
  also have " = (k = 0..n. ?s k * ((y + k - n) + (x - k)))"
  proof -
    have "?s k * (x + y - n) = ?s k * ((y + k - n) + (x - k))" for k
      by (cases "k  x  n - k  y") (auto simp add: ffact_nat_triv)
    from this show ?thesis
      by (auto intro: sum.cong simp only: refl)
  qed
  also have " = (k = 0..n. (n choose k) * (?t k + ?u k))"
    by (auto intro!: sum.cong simp add: Suc_diff_le ffact_Suc_rev_nat) algebra
  also have " = (k = 0..n. (n choose k) * ?t k) + (k = 0..n. (n choose k) * ?u k)"
    by (simp add: sum.distrib add_mult_distrib2 mult.commute mult.left_commute)
  also have " = ?t 0 + (k = 0..n. (n choose k + (n choose Suc k)) * ?u k)"
  proof -
    have " = (?t 0 + (k = 0..n. (n choose Suc k) * ?u k)) + (k = 0..n. (n choose k) * ?u k)"
    proof -
      have "(k = Suc 0..n. (n choose k) * ?t k) = (k = 0..n. (n choose Suc k) * ?u k)"
      proof -
        have "(k = Suc 0..n. (n choose k) * ?t k) = (k = Suc 0..Suc n. (n choose k) * ?t k)"
          by simp
        also have " = (sum ((λk. (n choose k) * ?t k) o Suc) {0..n})"
          by (simp only: sum.reindex[symmetric, of Suc] inj_Suc image_Suc_atLeastAtMost)
        also have " = (k = 0..n. (n choose Suc k) * ?u k)"
          by simp
        finally show ?thesis .
      qed
      from this show ?thesis
        by (simp add: sum.atLeast_Suc_atMost[of _ _ "λk. (n choose k) * ?t k"])
    qed
    also have " = ?t 0 + (k = 0..n. (n choose k + (n choose Suc k)) * ?u k)"
      by (simp add: distrib_right sum.distrib)
    finally show ?thesis .
  qed
  also have " = (k = 0..Suc n. (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
  proof -
    let ?v = "λk. (Suc n choose k) * ffact k x * ffact (Suc n - k) y"
    have " = ?v 0 + (k = 0..n. (Suc n choose (Suc k)) * ?u k)"
      by simp
    also have " = ?v 0 + (k = Suc 0..Suc n. ?v k)"
      by (simp only: sum.shift_bounds_cl_Suc_ivl diff_Suc_Suc mult.assoc)
    also have " = (k = 0..Suc n. (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
      by (simp add: sum.atLeast_Suc_atMost)
    finally show ?thesis .
  qed
  finally show ?case .
qed

(* TODO: what's the right class here? *)
lemma ffact_add:
  fixes x y :: "'a::{ab_group_add, comm_semiring_1_cancel, ring_1}"
  shows "ffact n (x + y) = (k=0..n. of_nat (n choose k) * ffact k x * ffact (n - k) y)"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  let ?s = "λk. of_nat (n choose k) * ffact k x * ffact (n - k) y"
  let ?t = "λk. ffact k x * ffact (Suc n - k) y"
  let ?u = "λk. ffact (Suc k) x * ffact (n - k) y"
  have "ffact (Suc n) (x + y) = (x + y - of_nat n) * ffact n (x + y)"
    by (simp add: ffact_Suc_rev)
  also have " = (x + y - of_nat n) * (k = 0..n. of_nat (n choose k) * ffact k x * ffact (n - k) y)"
    using Suc.hyps by simp
  also have " = (k = 0..n. ?s k * (x + y - of_nat n))"
    by (simp add: mult.commute sum_distrib_left)
  also have " = (k = 0..n. ?s k * ((y + of_nat k - of_nat n) + (x - of_nat k)))"
    by (auto intro: sum.cong simp add: diff_add_eq add_diff_eq add.commute)
  also have " = (k = 0..n. of_nat (n choose k) * (?t k + ?u k))"
  proof -
    {
      fix k
      assume "k  n"
      have "?u k = ffact k x * ffact (n - k) y * (x - of_nat k)"
        by (simp add: ffact_Suc_rev Suc_diff_le of_nat_diff mult.commute mult.left_commute)
      moreover from k  n have "?t k = ffact k x * ffact (n - k) y * (y + of_nat k - of_nat n)"
        by (simp add: ffact_Suc_rev Suc_diff_le of_nat_diff diff_diff_eq2 mult.commute mult.left_commute)
      ultimately have
        "?s k * ((y + of_nat k - of_nat n) + (x - of_nat k)) = of_nat (n choose k) * (?t k + ?u k)"
        by (metis (no_types, lifting) distrib_left mult.assoc)
    }
    from this show ?thesis by (auto intro: sum.cong)
  qed
  also have " = (k = 0..n. of_nat (n choose k) * ?t k) + (k = 0..n. of_nat (n choose k) * ?u k)"
    by (simp add: sum.distrib distrib_left mult.commute mult.left_commute)
  also have " = ?t 0 + (k = 0..n. of_nat (n choose k + (n choose Suc k)) * ?u k)"
  proof -
    have " = (?t 0 + (k = 0..n. of_nat (n choose Suc k) * ?u k)) + (k = 0..n. of_nat (n choose k) * ?u k)"
    proof -
      have "(k = Suc 0..n. of_nat (n choose k) * ?t k) = (k = 0..n. of_nat (n choose Suc k) * ?u k)"
      proof -
        have "(k = Suc 0..n. of_nat (n choose k) * ?t k) = (k = Suc 0..Suc n. of_nat (n choose k) * ?t k)"
          by (simp add: binomial_eq_0)
        also have " = (sum ((λk. of_nat (n choose k) * ?t k) o Suc) {0..n})"
          by (simp only: sum.reindex[symmetric, of Suc] inj_Suc image_Suc_atLeastAtMost)
        also have " = (k = 0..n. of_nat (n choose Suc k) * ?u k)"
          by simp
        finally show ?thesis .
      qed
      from this show ?thesis
        by (simp add: sum.atLeast_Suc_atMost[of _ _ "λk. of_nat (n choose k) * ?t k"])
    qed
    also have " = ?t 0 + (k = 0..n. of_nat (n choose k + (n choose Suc k)) * ?u k)"
      by (simp add: distrib_right sum.distrib)
    finally show ?thesis .
  qed
  also have " = (k = 0..Suc n. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
  proof -
    let ?v = "λk. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y"
    have " = ?v 0 + (k = 0..n. of_nat (Suc n choose (Suc k)) * ?u k)"
      by simp
    also have " = ?v 0 + (k = Suc 0..Suc n. ?v k)"
      by (simp only: sum.shift_bounds_cl_Suc_ivl diff_Suc_Suc mult.assoc)
    also have " = (k = 0..Suc n. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
      by (simp add: sum.atLeast_Suc_atMost)
    finally show ?thesis .
  qed
  finally show ?case .
qed

end

Theory Falling_Factorial_Sum_Vandermonde

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

section ‹Proving Falling Factorial of a Sum with Vandermonde Identity›

theory Falling_Factorial_Sum_Vandermonde
imports
  "Discrete_Summation.Factorials"
begin

text ‹Note the potentially special copyright license condition of the following proof.›

lemma ffact_add_nat:
  shows "ffact k (n + m) = (ik. (k choose i) * ffact i n * ffact (k - i) m)"
proof -
  have "ffact k (n + m) = fact k * ((n + m) choose k)"
    by (simp only: ffact_eq_fact_mult_binomial)
  also have " = fact k * (ik. (n choose i) * (m choose (k - i)))"
    by (simp only: vandermonde)
  also have " = (ik. fact k * (n choose i) * (m choose (k - i)))"
    by (simp add: sum_distrib_left field_simps)
  also have " = (ik. (fact i * fact (k - i) * (k choose i)) * (n choose i) * (m choose (k - i)))"
    by (simp add: binomial_fact_lemma)
  also have " = (ik. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))"
    by (auto intro: sum.cong)
  also have " = (ik. (k choose i) * ffact i n * ffact (k - i) m)"
    by (simp only: ffact_eq_fact_mult_binomial)
  finally show ?thesis .
qed

end