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"