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"
  by (simp add: finsets_def n_subsets)

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

lemma distinct_map_plus_iff [simp]:
  fixes a::"'a::linordered_cancel_ab_semigroup_add"
  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)"
  by (simp add: plus_list_def)

lemma plus_Nil [simp]: "[] + xs = []"
  by (simp add: plus_list_def)

lemma plus_Cons: "(y # ys) + (x # xs) = (y+x) # (ys+xs)"
  by (simp add: plus_list_def)

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"
  by (simp add: plus_list_def assms)


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)"
  by (simp add: minus_list_def)

lemma minus_Nil [simp]: "[] - xs = []"
  by (simp add: minus_list_def)

lemma minus_Cons: "(y # ys) - (x # xs) = (y-x) # (ys-xs)"
  by (simp add: minus_list_def)

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"
  by (simp add: minus_list_def assms)

instance list :: (ab_semigroup_add) ab_semigroup_add
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
        by (simp add: Cons add.assoc)
    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
        by (simp add: Cons.IH add.commute)
    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)"
  by (simp add: list_all2_conv_all_nth pointwise_le_def)

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

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"
  by (simp add: list.rel_refl pointwise_le_def)

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"
  by (simp add: pointwise_le_def)

lemma pointwise_le_Nil2 [simp]: "x ⊴ Nil ⟷ x = Nil"
  by (simp add: pointwise_le_def)

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"
  by (simp add: pointwise_less_def)

lemma pointwise_less_Nil2 [simp]: "¬ x ⊲ Nil"
  by (simp add: pointwise_less_def)

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
    by (simp add: pointwise_le_iff)
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
    by (simp add: Cons.IH add_le_mono)
qed

lemma sum_list_plus:
  fixes xs :: "'a::comm_monoid_add list"
  assumes "length xs = length ys" shows "σ (xs + ys) = σ xs + σ ys"
  using assms by (simp add: plus_list_def case_prod_unfold sum_list_addf)

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"
  by (simp add: min_pointwise_def pointwise_le_iff_nth)

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"
  by (simp add: max_pointwise_def pointwise_le_iff_nth)

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)
qed (simp add: pointwise_le_iff)

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"}›

locale Khovanskii = additive_abelian_group +
  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 = 𝟬"
  by (simp add: Gmult_def)

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

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

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

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

lemma Gmult_add_diff:
  assumes "a ∈ G"
  shows "Gmult a (n+k) ⊖ Gmult a n = Gmult a k"
  by (metis Gmult_add_add Gmult_in_G assms commutative inverse_closed invertible invertible_left_inverse2)

lemma Gmult_diff:
  assumes "a ∈ G" "n≤m"
  shows "Gmult a m ⊖ Gmult a n = Gmult a (m-n)"
  by (metis Gmult_add_diff assms le_add_diff_inverse)


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}"
    by (simp add: α_def plus_list_def)
  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}"
    by (intro fincomp_cong'; simp add: Gmult_add_add)
  also have "… = α x ⊕ α y"
    by (simp add: α_def fincomp_comp)
  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}"
    by (simp add: α_def minus_list_def)
  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 [] = []"
  by (simp add: list_incr_def)

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

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)"
  by (simp add: list_incr_def)

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)))"
    by (simp add: finite_length_sum_set)
  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)"
  by (metis assms diff_add sum_up_index_split)

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"
      by (simp add: sum_of_powers add.commute q_def)
    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"
      by (simp add: sum_list_update length_sum_set_def)
    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
    by (simp add: all_zeroes_replicate r_def)
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)"
    by (simp add: alpha_list_incr r_def)
  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
    by (simp add: card_image length_sum_set_def)
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)"
      by (simp add: leny')
    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›
          apply (simp add: pointwise_le_iff_nth VF_def)
          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 [] = []"
  by (simp add: dementum_def)

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"
  by (simp add: dementum_def)

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
    by (simp add: minus_Cons Cons)
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))"
      by (simp add: sum.head)
    also have "… = sum ((!) (a # ns)) {..i}"
      by (simp add: nth_Cons' atMost_atLeast0)
    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))"
      by (simp add: sum.head)
    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
      by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost)
    also have "… = (∑j=0..i. ns!j) - (∑j≤i-Suc 0. ns!j)"
      by (simp add:  sum.head [of 0 i])
    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"
      by (simp add: atLeast0AtMost)
    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"
        by (simp add: lenx' pointwise_le_plus)
      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)"
        by (simp add: u)
      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"
        apply (simp add: T_def length_sum_set_def)
        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)"
      by (simp add: card_finsets m_def)
    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"
        by (simp add: min_pointwise_def)
      show "min_pointwise r (C n x') ⊴ x'"
      proof (clarsimp simp add: pointwise_le_iff_nth)
        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 - {{}})"
      by (simp add: sum.reindex inj_on_imageC)
    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"
        by (simp add: max_pointwise_def)
      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"
      by (metis ‹1 < r› σ_max_pointwise_le add.commute add_le_mono less_or_eq_imp_le plus_1_eq_Suc)
    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