# Theory Erdoes_Szekeres

```(*   Title: HOL/ex/Erdős_Szekeres.thy
Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
*)

section ‹The Erdös-Szekeres Theorem›

theory Erdoes_Szekeres
imports Main
begin

lemma exists_set_with_max_card:
assumes "finite S" "S ≠ {}"
shows "∃s ∈ S. card s = Max (card ` S)"
by (metis (mono_tags, lifting) Max_in assms finite_imageI imageE image_is_empty)

subsection ‹Definition of Monotonicity over a Carrier Set›

definition
"gen_mono_on f R S = (∀i∈S. ∀j∈S. i ≤ j ⟶ R (f i) (f j))"

lemma gen_mono_on_empty [simp]: "gen_mono_on f R {}"
unfolding gen_mono_on_def by auto

lemma gen_mono_on_singleton [simp]: "reflp R ⟹ gen_mono_on f R {x}"
unfolding gen_mono_on_def reflp_def by auto

lemma gen_mono_on_subset: "T ⊆ S ⟹ gen_mono_on f R S ⟹ gen_mono_on f R T"
unfolding gen_mono_on_def by (simp add: subset_iff)

lemma not_gen_mono_on_subset: "T ⊆ S ⟹ ¬ gen_mono_on f R T ⟹ ¬ gen_mono_on f R S"
unfolding gen_mono_on_def by blast

lemma [simp]:
"reflp ((≤) :: 'a::order ⇒ _ ⇒ bool)"
"reflp ((≥) :: 'a::order ⇒ _ ⇒ bool)"
"transp ((≤) :: 'a::order ⇒ _ ⇒ bool)"
"transp ((≥) :: 'a::order ⇒ _ ⇒ bool)"
unfolding reflp_def transp_def by auto

subsection ‹The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument›

lemma Erdoes_Szekeres:
fixes f :: "_ ⇒ 'a::linorder"
shows "(∃S. S ⊆ {0..m * n} ∧ card S = m + 1 ∧ gen_mono_on f (≤) S) ∨
(∃S. S ⊆ {0..m * n} ∧ card S = n + 1 ∧ gen_mono_on f (≥) S)"
proof (rule ccontr)
let ?max_subseq = "λR k. Max (card ` {S. S ⊆ {0..k} ∧ gen_mono_on f R S ∧ k ∈ S})"
define phi where "phi k = (?max_subseq (≤) k, ?max_subseq (≥) k)" for k

have one_member: "⋀R k. reflp R ⟹ {k} ∈ {S. S ⊆ {0..k} ∧ gen_mono_on f R S ∧ k ∈ S}" by auto

{
fix R
assume reflp: "reflp (R :: 'a::linorder ⇒ _)"
from one_member[OF this] have non_empty: "⋀k. {S. S ⊆ {0..k} ∧ gen_mono_on f R S ∧ k ∈ S} ≠ {}" by force
from one_member[OF reflp] have "⋀k. card {k} ∈ card ` {S. S ⊆ {0..k} ∧ gen_mono_on f R S ∧ k ∈ S}" by blast
from this have lower_bound: "⋀k. k ≤ m * n ⟹ ?max_subseq R k ≥ 1"
by (auto intro!: Max_ge)

fix b
assume not_mono_at: "∀S. S ⊆ {0..m * n} ∧ card S = b + 1 ⟶ ¬ gen_mono_on f R S"

{
fix S
assume "S ⊆ {0..m * n}" "card S ≥ b + 1"
moreover from ‹card S ≥ b + 1› obtain T where "T ⊆ S ∧ card T = Suc b"
using obtain_subset_with_card_n by (metis Suc_eq_plus1)
ultimately have "¬ gen_mono_on f R S" using not_mono_at by (auto dest: not_gen_mono_on_subset)
}
from this have "∀S. S ⊆ {0..m * n} ∧ gen_mono_on f R S ⟶ card S ≤ b"
by (metis Suc_eq_plus1 Suc_leI not_le)
from this have "⋀k. k ≤ m * n ⟹ ∀S. S ⊆ {0..k} ∧ gen_mono_on f R S ⟶ card S ≤ b"
using order_trans by force
from this non_empty have upper_bound: "⋀k. k ≤ m * n ⟹ ?max_subseq R k ≤ b"
by (auto intro: Max.boundedI)

from upper_bound lower_bound have "⋀k. k ≤ m * n ⟹ 1 ≤ ?max_subseq R k ∧ ?max_subseq R k ≤ b"
by auto
} note bounds = this

