# 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 [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}" 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: "[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 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) = (∑i≤k. (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 * (∑i≤k. (n choose i) * (m choose (k - i)))" by (simp only: vandermonde) also have "… = (∑i≤k. fact k * (n choose i) * (m choose (k - i)))" by (simp add: sum_distrib_left field_simps) also have "… = (∑i≤k. (fact i * fact (k - i) * (k choose i)) * (n choose i) * (m choose (k - i)))" by (simp add: binomial_fact_lemma) also have "… = (∑i≤k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))" by (auto intro: sum.cong) also have "… = (∑i≤k. (k choose i) * ffact i n * ffact (k - i) m)" by (simp only: ffact_eq_fact_mult_binomial) finally show ?thesis . qed end