# Theory Khovanskii

```section‹Khovanskii's Theorem›

text‹We formalise the proof of an important theorem in additive combinatorics due to Khovanskii,
attesting that the cardinality of the set of all sums of \$n\$ many elements of \$A\$,
where \$A\$ is a finite subset of an abelian group, is a polynomial in \$n\$ for all sufficiently large \$n\$.
We follow a proof due to Nathanson and Ruzsa as presented in the notes
``Introduction to Additive Combinatorics'' by Timothy Gowers for the University of Cambridge.›

theory Khovanskii
imports
FiniteProduct
"Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality"
"Bernoulli.Bernoulli"               ― ‹sums of a fixed power are polynomials›
"HOL-Analysis.Weierstrass_Theorems" ― ‹needed for polynomial function›
"HOL-Library.List_Lenlexorder"      ― ‹lexicographic ordering for the type @{typ ‹nat list›}›
begin

text ‹The sum of the elements of a list›
abbreviation "σ ≡ sum_list"

text ‹Related to the nsets of Ramsey.thy, but simpler›
definition finsets :: "['a set, nat] ⇒ 'a set set"
where "finsets A n ≡ {N. N ⊆ A ∧ card N = n}"

lemma card_finsets: "finite N ⟹ card (finsets N k) = card N choose k"

lemma sorted_map_plus_iff [simp]:
shows "sorted (map ((+) a) xs) ⟷ sorted xs"
by (induction xs) auto

lemma distinct_map_plus_iff [simp]:
shows "distinct (map ((+) a) xs) ⟷ distinct xs"
by (induction xs) auto

subsection ‹Arithmetic operations on lists, pointwise on the elements›

text ‹Weak type class properties.
Cancellation is difficult to arrange because of complications when lists differ in length.›

instantiation list :: (plus) plus
begin
definition "plus_list ≡ map2 (+)"
instance..
end

lemma length_plus_list [simp]:
fixes xs :: "'a::plus list"
shows "length (xs+ys) = min (length xs) (length ys)"

lemma plus_Nil [simp]: "[] + xs = []"

lemma plus_Cons: "(y # ys) + (x # xs) = (y+x) # (ys+xs)"

lemma nth_plus_list [simp]:
fixes xs :: "'a::plus list"
assumes "i < length xs" "i < length ys"
shows "(xs+ys)!i = xs!i + ys!i"

instantiation list :: (minus) minus
begin
definition "minus_list ≡ map2 (-)"
instance..
end

lemma length_minus_list [simp]:
fixes xs :: "'a::minus list"
shows "length (xs-ys) = min (length xs) (length ys)"

lemma minus_Nil [simp]: "[] - xs = []"

lemma minus_Cons: "(y # ys) - (x # xs) = (y-x) # (ys-xs)"

lemma nth_minus_list [simp]:
fixes xs :: "'a::minus list"
assumes "i < length xs" "i < length ys"
shows "(xs-ys)!i = xs!i - ys!i"

proof
have "map2 (+) (map2 (+) xs ys) zs = map2 (+) xs (map2 (+) ys zs)" for xs ys zs :: "'a list"
proof (induction xs arbitrary: ys zs)
case (Cons x xs)
show ?case
proof (cases "ys=[] ∨ zs=[]")
case False
then obtain y ys' z zs' where "ys = y#ys'" "zs = z # zs'"
by (meson list.exhaust)
then show ?thesis
qed auto
qed auto
then show "a + b + c = a + (b + c)" for a b c :: "'a list"
by (auto simp: plus_list_def)
next
have "map2 (+) xs ys = map2 (+) ys xs" for xs ys :: "'a list"
proof (induction xs arbitrary: ys)
case (Cons x xs)
show ?case
proof (cases ys)
case (Cons y ys')
then show ?thesis
qed auto
qed auto
then show "a + b = b + a" for a b :: "'a list"
by (auto simp: plus_list_def)
qed

subsection ‹The pointwise ordering on two equal-length lists of natural numbers›

text ‹Gowers uses the usual symbol (\$\le\$) for his pointwise ordering.
In our development, \$\le\$ is the lexicographic ordering and \$\unlhd\$ is the pointwise ordering.›

definition pointwise_le :: "[nat list, nat list] ⇒ bool" (infixr "⊴" 50 )
where "x ⊴ y ≡ list_all2 (≤) x y"

definition pointwise_less :: "[nat list, nat list] ⇒ bool" (infixr "⊲" 50 )
where "x ⊲ y ≡ x ⊴ y ∧ x ≠ y"

lemma pointwise_le_iff_nth:
"x ⊴ y ⟷ length x = length y ∧ (∀i < length x. x!i ≤ y!i)"

lemma pointwise_le_iff:
"x ⊴ y ⟷ length x = length y ∧ (∀(i,j) ∈ set (zip x y). i≤j)"

lemma pointwise_append_le_iff [simp]: "u@x ⊴ u@y ⟷ x ⊴ y"
by (auto simp: pointwise_le_iff_nth nth_append)

lemma pointwise_le_refl [iff]: "x ⊴ x"

lemma pointwise_le_antisym: "⟦x ⊴ y; y ⊴ x⟧ ⟹ x=y"
by (metis antisym list_all2_antisym pointwise_le_def)

lemma pointwise_le_trans: "⟦x ⊴ y; y ⊴ z⟧ ⟹ x ⊴ z"
by (smt (verit, del_insts) le_trans list_all2_trans pointwise_le_def)

lemma pointwise_le_Nil [simp]: "Nil ⊴ x ⟷ x = Nil"

lemma pointwise_le_Nil2 [simp]: "x ⊴ Nil ⟷ x = Nil"

lemma pointwise_le_iff_less_equal: "x ⊴ y ⟷ x ⊲ y ∨ x = y"
using pointwise_less_def by blast

lemma pointwise_less_iff:
"x ⊲ y ⟷ x ⊴ y ∧ (∃(i,j) ∈ set (zip x y). i<j)"
using list_eq_iff_zip_eq pointwise_le_iff pointwise_less_def by fastforce

lemma pointwise_less_iff2: "x ⊲ y ⟷ x ⊴ y ∧ (∃k < length x. x!k <y ! k)"
unfolding pointwise_less_def pointwise_le_iff_nth
by (fastforce intro!: nth_equalityI)

lemma pointwise_less_Nil [simp]: "¬ Nil ⊲ x"

lemma pointwise_less_Nil2 [simp]: "¬ x ⊲ Nil"

lemma zero_pointwise_le_iff [simp]: "replicate r 0 ⊴ x ⟷ length x = r"
by (auto simp: pointwise_le_iff_nth)

lemma pointwise_le_imp_σ:
assumes "xs ⊴ ys" shows "σ xs ≤ σ ys"
using assms
proof (induction ys arbitrary: xs)
case Nil
then show ?case
next
case (Cons y ys)
then obtain x xs' where "x≤y" "xs = x#xs'" "xs' ⊴ ys"
by (auto simp: pointwise_le_def list_all2_Cons2)
then show ?case
qed

lemma sum_list_plus:
assumes "length xs = length ys" shows "σ (xs + ys) = σ xs + σ ys"

lemma sum_list_minus:
assumes "xs ⊴ ys" shows "σ (ys - xs) = σ ys - σ xs"
using assms
proof (induction ys arbitrary: xs)
case (Cons y ys)
then obtain x xs' where "x≤y" "xs = x#xs'" "xs' ⊴ ys"
by (auto simp: pointwise_le_def list_all2_Cons2)
then show ?case
using pointwise_le_imp_σ by (auto simp: Cons minus_Cons)
qed (auto simp: in_set_conv_nth)

subsection ‹Pointwise minimum and maximum of a set of lists›

definition min_pointwise :: "[nat, nat list set] ⇒ nat list"
where "min_pointwise ≡ λr U. map (λi. Min ((λu. u!i) ` U)) [0..<r]"