assume contraposition: "¬ ?thesis"
from contraposition bounds[of "(≤)" "m"] bounds[of "(≥)" "n"]
have "⋀k. k ≤ m * n ⟹ 1 ≤ ?max_subseq (≤) k ∧ ?max_subseq (≤) k ≤ m"
and  "⋀k. k ≤ m * n ⟹ 1 ≤ ?max_subseq (≥) k ∧ ?max_subseq (≥) k ≤ n"
using reflp_def by simp+
from this have "∀i ∈ {0..m * n}. phi i ∈ {1..m} × {1..n}"
unfolding phi_def by auto
from this have subseteq: "phi ` {0..m * n} ⊆ {1..m} × {1..n}" by blast
have card_product: "card ({1..m} × {1..n}) = m * n" by (simp add: card_cartesian_product)
have "finite ({1..m} × {1..n})" by blast
from subseteq card_product this have card_le: "card (phi ` {0..m * n}) ≤ m * n" by (metis card_mono)

{
fix i j
assume "i < (j :: nat)"
{
fix R
assume R: "reflp (R :: 'a::linorder ⇒ _)" "transp R" "R (f i) (f j)"
from one_member[OF ‹reflp R›, of "i"] have
"∃S ∈ {S. S ⊆ {0..i} ∧ gen_mono_on f R S ∧ i ∈ S}. card S = ?max_subseq R i"
by (intro exists_set_with_max_card) auto
from this obtain S where S: "S ⊆ {0..i} ∧ gen_mono_on f R S ∧ i ∈ S" "card S = ?max_subseq R i" by auto
from S ‹i < j› finite_subset have "j ∉ S" "finite S" "insert j S ⊆ {0..j}" by auto
from S(1) R ‹i < j› this have "gen_mono_on f R (insert j S)"
unfolding gen_mono_on_def reflp_def transp_def
by (metis atLeastAtMost_iff insert_iff le_antisym subsetCE)
from this have d: "insert j S ∈ {S. S ⊆ {0..j} ∧ gen_mono_on f R S ∧ j ∈ S}"
using ‹insert j S ⊆ {0..j}› by blast
from this ‹j ∉ S› S(1) have "card (insert j S) ∈
card ` {S. S ⊆ {0..j} ∧ gen_mono_on f R S ∧ j ∈ S} ∧ card S < card (insert j S)"
by (auto intro!: imageI) (auto simp add: ‹finite S›)
from this S(2) have "?max_subseq R i < ?max_subseq R j" by (auto intro!: Max_gr_iff [THEN iffD2])
} note max_subseq_increase = this
have "?max_subseq (≤) i < ?max_subseq (≤) j ∨ ?max_subseq (≥) i < ?max_subseq (≥) j"
proof (cases "f j ≥ f i")
case True
from this max_subseq_increase[of "(≤)", simplified] show ?thesis by simp
next
case False
from this max_subseq_increase[of "(≥)", simplified] show ?thesis by simp
qed
from this have "phi i ≠ phi j" using phi_def by auto
}
from this have "inj phi" unfolding inj_on_def by (metis less_linear)
from this have card_eq: "card (phi ` {0..m * n}) = m * n + 1" by (simp add: card_image inj_on_def)
from card_le card_eq show False by simp
qed

end
```