subsection \<open>The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument\<close>
lemma Erdoes_Szekeres: fixes f :: "_ \ 'a::linorder" shows"(\S. S \ {0..m * n} \ card S = m + 1 \ gen_mono_on f (\) S) \
(\<exists>S. S \<subseteq> {0..m * n} \<and> card S = n + 1 \<and> gen_mono_on f (\<ge>) 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" moreoverfrom\<open>card S \<ge> b + 1\<close> obtain T where "T \<subseteq> S \<and> card T = Suc b" using obtain_subset_with_card_n by (metis Suc_eq_plus1) ultimatelyhave"\ 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 \<open>reflp R\<close>, 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 \<open>i < j\<close> finite_subset have "j \<notin> S" "finite S" "insert j S \<subseteq> {0..j}" by auto from S(1) R \<open>i < j\<close> 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\<open>insert j S \<subseteq> {0..j}\<close> by blast from this \<open>j \<notin> S\<close> S(1) have "card (insert j S) \<in>
card ` {S. S \<subseteq> {0..j} \<and> gen_mono_on f R S \<and> j \<in> S} \<and> card S < card (insert j S)" by (auto intro!: imageI) (auto simp add: \<open>finite S\<close>) 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
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
