src/HOL/ex/Erdoes_Szekeres.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63040 eb4ddd18d635
child 67399 eab6ce8368fa
permissions -rw-r--r--
bundle lifting_syntax;
bulwahn@60603
     1
(*   Title: HOL/ex/Erdoes_Szekeres.thy
bulwahn@60603
     2
     Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
bulwahn@60603
     3
*)
bulwahn@60603
     4
wenzelm@61343
     5
section \<open>The Erdoes-Szekeres Theorem\<close>
bulwahn@60603
     6
bulwahn@60603
     7
theory Erdoes_Szekeres
bulwahn@60603
     8
imports Main
bulwahn@60603
     9
begin
bulwahn@60603
    10
wenzelm@61343
    11
subsection \<open>Addition to @{theory Lattices_Big} Theory\<close>
bulwahn@60603
    12
bulwahn@60603
    13
lemma Max_gr:
bulwahn@60603
    14
  assumes "finite A"
bulwahn@60603
    15
  assumes "a \<in> A" "a > x"
bulwahn@60603
    16
  shows "x < Max A"
bulwahn@60603
    17
using assms Max_ge less_le_trans by blast
bulwahn@60603
    18
wenzelm@61343
    19
subsection \<open>Additions to @{theory Finite_Set} Theory\<close>
bulwahn@60603
    20
bulwahn@60603
    21
lemma obtain_subset_with_card_n:
bulwahn@60603
    22
  assumes "n \<le> card S"
bulwahn@60603
    23
  obtains T where "T \<subseteq> S" "card T = n"
bulwahn@60603
    24
proof -
bulwahn@60603
    25
  from assms obtain n' where "card S = n + n'" by (metis le_add_diff_inverse)
bulwahn@60603
    26
  from this that show ?thesis
