(* Title: HOL/ex/Erdoes_Szekeres.thy Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *) section ‹The Erdoes-Szekeres Theorem› theory Erdoes_Szekeres imports Main begin subsection ‹Addition to \<^theory>‹HOL.Lattices_Big› Theory› lemma Max_gr: assumes "finite A" assumes "a ∈ A" "a > x" shows "x < Max A" using assms Max_ge less_le_trans by blast subsection ‹Additions to \<^theory>‹HOL.Finite_Set› Theory› lemma obtain_subset_with_card_n: assumes "n ≤ card S" obtains T where "T ⊆ S" "card T = n" proof - from assms obtain n' where "card S = n + n'" by (metis le_add_diff_inverse) from this that show ?thesis proof (induct n' arbitrary: S) case 0 from this show ?case by auto next case Suc from this show ?case by (simp add: card_Suc_eq) (metis subset_insertI2) qed qed lemma exists_set_with_max_card: assumes "finite S" "S ≠ {}" shows "∃s ∈ S. card s = Max (card ` S)" using assms proof (induct S rule: finite.induct) case (insertI S' s') show ?case proof (cases "S' ≠ {}") case True from this insertI.hyps(2) obtain s where s: "s ∈ S'" "card s = Max (card ` S')" by auto from this(1) have that: "(if card s ≥ card s' then s else s') ∈ insert s' S'" by auto have "card (if card s ≥ card s' then s else s') = Max (card ` insert s' S')" using insertI(1) ‹S' ≠ {}› s by auto from this that show ?thesis by blast qed (auto) qed (auto) subsection ‹Definition of Monotonicity over a Carrier Set› definition "mono_on f R S = (∀i∈S. ∀j∈S. i ≤ j ⟶ R (f i) (f j))" lemma mono_on_empty [simp]: "mono_on f R {}" unfolding mono_on_def by auto lemma mono_on_singleton [simp]: "reflp R ⟹ mono_on f R {x}" unfolding mono_on_def reflp_def by auto lemma mono_on_subset: "T ⊆ S ⟹ mono_on f R S ⟹ mono_on f R T" unfolding mono_on_def by (simp add: subset_iff) lemma not_mono_on_subset: "T ⊆ S ⟹ ¬ mono_on f R T ⟹ ¬ mono_on f R S" unfolding 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 ∧ mono_on f (≤) S) ∨ (∃S. S ⊆ {0..m * n} ∧ card S = n + 1 ∧ mono_on f (≥) S)" proof (rule ccontr) let ?max_subseq = "λR k. Max (card ` {S. S ⊆ {0..k} ∧ 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} ∧ 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} ∧ mono_on f R S ∧ k ∈ S} ≠ {}" by force from one_member[OF reflp] have "⋀k. card {k} ∈ card ` {S. S ⊆ {0..k} ∧ 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 ⟶ ¬ 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 "¬ mono_on f R S" using not_mono_at by (auto dest: not_mono_on_subset) } from this have "∀S. S ⊆ {0..m * n} ∧ 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} ∧ 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} ∧ 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} ∧ 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 "mono_on f R (insert j S)" unfolding 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} ∧ 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} ∧ 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) } 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