# Theory Falling_Factorial_Sum.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›

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
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

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

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 [z←zs . z ∈ X] [z←zs . z ∈ Y] zs"
using assms by (induct zs) (auto intro: interleavings.intros)

lemma interleavings_filter_eq1:
assumes "interleavings xs ys zs"
assumes "(∀x∈set xs. P x) ∧ (∀y∈set 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 "(∀x∈set xs. ¬ P x) ∧ (∀y∈set 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}"
also have "… = (length [] + length ys choose (length []))" by simp
finally show ?case .
next
case (2 xs)
have "card {zs. interleavings xs [] zs} = card {xs}"
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})"
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}"
moreover have "finite {y # zs |zs. interleavings (x # xs) ys zs}"
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})"
also have "… = card {zs. interleavings xs (y # ys) zs} + card {zs. interleavings (x#xs) ys zs}"
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: "[z←zs . z ∈ Y] = [z←zs . 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
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›
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"
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"
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))"
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
```