lemma min_pointwise_le: "⟦u ∈ U; finite U⟧ ⟹ min_pointwise (length u) U ⊴ u"

lemma min_pointwise_ge_iff:
assumes "finite U" "U ≠ {}" "⋀u. u ∈ U ⟹ length u = r" "length x = r"
shows "x ⊴ min_pointwise r U ⟷ (∀u ∈ U. x ⊴ u)"
by (auto simp: min_pointwise_def pointwise_le_iff_nth assms)

definition max_pointwise :: "[nat, nat list set] ⇒ nat list"
where "max_pointwise ≡ λr U. map (λi. Max ((λu. u!i) ` U)) [0..<r]"

lemma max_pointwise_ge: "⟦u ∈ U; finite U⟧ ⟹ u ⊴ max_pointwise (length u) U"

lemma max_pointwise_le_iff:
assumes "finite U" "U ≠ {}" "⋀u. u ∈ U ⟹ length u = r" "length x = r"
shows "max_pointwise r U ⊴ x ⟷ (∀u ∈ U. u ⊴ x)"
by (auto simp: max_pointwise_def pointwise_le_iff_nth assms)

lemma max_pointwise_mono:
assumes "X' ⊆ X" "finite X" "X' ≠ {}"
shows  "max_pointwise r X' ⊴ max_pointwise r X"
using assms by (simp add: max_pointwise_def pointwise_le_iff_nth Max_mono image_mono)

lemma pointwise_le_plus: "⟦xs ⊴ ys; length ys ≤ length zs⟧ ⟹ xs ⊴ ys+zs"
proof (induction xs arbitrary: ys zs)
case (Cons x xs)
then obtain y ys' z zs' where "ys = y#ys'" "zs = z#zs'"
unfolding pointwise_le_iff by (metis Suc_le_length_iff le_refl length_Cons)
with Cons show ?case
by (auto simp: plus_list_def pointwise_le_def)

lemma pairwise_minus_cancel: "⟦z ⊴ x;  z ⊴ y; x - z = y - z⟧ ⟹ x = y"
unfolding pointwise_le_iff_nth by (metis eq_diff_iff nth_equalityI nth_minus_list)

subsection ‹A locale to fix the finite subset @{term "A ⊆ G"}›

fixes A :: "'a set"
assumes AsubG: "A ⊆ G" and finA: "finite A"

begin

text ‹finite products of a group element›
definition Gmult :: "'a ⇒ nat ⇒ 'a"
where "Gmult a n ≡ (((⊕)a) ^^ n) 𝟬"

lemma Gmult_0 [simp]: "Gmult a 0 = 𝟬"

lemma Gmult_1 [simp]: "a ∈ G ⟹ Gmult a (Suc 0) = a"

lemma Gmult_Suc [simp]: "Gmult a (Suc n) = a ⊕ Gmult a n"

lemma Gmult_in_G [simp,intro]: "a ∈ G ⟹ Gmult a n ∈ G"
by (induction n) auto

assumes "a ∈ G"
shows "Gmult a (m+n) = Gmult a m ⊕ Gmult a n"
by (induction m) (use assms local.associative in fastforce)+

assumes "a ∈ G"
shows "Gmult a (n+k) ⊖ Gmult a n = Gmult a k"

lemma Gmult_diff:
assumes "a ∈ G" "n≤m"
shows "Gmult a m ⊖ Gmult a n = Gmult a (m-n)"

text ‹Mapping elements of @{term A} to their numeric subscript›
abbreviation "idx ≡ to_nat_on A"

text ‹The elements of @{term A} in order›
definition aA :: "'a list"
where "aA ≡ map (from_nat_into A) [0..<card A]"

definition α :: "nat list ⇒ 'a"
where "α ≡ λx. fincomp (λi. Gmult (aA!i) (x!i)) {..<card A}"

text ‹The underlying assumption is @{term "length y = length x"}›
definition useless:: "nat list  ⇒ bool"
where "useless x ≡ ∃y < x. σ y = σ x ∧ α y = α x ∧ length y = length x"

abbreviation "useful x ≡ ¬ useless x"

lemma alpha_replicate_0 [simp]: "α (replicate (card A) 0) = 𝟬"
by (auto simp: α_def intro: fincomp_unit_eqI)

lemma idx_less_cardA:
assumes "a ∈ A" shows "idx a < card A"
by (metis assms bij_betw_def finA imageI lessThan_iff to_nat_on_finite)

lemma aA_idx_eq [simp]:
assumes "a ∈ A" shows "aA ! (idx a) = a"
by (simp add: aA_def assms countable_finite finA idx_less_cardA)

lemma set_aA: "set aA = A"
using bij_betw_from_nat_into_finite [OF finA]
by (simp add: aA_def atLeast0LessThan bij_betw_def)

lemma nth_aA_in_G [simp]: "i < card A ⟹ aA!i ∈ G"
using AsubG aA_def set_aA by auto

lemma alpha_in_G [iff]: "α x ∈ G"
using nth_aA_in_G fincomp_closed by (simp add: α_def)

lemma Gmult_in_PiG [simp]: "(λi. Gmult (aA!i) (f i)) ∈ {..<card A} → G"
by simp

