Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Erdoes_Szekeres.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>The Erdös-Szekeres Theorem\<close>

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 \<open>Definition of Monotonicity over a Carrier Set\<close>

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 \<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"
      moreover from \<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)
      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 \<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.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.