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