lemma alpha_plus:
assumes "length x = card A" "length y = card A"
shows "α (x + y) = α x ⊕ α y"
proof -
have "α (x + y) = fincomp (λi. Gmult (aA!i) (map2 (+) x y!i)) {..<card A}"
also have "… = fincomp (λi. Gmult (aA!i) (x!i + y!i)) {..<card A}"
by (intro fincomp_cong'; simp add: assms)
also have "… = fincomp (λi. Gmult (aA!i) (x!i) ⊕ Gmult (aA!i) (y!i)) {..<card A}"
also have "… = α x ⊕ α y"
finally show ?thesis .
qed

lemma alpha_minus:
assumes "y ⊴ x" "length y = card A"
shows "α (x - y) = α x ⊖ α y"
proof -
have "α (x - y) = fincomp (λi. Gmult (aA!i) (map2 (-) x y!i)) {..<card A}"
also have "… = fincomp (λi. Gmult (aA!i) (x!i - y!i)) {..<card A}"
using assms by (intro fincomp_cong') (auto simp: pointwise_le_iff)
also have "… = fincomp (λi. Gmult (aA!i) (x!i) ⊖ Gmult (aA!i) (y!i)) {..<card A}"
using assms
by (intro fincomp_cong') (simp add: pointwise_le_iff_nth Gmult_diff)+
also have "… = α x ⊖ α y"
by (simp add: α_def fincomp_comp fincomp_inverse)
finally show ?thesis .
qed

subsection ‹Adding one to a list element›

definition list_incr :: "nat ⇒ nat list ⇒ nat list"
where "list_incr i x ≡ x[i := Suc (x!i)]"

lemma list_incr_Nil [simp]: "list_incr i [] = []"

lemma list_incr_Cons [simp]: "list_incr (Suc i) (k#ks) = k # list_incr i ks"

lemma sum_list_incr [simp]: "i < length x ⟹ σ (list_incr i x) = Suc (σ x)"
by (auto simp: list_incr_def sum_list_update)

lemma length_list_incr [simp]: "length (list_incr i x) = length x"
by (auto simp: list_incr_def)

lemma nth_le_list_incr: "i < card A ⟹ x!i ≤ list_incr (idx a) x!i"
unfolding list_incr_def
by (metis Suc_leD linorder_not_less list_update_beyond nth_list_update_eq nth_list_update_neq order_refl)

lemma list_incr_nth_diff: "i < length x ⟹ list_incr j x!i - x!i = (if i = j then 1 else 0)"

subsection ‹The set of all @{term r}-tuples that sum to @{term n}›

definition length_sum_set :: "nat ⇒ nat ⇒ nat list set"
where "length_sum_set r n ≡ {x. length x = r ∧ σ x = n}"

lemma length_sum_set_Nil [simp]: "length_sum_set 0 n = (if n=0 then {[]} else {})"
by (auto simp: length_sum_set_def)

lemma length_sum_set_Suc [simp]: "k#ks ∈ length_sum_set (Suc r) n ⟷ (∃m. ks ∈ length_sum_set r m ∧ n = m+k)"
by (auto simp: length_sum_set_def)

lemma length_sum_set_Suc_eqpoll: "length_sum_set (Suc r) n ≈ Sigma {..n} (λi. length_sum_set r (n-i))" (is "?L ≈ ?R")
unfolding eqpoll_def
proof
let ?f = "(λl. (hd l, tl l))"
show "bij_betw ?f ?L ?R"
proof (intro bij_betw_imageI)
show "inj_on ?f ?L"
by (force simp: inj_on_def length_sum_set_def intro: list.expand)
show "?f ` ?L = ?R"
by (force simp: length_sum_set_def length_Suc_conv)
qed
qed

lemma finite_length_sum_set: "finite (length_sum_set r n)"
proof (induction r arbitrary: n)
case 0
then show ?case
by (auto simp: length_sum_set_def)
next
case (Suc r)
then show ?case
using length_sum_set_Suc_eqpoll eqpoll_finite_iff by blast
qed

lemma card_length_sum_set: "card (length_sum_set (Suc r) n) = (∑i≤n. card (length_sum_set r (n-i)))"
proof -
have "card (length_sum_set (Suc r) n) = card (Sigma {..n} (λi. length_sum_set r (n-i)))"
by (metis eqpoll_finite_iff eqpoll_iff_card finite_length_sum_set length_sum_set_Suc_eqpoll)
also have "… = (∑i≤n. card (length_sum_set r (n-i)))"
finally show ?thesis .
qed

lemma sum_up_index_split':
assumes "N ≤ n" shows "(∑i≤n. f i) = (∑i≤n-N. f i) + (∑i=Suc (n-N)..n. f i)"

lemma sum_invert: "N ≤ n ⟹ (∑i = Suc (n - N)..n. f (n - i)) = (∑j<N. f j)"
proof (induction N)
case (Suc N)
then show ?case
apply (auto simp: Suc_diff_Suc)
by (metis sum.atLeast_Suc_atMost Suc_leD add.commute diff_diff_cancel diff_le_self)
qed auto

lemma real_polynomial_function_length_sum_set:
"∃p. real_polynomial_function p ∧ (∀n>0. real (card (length_sum_set r n)) = p (real n))"
proof (induction r)
case 0
have "∀n>0. real (card (length_sum_set 0 n)) = 0"
by auto
then show ?case
by blast
next
case (Suc r)
then obtain p where poly: "real_polynomial_function p"
and p: "⋀n. n>0 ⟹ real (card (length_sum_set r n)) = p (real n)"
by blast
then obtain a n where p_eq: "p = (λx. ∑i≤n. a i * x ^ i)"
using real_polynomial_function_iff_sum by auto
define q where "q ≡ λx. ∑j≤n. a j * ((bernpoly (Suc j) (1 + x) - bernpoly (Suc j) 0)
/ (1 + real j) - 0 ^ j)"
have rp_q: "real_polynomial_function q"
by (fastforce simp: bernpoly_def p_eq q_def)
have q_eq: "(∑x≤k-1. p (k-x)) = q k" if "k>0" for k::nat
proof -
have "(∑x≤k-1. p (k-x)) = (∑j≤n. a j * ((∑x≤k. real x ^ j) - 0^j))"
using that
by (simp add: p_eq sum.swap flip: sum_distrib_left sum_diff_split[where f="λi. real i ^ _"])
also have "… = q k"
finally show ?thesis .
qed
define p' where "p' ≡ λx. q x + real (card (length_sum_set r 0))"
have "real_polynomial_function p'"
using rp_q by (force simp: p'_def)
moreover have "(∑x≤n - Suc 0. p (real (n - x))) +
real (card (length_sum_set r 0)) = p' (real n)" if "n>0" for n
using that q_eq by (auto simp: p'_def)
ultimately show ?case
unfolding card_length_sum_set
by (force simp: sum_up_index_split' [of 1] p sum_invert)
qed

lemma all_zeroes_replicate: "length_sum_set r 0 = {replicate r 0}"
by (auto simp: length_sum_set_def replicate_eqI)

lemma length_sum_set_Suc_eq_UN: "length_sum_set r (Suc n) = (⋃i<r. list_incr i ` length_sum_set r n)"
proof -
have "∃i<r. x ∈ list_incr i ` length_sum_set r n"
if "σ x = Suc n" and "r = length x" for x
proof -
have "x ≠ replicate r 0"
using that by (metis sum_list_replicate Zero_not_Suc mult_zero_right)
then obtain i where i: "i < r" "x!i ≠ 0"
by (metis ‹r = length x› in_set_conv_nth replicate_eqI)
with that have "x[i := x!i - 1] ∈ length_sum_set r n"
with i that show ?thesis
unfolding list_incr_def by force
qed
then show ?thesis
by (auto simp: length_sum_set_def Bex_def)
qed

lemma alpha_list_incr:
assumes "a ∈ A" "x ∈ length_sum_set (card A) n"
shows "α (list_incr (idx a) x) = a ⊕ α x"
proof -
have lenx: "length x = card A"
using assms length_sum_set_def by blast
have "α (list_incr (idx a) x) ⊖ α x = fincomp (λi. Gmult (aA!i) (list_incr (idx a) x!i) ⊖ Gmult (aA!i) (x!i)) {..<card A}"
by (simp add: α_def fincomp_comp fincomp_inverse)
also have "… = fincomp (λi. Gmult (aA!i) (list_incr (idx a) x!i - x!i)) {..<card A}"
by (intro fincomp_cong; simp add: Gmult_diff nth_le_list_incr)
also have "… = fincomp (λi. if i = idx a then (aA!i) else 𝟬) {..<card A}"
by (intro fincomp_cong'; simp add: list_incr_nth_diff lenx)
also have "… = a"
using assms by (simp add: fincomp_singleton_swap idx_less_cardA)
finally have "α (list_incr (idx a) x) ⊖ α x = a" .
then show ?thesis
by (metis alpha_in_G associative inverse_closed invertible invertible_left_inverse right_unit)
qed

lemma sumset_iterated_enum:
defines "r ≡ card A"
shows "sumset_iterated A n = α ` length_sum_set r n"
proof (induction n)
case 0
then show ?case
next
case (Suc n)
have eq: "{..<r} = idx ` A"
by (metis bij_betw_def finA r_def to_nat_on_finite)
have "sumset_iterated A (Suc n) = (⋃a∈A. (λi. a ⊕ α i) ` length_sum_set r n)"
using AsubG by (auto simp: Suc sumset)
also have "… = (⋃a∈A. (λi. α (list_incr (idx a) i)) ` length_sum_set r n)"
also have "… = α ` length_sum_set r (Suc n)"
by (simp add: image_UN image_comp length_sum_set_Suc_eq_UN eq)
finally show ?case .
qed

subsection ‹Lemma 2.7 in Gowers's notes›

text‹The following lemma corresponds to a key fact about the cardinality of the set of all sums of
\$n\$ many elements of \$A\$, stated before Gowers's Lemma 2.7.›

lemma card_sumset_iterated_length_sum_set_useful:
defines "r ≡ card A"
shows "card(sumset_iterated A n) = card (length_sum_set r n ∩ {x. useful x})"
(is "card ?L = card ?R")
proof -
have "α x ∈ α ` (length_sum_set r n ∩ {x. useful x})"
if "x ∈ length_sum_set r n" for x
proof -
define y where "y ≡ LEAST y. y ∈ length_sum_set r n ∧ α y = α x"
have y: "y ∈ length_sum_set (card A) n ∧ α y = α x"
by (metis (mono_tags, lifting) LeastI r_def y_def that)
moreover
have "useful y"
proof (clarsimp simp: useless_def)
show False
if "σ z = σ y" "length z = length y" and "z < y" "α z = α y" for z
using that Least_le length_sum_set_def not_less_Least r_def y y_def by fastforce
qed
ultimately show ?thesis
unfolding image_iff length_sum_set_def r_def by (smt (verit) Int_Collect)
qed
then have "sumset_iterated A n = α ` (length_sum_set r n ∩ {x. useful x})"
by (auto simp: sumset_iterated_enum length_sum_set_def r_def)
moreover have "inj_on α (length_sum_set r n ∩ {x. useful x})"
apply (simp add: image_iff length_sum_set_def r_def inj_on_def useless_def Ball_def)
by (metis linorder_less_linear)
ultimately show ?thesis
qed

text‹The following lemma corresponds to Lemma 2.7 in Gowers's notes.›

lemma useless_leq_useless:
defines "r ≡ card A"
assumes "useless x" and "x ⊴ y" and "length x = r"
shows "useless y "
proof -
have leny: "length y = r"
using pointwise_le_iff assms by auto
obtain x' where "x'< x" and σx': "σ x' = σ x" and αx': "α x' = α x" and lenx': "length x' = length x"
using assms useless_def by blast
obtain i where "i < card A" and xi: "x'!i < x!i" and takex': "take i x' = take i x"
using ‹x'<x› lenx' assms by (auto simp: list_less_def lenlex_def elim!: lex_take_index)
define y' where "y' ≡ y+x'-x"
have leny': "length y' = length y"
using assms lenx' pointwise_le_iff  by (simp add: y'_def)
have "x!i ≤ y!i"
using ‹x ⊴ y› ‹i < card A› assms by (simp add: pointwise_le_iff_nth)
then have "y'!i < y!i"
using ‹i < card A› assms lenx' xi pointwise_le_iff by (simp add: y'_def plus_list_def minus_list_def)
moreover have "take i y' = take i y"
proof (intro nth_equalityI)
show "length (take i y') = length (take i y)"
show "⋀k. k < length (take i y') ⟹ take i y' ! k = take i y!k"
using takex' by (simp add: y'_def plus_list_def minus_list_def take_map take_zip)
qed
ultimately have "y' < y"
using leny' ‹i < card A› assms pointwise_le_iff
by (auto simp: list_less_def lenlex_def lexord_lex lexord_take_index_conv)
moreover have "σ y' = σ y"
using assms
by (simp add: σx' lenx' leny pointwise_le_plus sum_list_minus sum_list_plus y'_def)
moreover have "α y' = α y"
using assms lenx' αx' leny
by (fastforce simp: y'_def pointwise_le_plus alpha_minus alpha_plus local.associative)
ultimately show ?thesis
using leny' useless_def by blast
qed

inductive_set minimal_elements for U
where "⟦x ∈ U; ⋀y. y ∈ U ⟹ ¬ y ⊲ x⟧ ⟹ x ∈ minimal_elements U"

lemma pointwise_less_imp_σ:
assumes "xs ⊲ ys" shows "σ xs < σ ys"
proof -
have eq: "length ys = length xs" and "xs ⊴ ys"
using assms by (auto simp: pointwise_le_iff pointwise_less_iff)
have "∀k<length xs. xs!k ≤ ys!k"
using ‹xs ⊴ ys› list_all2_nthD pointwise_le_def by auto
moreover have "∃k<length xs. xs!k < ys!k"
using assms pointwise_less_iff2 by force
ultimately show ?thesis
by (force simp: eq sum_list_sum_nth intro: sum_strict_mono_ex1)
qed

lemma wf_measure_σ: "wf (inv_image less_than σ)"
by blast

lemma WFP: "wfP (⊲)"
by (auto simp: wfP_def pointwise_less_imp_σ intro: wf_subset [OF wf_measure_σ])

text‹The following is a direct corollary of the above lemma, i.e. a corollary of
Lemma 2.7 in Gowers's notes.›

corollary useless_iff:
assumes "length x = card A"
shows "useless x ⟷ (∃x' ∈ minimal_elements (Collect useless). x' ⊴ x)"  (is "_=?R")
proof
assume "useless x"
obtain z where z: "useless z" "z ⊴ x" and zmin: "⋀y. y ⊲ z ⟹ y ⊴ x ⟹ useful y"
using wfE_min [to_pred, where Q = "{z. useless z ∧ z ⊴ x}", OF WFP]
by (metis (no_types, lifting) ‹useless x› mem_Collect_eq pointwise_le_refl)
then show ?R
by (smt (verit) mem_Collect_eq minimal_elements.intros pointwise_le_trans pointwise_less_def)
next
assume ?R
with useless_leq_useless minimal_elements.cases show "useless x"
by (metis assms mem_Collect_eq pointwise_le_iff)
qed

subsection ‹The set of minimal elements of a set of \$r\$-tuples is finite›

text‹The following general finiteness claim corresponds to Lemma 2.8 in Gowers's notes and is key to
the main proof.›

lemma minimal_elements_set_tuples_finite:
assumes Ur: "⋀x. x ∈ U ⟹ length x = r"
shows "finite (minimal_elements U)"
using assms
proof (induction r arbitrary: U)
case 0
then have "U ⊆ {[]}"
by auto
then show ?case
by (metis finite.simps minimal_elements.cases finite_subset subset_eq)
next
case (Suc r)
show ?case
proof (cases "U={}")
case True
with Suc.IH show ?thesis by blast
next
case False
then obtain u where u: "u ∈ U" and zmin: "⋀y. y ⊲ u ⟹ y ∉ U"
using wfE_min [to_pred, where Q = "U", OF WFP] by blast
define V where "V = {v ∈ U. ¬ u ⊴ v}"
define VF where "VF ≡ λi t. {v ∈ V. v!i = t}"
have [simp]: "length v = Suc r" if "v ∈ VF i t" for v i t
using that by (simp add: Suc.prems VF_def V_def)
have *: "∃i≤r. v!i < u!i" if "v ∈ V" for v
using that u Suc.prems
by (force simp: V_def pointwise_le_iff_nth not_le less_Suc_eq_le)
with u have "minimal_elements U ≤ insert u (⋃i≤r. ⋃t < u!i. minimal_elements (VF i t))"
by (force simp: VF_def V_def minimal_elements.simps pointwise_less_def)
moreover
have "finite (minimal_elements (VF i t))" if "i≤r" "t < u!i" for i t
proof -
define delete where "delete ≡ λv::nat list. take i v @ drop (Suc i) v" ― ‹deletion of @{term i}›
have len_delete[simp]: "length (delete u) = r" if "u ∈ VF i t" for u
using Suc.prems VF_def V_def ‹i ≤ r› delete_def that by auto
have nth_delete: "delete u!k = (if k<i then u!k else u!Suc k)" if "u ∈ VF i t" "k<r" for u k
using that by (simp add: delete_def nth_append)
have delete_le_iff [simp]: "delete u ⊴ delete v ⟷ u ⊴ v" if "u ∈ VF i t" "v ∈ VF i t" for u v
proof
assume "delete u ⊴ delete v"
then have "∀j. (j < i ⟶ u!j ≤ v!j) ∧ (j < r ⟶ i ≤ j ⟶ u!Suc j ≤ v!Suc j)"
using that ‹i ≤ r›
by (force simp: pointwise_le_iff_nth nth_delete split: if_split_asm cong: conj_cong)
then show "u ⊴ v"
using that ‹i ≤ r›
by (metis eq_iff le_Suc_eq less_Suc_eq_0_disj linorder_not_less)
next
assume "u ⊴ v" then show "delete u ⊴ delete v"
using that by (simp add: pointwise_le_iff_nth nth_delete)
qed
then have delete_eq_iff: "delete u = delete v ⟷ u = v" if "u ∈ VF i t" "v ∈ VF i t" for u v
by (metis that pointwise_le_antisym pointwise_le_refl)
have delete_less_iff: "delete u ⊲ delete v ⟷ u ⊲ v" if "u ∈ VF i t" "v ∈ VF i t" for u v
by (metis delete_le_iff pointwise_le_antisym pointwise_less_def that)
have "length (delete v) = r" if "v ∈ V" for v
using id_take_nth_drop Suc.prems V_def ‹i ≤ r› delete_def that by auto
then have "finite (minimal_elements (delete ` V))"
by (metis (mono_tags, lifting) Suc.IH image_iff)
moreover have "inj_on delete (minimal_elements (VF i t))"
by (simp add: delete_eq_iff inj_on_def minimal_elements.simps)
moreover have "delete ` (minimal_elements (VF i t)) ⊆ minimal_elements (delete ` (VF i t))"
by (auto simp: delete_less_iff minimal_elements.simps)
ultimately show ?thesis
by (metis (mono_tags, lifting) Suc.IH image_iff inj_on_finite len_delete)
qed
ultimately show ?thesis
by (force elim: finite_subset)
qed
qed

subsection ‹Towards Lemma 2.9 in Gowers's notes›

text ‹Increasing sequences›
fun augmentum :: "nat list ⇒ nat list"
where "augmentum [] = []"
| "augmentum (n#ns) = n # map ((+)n) (augmentum ns)"

definition dementum:: "nat list ⇒ nat list"
where "dementum xs ≡ xs - (0#xs)"

lemma dementum_Nil [simp]: "dementum [] = []"

lemma zero_notin_augmentum [simp]: "0 ∉ set ns ⟹ 0 ∉ set (augmentum ns)"
by (induction ns) auto

lemma length_augmentum [simp]:"length (augmentum xs) = length xs"
by (induction xs) auto

lemma sorted_augmentum [simp]: "0 ∉ set ns ⟹ sorted (augmentum ns)"
by (induction ns) auto

lemma distinct_augmentum [simp]: "0 ∉ set ns ⟹ distinct (augmentum ns)"
by (induction ns) (simp_all add: image_iff)

lemma augmentum_subset_sum_list: "set (augmentum ns) ⊆ {..σ ns}"
by (induction ns) auto

lemma sum_list_augmentum: "σ ns ∈ set (augmentum ns) ⟷ length ns > 0"
by (induction ns) auto

lemma length_dementum [simp]: "length (dementum xs) = length xs"

lemma sorted_imp_pointwise:
assumes "sorted (xs@[n])"
shows "0 # xs ⊴ xs @ [n]"
using assms
by (simp add: pointwise_le_iff_nth nth_Cons' nth_append sorted_append sorted_wrt_append sorted_wrt_nth_less)

lemma sum_list_dementum:
assumes "sorted (xs@[n])"
shows "σ (dementum (xs@[n])) = n"
proof -
have "dementum (xs@[n]) = (xs@[n]) - (0 # xs)"
by (rule nth_equalityI; simp add: nth_append dementum_def nth_Cons')
then show ?thesis
by (simp add: sum_list_minus sorted_imp_pointwise assms)
qed

lemma augmentum_cancel: "map ((+)k) (augmentum ns) - (k # map ((+)k) (augmentum ns)) = ns"
proof (induction ns arbitrary: k)
case Nil
then show ?case
by simp
next
case (Cons n ns)
have "(+) k ∘ (+) n = (+) (k+n)" by auto
then show ?case
qed

lemma dementum_augmentum [simp]:
assumes "0 ∉ set ns"
shows "(dementum ∘ sorted_list_of_set) ((set ∘ augmentum) ns) = ns" (is "?L ns = _")
using assms augmentum_cancel [of 0]
by (simp add: dementum_def map_idI sorted_list_of_set.idem_if_sorted_distinct)

lemma dementum_nonzero:
assumes ns: "sorted_wrt (<) ns" and 0: "0 ∉ set ns"
shows "0 ∉ set (dementum ns)"
unfolding dementum_def minus_list_def
using sorted_wrt_nth_less [OF ns] 0
by (auto simp: in_set_conv_nth image_iff set_zip nth_Cons' dest: leD)

lemma nth_augmentum [simp]: "i < length ns ⟹ augmentum ns!i = (∑j≤i. ns!j)"
proof (induction ns arbitrary: i)
case Nil
then show ?case
by simp
next
case (Cons a ns)
show ?case
proof (cases "i=0")
case False
then have "augmentum (a # ns)!i = a + sum ((!) ns) {..i-1}"
using Cons.IH Cons.prems by auto
also have "… = a + (∑j∈{0<..i}. ns!(j-1))"
using sum.reindex [of Suc "{..i - Suc 0}" "λj. ns!(j-1)", symmetric] False
by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost del: sum.cl_ivl_Suc)
also have "… = (∑j = 0..i. if j=0 then a else ns!(j-1))"
also have "… = sum ((!) (a # ns)) {..i}"
finally show ?thesis .
qed auto
qed

lemma augmentum_dementum [simp]:
assumes "0 ∉ set ns" "sorted ns"
shows "augmentum (dementum ns) = ns"
proof (rule nth_equalityI)
fix i
assume "i < length (augmentum (dementum ns))"
then have i: "i < length ns"
by simp
show "augmentum (dementum ns)!i = ns!i"
proof (cases "i=0")
case True
then show ?thesis
using nth_augmentum dementum_def i by auto
next
case False
have ns_le: "⋀j. ⟦0 < j; j ≤ i⟧ ⟹ ns ! (j - Suc 0) ≤ ns ! j"
using ‹sorted ns› i by (simp add: sorted_iff_nth_mono)
have "augmentum (dementum ns)!i = (∑j≤i. ns!j - (if j = 0 then 0 else ns!(j-1)))"
using i by (simp add: dementum_def nth_Cons')
also have "… = (∑j=0..i. if j = 0 then ns!0 else ns!j - ns!(j-1))"
by (smt (verit, del_insts) diff_zero sum.cong atMost_atLeast0)
also have "… = ns!0 + (∑j∈{0<..i}. ns!j - ns!(j-1))"
also have "… = ns!0 + ((∑j∈{0<..i}. ns!j) - (∑j∈{0<..i}. ns!(j-1)))"
by (auto simp: ns_le intro: sum_subtractf_nat)
also have "… = ns!0 + (∑j∈{0<..i}. ns!j) - (∑j∈{0<..i}. ns!(j-1))"
proof -
have "(∑j∈{0<..i}. ns ! (j - 1)) ≤ sum ((!) ns) {0<..i}"
by (metis One_nat_def greaterThanAtMost_iff ns_le sum_mono)
then show ?thesis by simp
qed
also have "… = ns!0 + (∑j∈{0<..i}. ns!j) - (∑j≤i-Suc 0. ns!j)"
using sum.reindex [of Suc "{..i - Suc 0}" "λj. ns!(j-1)", symmetric] False
also have "… = (∑j=0..i. ns!j) - (∑j≤i-Suc 0. ns!j)"
also have "… = (∑j=0..i-Suc 0. ns!j) + ns!i - (∑j≤i-Suc 0. ns!j)"
by (metis False Suc_pred less_Suc0 not_less_eq sum.atLeast0_atMost_Suc)
also have "… = ns!i"
finally show "augmentum (dementum ns)!i = ns!i" .
qed
qed auto

text‹The following lemma corresponds to Lemma 2.9 in Gowers's notes. The proof involves introducing
bijective maps between r-tuples that fulfill certain properties/r-tuples and subsets of naturals,
so as to show the cardinality claim.  ›

lemma bound_sum_list_card:
assumes "r > 0" and n: "n ≥ σ x'" and lenx': "length x' = r"
defines "S ≡ {x. x' ⊴ x ∧ σ x = n}"
shows "card S = (n - σ x' + r - 1) choose (r-1)"
proof-
define m where "m ≡ n - σ x'"
define f where "f ≡ λx::nat list. x - x'"
have f: "bij_betw f S (length_sum_set r m)"
proof (intro bij_betw_imageI)
show "inj_on f S"
using pairwise_minus_cancel by (force simp: S_def f_def inj_on_def)
have "⋀x. x ∈ S ⟹ f x ∈ length_sum_set r m"
by (simp add: S_def f_def length_sum_set_def lenx' m_def pointwise_le_iff sum_list_minus)
moreover have "x ∈ f ` S" if "x ∈ length_sum_set r m" for x
proof
have x[simp]: "length x = r" "σ x = m"
using that by (auto simp: length_sum_set_def)
have "x = x' + x - x'"
by (rule nth_equalityI; simp add: lenx')
then show "x = f (x' + x)"
unfolding f_def by fastforce
have "x' ⊴ x' + x"
moreover have "σ (x' + x) = n"
by (simp add: lenx' m_def n sum_list_plus)
ultimately show "x' + x ∈ S"
using S_def by blast
qed
ultimately show "f ` S = length_sum_set r m" by auto
qed
define g where "g ≡ λx::nat list. map Suc x"
define g' where "g' ≡ λx::nat list. x - replicate (length x) 1"
define T where "T ≡ length_sum_set r (m+r) ∩ lists(-{0})"
have g: "bij_betw g (length_sum_set r m) T"
proof (intro bij_betw_imageI)
show "inj_on g (length_sum_set r m)"
by (auto simp: g_def inj_on_def)
have "⋀x. x ∈ length_sum_set r m ⟹ g x ∈ T"
by (auto simp: g_def length_sum_set_def sum_list_Suc T_def)
moreover have "x ∈ g ` length_sum_set r m" if "x ∈ T" for x
proof
have [simp]: "length x = r"
using length_sum_set_def that T_def by auto
have r1_x: "replicate r (Suc 0) ⊴ x"
using that unfolding T_def pointwise_le_iff_nth
by (simp add: lists_def in_listsp_conv_set Suc_leI)
show "x = g (g' x)"
using that by (intro nth_equalityI) (auto simp: g_def g'_def T_def)
show "g' x ∈ length_sum_set r m"
using that T_def by (simp add: g'_def r1_x sum_list_minus length_sum_set_def sum_list_replicate)
qed
ultimately show "g ` (length_sum_set r m) = T" by auto
qed
define U where "U ≡ (insert (m+r)) ` finsets {0<..<m+r} (r-1)"
have h: "bij_betw (set ∘ augmentum) T U"
proof (intro bij_betw_imageI)
show "inj_on ((set ∘ augmentum)) T"
unfolding inj_on_def T_def
by (metis ComplD IntE dementum_augmentum in_listsD insertI1)
have "(set ∘ augmentum) t ∈ U" if "t ∈ T" for t
proof -
have t: "length t = r" "σ t = m+r" "0 ∉ set t"
using that by (force simp: T_def length_sum_set_def)+
then have mrt: "m + r ∈ set (augmentum t)"
by (metis ‹r>0› sum_list_augmentum)
then have "set (augmentum t) = insert (m + r) (set (augmentum t) - {m + r})"
by blast
moreover have "set (augmentum t) - {m + r} ∈ finsets {0<..<m + r} (r - Suc 0)"
apply (auto simp: finsets_def mrt distinct_card t)
by (metis atMost_iff augmentum_subset_sum_list le_eq_less_or_eq subsetD t(2))
ultimately show ?thesis
by (metis One_nat_def U_def comp_apply imageI)
qed
moreover have "u ∈ (set ∘ augmentum) ` T" if "u ∈ U" for u
proof
from that
obtain N where u: "u = insert (m + r) N" and Nsub: "N ⊆ {0<..<m + r}"
and [simp]: "card N = r - Suc 0"
by (auto simp: U_def finsets_def)
have [simp]: "0 ∉ N" "m+r ∉ N" "finite N"
using finite_subset Nsub by auto
have [simp]: "card u = r"
using Nsub ‹r>0› by (auto simp: u card_insert_if)
have ssN: "sorted (sorted_list_of_set N @ [m + r])"
using Nsub by (simp add: less_imp_le_nat sorted_wrt_append subset_eq)
have so_u_N: "sorted_list_of_set u = insort (m+r) (sorted_list_of_set N)"
also have "… = sorted_list_of_set N @ [m+r]"
using Nsub by (force intro: sorted_insort_is_snoc)
finally have so_u: "sorted_list_of_set u = sorted_list_of_set N @ [m+r]" .
have 0: "0 ∉ set (sorted_list_of_set u)"
by (simp add: ‹r>0› set_insort_key so_u_N)
show "u = (set ∘ augmentum) ((dementum ∘ sorted_list_of_set)u)"
using 0 so_u ssN u by force
have sortd_wrt_u: "sorted_wrt (<) (sorted_list_of_set u)"
by simp
show "(dementum ∘ sorted_list_of_set) u ∈ T"
using sum_list_dementum [OF ssN] sortd_wrt_u 0 by (force simp: so_u dementum_nonzero)+
qed
ultimately show "(set ∘ augmentum) ` T = U" by auto
qed
obtain φ where "bij_betw φ S U"
by (meson bij_betw_trans f g h)
moreover have "card U = (n - σ x' + r-1) choose (r-1)"
proof -
have "inj_on (insert (m + r)) (finsets {0<..<m + r} (r - Suc 0))"
by (simp add: inj_on_def finsets_def subset_iff) (meson insert_ident order_less_le)
then have "card U = card (finsets {0<..<m + r} (r - 1))"
unfolding U_def by (simp add: card_image)
also have "… = (n - σ x' + r-1) choose (r-1)"
finally show ?thesis .
qed
ultimately show ?thesis
by (metis bij_betw_same_card)
qed

subsection ‹Towards the main theorem›

lemma extend_tuple:
assumes "σ xs ≤ n" "length xs ≠ 0"
obtains ys where "σ ys = n" "xs ⊴ ys"
proof -
obtain x xs' where xs: "xs = x#xs'"
using assms list.exhaust by auto
define y where "y ≡ x + n - σ xs"
show thesis
proof
show "σ (y#xs') = n"
using assms xs y_def by auto
show "xs ⊴ y#xs'"
using assms y_def pointwise_le_def xs by auto
qed
qed

lemma extend_preserving:
assumes "σ xs ≤ n" "length xs > 1" "i < length xs"
obtains ys where "σ ys = n" "xs ⊴ ys" "ys!i = xs!i"
proof -
define j where "j ≡ Suc i mod length xs"
define xs1 where "xs1 = take j xs"
define xs2 where "xs2 = drop (Suc j) xs"
define x where "x = xs!j"
have xs: "xs = xs1 @ [x] @ xs2"
using assms
apply (simp add: Cons_nth_drop_Suc assms x_def xs1_def xs2_def j_def)
by (meson Suc_lessD id_take_nth_drop mod_less_divisor)
define y where "y ≡ x + n - σ xs"
define ys where "ys ≡ xs1 @ [y] @ xs2"
have "x ≤ y"
using assms y_def by linarith
show thesis
proof
show "σ ys = n"
using assms(1) xs y_def ys_def by auto
show "xs ⊴ ys"
using xs ys_def ‹x ≤ y› pointwise_append_le_iff pointwise_le_def by fastforce
have "length xs1 ≠ i"
using assms by (simp add: xs1_def j_def min_def mod_Suc)
then show "ys!i = xs!i"
by (auto simp: ys_def xs nth_append nth_Cons')
qed
qed

text‹The proof of the main theorem will make use of the inclusion-exclusion formula, in addition to
the previously shown results.›

theorem Khovanskii:
assumes "card A > 1"
defines "f ≡ λn. card(sumset_iterated A n)"
obtains N p where "real_polynomial_function p" "⋀n. n ≥ N ⟹ real (f n) = p (real n)"
proof -
define r where "r ≡ card A"
define C where "C ≡ λn x'. {x. x' ⊴ x ∧ σ x = n}"
define X where "X ≡ minimal_elements {x. useless x ∧ length x = r}"
have "r > 1" "r ≠ 0"
using assms r_def by auto
have Csub: "C n x' ⊆ length_sum_set (length x') n" for n x'
by (auto simp: C_def length_sum_set_def pointwise_le_iff)
then have finC: "finite (C n x')" for n x'
by (meson finite_length_sum_set finite_subset)
have "finite X"
using "minimal_elements_set_tuples_finite" X_def by force
then have max_X: "⋀x'. x' ∈ X ⟹  σ x' ≤ σ (max_pointwise r X)"
using X_def max_pointwise_ge minimal_elements.simps pointwise_le_imp_σ by force
let ?z0 = "replicate r 0"
have Cn0: "C n ?z0 = length_sum_set r n" for n
by (auto simp: C_def length_sum_set_def)
then obtain p0 where pf_p0: "real_polynomial_function p0" and p0: "⋀n. n>0 ⟹ p0 (real n) = real (card (C n ?z0))"
by (metis real_polynomial_function_length_sum_set)
obtain q where pf_q: "real_polynomial_function q" and q: "⋀x. q x = x gchoose (r-1)"
using real_polynomial_function_gchoose by metis
define p where "p ≡ λx::real. p0 x - (∑Y | Y ⊆ X ∧ Y ≠ {}. (- 1) ^ (card Y + 1) * q((x - real(σ (max_pointwise r Y)) + real r - 1)))"
show thesis
proof
note pf_q' = real_polynomial_function_compose [OF _ pf_q, unfolded o_def]
note pf_intros = real_polynomial_function_sum real_polynomial_function_diff real_polynomial_function.intros
show "real_polynomial_function p"
unfolding p_def using ‹finite X› by (intro pf_p0 pf_q' pf_intros | force)+
next
fix n
assume "n ≥ max 1 (σ (max_pointwise r X))"
then have nlarge: "n ≥ σ (max_pointwise r X)" and "n > 0"
by auto
define U where "U ≡ λn. length_sum_set r n ∩ {x. useful x}"
have 2: "(length_sum_set r n ∩ {x. useless x}) = (⋃x'∈X. C n x')"
unfolding C_def X_def length_sum_set_def r_def
using useless_leq_useless by (force simp: minimal_elements.simps pointwise_le_iff useless_iff)
define SUM1 where "SUM1 ≡ ∑I | I ⊆ C n ` X ∧ I ≠ {}. (- 1) ^ (card I + 1) * int (card (⋂I))"
define SUM2 where "SUM2 ≡ ∑Y | Y ⊆ X ∧ Y ≠ {}. (- 1) ^ (card Y + 1) * int (card (⋂(C n ` Y)))"
have SUM1_card: "card(length_sum_set r n ∩ {x. useless x}) = nat SUM1"
unfolding SUM1_def 2 using ‹finite X› finC by (intro card_UNION; force)
have "SUM1 ≥ 0"
unfolding SUM1_def using card_UNION_nonneg finC ‹finite X› by auto
have C_empty_iff: "C n x' = {} ⟷ σ x' > n" if "length x' ≠ 0" for x'
by (simp add: set_eq_iff C_def) (meson extend_tuple linorder_not_le pointwise_le_imp_σ that)
have C_eq_1: "C n x' = {[n]}" if "σ x' ≤ n" "length x' = 1" for x'
using that by (auto simp: C_def length_Suc_conv pointwise_le_def elim!: list.rel_cases)
have n_ge_X: "σ x ≤ n" if "x ∈ X" for x
by (meson le_trans max_X nlarge that)
have len_X_r: "x ∈ X ⟹ length x = r" for x
by (auto simp: X_def minimal_elements.simps)

have "min_pointwise r (C n x') = x'" if "r > 1" "x' ∈ X" for x'
proof (rule pointwise_le_antisym)
have [simp]: "length x' = r" "σ x' ≤ n"
using X_def minimal_elements.cases that(2) n_ge_X by auto
have [simp]: "length (min_pointwise r (C n x')) = r"
show "min_pointwise r (C n x') ⊴ x'"
fix i
assume "i < r"
then obtain y where "σ y = n ∧ x' ⊴ y ∧ y!i ≤ x'!i"
by (metis extend_preserving ‹1 < r› ‹length x' = r› ‹x' ∈ X› order.refl n_ge_X)
then have "∃y∈C n x'. y!i ≤ x'!i"
using C_def by blast
with ‹i < r› show "min_pointwise r (C n x')!i ≤ x'!i"
by (simp add: min_pointwise_def Min_le_iff finC C_empty_iff leD)
qed
have "x' ⊴ min_pointwise r (C n x')" if "σ x' ≤ n" "length x' = r" for x'
by (smt (verit, del_insts) C_def C_empty_iff ‹r ≠ 0› finC leD mem_Collect_eq min_pointwise_ge_iff pointwise_le_iff that)
then show "x' ⊴ min_pointwise r (C n x')"
using X_def minimal_elements.cases that by force
qed
then have inj_C: "inj_on (C n) X"
by (smt (verit, best) inj_onI mem_Collect_eq ‹r>1›)
have inj_on_imageC: "inj_on (image (C n)) (Pow X - {{}})"
by (simp add: inj_C inj_on_diff inj_on_image_Pow)

have "Pow (C n ` X) - {{}} ⊆ (image (C n)) ` (Pow X - {{}})"
by (metis Pow_empty image_Pow_surj image_diff_subset image_empty)
then have "(image (C n)) ` (Pow X - {{}}) = Pow (C n ` X) - {{}}"
by blast
then have "SUM1 = sum (λI. (- 1) ^ (card I + 1) * int (card (⋂I))) ((image (C n)) ` (Pow X - {{}}))"
unfolding SUM1_def by (auto intro: sum.cong)
also have "… = sum ((λI. (- 1) ^ (card I + 1) * int (card (⋂ I))) ∘ (image (C n))) (Pow X - {{}})"
also have "… = SUM2"
unfolding SUM2_def using subset_inj_on [OF inj_C] by (force simp: card_image intro: sum.cong)
finally have "SUM1 = SUM2" .

have "length_sum_set r n = (length_sum_set r n ∩ {x. useful x}) ∪ (length_sum_set r n ∩ {x. useless x})"
by auto
then have "card (length_sum_set r n) =
card (length_sum_set r n ∩ {x. useful x}) +
card (length_sum_set r n ∩ Collect useless)"
by (simp add: finite_length_sum_set disjnt_iff flip: card_Un_disjnt)
moreover have "C n ?z0 = length_sum_set r n"
by (auto simp: C_def length_sum_set_def)
ultimately have "card (C n ?z0) = card (U n) + nat SUM2"
by (simp add: U_def flip: ‹SUM1 = SUM2› SUM1_card)
then have SUM2_le: "nat SUM2 ≤ card (C n ?z0)"
by arith
have σ_max_pointwise_le: "⋀Y. ⟦Y ⊆ X; Y ≠ {}⟧ ⟹ σ (max_pointwise r Y) ≤ n"
by (meson ‹finite X› le_trans max_pointwise_mono nlarge pointwise_le_imp_σ)

have card_C_max: "card (C n (max_pointwise r Y)) =
(n - σ (max_pointwise r Y) + r - Suc 0 choose (r - Suc 0))"
if "Y ⊆ X" "Y ≠ {}" for Y
proof -
have [simp]: "length (max_pointwise r Y) = r"
then show ?thesis
using ‹r ≠ 0› that C_def by (simp add: bound_sum_list_card [of r] σ_max_pointwise_le)
qed

define SUM3 where "SUM3 ≡ (∑Y | Y ⊆ X ∧ Y ≠ {}.
- ((- 1) ^ (card Y) * ((n - σ (max_pointwise r Y) + r - 1 choose (r - 1)))))"
have "⋂(C n ` Y) = C n (max_pointwise r Y)" if "Y ⊆ X" "Y ≠ {}" for Y
proof
show "⋂ (C n ` Y) ⊆ C n (max_pointwise r Y)"
unfolding C_def
proof clarsimp
fix x
assume "∀y∈Y. y ⊴ x ∧ σ x = n"
moreover have "finite Y"
using ‹finite X› infinite_super that by blast
moreover have "⋀u. u ∈ Y ⟹ length u = r"
using len_X_r that by blast
ultimately show "max_pointwise r Y ⊴ x ∧ σ x = n"
by (smt (verit, del_insts) all_not_in_conv max_pointwise_le_iff pointwise_le_iff_nth that(2))
qed
next
show "C n (max_pointwise r Y) ⊆ ⋂ (C n ` Y)"
apply (clarsimp simp: C_def)
by (metis ‹finite X› finite_subset len_X_r max_pointwise_ge pointwise_le_trans subsetD that(1))
qed
then have "SUM2 = SUM3"
by (simp add: SUM2_def SUM3_def card_C_max)
have "U n = C n ?z0 - (length_sum_set r n ∩ {x. useless x})"
by (auto simp: U_def C_def length_sum_set_def)
then have "card (U n) = card (C n ?z0) - card(length_sum_set r n ∩ {x. useless x})"
using finite_length_sum_set
by (simp add: C_def Collect_mono_iff inf.coboundedI1 length_sum_set_def flip: card_Diff_subset)
then have card_U_eq_diff: "card (U n) = card (C n ?z0) - nat SUM1"
using SUM1_card by presburger
have "SUM3 ≥ 0"
using ‹0 ≤ SUM1› ‹SUM1 = SUM2› ‹SUM2 = SUM3› by blast
have **: "⋀Y. ⟦Y ⊆ X; Y ≠ {}⟧ ⟹ Suc (σ (max_pointwise r Y)) ≤ n + r"
have "real (f n) = card (U n)"
unfolding f_def r_def U_def length_sum_set_def
using card_sumset_iterated_length_sum_set_useful length_sum_set_def by presburger
also have "… = card (C n ?z0) -  nat SUM3"
using card_U_eq_diff ‹SUM1 = SUM2› ‹SUM2 = SUM3› by presburger
also have "… = real (card (C n (replicate r 0))) - real (nat SUM3)"
using SUM2_le ‹SUM2 = SUM3› of_nat_diff by blast
also have "… = p (real n)"
using ‹1 < r› ‹n>0›
apply (simp add: p_def p0 q ‹SUM3 ≥ 0›)
apply (simp add: SUM3_def binomial_gbinomial of_nat_diff σ_max_pointwise_le algebra_simps **)
done
finally show "real (f n) = p (real n)" .
qed
qed

end

end
```