diff --git a/thys/Khovanskii_Theorem/FiniteProduct.thy b/thys/Khovanskii_Theorem/FiniteProduct.thy
new file mode 100644
--- /dev/null
+++ b/thys/Khovanskii_Theorem/FiniteProduct.thy
@@ -0,0 +1,330 @@
+section \<open>Product Operator for Commutative Monoids\<close>
+
+(*
+  Finite products in group theory. This theory is largely based on HOL/Algebra/FiniteProduct.thy. 
+  --L C Paulson
+*)
+
+theory FiniteProduct
+  imports 
+    "Jacobson_Basic_Algebra.Group_Theory"
+
+begin
+
+subsection \<open>Products over Finite Sets\<close>
+
+context commutative_monoid begin
+
+definition "M_ify x \<equiv> if x \<in> M then x else \<one>"
+
+definition "fincomp f A \<equiv> if finite A then Finite_Set.fold (\<lambda>x y. f x \<cdot> M_ify y) \<one> A else \<one>"
+
+lemma fincomp_empty [simp]: "fincomp f {} = \<one>"
+  by (simp add: fincomp_def)
+
+lemma fincomp_infinite[simp]: "infinite A \<Longrightarrow> fincomp f A = \<one>"
+  by (simp add: fincomp_def)
+
+lemma left_commute: "\<lbrakk> a \<in> M; b \<in> M; c \<in> M \<rbrakk> \<Longrightarrow> b \<cdot> (a \<cdot> c) = a \<cdot> (b \<cdot> c)"
+  using commutative by force
+
+
+lemma comp_fun_commute_onI:
+  assumes "f \<in> F \<rightarrow> M"
+  shows "comp_fun_commute_on F (\<lambda>x y. f x \<cdot> M_ify y)"
+  using assms
+  by (auto simp add: comp_fun_commute_on_def Pi_iff M_ify_def left_commute)
+
+lemma fincomp_closed [simp]:
+  assumes "f \<in> F \<rightarrow> M" 
+  shows "fincomp f F \<in> M"
+proof -
+  interpret comp_fun_commute_on F "\<lambda>x y. f x \<cdot> M_ify y"
+    by (simp add: assms comp_fun_commute_onI)
+  show ?thesis
+    unfolding fincomp_def
+    by (smt (verit, ccfv_threshold) M_ify_def Pi_iff fold_graph_fold assms composition_closed equalityE fold_graph_closed_lemma unit_closed)
+qed
+
+lemma fincomp_insert [simp]:
+  assumes F: "finite F" "a \<notin> F" and f: "f \<in> F \<rightarrow> M" "f a \<in> M"
+  shows "fincomp f (insert a F) = f a \<cdot> fincomp f F"
+proof -
+  interpret comp_fun_commute_on "insert a F" "\<lambda>x y. f x \<cdot> M_ify y"
+    by (simp add: comp_fun_commute_onI f)
+  show ?thesis
+    using assms fincomp_closed commutative_monoid.M_ify_def commutative_monoid_axioms
+    by (fastforce simp add: fincomp_def)
+qed
+
+lemma fincomp_unit_eqI: "(\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> fincomp f A = \<one>"
+proof (induct A rule: infinite_finite_induct)
+  case empty show ?case by simp
+next
+  case (insert a A)
+  have "(\<lambda>i. \<one>) \<in> A \<rightarrow> M" by auto
+  with insert show ?case by simp
+qed simp
+
+lemma fincomp_unit [simp]: "fincomp (\<lambda>i. \<one>) A = \<one>"
+  by (simp add: fincomp_unit_eqI)
+
+lemma funcset_Int_left [simp, intro]:
+  "\<lbrakk>f \<in> A \<rightarrow> C; f \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> f \<in> A Int B \<rightarrow> C"
+  by fast
+
+lemma funcset_Un_left [iff]:
+  "(f \<in> A Un B \<rightarrow> C) = (f \<in> A \<rightarrow> C \<and> f \<in> B \<rightarrow> C)"
+  by fast
+
+lemma fincomp_Un_Int:
+  "\<lbrakk>finite A; finite B; g \<in> A \<rightarrow> M; g \<in> B \<rightarrow> M\<rbrakk> \<Longrightarrow>
+     fincomp g (A \<union> B) \<cdot> fincomp g (A \<inter> B) =
+     fincomp g A \<cdot> fincomp g B"
+  \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
+proof (induct set: finite)
+  case empty then show ?case by simp
+next
+  case (insert a A)
+  then have "g a \<in> M" "g \<in> A \<rightarrow> M" by blast+
+  with insert show ?case
+    by (simp add: Int_insert_left associative insert_absorb left_commute)
+qed
+
+lemma fincomp_Un_disjoint:
+  "\<lbrakk>finite A; finite B; A \<inter> B = {}; g \<in> A \<rightarrow> M; g \<in> B \<rightarrow> M\<rbrakk>
+   \<Longrightarrow> fincomp g (A \<union> B) = fincomp g A \<cdot> fincomp g B"
+  by (metis Pi_split_domain fincomp_Un_Int fincomp_closed fincomp_empty right_unit)
+
+lemma fincomp_comp:
+  "\<lbrakk>f \<in> A \<rightarrow> M; g \<in> A \<rightarrow> M\<rbrakk> \<Longrightarrow> fincomp (\<lambda>x. f x \<cdot> g x) A = (fincomp f A \<cdot> fincomp g A)"
+proof (induct A rule: infinite_finite_induct)
+  case empty show ?case by simp
+next
+  case (insert a A) 
+  then have "f a \<in> M" "g \<in> A \<rightarrow> M" "g a \<in> M" "f \<in> A \<rightarrow> M" "(\<lambda>x. f x \<cdot> g x) \<in> A \<rightarrow> M"
+    by blast+
+  then show ?case
+    by (simp add: insert associative left_commute)
+qed simp
+
+lemma fincomp_cong':
+  assumes "A = B" "g \<in> B \<rightarrow> M" "\<And>i. i \<in> B \<Longrightarrow> f i = g i"
+  shows "fincomp f A = fincomp g B"
+proof (cases "finite B")
+  case True
+  then have ?thesis
+    using assms
+  proof (induct arbitrary: A)
+    case empty thus ?case by simp
+  next
+    case (insert x B)
+    then have "fincomp f A = fincomp f (insert x B)" by simp
+    also from insert have "... = f x \<cdot> fincomp f B"
+      by (simp add: Pi_iff)
+    also from insert have "... = g x \<cdot> fincomp g B" by fastforce
+    also from insert have "... = fincomp g (insert x B)"
+      by (intro fincomp_insert [THEN sym]) auto
+    finally show ?case .
+  qed
+  with assms show ?thesis by simp
+next
+  case False with assms show ?thesis by simp
+qed
+
+lemma fincomp_cong:
+  assumes "A = B" "g \<in> B \<rightarrow> M" "\<And>i. i \<in> B =simp=> f i = g i"
+  shows "fincomp f A = fincomp g B"
+  using assms unfolding simp_implies_def by (blast intro: fincomp_cong')
+
+text \<open>Usually, if this rule causes a failed congruence proof error,
+  the reason is that the premise \<open>g \<in> B \<rightarrow> M\<close> cannot be shown.
+  Adding @{thm [source] Pi_def} to the simpset is often useful.
+  For this reason, @{thm [source] fincomp_cong}
+  is not added to the simpset by default.
+\<close>
+
+lemma fincomp_0 [simp]:
+  "f \<in> {0::nat} \<rightarrow> M \<Longrightarrow> fincomp f {..0} = f 0"
+  by (simp add: Pi_def)
+
+lemma fincomp_0': "f \<in> {..n} \<rightarrow> M \<Longrightarrow> (f 0) \<cdot> fincomp f {Suc 0..n} = fincomp f {..n}"
+  by (metis Pi_split_insert_domain Suc_n_not_le_n atLeastAtMost_iff atLeastAtMost_insertL atMost_atLeast0 finite_atLeastAtMost fincomp_insert le0)
+
+lemma fincomp_Suc [simp]:
+  "f \<in> {..Suc n} \<rightarrow> M \<Longrightarrow> fincomp f {..Suc n} = (f (Suc n) \<cdot> fincomp f {..n})"
+  by (simp add: Pi_def atMost_Suc)
+
+lemma fincomp_Suc2:
+  "f \<in> {..Suc n} \<rightarrow> M \<Longrightarrow> fincomp f {..Suc n} = (fincomp (%i. f (Suc i)) {..n} \<cdot> f 0)"
+proof (induct n)
+  case 0 thus ?case by (simp add: Pi_def)
+next
+  case Suc thus ?case 
+    by (simp add: associative Pi_def)
+qed
+
+lemma fincomp_Suc3:
+  assumes "f \<in> {..n :: nat} \<rightarrow> M"
+  shows "fincomp f {.. n} = (f n) \<cdot> fincomp f {..< n}"
+proof (cases "n = 0")
+  case True thus ?thesis
+    using assms atMost_Suc by simp
+next
+  case False
+  then obtain k where "n = Suc k"
+    using not0_implies_Suc by blast
+  thus ?thesis
+    using fincomp_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp
+qed
+
+lemma fincomp_reindex: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
+  "f \<in> (h ` A) \<rightarrow> M \<Longrightarrow>
+        inj_on h A \<Longrightarrow> fincomp f (h ` A) = fincomp (\<lambda>x. f (h x)) A"
+proof (induct A rule: infinite_finite_induct)
+  case (infinite A)
+  hence "\<not> finite (h ` A)"
+    using finite_imageD by blast
+  with \<open>\<not> finite A\<close> show ?case by simp
+qed (auto simp add: Pi_def)
+
+lemma fincomp_const: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close>
+  assumes a [simp]: "a \<in> M"
+  shows "fincomp (\<lambda>x. a) A = rec_nat \<one> (\<lambda>u. (\<cdot>) a) (card A)"
+  by (induct A rule: infinite_finite_induct) auto
+
+lemma fincomp_singleton: \<^marker>\<open>contributor \<open>Jesus Aransay\<close>\<close>
+  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> M"
+  shows "fincomp (\<lambda>j. if i = j then f j else \<one>) A = f i"
+  using i_in_A fincomp_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
+    fin_A f_Pi fincomp_unit [of "A - {i}"]
+    fincomp_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"]
+  unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
+
+lemma fincomp_singleton_swap:
+  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> M"
+  shows "fincomp (\<lambda>j. if j = i then f j else \<one>) A = f i"
+  using fincomp_singleton [OF assms] by (simp add: eq_commute)
+
+lemma fincomp_mono_neutral_cong_left:
+  assumes "finite B"
+    and "A \<subseteq> B"
+    and 1: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>"
+    and gh: "\<And>x. x \<in> A \<Longrightarrow> g x = h x"
+    and h: "h \<in> B \<rightarrow> M"
+  shows "fincomp g A = fincomp h B"
+proof-
+  have eq: "A \<union> (B - A) = B" using \<open>A \<subseteq> B\<close> by blast
+  have d: "A \<inter> (B - A) = {}" using \<open>A \<subseteq> B\<close> by blast
+  from \<open>finite B\<close> \<open>A \<subseteq> B\<close> have f: "finite A" "finite (B - A)"
+    by (auto intro: finite_subset)
+  have "h \<in> A \<rightarrow> M" "h \<in> B - A \<rightarrow> M"
+    using assms by (auto simp: image_subset_iff_funcset)
+  moreover have "fincomp g A = fincomp h A \<cdot> fincomp h (B - A)"
+  proof -
+    have "fincomp h (B - A) = \<one>"
+      using "1" fincomp_unit_eqI by blast
+    moreover have "fincomp g A = fincomp h A"
+      using \<open>h \<in> A \<rightarrow> M\<close> fincomp_cong' gh by blast
+    ultimately show ?thesis
+      by (simp add: \<open>h \<in> A \<rightarrow> M\<close>)
+  qed
+  ultimately show ?thesis
+    by (simp add: fincomp_Un_disjoint [OF f d, unfolded eq])
+qed
+
+lemma fincomp_mono_neutral_cong_right:
+  assumes "finite B"
+    and "A \<subseteq> B" "\<And>i. i \<in> B - A \<Longrightarrow> g i = \<one>" "\<And>x. x \<in> A \<Longrightarrow> g x = h x" "g \<in> B \<rightarrow> M"
+  shows "fincomp g B = fincomp h A"
+  using assms  by (auto intro!: fincomp_mono_neutral_cong_left [symmetric])
+
+lemma fincomp_mono_neutral_cong:
+  assumes [simp]: "finite B" "finite A"
+    and *: "\<And>i. i \<in> B - A \<Longrightarrow> h i = \<one>" "\<And>i. i \<in> A - B \<Longrightarrow> g i = \<one>"
+    and gh: "\<And>x. x \<in> A \<inter> B \<Longrightarrow> g x = h x"
+    and g: "g \<in> A \<rightarrow> M"
+    and h: "h \<in> B \<rightarrow> M"
+  shows "fincomp g A = fincomp h B"
+proof-
+  have "fincomp g A = fincomp g (A \<inter> B)"
+    by (rule fincomp_mono_neutral_cong_right) (use assms in auto)
+  also have "\<dots> = fincomp h (A \<inter> B)"
+    by (rule fincomp_cong) (use assms in auto)
+  also have "\<dots> = fincomp h B"
+    by (rule fincomp_mono_neutral_cong_left) (use assms in auto)
+  finally show ?thesis .
+qed
+
+
+lemma fincomp_UN_disjoint:
+  assumes
+    "finite I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "pairwise (\<lambda>i j. disjnt (A i) (A j)) I"
+    "\<And>i x. i \<in> I \<Longrightarrow> x \<in> A i \<Longrightarrow> g x \<in> M"
+  shows "fincomp g (\<Union>(A ` I)) = fincomp (\<lambda>i. fincomp g (A i)) I"
+  using assms
+proof (induction set: finite)
+  case empty
+  then show ?case
+    by force
+next
+  case (insert i I)
+  then show ?case
+    unfolding pairwise_def disjnt_def
+    apply clarsimp
+    apply (subst fincomp_Un_disjoint)
+         apply (fastforce intro!: funcsetI fincomp_closed)+
+    done
+qed
+
+lemma fincomp_Union_disjoint:
+  "\<lbrakk>finite C; \<And>A. A \<in> C \<Longrightarrow> finite A \<and> (\<forall>x\<in>A. f x \<in> M); pairwise disjnt C\<rbrakk> \<Longrightarrow>
+    fincomp f (\<Union>C) = fincomp (fincomp f) C"
+  by (frule fincomp_UN_disjoint [of C id f]) auto
+
+end
+
+subsection \<open>Results for Abelian Groups\<close>
+
+context abelian_group begin
+
+lemma fincomp_inverse:
+  "f \<in> A \<rightarrow> G \<Longrightarrow> fincomp (\<lambda>x. inverse (f x)) A = inverse (fincomp f A)"
+proof (induct A rule: infinite_finite_induct)
+  case empty show ?case by simp
+next
+  case (insert a A) 
+  then have "f a \<in> G" "f \<in> A \<rightarrow> G" "(\<lambda>x. inverse (f x)) \<in> A \<rightarrow> G"
+    by blast+
+  with insert show ?case
+    by (simp add: commutative inverse_composition_commute)
+qed simp
+
+text \<open> Jeremy Avigad. This should be generalized to arbitrary groups, not just Abelian
+   ones, using Lagrange's theorem.\<close>
+lemma power_order_eq_one:
+  assumes fin [simp]: "finite G"
+    and a [simp]: "a \<in> G"
+  shows "rec_nat \<one> (\<lambda>u. (\<cdot>) a) (card G) = \<one>"
+proof -
+  have rec_G: "rec_nat \<one> (\<lambda>u. (\<cdot>) a) (card G) \<in> G"
+    by (metis Pi_I' a fincomp_closed fincomp_const)
+  have "\<And>x. x \<in> G \<Longrightarrow> x \<in> (\<cdot>) a ` G"
+    by (metis a composition_closed imageI invertible invertible_inverse_closed invertible_right_inverse2)
+  with a have "(\<cdot>) a ` G = G" by blast
+  then have "\<one> \<cdot> fincomp (\<lambda>x. x) G = fincomp (\<lambda>x. x) ((\<cdot>) a ` G)"
+    by simp
+  also have "\<dots> = fincomp (\<lambda>x. a \<cdot> x) G"
+    using fincomp_reindex
+    by (subst (2) fincomp_reindex [symmetric]) (auto simp: inj_on_def)
+  also have "\<dots> = fincomp (\<lambda>x. a) G \<cdot> fincomp (\<lambda>x. x) G"
+    by (simp add: fincomp_comp)
+  also have "fincomp (\<lambda>x. a) G = rec_nat \<one> (\<lambda>u. (\<cdot>) a) (card G)"
+    by (simp add: fincomp_const)
+  finally show ?thesis
+    by (metis commutative fincomp_closed funcset_id invertible invertible_left_cancel rec_G unit_closed)
+qed
+
+end
+
+end
diff --git a/thys/Khovanskii_Theorem/For_2022.thy b/thys/Khovanskii_Theorem/For_2022.thy
new file mode 100644
--- /dev/null
+++ b/thys/Khovanskii_Theorem/For_2022.thy
@@ -0,0 +1,151 @@
+section\<open>Temporary Preliminaries\<close>
+
+text \<open>Everything here will become redundant in Isabelle 2022\<close>
+
+theory For_2022
+  imports
+    "HOL-Analysis.Weierstrass_Theorems" \<comment> \<open>needed for polynomial function\<close>
+    "HOL-Library.List_Lenlexorder"      \<comment> \<open>lexicographic ordering for the type @{typ \<open>nat list\<close>}\<close>
+begin
+
+
+thm card_UNION
+text \<open>The famous inclusion-exclusion formula for the cardinality of a union\<close>
+lemma int_card_UNION:
+  assumes "finite A"
+    and "\<forall>k \<in> A. finite k"
+  shows "int (card (\<Union>A)) = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
+    (is "?lhs = ?rhs")
+proof -
+  have "?rhs = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))"
+    by simp
+  also have "\<dots> = (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))"
+    by (subst sum_distrib_left) simp
+  also have "\<dots> = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
+    using assms by (subst sum.Sigma) auto
+  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
+    by (rule sum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI)
+  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
+    using assms
+    by (auto intro!: sum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
+  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
+    using assms by (subst sum.Sigma) auto
+  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "sum ?lhs _ = _")
+  proof (rule sum.cong[OF refl])
+    fix x
+    assume x: "x \<in> \<Union>A"
+    define K where "K = {X \<in> A. x \<in> X}"
+    with \<open>finite A\<close> have K: "finite K"
+      by auto
+    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
+    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
+      using assms by (auto intro!: inj_onI)
+    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
+      using assms
+      by (auto intro!: rev_image_eqI[where x="(card a, a)" for a]
+          simp add: card_gt_0_iff[folded Suc_le_eq]
+          dest: finite_subset intro: card_mono)
+    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
+      by (rule sum.reindex_cong [where l = snd]) fastforce
+    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
+      using assms by (subst sum.Sigma) auto
+    also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
+      by (subst sum_distrib_left) simp
+    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))"
+      (is "_ = ?rhs")
+    proof (rule sum.mono_neutral_cong_right[rule_format])
+      show "finite {1..card A}"
+        by simp
+      show "{1..card K} \<subseteq> {1..card A}"
+        using \<open>finite A\<close> by (auto simp add: K_def intro: card_mono)
+    next
+      fix i
+      assume "i \<in> {1..card A} - {1..card K}"
+      then have i: "i \<le> card A" "card K < i"
+        by auto
+      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
+        by (auto simp add: K_def)
+      also have "\<dots> = {}"
+        using \<open>finite A\<close> i by (auto simp add: K_def dest: card_mono[rotated 1])
+      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
+        by (metis mult_zero_right sum.empty)
+    next
+      fix i
+      have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
+        (is "?lhs = ?rhs")
+        by (rule sum.cong) (auto simp add: K_def)
+      then show "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs"
+        by simp
+    qed
+    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}"
+      using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset)
+    then have "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
+      by (subst (2) sum.atLeast_Suc_atMost) simp_all
+    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
+      using K by (subst n_subsets[symmetric]) simp_all
+    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
+      by (subst sum_distrib_left[symmetric]) simp
+    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
+      by (subst binomial_ring) (simp add: ac_simps atMost_atLeast0)
+    also have "\<dots> = 1"
+      using x K by (auto simp add: K_def card_gt_0_iff)
+    finally show "?lhs x = 1" .
+  qed
+  also have "\<dots> = int (card (\<Union>A))"
+    by simp
+  finally show ?thesis ..
+qed
+
+lemma card_UNION:
+  assumes "finite A"
+    and "\<forall>k \<in> A. finite k"
+  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
+  by (simp only: flip: int_card_UNION [OF assms])
+
+lemma card_UNION_nonneg:
+  assumes "finite A"
+    and "\<forall>k \<in> A. finite k"
+  shows "(\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I))) \<ge> 0"
+  using int_card_UNION [OF assms] by presburger
+
+lemma real_polynomial_function_divide [intro]:
+  assumes "real_polynomial_function p" shows "real_polynomial_function (\<lambda>x. p x / c)"
+proof -
+  have "real_polynomial_function (\<lambda>x. p x * Fields.inverse c)"
+    using assms by auto
+  then show ?thesis
+    by (simp add: divide_inverse)
+qed
+
+lemma real_polynomial_function_prod [intro]:
+  "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> real_polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. prod (f x) I)"
+  by (induct I rule: finite_induct) auto
+
+lemma real_polynomial_function_gchoose:
+  obtains p where "real_polynomial_function p" "\<And>x. x gchoose r = p x"
+proof
+  show "real_polynomial_function (\<lambda>x. (\<Prod>i = 0..<r. x - real i) / fact r)"
+    by (force simp add: )
+qed (simp add: gbinomial_prod_rev)
+
+lemma sorted_map_plus_iff [simp]:
+  fixes a::"'a::linordered_cancel_ab_semigroup_add"
+  shows "sorted (map ((+) a) xs) \<longleftrightarrow> 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) \<longleftrightarrow> distinct xs"
+  by (induction xs) auto
+
+subsection \<open>Preliminary type instantiations\<close>
+
+instance list :: (wellorder) wellorder
+proof
+  show "P a"
+    if "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x" for P and a :: "'a list"
+    using that unfolding list_less_def
+    by (metis wf_lenlex wf_induct wf_lenlex wf)
+qed
+
+end
diff --git a/thys/Khovanskii_Theorem/Khovanskii.thy b/thys/Khovanskii_Theorem/Khovanskii.thy
new file mode 100644
--- /dev/null
+++ b/thys/Khovanskii_Theorem/Khovanskii.thy
@@ -0,0 +1,1250 @@
+section\<open>Khovanskii's Theorem\<close>
+
+text\<open>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.\<close>
+
+theory Khovanskii
+  imports
+    Complex_Main
+    FiniteProduct
+    "HOL-Library.Equipollence"
+    "Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality"
+    "Bernoulli.Bernoulli"               \<comment> \<open>sums of a fixed power are polynomials\<close>
+    "HOL-Analysis.Weierstrass_Theorems" \<comment> \<open>needed for polynomial function\<close>
+    "HOL-Library.List_Lenlexorder"      \<comment> \<open>lexicographic ordering for the type @{typ \<open>nat list\<close>}\<close>
+    For_2022
+begin
+
+lemma real_polynomial_function_sum_of_powers:
+  "\<exists>p. real_polynomial_function p \<and> (\<forall>n. (\<Sum>i\<le>n. real i ^ j) = p (real n))"
+proof (intro exI conjI strip)
+  let ?p = "\<lambda>n. (bernpoly (Suc j) (1 + n) - bernpoly (Suc j) 0) / (Suc j)"
+  show "real_polynomial_function ?p"
+    by (force simp add: bernpoly_def)
+qed (simp add: add.commute sum_of_powers)
+
+text \<open>The sum of the elements of a list\<close>
+abbreviation "\<sigma> \<equiv> sum_list"
+
+text \<open>Related to the nsets of Ramsey.thy, but simpler\<close>
+definition finsets :: "['a set, nat] \<Rightarrow> 'a set set"
+  where "finsets A n \<equiv> {N. N \<subseteq> A \<and> card N = n}"
+
+lemma card_finsets: "finite N \<Longrightarrow> card (finsets N k) = card N choose k"
+  by (simp add: finsets_def n_subsets)
+
+
+subsection \<open>Arithmetic operations on lists, pointwise on the elements\<close>
+
+text \<open>Weak type class properties.
+ Cancellation is difficult to arrange because of complications when lists differ in length.\<close>
+
+instantiation list :: (plus) plus
+begin
+definition "plus_list \<equiv> 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 \<equiv> 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=[] \<or> 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 \<open>The pointwise ordering on two equal-length lists of natural numbers\<close>
+
+text \<open>Gowers uses the usual symbol ($\le$) for his pointwise ordering.
+   In our development, $\le$ is the lexicographic ordering and $\unlhd$ is the pointwise ordering.\<close>
+
+definition pointwise_le :: "[nat list, nat list] \<Rightarrow> bool" (infixr "\<unlhd>" 50 )
+  where "x \<unlhd> y \<equiv> list_all2 (\<le>) x y"
+
+definition pointwise_less :: "[nat list, nat list] \<Rightarrow> bool" (infixr "\<lhd>" 50 )
+  where "x \<lhd> y \<equiv> x \<unlhd> y \<and> x \<noteq> y"
+
+lemma pointwise_le_iff_nth:
+  "x \<unlhd> y \<longleftrightarrow> length x = length y \<and> (\<forall>i < length x. x!i \<le> y!i)"
+  by (simp add: list_all2_conv_all_nth pointwise_le_def)
+
+lemma pointwise_le_iff:
+  "x \<unlhd> y \<longleftrightarrow> length x = length y \<and> (\<forall>(i,j) \<in> set (zip x y). i\<le>j)"
+  by (simp add: list_all2_iff pointwise_le_def)
+
+lemma pointwise_append_le_iff [simp]: "u@x \<unlhd> u@y \<longleftrightarrow> x \<unlhd> y"
+  by (auto simp: pointwise_le_iff_nth nth_append)
+
+lemma pointwise_le_refl [iff]: "x \<unlhd> x"
+  by (simp add: list.rel_refl pointwise_le_def)
+
+lemma pointwise_le_antisym: "\<lbrakk>x \<unlhd> y; y \<unlhd> x\<rbrakk> \<Longrightarrow> x=y"
+  by (metis antisym list_all2_antisym pointwise_le_def)
+
+lemma pointwise_le_trans: "\<lbrakk>x \<unlhd> y; y \<unlhd> z\<rbrakk> \<Longrightarrow> x \<unlhd> z"
+  by (smt (verit, del_insts) le_trans list_all2_trans pointwise_le_def)
+
+lemma pointwise_le_Nil [simp]: "Nil \<unlhd> x \<longleftrightarrow> x = Nil"
+  by (simp add: pointwise_le_def)
+
+lemma pointwise_le_Nil2 [simp]: "x \<unlhd> Nil \<longleftrightarrow> x = Nil"
+  by (simp add: pointwise_le_def)
+
+lemma pointwise_le_iff_less_equal: "x \<unlhd> y \<longleftrightarrow> x \<lhd> y \<or> x = y"
+  using pointwise_le_refl pointwise_less_def by blast
+
+lemma pointwise_less_iff:
+  "x \<lhd> y \<longleftrightarrow> x \<unlhd> y \<and> (\<exists>(i,j) \<in> 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 \<lhd> y \<longleftrightarrow> x \<unlhd> y \<and> (\<exists>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]: "\<not> Nil \<lhd> x"
+  by (simp add: pointwise_less_def)
+
+lemma pointwise_less_Nil2 [simp]: "\<not> x \<lhd> Nil"
+  by (simp add: pointwise_less_def)
+
+lemma zero_pointwise_le_iff [simp]: "replicate r 0 \<unlhd> x \<longleftrightarrow> length x = r"
+  by (auto simp add: pointwise_le_iff_nth)
+
+lemma pointwise_le_imp_\<sigma>:
+  assumes "xs \<unlhd> ys" shows "\<sigma> xs \<le> \<sigma> 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\<le>y" "xs = x#xs'" "xs' \<unlhd> 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 "\<sigma> (xs + ys) = \<sigma> xs + \<sigma> ys"
+  using assms by (simp add: plus_list_def case_prod_unfold sum_list_addf)
+
+lemma sum_list_minus:
+  assumes "xs \<unlhd> ys" shows "\<sigma> (ys - xs) = \<sigma> ys - \<sigma> xs"
+  using assms
+proof (induction ys arbitrary: xs)
+  case (Cons y ys)
+  then obtain x xs' where "x\<le>y" "xs = x#xs'" "xs' \<unlhd> ys"
+    by (auto simp: pointwise_le_def list_all2_Cons2)
+  then show ?case
+    using pointwise_le_imp_\<sigma> by (auto simp: Cons minus_Cons)
+qed (auto simp: in_set_conv_nth)
+
+
+subsection \<open>Pointwise minimum and maximum of a set of lists\<close>
+
+definition min_pointwise :: "[nat, nat list set] \<Rightarrow> nat list"
+  where "min_pointwise \<equiv> \<lambda>r U. map (\<lambda>i. Min ((\<lambda>u. u!i) ` U)) [0..<r]"
+
+lemma min_pointwise_le: "\<lbrakk>u \<in> U; finite U\<rbrakk> \<Longrightarrow> min_pointwise (length u) U \<unlhd> u"
+  by (simp add: min_pointwise_def pointwise_le_iff_nth)
+
+lemma min_pointwise_ge_iff:
+  assumes "finite U" "U \<noteq> {}" "\<And>u. u \<in> U \<Longrightarrow> length u = r" "length x = r"
+  shows "x \<unlhd> min_pointwise r U \<longleftrightarrow> (\<forall>u \<in> U. x \<unlhd> u)"
+  by (auto simp: min_pointwise_def pointwise_le_iff_nth assms)
+
+definition max_pointwise :: "[nat, nat list set] \<Rightarrow> nat list"
+  where "max_pointwise \<equiv> \<lambda>r U. map (\<lambda>i. Max ((\<lambda>u. u!i) ` U)) [0..<r]"
+
+lemma max_pointwise_ge: "\<lbrakk>u \<in> U; finite U\<rbrakk> \<Longrightarrow> u \<unlhd> max_pointwise (length u) U"
+  by (simp add: max_pointwise_def pointwise_le_iff_nth)
+
+lemma max_pointwise_le_iff:
+  assumes "finite U" "U \<noteq> {}" "\<And>u. u \<in> U \<Longrightarrow> length u = r" "length x = r"
+  shows "max_pointwise r U \<unlhd> x \<longleftrightarrow> (\<forall>u \<in> U. u \<unlhd> x)"
+  by (auto simp: max_pointwise_def pointwise_le_iff_nth assms)
+
+lemma max_pointwise_mono:
+  assumes "X' \<subseteq> X" "finite X" "X' \<noteq> {}"
+  shows  "max_pointwise r X' \<unlhd> max_pointwise r X"
+  using assms by (simp add: max_pointwise_def pointwise_le_iff_nth Max_mono image_mono)
+
+lemma pointwise_le_plus: "\<lbrakk>xs \<unlhd> ys; length ys \<le> length zs\<rbrakk> \<Longrightarrow> xs \<unlhd> 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: "\<lbrakk>z \<unlhd> x;  z \<unlhd> y; x - z = y - z\<rbrakk> \<Longrightarrow> x = y"
+  unfolding pointwise_le_iff_nth by (metis eq_diff_iff nth_equalityI nth_minus_list)
+
+
+subsection \<open>A locale to fix the finite subset @{term "A \<subseteq> G"}\<close>
+
+locale Khovanskii = additive_abelian_group +
+  fixes A :: "'a set"
+  assumes AsubG: "A \<subseteq> G" and finA: "finite A" and nonempty: "A \<noteq> {}"
+
+begin
+
+text \<open>finite products of a group element\<close>
+definition Gmult :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
+  where "Gmult a n \<equiv> (((\<oplus>)a) ^^ n) \<zero>"
+
+lemma Gmult_0 [simp]: "Gmult a 0 = \<zero>"
+  by (simp add: Gmult_def)
+
+lemma Gmult_1 [simp]: "a \<in> G \<Longrightarrow> Gmult a (Suc 0) = a"
+  by (simp add: Gmult_def)
+
+lemma Gmult_Suc [simp]: "Gmult a (Suc n) = a \<oplus> Gmult a n"
+  by (simp add: Gmult_def)
+
+lemma Gmult_in_G [simp,intro]: "a \<in> G \<Longrightarrow> Gmult a n \<in> G"
+  by (induction n) auto
+
+lemma Gmult_add_add:
+  assumes "a \<in> G"
+  shows "Gmult a (m+n) = Gmult a m \<oplus> Gmult a n"
+  by (induction m) (use assms local.associative in fastforce)+
+
+lemma Gmult_add_diff:
+  assumes "a \<in> G"
+  shows "Gmult a (n+k) \<ominus> 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 \<in> G" "n\<le>m"
+  shows "Gmult a m \<ominus> Gmult a n = Gmult a (m-n)"
+  by (metis Gmult_add_diff assms le_add_diff_inverse)
+
+
+text \<open>Mapping elements of @{term A} to their numeric subscript\<close>
+abbreviation "idx \<equiv> to_nat_on A"
+
+text \<open>The elements of @{term A} in order\<close>
+definition aA :: "'a list"
+  where "aA \<equiv> map (from_nat_into A) [0..<card A]"
+
+definition \<alpha> :: "nat list \<Rightarrow> 'a"
+  where "\<alpha> \<equiv> \<lambda>x. fincomp (\<lambda>i. Gmult (aA!i) (x!i)) {..<card A}"
+
+text \<open>The underlying assumption is @{term "length y = length x"}\<close>
+definition useless:: "nat list  \<Rightarrow> bool"
+  where "useless x \<equiv> \<exists>y < x. \<sigma> y = \<sigma> x \<and> \<alpha> y = \<alpha> x \<and> length y = length x"
+
+abbreviation "useful x \<equiv> \<not> useless x"
+
+lemma alpha_replicate_0 [simp]: "\<alpha> (replicate (card A) 0) = \<zero>"
+  by (auto simp: \<alpha>_def intro: fincomp_unit_eqI)
+
+lemma idx_less_cardA:
+  assumes "a \<in> 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 \<in> 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 \<Longrightarrow> aA!i \<in> G"
+  using AsubG aA_def set_aA by auto
+
+lemma alpha_in_G [iff]: "\<alpha> x \<in> G"
+  using nth_aA_in_G fincomp_closed by (simp add: \<alpha>_def)
+
+lemma Gmult_in_PiG [simp]: "(\<lambda>i. Gmult (aA!i) (f i)) \<in> {..<card A} \<rightarrow> G"
+  by simp
+
+lemma alpha_plus:
+  assumes "length x = card A" "length y = card A"
+  shows "\<alpha> (x + y) = \<alpha> x \<oplus> \<alpha> y"
+proof -
+  have "\<alpha> (x + y) = fincomp (\<lambda>i. Gmult (aA!i) (map2 (+) x y!i)) {..<card A}"
+    by (simp add: \<alpha>_def plus_list_def)
+  also have "\<dots> = fincomp (\<lambda>i. Gmult (aA!i) (x!i + y!i)) {..<card A}"
+    by (intro fincomp_cong'; simp add: assms)
+  also have "\<dots> = fincomp (\<lambda>i. Gmult (aA!i) (x!i) \<oplus> Gmult (aA!i) (y!i)) {..<card A}"
+    by (intro fincomp_cong'; simp add: Gmult_add_add)
+  also have "\<dots> = \<alpha> x \<oplus> \<alpha> y"
+    by (simp add: \<alpha>_def fincomp_comp)
+  finally show ?thesis .
+qed
+
+lemma alpha_minus:
+  assumes "y \<unlhd> x" "length y = card A"
+  shows "\<alpha> (x - y) = \<alpha> x \<ominus> \<alpha> y"
+proof -
+  have "\<alpha> (x - y) = fincomp (\<lambda>i. Gmult (aA!i) (map2 (-) x y!i)) {..<card A}"
+    by (simp add: \<alpha>_def minus_list_def)
+  also have "\<dots> = fincomp (\<lambda>i. Gmult (aA!i) (x!i - y!i)) {..<card A}"
+    using assms by (intro fincomp_cong') (auto simp: pointwise_le_iff)
+  also have "\<dots> = fincomp (\<lambda>i. Gmult (aA!i) (x!i) \<ominus> Gmult (aA!i) (y!i)) {..<card A}"
+    using assms
+    by (intro fincomp_cong') (simp add: pointwise_le_iff_nth Gmult_diff)+
+  also have "\<dots> = \<alpha> x \<ominus> \<alpha> y"
+    by (simp add: \<alpha>_def fincomp_comp fincomp_inverse)
+  finally show ?thesis .
+qed
+
+subsection \<open>Adding one to a list element\<close>
+
+definition list_incr :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
+  where "list_incr i x \<equiv> 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 \<Longrightarrow> \<sigma> (list_incr i x) = Suc (\<sigma> 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 \<Longrightarrow> x!i \<le> 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 \<Longrightarrow> list_incr j x!i - x!i = (if i = j then 1 else 0)"
+  by (simp add: list_incr_def)
+
+subsection \<open>The set of all @{term r}-tuples that sum to @{term n}\<close>
+
+definition length_sum_set :: "nat \<Rightarrow> nat \<Rightarrow> nat list set"
+  where "length_sum_set r n \<equiv> {x. length x = r \<and> \<sigma> 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 \<in> length_sum_set (Suc r) n \<longleftrightarrow> (\<exists>m. ks \<in> length_sum_set r m \<and> n = m+k)"
+  by (auto simp: length_sum_set_def)
+
+lemma length_sum_set_Suc_eqpoll: "length_sum_set (Suc r) n \<approx> Sigma {..n} (\<lambda>i. length_sum_set r (n-i))" (is "?L \<approx> ?R")
+  unfolding eqpoll_def
+proof
+  let ?f = "(\<lambda>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) = (\<Sum>i\<le>n. card (length_sum_set r (n-i)))"
+proof -
+  have "card (length_sum_set (Suc r) n) = card (Sigma {..n} (\<lambda>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 "\<dots> = (\<Sum>i\<le>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 \<le> n" shows "(\<Sum>i\<le>n. f i) = (\<Sum>i\<le>n-N. f i) + (\<Sum>i=Suc (n-N)..n. f i)"
+  by (metis assms diff_add sum_up_index_split)
+
+lemma sum_invert: "N \<le> n \<Longrightarrow> (\<Sum>i = Suc (n - N)..n. f (n - i)) = (\<Sum>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 sum_diff_split:
+  assumes "N \<le> n"
+  shows "(\<Sum>i\<le>n - N. real (n - i) ^ j) = (\<Sum>i\<le>n. real i ^ j) - (\<Sum>i<N. real i ^ j)"
+proof -
+  have inj: "inj_on ((-) n) {N..n}"
+    by (auto simp: inj_on_def)
+  have "(\<Sum>i\<le>n - N. real (n - i) ^ j) = (\<Sum>i\<in>(-) n ` {N..n}. real (n - i) ^ j)"
+  proof (rule sum.cong)
+    have "\<And>x. x \<le> n - N \<Longrightarrow> \<exists>m\<ge>N. m \<le> n \<and> x = n - m"
+      by (metis assms diff_diff_cancel diff_le_mono2 diff_le_self le_trans)
+    then show "{..n - N} = (-) n ` {N..n}"
+      by (auto simp add: image_iff Bex_def)
+  qed auto
+  also have "\<dots> = (\<Sum>i=N..n. real i ^ j)"
+    using sum.reindex [OF inj, of "\<lambda>i. real (n - i) ^ j", symmetric]
+    by (simp add: )
+  also have "\<dots> = (\<Sum>i\<le>n. real i ^ j) - (\<Sum>i<N. real i ^ j)"
+  proof (cases N)
+    case 0
+    then show ?thesis
+      using atMost_atLeast0 by auto
+  next
+    case (Suc N')
+    then show ?thesis
+      using assms sum_up_index_split [of _ N' "n-N'"]
+      by (smt (verit, best) Suc_diff_le add_Suc_shift diff_Suc_Suc le_add_diff_inverse lessThan_Suc_atMost)
+  qed
+  finally show ?thesis .
+qed
+
+
+lemma real_polynomial_function_length_sum_set:
+  "\<exists>p. real_polynomial_function p \<and> (\<forall>n>0. real (card (length_sum_set r n)) = p (real n))"
+proof (induction r)
+  case 0
+  have "\<forall>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: "\<And>n. n>0 \<Longrightarrow> real (card (length_sum_set r n)) = p (real n)"
+    by blast
+  then obtain a n where p_eq: "p = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i)"
+    using real_polynomial_function_iff_sum by auto
+  define q where "q \<equiv> \<lambda>x. \<Sum>j\<le>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: "(\<Sum>x\<le>n - 1. p (real (n - x))) = q (real n)" if "n>0" for n
+    using that
+    by (simp add: p_eq q_def sum.swap sum_diff_split add.commute sum_of_powers flip: sum_distrib_left)
+  define p' where "p' \<equiv> \<lambda>x. q x + real (card (length_sum_set r 0))"
+  have "real_polynomial_function p'"
+    using rp_q by (force simp add: p'_def)
+  moreover have "(\<Sum>x\<le>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) = (\<Union>i<r. list_incr i ` length_sum_set r n)"
+proof -
+  have "\<exists>i<r. x \<in> list_incr i ` length_sum_set r n"
+    if "\<sigma> x = Suc n" and "r = length x" for x
+  proof -
+    have "x \<noteq> 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 \<noteq> 0"
+      by (metis \<open>r = length x\<close> in_set_conv_nth replicate_eqI)
+    with that have "x[i := x!i - 1] \<in> 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 \<in> A" "x \<in> length_sum_set (card A) n"
+  shows "\<alpha> (list_incr (idx a) x) = a \<oplus> \<alpha> x"
+proof -
+  have lenx: "length x = card A"
+    using assms length_sum_set_def by blast
+  have "\<alpha> (list_incr (idx a) x) \<ominus> \<alpha> x = fincomp (\<lambda>i. Gmult (aA!i) (list_incr (idx a) x!i) \<ominus> Gmult (aA!i) (x!i)) {..<card A}"
+    by (simp add: \<alpha>_def fincomp_comp fincomp_inverse)
+  also have "\<dots> = fincomp (\<lambda>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 "\<dots> = fincomp (\<lambda>i. if i = idx a then (aA!i) else \<zero>) {..<card A}"
+    by (intro fincomp_cong'; simp add: list_incr_nth_diff lenx)
+  also have "\<dots> = a"
+    using assms by (simp add: fincomp_singleton_swap idx_less_cardA)
+  finally have "\<alpha> (list_incr (idx a) x) \<ominus> \<alpha> 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 \<equiv> card A"
+  shows "sumset_iterated A n = \<alpha> ` 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) = (\<Union>a\<in>A. (\<lambda>i. a \<oplus> \<alpha> i) ` length_sum_set r n)"
+    using AsubG by (auto simp: Suc sumset)
+  also have "\<dots> = (\<Union>a\<in>A. (\<lambda>i. \<alpha> (list_incr (idx a) i)) ` length_sum_set r n)"
+    by (simp add: alpha_list_incr r_def)
+  also have "\<dots> = \<alpha> ` 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 \<open>Lemma 2.7 in Gowers's notes\<close>
+
+text\<open>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.\<close>
+
+lemma card_sumset_iterated_length_sum_set_useful:
+  defines "r \<equiv> card A"
+  shows "card(sumset_iterated A n) = card (length_sum_set r n \<inter> {x. useful x})"
+    (is "card ?L = card ?R")
+proof -
+  have "\<alpha> x \<in> \<alpha> ` (length_sum_set r n \<inter> {x. useful x})"
+    if "x \<in> length_sum_set r n" for x
+  proof -
+    define y where "y \<equiv> LEAST y. y \<in> length_sum_set r n \<and> \<alpha> y = \<alpha> x"
+    have y: "y \<in> length_sum_set (card A) n \<and> \<alpha> y = \<alpha> x"
+      by (metis (mono_tags, lifting) LeastI r_def y_def that)
+    moreover
+    have "useful y"
+    proof (clarsimp simp: useless_def)
+      show False
+        if "\<sigma> z = \<sigma> y" "length z = length y" and "z < y" "\<alpha> z = \<alpha> 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 = \<alpha> ` (length_sum_set r n \<inter> {x. useful x})"
+    by (auto simp: sumset_iterated_enum length_sum_set_def r_def)
+  moreover have "inj_on \<alpha> (length_sum_set r n \<inter> {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\<open>The following lemma corresponds to Lemma 2.7 in Gowers's notes.\<close>
+
+lemma useless_leq_useless:
+  defines "r \<equiv> card A"
+  assumes "useless x" and "x \<unlhd> 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 \<sigma>x': "\<sigma> x' = \<sigma> x" and \<alpha>x': "\<alpha> x' = \<alpha> 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 \<open>x'<x\<close> lenx' assms by (auto simp: list_less_def lenlex_def elim!: lex_take_index)
+  define y' where "y' \<equiv> y+x'-x"
+  have leny': "length y' = length y"
+    using assms lenx' pointwise_le_iff  by (simp add: y'_def)
+  have "x!i \<le> y!i"
+    using \<open>x \<unlhd> y\<close> \<open>i < card A\<close> assms by (simp add: pointwise_le_iff_nth)
+  then have "y'!i < y!i"
+    using \<open>i < card A\<close> 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 "\<And>k. k < length (take i y') \<Longrightarrow> 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' \<open>i < card A\<close> assms pointwise_le_iff
+    by (auto simp: list_less_def lenlex_def lexord_lex lexord_take_index_conv)
+  moreover have "\<sigma> y' = \<sigma> y"
+    using assms
+    by (simp add: \<sigma>x' lenx' leny pointwise_le_plus sum_list_minus sum_list_plus y'_def)
+  moreover have "\<alpha> y' = \<alpha> y"
+    using assms lenx' \<alpha>x' leny
+    by (fastforce simp add: 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 "\<lbrakk>x \<in> U; \<And>y. y \<in> U \<Longrightarrow> \<not> y \<lhd> x\<rbrakk> \<Longrightarrow> x \<in> minimal_elements U"
+
+
+lemma pointwise_less_imp_\<sigma>:
+  assumes "xs \<lhd> ys" shows "\<sigma> xs < \<sigma> ys"
+proof -
+  have eq: "length ys = length xs" and "xs \<unlhd> ys"
+    using assms by (auto simp: pointwise_le_iff pointwise_less_iff)
+  have "\<forall>k<length xs. xs!k \<le> ys!k"
+    using \<open>xs \<unlhd> ys\<close> list_all2_nthD pointwise_le_def by auto
+  moreover have "\<exists>k<length xs. xs!k < ys!k"
+    using assms pointwise_less_iff2 by force
+  ultimately show ?thesis
+    by (force simp add: eq sum_list_sum_nth intro: sum_strict_mono_ex1)
+qed
+
+lemma wf_measure_\<sigma>: "wf (inv_image less_than \<sigma>)"
+  by blast
+
+lemma WFP: "wfP (\<lhd>)"
+  by (auto simp: wfP_def pointwise_less_imp_\<sigma> intro: wf_subset [OF wf_measure_\<sigma>])
+
+text\<open>The following is a direct corollary of the above lemma, i.e. a corollary of
+ Lemma 2.7 in Gowers's notes.\<close>
+
+corollary useless_iff:
+  assumes "length x = card A"
+  shows "useless x \<longleftrightarrow> (\<exists>x' \<in> minimal_elements (Collect useless). x' \<unlhd> x)"  (is "_=?R")
+proof
+  assume "useless x"
+  obtain z where z: "useless z" "z \<unlhd> x" and zmin: "\<And>y. y \<lhd> z \<Longrightarrow> y \<unlhd> x \<Longrightarrow> useful y"
+    using wfE_min [to_pred, where Q = "{z. useless z \<and> z \<unlhd> x}", OF WFP]
+    by (metis (no_types, lifting) \<open>useless x\<close> 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 \<open>The set of minimal elements of a set of $r$-tuples is finite\<close>
+
+text\<open>The following general finiteness claim corresponds to Lemma 2.8 in Gowers's notes and is key to
+the main proof.\<close>
+
+lemma minimal_elements_set_tuples_finite:
+  assumes Ur: "\<And>x. x \<in> U \<Longrightarrow> length x = r"
+  shows "finite (minimal_elements U)"
+  using assms
+proof (induction r arbitrary: U)
+  case 0
+  then have "U \<subseteq> {[]}"
+    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 \<in> U" and zmin: "\<And>y. y \<lhd> u \<Longrightarrow> y \<notin> U"
+      using wfE_min [to_pred, where Q = "U", OF WFP] by blast
+    define V where "V = {v \<in> U. \<not> u \<unlhd> v}"
+    define VF where "VF \<equiv> \<lambda>i t. {v \<in> V. v!i = t}"
+    have [simp]: "length v = Suc r" if "v \<in> VF i t" for v i t
+      using that by (simp add: Suc.prems VF_def V_def)
+    have *: "\<exists>i\<le>r. v!i < u!i" if "v \<in> V" for v
+      using that u Suc.prems
+      by (force simp add: V_def pointwise_le_iff_nth not_le less_Suc_eq_le)
+    with u have "minimal_elements U \<le> insert u (\<Union>i\<le>r. \<Union>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\<le>r" "t < u!i" for i t
+    proof -
+      define delete where "delete \<equiv> \<lambda>v::nat list. take i v @ drop (Suc i) v" \<comment> \<open>deletion of @{term i}\<close>
+      have len_delete[simp]: "length (delete u) = r" if "u \<in> VF i t" for u
+        using Suc.prems VF_def V_def \<open>i \<le> r\<close> delete_def that by auto
+      have nth_delete: "delete u!k = (if k<i then u!k else u!Suc k)" if "u \<in> VF i t" "k<r" for u k
+        using that by (simp add: delete_def nth_append)
+      have delete_le_iff [simp]: "delete u \<unlhd> delete v \<longleftrightarrow> u \<unlhd> v" if "u \<in> VF i t" "v \<in> VF i t" for u v
+      proof
+        assume "delete u \<unlhd> delete v"
+        then have "\<forall>j. (j < i \<longrightarrow> u!j \<le> v!j) \<and> (j < r \<longrightarrow> i \<le> j \<longrightarrow> u!Suc j \<le> v!Suc j)"
+          using that \<open>i \<le> r\<close>
+          by (force simp add: pointwise_le_iff_nth nth_delete split: if_split_asm cong: conj_cong)
+        then show "u \<unlhd> v"
+          using that \<open>i \<le> r\<close>
+          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 \<unlhd> v" then show "delete u \<unlhd> delete v"
+          using that by (simp add: pointwise_le_iff_nth nth_delete)
+      qed
+      then have delete_eq_iff: "delete u = delete v \<longleftrightarrow> u = v" if "u \<in> VF i t" "v \<in> VF i t" for u v
+        by (metis that pointwise_le_antisym pointwise_le_refl)
+      have delete_less_iff: "delete u \<lhd> delete v \<longleftrightarrow> u \<lhd> v" if "u \<in> VF i t" "v \<in> 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 \<in> V" for v
+        using id_take_nth_drop Suc.prems V_def \<open>i \<le> r\<close> 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)) \<subseteq> 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 \<open>Towards Lemma 2.9 in Gowers's notes\<close>
+
+text \<open>Increasing sequences\<close>
+fun augmentum :: "nat list \<Rightarrow> nat list"
+  where "augmentum [] = []"
+  | "augmentum (n#ns) = n # map ((+)n) (augmentum ns)"
+
+definition dementum:: "nat list \<Rightarrow> nat list"
+  where "dementum xs \<equiv> xs - (0#xs)"
+
+lemma dementum_Nil [simp]: "dementum [] = []"
+  by (simp add: dementum_def)
+
+lemma zero_notin_augmentum [simp]: "0 \<notin> set ns \<Longrightarrow> 0 \<notin> 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 \<notin> set ns \<Longrightarrow> sorted (augmentum ns)"
+  by (induction ns) auto
+
+lemma distinct_augmentum [simp]: "0 \<notin> set ns \<Longrightarrow> distinct (augmentum ns)"
+  by (induction ns) (simp_all add: image_iff)
+
+lemma augmentum_subset_sum_list: "set (augmentum ns) \<subseteq> {..\<sigma> ns}"
+  by (induction ns) auto
+
+lemma sum_list_augmentum: "\<sigma> ns \<in> set (augmentum ns) \<longleftrightarrow> 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 \<unlhd> 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 "\<sigma> (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 \<circ> (+) n = (+) (k+n)" by auto
+  then show ?case
+    by (simp add: minus_Cons Cons)
+qed
+
+lemma dementum_augmentum [simp]:
+  assumes "0 \<notin> set ns"
+  shows "(dementum \<circ> sorted_list_of_set) ((set \<circ> 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 \<notin> set ns"
+  shows "0 \<notin> set (dementum ns)"
+  unfolding dementum_def minus_list_def
+  using sorted_wrt_nth_less [OF ns] 0
+  by (auto simp add: in_set_conv_nth image_iff set_zip nth_Cons' dest: leD)
+
+lemma nth_augmentum [simp]: "i < length ns \<Longrightarrow> augmentum ns!i = (\<Sum>j\<le>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 "\<dots> = a + (\<Sum>j\<in>{0<..i}. ns!(j-1))"
+      using sum.reindex [of Suc "{..i - Suc 0}" "\<lambda>j. ns!(j-1)", symmetric] False
+      by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost del: sum.cl_ivl_Suc)
+    also have "\<dots> = (\<Sum>j = 0..i. if j=0 then a else ns!(j-1))"
+      by (simp add: sum.head)
+    also have "\<dots> = sum ((!) (a # ns)) {..i}"
+      by (simp add: nth_Cons' atMost_atLeast0)
+    finally show ?thesis .
+  qed auto
+qed
+
+lemma augmentum_dementum [simp]:
+  assumes "0 \<notin> 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: "\<And>j. \<lbrakk>0 < j; j \<le> i\<rbrakk> \<Longrightarrow> ns ! (j - Suc 0) \<le> ns ! j"
+      using \<open>sorted ns\<close> i by (simp add: sorted_iff_nth_mono)
+    have "augmentum (dementum ns)!i = (\<Sum>j\<le>i. ns!j - (if j = 0 then 0 else ns!(j-1)))"
+      using i by (simp add: dementum_def nth_Cons')
+    also have "\<dots> = (\<Sum>j=0..i. if j = 0 then ns!0 else ns!j - ns!(j-1))"
+      by (smt (verit, best) diff_zero sum.cong atMost_atLeast0)
+    also have "\<dots> = ns!0 + (\<Sum>j\<in>{0<..i}. ns!j - ns!(j-1))"
+      by (simp add: sum.head)
+    also have "\<dots> = ns!0 + ((\<Sum>j\<in>{0<..i}. ns!j) - (\<Sum>j\<in>{0<..i}. ns!(j-1)))"
+      by (auto simp: ns_le intro: sum_subtractf_nat)
+    also have "\<dots> = ns!0 + (\<Sum>j\<in>{0<..i}. ns!j) - (\<Sum>j\<in>{0<..i}. ns!(j-1))"
+    proof -
+      have "(\<Sum>j\<in>{0<..i}. ns ! (j - 1)) \<le> sum ((!) ns) {0<..i}"
+        by (metis One_nat_def greaterThanAtMost_iff ns_le sum_mono)
+      then show ?thesis by simp
+    qed
+    also have "\<dots> = ns!0 + (\<Sum>j\<in>{0<..i}. ns!j) - (\<Sum>j\<le>i-Suc 0. ns!j)"
+      using sum.reindex [of Suc "{..i - Suc 0}" "\<lambda>j. ns!(j-1)", symmetric] False
+      by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost)
+    also have "\<dots> = (\<Sum>j=0..i. ns!j) - (\<Sum>j\<le>i-Suc 0. ns!j)"
+      by (simp add:  sum.head [of 0 i])
+    also have "\<dots> = (\<Sum>j=0..i-Suc 0. ns!j) + ns!i - (\<Sum>j\<le>i-Suc 0. ns!j)"
+      by (metis False Suc_pred less_Suc0 not_less_eq sum.atLeast0_atMost_Suc)
+    also have "\<dots> = ns!i"
+      by (simp add: atLeast0AtMost)
+    finally show "augmentum (dementum ns)!i = ns!i" .
+  qed
+qed auto
+
+text\<open>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.  \<close>
+
+lemma bound_sum_list_card:
+  assumes "r > 0" and n: "n \<ge> \<sigma> x'" and lenx': "length x' = r"
+  defines "S \<equiv> {x. x' \<unlhd> x \<and> \<sigma> x = n}"
+  shows "card S = (n - \<sigma> x' + r - 1) choose (r-1)"
+proof-
+  define m where "m \<equiv> n - \<sigma> x'"
+  define f where "f \<equiv> \<lambda>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 "\<And>x. x \<in> S \<Longrightarrow> f x \<in> 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 \<in> f ` S" if "x \<in> length_sum_set r m" for x
+    proof
+      have x[simp]: "length x = r" "\<sigma> 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' \<unlhd> x' + x"
+        by (simp add: lenx' pointwise_le_plus)
+      moreover have "\<sigma> (x' + x) = n"
+        by (simp add: lenx' m_def n sum_list_plus)
+      ultimately show "x' + x \<in> S"
+        using S_def by blast
+    qed
+    ultimately show "f ` S = length_sum_set r m" by auto
+  qed
+  define g where "g \<equiv> \<lambda>x::nat list. map Suc x"
+  define g' where "g' \<equiv> \<lambda>x::nat list. x - replicate (length x) 1"
+  define T where "T \<equiv> length_sum_set r (m+r) \<inter> 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 "\<And>x. x \<in> length_sum_set r m \<Longrightarrow> g x \<in> T"
+      by (auto simp: g_def length_sum_set_def sum_list_Suc T_def)
+    moreover have "x \<in> g ` length_sum_set r m" if "x \<in> 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) \<unlhd> 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 \<in> 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 \<equiv> (insert (m+r)) ` finsets {0<..<m+r} (r-1)"
+  have h: "bij_betw (set \<circ> augmentum) T U"
+  proof (intro bij_betw_imageI)
+    show "inj_on ((set \<circ> augmentum)) T"
+      unfolding inj_on_def T_def
+      by (metis ComplD IntE dementum_augmentum in_listsD insertI1)
+    have "(set \<circ> augmentum) t \<in> U" if "t \<in> T" for t
+    proof -
+      have t: "length t = r" "\<sigma> t = m+r" "0 \<notin> set t"
+        using that by (force simp add: T_def length_sum_set_def)+
+      then have mrt: "m + r \<in> set (augmentum t)"
+        by (metis \<open>r>0\<close> 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} \<in> 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 \<in> (set \<circ> augmentum) ` T" if "u \<in> U" for u
+    proof
+      from that
+      obtain N where u: "u = insert (m + r) N" and Nsub: "N \<subseteq> {0<..<m + r}"
+        and [simp]: "card N = r - Suc 0"
+        by (auto simp add: U_def finsets_def)
+      have [simp]: "0 \<notin> N" "m+r \<notin> N" "finite N"
+        using finite_subset Nsub by auto
+      have [simp]: "card u = r"
+        using Nsub \<open>r>0\<close> by (auto simp add: 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 "\<dots> = 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 \<notin> set (sorted_list_of_set u)"
+        by (simp add: \<open>r>0\<close> set_insort_key so_u_N)
+      show "u = (set \<circ> augmentum) ((dementum \<circ> 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 \<circ> sorted_list_of_set) u \<in> 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 \<circ> augmentum) ` T = U" by auto
+  qed
+  obtain \<phi> where "bij_betw \<phi> S U"
+    by (meson bij_betw_trans f g h)
+  moreover have "card U = (n - \<sigma> 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 "\<dots> = (n - \<sigma> 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 \<open>Towards the main theorem\<close>
+
+lemma extend_tuple:
+  assumes "\<sigma> xs \<le> n" "length xs \<noteq> 0"
+  obtains ys where "\<sigma> ys = n" "xs \<unlhd> ys"
+proof -
+  obtain x xs' where xs: "xs = x#xs'"
+    using assms list.exhaust by auto
+  define y where "y \<equiv> x + n - \<sigma> xs"
+  show thesis
+  proof
+    show "\<sigma> (y#xs') = n"
+      using assms xs y_def by auto
+    show "xs \<unlhd> y#xs'"
+      using assms y_def pointwise_le_def xs by auto
+  qed
+qed
+
+lemma extend_preserving:
+  assumes "\<sigma> xs \<le> n" "length xs > 1" "i < length xs"
+  obtains ys where "\<sigma> ys = n" "xs \<unlhd> ys" "ys!i = xs!i"
+proof -
+  define j where "j \<equiv> 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 \<equiv> x + n - \<sigma> xs"
+  define ys where "ys \<equiv> xs1 @ [y] @ xs2"
+  have "x \<le> y"
+    using assms y_def by linarith
+  show thesis
+  proof
+    show "\<sigma> ys = n"
+      using assms(1) xs y_def ys_def by auto
+    show "xs \<unlhd> ys"
+      using xs ys_def \<open>x \<le> y\<close> pointwise_append_le_iff pointwise_le_def by fastforce
+    have "length xs1 \<noteq> 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\<open>The proof of the main theorem will make use of the inclusion-exclusion formula, in addition to
+the previously shown results.\<close>
+
+theorem Khovanskii:
+  assumes "card A > 1"
+  defines "f \<equiv> \<lambda>n. card(sumset_iterated A n)"
+  obtains N p where "real_polynomial_function p" "\<And>n. n \<ge> N \<Longrightarrow> real (f n) = p (real n)"
+proof -
+  define r where "r \<equiv> card A"
+  define C where "C \<equiv> \<lambda>n x'. {x. x' \<unlhd> x \<and> \<sigma> x = n}"
+  define X where "X \<equiv> minimal_elements {x. useless x \<and> length x = r}"
+  have "r > 1" "r \<noteq> 0"
+    using assms r_def by auto
+  have Csub: "C n x' \<subseteq> length_sum_set (length x') n" for n x'
+    by (auto simp add: 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: "\<And>x'. x' \<in> X \<Longrightarrow>  \<sigma> x' \<le> \<sigma> (max_pointwise r X)"
+    using X_def max_pointwise_ge minimal_elements.simps pointwise_le_imp_\<sigma> 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: "\<And>n. n>0 \<Longrightarrow> 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: "\<And>x. q x = x gchoose (r-1)"
+    using real_polynomial_function_gchoose by metis
+  define p where "p \<equiv> \<lambda>x::real. p0 x - (\<Sum>Y | Y \<subseteq> X \<and> Y \<noteq> {}. (- 1) ^ (card Y + 1) * q((x - real(\<sigma> (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 \<open>finite X\<close> by (intro pf_p0 pf_q' pf_intros | force)+
+  next
+    fix n
+    assume "n \<ge> max 1 (\<sigma> (max_pointwise r X))"
+    then have nlarge: "n \<ge> \<sigma> (max_pointwise r X)" and "n > 0"
+      by auto
+    define U where "U \<equiv> \<lambda>n. length_sum_set r n \<inter> {x. useful x}"
+    have 2: "(length_sum_set r n \<inter> {x. useless x}) = (\<Union>x'\<in>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 \<equiv> \<Sum>I | I \<subseteq> C n ` X \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I))"
+    define SUM2 where "SUM2 \<equiv> \<Sum>Y | Y \<subseteq> X \<and> Y \<noteq> {}. (- 1) ^ (card Y + 1) * int (card (\<Inter>(C n ` Y)))"
+    have SUM1_card: "card(length_sum_set r n \<inter> {x. useless x}) = nat SUM1"
+      unfolding SUM1_def using \<open>finite X\<close> by (simp add: finC 2 card_UNION)
+    have "SUM1 \<ge> 0"
+      unfolding SUM1_def using card_UNION_nonneg finC \<open>finite X\<close> by auto
+    have C_empty_iff: "C n x' = {} \<longleftrightarrow> \<sigma> x' > n" if "length x' \<noteq> 0" for x'
+      by (simp add: set_eq_iff C_def) (meson extend_tuple linorder_not_le pointwise_le_imp_\<sigma> that)
+    have C_eq_1: "C n x' = {[n]}" if "\<sigma> x' \<le> 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: "\<sigma> x \<le> n" if "x \<in> X" for x
+      by (meson le_trans max_X nlarge that)
+    have len_X_r: "x \<in> X \<Longrightarrow> 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' \<in> X" for x'
+    proof (rule pointwise_le_antisym)
+      have [simp]: "length x' = r" "\<sigma> x' \<le> 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') \<unlhd> x'"
+      proof (clarsimp simp add: pointwise_le_iff_nth)
+        fix i
+        assume "i < r"
+        then obtain y where "\<sigma> y = n \<and> x' \<unlhd> y \<and> y!i \<le> x'!i"
+          by (metis extend_preserving \<open>1 < r\<close> \<open>length x' = r\<close> \<open>x' \<in> X\<close> order.refl n_ge_X)
+        then have "\<exists>y\<in>C n x'. y!i \<le> x'!i"
+          using C_def by blast
+        with \<open>i < r\<close> show "min_pointwise r (C n x')!i \<le> x'!i"
+          by (simp add: min_pointwise_def Min_le_iff finC C_empty_iff leD)
+      qed
+      have "x' \<unlhd> min_pointwise r (C n x')" if "\<sigma> x' \<le> n" "length x' = r" for x'
+        by (smt (verit, del_insts) C_def C_empty_iff \<open>r \<noteq> 0\<close> finC leD mem_Collect_eq min_pointwise_ge_iff pointwise_le_iff that)
+      then show "x' \<unlhd> 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 \<open>r>1\<close>)
+    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) - {{}} \<subseteq> (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 (\<lambda>I. (- 1) ^ (card I + 1) * int (card (\<Inter>I))) ((image (C n)) ` (Pow X - {{}}))"
+      unfolding SUM1_def by (auto intro: sum.cong)
+    also have "\<dots> = sum ((\<lambda>I. (- 1) ^ (card I + 1) * int (card (\<Inter> I))) \<circ> (image (C n))) (Pow X - {{}})"
+      by (simp add: sum.reindex inj_on_imageC)
+    also have "\<dots> = 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 \<inter> {x. useful x}) \<union> (length_sum_set r n \<inter> {x. useless x})"
+      by auto
+    then have "card (length_sum_set r n) =
+                card (length_sum_set r n \<inter> {x. useful x}) +
+                card (length_sum_set r n \<inter> 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: \<open>SUM1 = SUM2\<close> SUM1_card)
+    then have SUM2_le: "nat SUM2 \<le> card (C n ?z0)"
+      by arith
+    have \<sigma>_max_pointwise_le: "\<And>Y. \<lbrakk>Y \<subseteq> X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> \<sigma> (max_pointwise r Y) \<le> n"
+      by (meson \<open>finite X\<close> le_trans max_pointwise_mono nlarge pointwise_le_imp_\<sigma>)
+
+    have card_C_max: "card (C n (max_pointwise r Y)) =
+             (n - \<sigma> (max_pointwise r Y) + r - Suc 0 choose (r - Suc 0))"
+      if "Y \<subseteq> X" "Y \<noteq> {}" for Y
+    proof -
+      have [simp]: "length (max_pointwise r Y) = r"
+        by (simp add: max_pointwise_def)
+      then show ?thesis
+        using \<open>r \<noteq> 0\<close> that C_def by (simp add: bound_sum_list_card [of r] \<sigma>_max_pointwise_le)
+    qed
+
+    define SUM3 where "SUM3 \<equiv> (\<Sum>Y | Y \<subseteq> X \<and> Y \<noteq> {}.
+         - ((- 1) ^ (card Y) * ((n - \<sigma> (max_pointwise r Y) + r - 1 choose (r - 1)))))"
+    have "\<Inter>(C n ` Y) = C n (max_pointwise r Y)" if "Y \<subseteq> X" "Y \<noteq> {}" for Y
+    proof
+      show "\<Inter> (C n ` Y) \<subseteq> C n (max_pointwise r Y)"
+        unfolding C_def
+      proof clarsimp
+        fix x
+        assume "\<forall>y\<in>Y. y \<unlhd> x \<and> \<sigma> x = n"
+        moreover have "finite Y"
+          using \<open>finite X\<close> infinite_super that by blast
+        moreover have "\<And>u. u \<in> Y \<Longrightarrow> length u = r"
+          using len_X_r that by blast
+        ultimately show "max_pointwise r Y \<unlhd> x \<and> \<sigma> 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) \<subseteq> \<Inter> (C n ` Y)"
+        apply (clarsimp simp: C_def)
+        by (metis \<open>finite X\<close> 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 \<inter> {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 \<inter> {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 \<ge> 0"
+      using \<open>0 \<le> SUM1\<close> \<open>SUM1 = SUM2\<close> \<open>SUM2 = SUM3\<close> by blast
+    have **: "\<And>Y. \<lbrakk>Y \<subseteq> X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> Suc (\<sigma> (max_pointwise r Y)) \<le> n + r"
+      by (metis \<open>1 < r\<close> \<sigma>_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 "\<dots> = card (C n ?z0) -  nat SUM3"
+      using card_U_eq_diff \<open>SUM1 = SUM2\<close> \<open>SUM2 = SUM3\<close> by presburger
+    also have "\<dots> = real (card (C n (replicate r 0))) - real (nat SUM3)"
+      using SUM2_le \<open>SUM2 = SUM3\<close> of_nat_diff by blast
+    also have "\<dots> = p (real n)"
+      using \<open>1 < r\<close> \<open>n>0\<close>
+      apply (simp add: p_def p0 q \<open>SUM3 \<ge> 0\<close>)
+      apply (simp add: SUM3_def binomial_gbinomial of_nat_diff \<sigma>_max_pointwise_le algebra_simps **)
+      done
+    finally show "real (f n) = p (real n)" .
+  qed
+qed
+
+end
+
+end
diff --git a/thys/Khovanskii_Theorem/ROOT b/thys/Khovanskii_Theorem/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Khovanskii_Theorem/ROOT
@@ -0,0 +1,15 @@
+chapter AFP
+
+session Khovanskii_Theorem (AFP) = "HOL-Analysis" +
+  options [timeout = 600]
+  sessions
+    Jacobson_Basic_Algebra
+    Pluennecke_Ruzsa_Inequality
+    Bernoulli
+    "HOL-Library"
+  theories
+    Khovanskii
+  document_files
+    "root.tex"
+    "root.bib"
+
diff --git a/thys/Khovanskii_Theorem/document/root.bib b/thys/Khovanskii_Theorem/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Khovanskii_Theorem/document/root.bib
@@ -0,0 +1,70 @@
+%% This BibTeX bibliography file was created using BibDesk.
+%% http://bibdesk.sourceforge.net/
+
+
+%% Created for Larry Paulson at 2022-09-02 15:10:09 +0100 
+
+
+%% Saved with string encoding Unicode (UTF-8) 
+
+
+
+@article{nathanson-polynomial-growth,
+	author = {Nathanson, Melvyn B. and Ruzsa, Imre Z.},
+	date-added = {2022-09-02 15:10:06 +0100},
+	date-modified = {2022-09-02 15:10:06 +0100},
+	journal = {Journal de Th{\'e}orie des Nombres de Bordeaux},
+	number = {2},
+	pages = {553-560},
+	title = {Polynomial Growth of Sumsets in Abelian Semigroups},
+	volume = {14},
+	year = {2002}}
+
+@unpublished{ruzsa-sumsets-structure,
+	author = {Imre Z. Ruzsa},
+	date-added = {2022-09-02 15:09:54 +0100},
+	date-modified = {2022-09-02 15:09:54 +0100},
+	note = {Lecture notes, Institute of Mathematics, Budapest},
+	title = {Sumsets and Structure}}
+
+@article{khovanskii-newton-polyhedron,
+	author = {Khovanskii, A.  G. },
+	date = {1992/10/01},
+	date-added = {2022-09-02 15:08:56 +0100},
+	date-modified = {2022-09-02 15:08:56 +0100},
+	doi = {10.1007/BF01075048},
+	id = {Khovanskii1992},
+	isbn = {1573-8485},
+	journal = {Functional Analysis and Its Applications},
+	number = {4},
+	pages = {276-281},
+	title = {{Newton} Polyhedron, {Hilbert} Polynomial, and Sums of Finite Sets},
+	url = {https://doi.org/10.1007/BF01075048},
+	volume = {26},
+	year = {1992},
+	bdsk-url-1 = {https://doi.org/10.1007/BF01075048}}
+
+@article{khovanskii-sums-finite,
+	author = {Khovanskii, A.  G. },
+	date = {1995/04/01},
+	date-added = {2022-09-02 15:08:53 +0100},
+	date-modified = {2022-09-02 15:08:53 +0100},
+	doi = {10.1007/BF01080008},
+	id = {Khovanskii1995},
+	isbn = {1573-8485},
+	journal = {Functional Analysis and Its Applications},
+	number = {2},
+	pages = {102-112},
+	title = {Sums of finite sets, orbits of commutative semigroups, and {Hilbert} functions},
+	url = {https://doi.org/10.1007/BF01080008},
+	volume = {29},
+	year = {1995},
+	bdsk-url-1 = {https://doi.org/10.1007/BF01080008}}
+
+@unpublished{gowers-introduction-additive,
+	author = {W. T. Gowers},
+	date-added = {2022-09-02 15:08:26 +0100},
+	date-modified = {2022-09-02 15:08:26 +0100},
+	note = {Lecture notes, University of Cambridge},
+	title = {Introduction to Additive Combinatorics},
+	year = {2022}}
diff --git a/thys/Khovanskii_Theorem/document/root.tex b/thys/Khovanskii_Theorem/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Khovanskii_Theorem/document/root.tex
@@ -0,0 +1,41 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+\usepackage{amssymb}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Khovanskii's Theorem}
+\author{Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson}
+\maketitle
+
+\begin{abstract}
+We formalise the proof of an important theorem in additive combinatorics due to Khovanskii~\cite{khovanskii-newton-polyhedron,khovanskii-sums-finite}, 
+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 of the theorem due to Nathanson and Ruzsa~\cite{nathanson-polynomial-growth,ruzsa-sumsets-structure} as presented in the notes ``Introduction to Additive Combinatorics''
+by Timothy Gowers~\cite{gowers-introduction-additive} for the University of Cambridge. 
+\end{abstract}
+
+\newpage
+\tableofcontents
+
+\paragraph*{Acknowledgements}
+The authors were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council. 
+
+\newpage
+
+% include generated text of all theories
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,698 +1,699 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DPRM_Theorem
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 FO_Theory_Rewriting
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 IsaNet
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
+Khovanskii_Theorem
 Kleene_Algebra
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 LP_Duality
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multiset_Ordering_NPC
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 Package_logic
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quasi_Borel_Spaces
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sophomores_Dream
 Solidity
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 VYDRA_MDL
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL