src/HOL/ex/Erdoes_Szekeres.thy
 changeset 61343 5b5656a63bd6 parent 60603 09ecbd791d4a child 62390 842917225d56
```     1.1 --- a/src/HOL/ex/Erdoes_Szekeres.thy	Tue Oct 06 17:46:07 2015 +0200
1.2 +++ b/src/HOL/ex/Erdoes_Szekeres.thy	Tue Oct 06 17:47:28 2015 +0200
1.3 @@ -2,13 +2,13 @@
1.4       Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
1.5  *)
1.6
1.7 -section {* The Erdoes-Szekeres Theorem *}
1.8 +section \<open>The Erdoes-Szekeres Theorem\<close>
1.9
1.10  theory Erdoes_Szekeres
1.11  imports Main
1.12  begin
1.13
1.14 -subsection {* Addition to @{theory Lattices_Big} Theory *}
1.15 +subsection \<open>Addition to @{theory Lattices_Big} Theory\<close>
1.16
1.17  lemma Max_gr:
1.18    assumes "finite A"
1.19 @@ -16,7 +16,7 @@
1.20    shows "x < Max A"
1.21  using assms Max_ge less_le_trans by blast
1.22
1.23 -subsection {* Additions to @{theory Finite_Set} Theory *}
1.24 +subsection \<open>Additions to @{theory Finite_Set} Theory\<close>
1.25
1.26  lemma obtain_subset_with_card_n:
1.27    assumes "n \<le> card S"
1.28 @@ -43,12 +43,12 @@
1.29      from this insertI.hyps(2) obtain s where s: "s \<in> S'" "card s = Max (card ` S')" by auto
1.30      from this(1) have that: "(if card s \<ge> card s' then s else s') \<in> insert s' S'" by auto
1.31      have "card (if card s \<ge> card s' then s else s') = Max (card ` insert s' S')"
1.32 -      using insertI(1) `S' \<noteq> {}` s by auto
1.33 +      using insertI(1) \<open>S' \<noteq> {}\<close> s by auto
1.34      from this that show ?thesis by blast
1.35    qed (auto)
1.36  qed (auto)
1.37
1.38 -subsection {* Definition of Monotonicity over a Carrier Set *}
1.39 +subsection \<open>Definition of Monotonicity over a Carrier Set\<close>
1.40
1.41  definition
1.42    "mono_on f R S = (\<forall>i\<in>S. \<forall>j\<in>S. i \<le> j \<longrightarrow> R (f i) (f j))"
1.43 @@ -72,7 +72,7 @@
1.44    "transp (op \<ge> :: 'a::order \<Rightarrow> _ \<Rightarrow> bool)"
1.45  unfolding reflp_def transp_def by auto
1.46
1.47 -subsection {* The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument *}
1.48 +subsection \<open>The Erdoes-Szekeres Theorem following Seidenberg's (1959) argument\<close>
1.49
1.50  lemma Erdoes_Szekeres:
1.51    fixes f :: "_ \<Rightarrow> 'a::linorder"
1.52 @@ -98,7 +98,7 @@
1.53      {
1.54        fix S
1.55        assume "S \<subseteq> {0..m * n}" "card S \<ge> b + 1"
1.56 -      moreover from `card S \<ge> b + 1` obtain T where "T \<subseteq> S \<and> card T = Suc b"
1.57 +      moreover from \<open>card S \<ge> b + 1\<close> obtain T where "T \<subseteq> S \<and> card T = Suc b"
1.58          using obtain_subset_with_card_n by (metis Suc_eq_plus1)
1.59        ultimately have "\<not> mono_on f R S" using not_mono_at by (auto dest: not_mono_on_subset)
1.60      }
1.61 @@ -131,19 +131,19 @@
1.62      {
1.63        fix R
1.64        assume R: "reflp (R :: 'a::linorder \<Rightarrow> _)" "transp R" "R (f i) (f j)"
1.65 -      from one_member[OF `reflp R`, of "i"] have
1.66 +      from one_member[OF \<open>reflp R\<close>, of "i"] have
1.67          "\<exists>S \<in> {S. S \<subseteq> {0..i} \<and> mono_on f R S \<and> i \<in> S}. card S = ?max_subseq R i"
1.68          by (intro exists_set_with_max_card) auto
1.69        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
1.70 -      from S `i < j` finite_subset have "j \<notin> S" "finite S" "insert j S \<subseteq> {0..j}" by auto
1.71 -      from S(1) R `i < j` this have "mono_on f R (insert j S)"
1.72 +      from S \<open>i < j\<close> finite_subset have "j \<notin> S" "finite S" "insert j S \<subseteq> {0..j}" by auto
1.73 +      from S(1) R \<open>i < j\<close> this have "mono_on f R (insert j S)"
1.74          unfolding mono_on_def reflp_def transp_def
1.75          by (metis atLeastAtMost_iff insert_iff le_antisym subsetCE)
1.76        from this have d: "insert j S \<in> {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S}"
1.77 -        using `insert j S \<subseteq> {0..j}` by blast
1.78 -      from this `j \<notin> S` S(1) have "card (insert j S) \<in>
1.79 +        using \<open>insert j S \<subseteq> {0..j}\<close> by blast
1.80 +      from this \<open>j \<notin> S\<close> S(1) have "card (insert j S) \<in>
1.81          card ` {S. S \<subseteq> {0..j} \<and> mono_on f R S \<and> j \<in> S} \<and> card S < card (insert j S)"
1.82 -        by (auto intro!: imageI) (auto simp add: `finite S`)
1.83 +        by (auto intro!: imageI) (auto simp add: \<open>finite S\<close>)
1.84        from this S(2) have "?max_subseq R i < ?max_subseq R j" by (auto intro: Max_gr)
1.85      } note max_subseq_increase = this
1.86      have "?max_subseq (op \<le>) i < ?max_subseq (op \<le>) j \<or> ?max_subseq (op \<ge>) i < ?max_subseq (op \<ge>) j"
```