bulwahn@60603
    27
  proof (induct n' arbitrary: S)
bulwahn@60603
    28
    case 0 from this show ?case by auto
bulwahn@60603
    29
  next
bulwahn@60603
    30
    case Suc from this show ?case by (simp add: card_Suc_eq) (metis subset_insertI2)
bulwahn@60603
    31
  qed
bulwahn@60603
    32
qed
bulwahn@60603
    33
bulwahn@60603
    34
lemma exists_set_with_max_card:
bulwahn@60603
    35
  assumes "finite S" "S \<noteq> {}"
bulwahn@60603
    36
  shows "\<exists>s \<in> S. card s = Max (card ` S)"
bulwahn@60603
    37
using assms
bulwahn@60603
    38
proof (induct S rule: finite.induct)
bulwahn@60603
    39
  case (insertI S' s')
bulwahn@60603
    40
  show ?case
bulwahn@60603
    41
  proof (cases "S' \<noteq> {}")
bulwahn@60603
    42
    case True
bulwahn@60603
    43
    from this insertI.hyps(2) obtain s where s: "s \<in> S'" "card s = Max (card ` S')" by auto
bulwahn@60603
    44
    from this(1) have that: "(if card s \<ge> card s' then s else s') \<in> insert s' S'" by auto
bulwahn@60603
    45
    have "card (if card s \<ge> card s' then s else s') = Max (card ` insert s' S')"
wenzelm@61343
    46
      using insertI(1) \<open>S' \<noteq> {}\<close> s by auto
bulwahn@60603
    47
    from this that show ?thesis by blast
bulwahn@60603
    48
  qed (auto)
bulwahn@60603
    49
qed (auto)
bulwahn@60603
    50
wenzelm@61343
    51
subsection \<open>Definition of Monotonicity over a Carrier Set\<close>
bulwahn@60603
    52
bulwahn@60603
    53
definition
bulwahn@60603
    54
  "mono_on f R S = (\<forall>i\<in>S. \<forall>j\<in>S. i \<le> j \<longrightarrow> R (f i) (f j))"
bulwahn@60603
    55
bulwahn@60603
    56
lemma mono_on_empty [simp]: "mono_on f R {}"
bulwahn@60603
    57
unfolding mono_on_def by auto
bulwahn@60603
    58
bulwahn@60603
    59
lemma mono_on_singleton [simp]: "reflp R \<Longrightarrow> mono_on f R {x}"
bulwahn@60603
    60
unfolding mono_on_def reflp_def by auto
bulwahn@60603
    61
bulwahn@60603
    62
lemma mono_on_subset: "T \<subseteq> S \<Longrightarrow> mono_on f R S \<Longrightarrow> mono_on f R T"
bulwahn@60603
    63
unfolding mono_on_def by (simp add: subset_iff)
bulwahn@60603
    64
bulwahn@60603
    65
lemma not_mono_on_subset: "T \<subseteq> S \<Longrightarrow> \<not> mono_on f R T \<Longrightarrow> \<not> mono_on f R S"
bulwahn@60603
    66
unfolding mono_on_def by blast
bulwahn@60603
    67
bulwahn@60603
    68
lemma [simp]:
bulwahn@60603
    69
  "reflp (op \<le> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
bulwahn@60603
    70
  "reflp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
bulwahn@60603
    71
  "transp (op \<le> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
bulwahn@60603
    72
  "transp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
bulwahn@60603
    73
unfolding reflp_def transp_def by auto
bulwahn@60603
    74
wenzelm@61343
    75
subsection \<open>The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument\<close>
bulwahn@60603
    76
bulwahn@60603
    77
lemma Erdoes_Szekeres:
bulwahn@60603
    78
  fixes f :: "_ \<Rightarrow> 'a::linorder"
bulwahn@60603
    79
  shows "(\<exists>S. S \<subseteq> {0..m * n} \<and> card S = m + 1 \<and> mono_on f (op \<le>) S) \<or>
bulwahn@60603
    80
         (\<exists>S. S \<subseteq> {0..m * n} \<and> card S = n + 1 \<and> mono_on f (op \<ge>) S)"
bulwahn@60603
    81
proof (rule ccontr)
bulwahn@60603
    82
  let ?max_subseq = "\<lambda>R k. Max (card ` {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S})"
wenzelm@63040
    83
  define phi where "phi k = (?max_subseq (op \<le>) k, ?max_subseq (op \<ge>) k)" for k
bulwahn@60603
    84
bulwahn@60603
    85
  have one_member: "\<And>R k. reflp R \<Longrightarrow> {k} \<in> {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S}" by auto
bulwahn@60603
    86
bulwahn@60603
    87
  {
bulwahn@60603
    88
    fix R
bulwahn@60603
    89
    assume reflp: "reflp (R :: 'a::linorder \<Rightarrow> _)"
bulwahn@60603
    90
    from one_member[OF this] have non_empty: "\<And>k. {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S} \<noteq> {}" by force
bulwahn@60603
    91
    from one_member[OF reflp] have "\<And>k. card {k} \<in> card ` {S. S \<subseteq> {0..k} \<and> mono_on f R S \<and> k \<in> S}" by blast
bulwahn@60603
    92
    from this have lower_bound: "\<And>k. k \<le> m * n \<Longrightarrow> ?max_subseq R k \<ge> 1"
bulwahn@60603
    93
      by (auto intro!: Max_ge)
bulwahn@60603
    94
bulwahn@60603
    95
    fix b
bulwahn@60603
    96
    assume not_mono_at: "\<forall>S. S \<subseteq> {0..m * n} \<and> card S = b + 1 \<longrightarrow> \<not> mono_on f R S"
bulwahn@60603
    97
bulwahn@60603
    98
    {
bulwahn@60603
    99
      fix S
bulwahn@60603
   100
      assume "S \<subseteq> {0..m * n}" "card S \<ge> b + 1"
wenzelm@61343
   101
      moreover from \<open>card S \<ge> b + 1\<close> obtain T where "T \<subseteq> S \<and> card T = Suc b"
bulwahn@60603
   102
        using obtain_subset_with_card_n by (metis Suc_eq_plus1)
bulwahn@60603
   103
      ultimately have "\<not> mono_on f R S" using not_mono_at by (auto dest: not_mono_on_subset)
bulwahn@60603
   104
    }
bulwahn@60603
   105
    from this have "\<forall>S. S \<subseteq> {0..m * n} \<and> mono_on f R S \<longrightarrow> card S \<le> b"
bulwahn@60603
   106
      by (metis Suc_eq_plus1 Suc_leI not_le)
bulwahn@60603
   107
    from this have "\<And>k. k \<le> m * n \<Longrightarrow> \<forall>S. S \<subseteq> {0..k} \<and> mono_on f R S \<longrightarrow> card S \<le> b"
bulwahn@60603
   108
      using order_trans by force
bulwahn@60603
   109
    from this non_empty have upper_bound: "\<And>k. k \<le> m * n \<Longrightarrow> ?max_subseq R k \<le> b"
bulwahn@60603
   110
      by (auto intro: Max.boundedI)
bulwahn@60603
   111
bulwahn@60603
   112
    from upper_bound lower_bound have "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq R k \<and> ?max_subseq R k \<le> b"
bulwahn@60603
   113
      by auto
bulwahn@60603
   114
  } note bounds = this
bulwahn@60603
   115
bulwahn@60603
   116
  assume contraposition: "\<not> ?thesis"
bulwahn@60603
   117
  from contraposition bounds[of "op \<le>" "m"] bounds[of "op \<ge>" "n"]
bulwahn@60603
   118
    have "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq (op \<le>) k \<and> ?max_subseq (op \<le>) k \<le> m"
bulwahn@60603
   119
    and  "\<And>k. k \<le> m * n \<Longrightarrow> 1 \<le> ?max_subseq (op \<ge>) k \<and> ?max_subseq (op \<ge>) k \<le> n"
bulwahn@60603
   120
    using reflp_def by simp+
bulwahn@60603
   121
  from this have "\<forall>i \<in> {0..m * n}. phi i \<in> {1..m} \<times> {1..n}"
bulwahn@60603
   122
    unfolding phi_def by auto
bulwahn@60603
   123
  from this have subseteq: "phi ` {0..m * n} \<subseteq> {1..m} \<times> {1..n}" by blast
bulwahn@60603
   124
  have card_product: "card ({1..m} \<times> {1..n}) = m * n" by (simp add: card_cartesian_product)
bulwahn@60603
   125
  have "finite ({1..m} \<times> {1..n})" by blast
bulwahn@60603
   126
  from subseteq card_product this have card_le: "card (phi ` {0..m * n}) \<le> m * n" by (metis card_mono)
bulwahn@60603
   127
bulwahn@60603
   128
  {
bulwahn@60603
   129
    fix i j
bulwahn@60603
   130
    assume "i < (j :: nat)"
bulwahn@60603
   131
    {
bulwahn@60603
   132
      fix R
bulwahn@60603
   133
      assume R: "reflp (R :: 'a::linorder \<Rightarrow> _)" "transp R" "R (f i) (f j)"
wenzelm@61343
   134
      from one_member[OF \<open>reflp R\<close>, of "i"] have
bulwahn@60603
   135
        "\<exists>S \<in> {S. S \<subseteq> {0..i} \<and> mono_on f R S \<and> i \<in> S}. card S = ?max_subseq R i"
bulwahn@60603
   136
        by (intro exists_set_with_max_card) auto
bulwahn@60603
   137
      from this obtain S where S: "S \<subseteq> {0..i} \<and> mono_on f R S \<and> i \<in> S" "card S = ?max_subseq R i" by auto
wenzelm@61343
   138
      from S \<open>i < j\<close> finite_subset have "j \<notin> S" "finite S" "insert j S \<subseteq> {0..j}" by auto
wenzelm@61343
   139
      from S(1) R \<open>i < j\<close> this have "mono_on f R (insert j S)"
bulwahn@60603
   140
        unfolding mono_on_def reflp_def transp_def
bulwahn@60603
   141
        by (metis atLeastAtMost_iff insert_iff le_antisym subsetCE)
bulwahn@60603
   142
      from this have d: "insert j S \<in> {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S}"
wenzelm@61343
   143
        using \<open>insert j S \<subseteq> {0..j}\<close> by blast
wenzelm@61343
   144
      from this \<open>j \<notin> S\<close> S(1) have "card (insert j S) \<in>
bulwahn@60603
   145
        card ` {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S} \<and> card S < card (insert j S)"
wenzelm@61343
   146
        by (auto intro!: imageI) (auto simp add: \<open>finite S\<close>)
bulwahn@60603
   147
      from this S(2) have "?max_subseq R i < ?max_subseq R j" by (auto intro: Max_gr)
bulwahn@60603
   148
    } note max_subseq_increase = this
bulwahn@60603
   149
    have "?max_subseq (op \<le>) i < ?max_subseq (op \<le>) j \<or> ?max_subseq (op \<ge>) i < ?max_subseq (op \<ge>) j"
bulwahn@60603
   150
    proof (cases "f j \<ge> f i")
bulwahn@60603
   151
      case True
bulwahn@60603
   152
      from this max_subseq_increase[of "op \<le>", simplified] show ?thesis by simp
bulwahn@60603
   153
    next
bulwahn@60603
   154
      case False
bulwahn@60603
   155
      from this max_subseq_increase[of "op \<ge>", simplified] show ?thesis by simp
bulwahn@60603
   156
    qed
bulwahn@60603
   157
    from this have "phi i \<noteq> phi j" using phi_def by auto
bulwahn@60603
   158
  }
bulwahn@60603
   159
  from this have "inj phi" unfolding inj_on_def by (metis less_linear)
bulwahn@60603
   160
  from this have card_eq: "card (phi ` {0..m * n}) = m * n + 1" by (simp add: card_image inj_on_def)
bulwahn@60603
   161
  from card_le card_eq show False by simp
bulwahn@60603
   162
qed
bulwahn@60603
   163
nipkow@62390
   164
end