author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 67091 1393c2340eec
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned equation
     1 (*  Title:      HOL/Library/Ramsey.thy
     2     Author:     Tom Ridge.  Converted to structured Isar by L C Paulson
     3 *)
     5 section \<open>Ramsey's Theorem\<close>
     7 theory Ramsey
     8   imports Infinite_Set
     9 begin
    11 subsection \<open>Finite Ramsey theorem(s)\<close>
    13 text \<open>
    14   To distinguish the finite and infinite ones, lower and upper case
    15   names are used.
    17   This is the most basic version in terms of cliques and independent
    18   sets, i.e. the version for graphs and 2 colours.
    19 \<close>
    21 definition "clique V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<in> E)"
    22 definition "indep V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<notin> E)"
    24 lemma ramsey2:
    25   "\<exists>r\<ge>1. \<forall>(V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
    26     (\<exists>R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
    27   (is "\<exists>r\<ge>1. ?R m n r")
    28 proof (induct k \<equiv> "m + n" arbitrary: m n)
    29   case 0
    30   show ?case (is "\<exists>r. ?Q r")
    31   proof
    32     from 0 show "?Q 1"
    33       by (clarsimp simp: indep_def) (metis card.empty emptyE empty_subsetI)
    34   qed
    35 next
    36   case (Suc k)
    37   consider "m = 0 \<or> n = 0" | "m \<noteq> 0" "n \<noteq> 0" by auto
    38   then show ?case (is "\<exists>r. ?Q r")
    39   proof cases
    40     case 1
    41     then have "?Q 1"
    42       by (simp add: clique_def) (meson card_empty empty_iff empty_subsetI indep_def)
    43     then show ?thesis ..
    44   next
    45     case 2
    46     with Suc(2) have "k = (m - 1) + n" "k = m + (n - 1)" by auto
    47     from this [THEN Suc(1)]
    48     obtain r1 r2 where "r1 \<ge> 1" "r2 \<ge> 1" "?R (m - 1) n r1" "?R m (n - 1) r2" by auto
    49     then have "r1 + r2 \<ge> 1" by arith
    50     moreover have "?R m n (r1 + r2)" (is "\<forall>V E. _ \<longrightarrow> ?EX V E m n")
    51     proof clarify
    52       fix V :: "'a set"
    53       fix E :: "'a set set"
    54       assume "finite V" "r1 + r2 \<le> card V"
    55       with \<open>r1 \<ge> 1\<close> have "V \<noteq> {}" by auto
    56       then obtain v where "v \<in> V" by blast
    57       let ?M = "{w \<in> V. w \<noteq> v \<and> {v, w} \<in> E}"
    58       let ?N = "{w \<in> V. w \<noteq> v \<and> {v, w} \<notin> E}"
    59       from \<open>v \<in> V\<close> have "V = insert v (?M \<union> ?N)" by auto
    60       then have "card V = card (insert v (?M \<union> ?N))" by metis
    61       also from \<open>finite V\<close> have "\<dots> = card ?M + card ?N + 1"
    62         by (fastforce intro: card_Un_disjoint)
    63       finally have "card V = card ?M + card ?N + 1" .
    64       with \<open>r1 + r2 \<le> card V\<close> have "r1 + r2 \<le> card ?M + card ?N + 1" by simp
    65       then consider "r1 \<le> card ?M" | "r2 \<le> card ?N" by arith
    66       then show "?EX V E m n"
    67       proof cases
    68         case 1
    69         from \<open>finite V\<close> have "finite ?M" by auto
    70         with \<open>?R (m - 1) n r1\<close> and 1 have "?EX ?M E (m - 1) n" by blast
    71         then obtain R where "R \<subseteq> ?M" "v \<notin> R"
    72           and CI: "card R = m - 1 \<and> clique R E \<or> card R = n \<and> indep R E" (is "?C \<or> ?I")
    73           by blast
    74         from \<open>R \<subseteq> ?M\<close> have "R \<subseteq> V" by auto
    75         with \<open>finite V\<close> have "finite R" by (metis finite_subset)
    76         from CI show ?thesis
    77         proof
    78           assume "?I"
    79           with \<open>R \<subseteq> V\<close> show ?thesis by blast
    80         next
    81           assume "?C"
    82           with \<open>R \<subseteq> ?M\<close> have *: "clique (insert v R) E"
    83             by (auto simp: clique_def insert_commute)
    84           from \<open>?C\<close> \<open>finite R\<close> \<open>v \<notin> R\<close> \<open>m \<noteq> 0\<close> have "card (insert v R) = m" by simp
    85           with \<open>R \<subseteq> V\<close> \<open>v \<in> V\<close> * show ?thesis by (metis insert_subset)
    86         qed
    87       next
    88         case 2
    89         from \<open>finite V\<close> have "finite ?N" by auto
    90         with \<open>?R m (n - 1) r2\<close> 2 have "?EX ?N E m (n - 1)" by blast
    91         then obtain R where "R \<subseteq> ?N" "v \<notin> R"
    92           and CI: "card R = m \<and> clique R E \<or> card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
    93           by blast
    94         from \<open>R \<subseteq> ?N\<close> have "R \<subseteq> V" by auto
    95         with \<open>finite V\<close> have "finite R" by (metis finite_subset)
    96         from CI show ?thesis
    97         proof
    98           assume "?C"
    99           with \<open>R \<subseteq> V\<close> show ?thesis by blast
   100         next
   101           assume "?I"
   102           with \<open>R \<subseteq> ?N\<close> have *: "indep (insert v R) E"
   103             by (auto simp: indep_def insert_commute)
   104           from \<open>?I\<close> \<open>finite R\<close> \<open>v \<notin> R\<close> \<open>n \<noteq> 0\<close> have "card (insert v R) = n" by simp
   105           with \<open>R \<subseteq> V\<close> \<open>v \<in> V\<close> * show ?thesis by (metis insert_subset)
   106         qed
   107       qed
   108     qed
   109     ultimately show ?thesis by blast
   110   qed
   111 qed
   114 subsection \<open>Preliminaries\<close>
   116 subsubsection \<open>``Axiom'' of Dependent Choice\<close>
   118 primrec choice :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a"
   119   where \<comment> \<open>An integer-indexed chain of choices\<close>
   120     choice_0: "choice P r 0 = (SOME x. P x)"
   121   | choice_Suc: "choice P r (Suc n) = (SOME y. P y \<and> (choice P r n, y) \<in> r)"
   123 lemma choice_n:
   124   assumes P0: "P x0"
   125     and Pstep: "\<And>x. P x \<Longrightarrow> \<exists>y. P y \<and> (x, y) \<in> r"
   126   shows "P (choice P r n)"
   127 proof (induct n)
   128   case 0
   129   show ?case by (force intro: someI P0)
   130 next
   131   case Suc
   132   then show ?case by (auto intro: someI2_ex [OF Pstep])
   133 qed
   135 lemma dependent_choice:
   136   assumes trans: "trans r"
   137     and P0: "P x0"
   138     and Pstep: "\<And>x. P x \<Longrightarrow> \<exists>y. P y \<and> (x, y) \<in> r"
   139   obtains f :: "nat \<Rightarrow> 'a" where "\<And>n. P (f n)" and "\<And>n m. n < m \<Longrightarrow> (f n, f m) \<in> r"
   140 proof
   141   fix n
   142   show "P (choice P r n)"
   143     by (blast intro: choice_n [OF P0 Pstep])
   144 next
   145   fix n m :: nat
   146   assume "n < m"
   147   from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) \<in> r" for k
   148     by (auto intro: someI2_ex)
   149   then show "(choice P r n, choice P r m) \<in> r"
   150     by (auto intro: less_Suc_induct [OF \<open>n < m\<close>] transD [OF trans])
   151 qed
   154 subsubsection \<open>Partitions of a Set\<close>
   156 definition part :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool"
   157   \<comment> \<open>the function @{term f} partitions the @{term r}-subsets of the typically
   158       infinite set @{term Y} into @{term s} distinct categories.\<close>
   159   where "part r s Y f \<longleftrightarrow> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X < s)"
   161 text \<open>For induction, we decrease the value of @{term r} in partitions.\<close>
   162 lemma part_Suc_imp_part:
   163   "\<lbrakk>infinite Y; part (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part r s (Y - {y}) (\<lambda>u. f (insert y u))"
   164   apply (simp add: part_def)
   165   apply clarify
   166   apply (drule_tac x="insert y X" in spec)
   167   apply force
   168   done
   170 lemma part_subset: "part r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part r s Y f"
   171   unfolding part_def by blast
   174 subsection \<open>Ramsey's Theorem: Infinitary Version\<close>
   176 lemma Ramsey_induction:
   177   fixes s r :: nat
   178     and YY :: "'a set"
   179     and f :: "'a set \<Rightarrow> nat"
   180   assumes "infinite YY" "part r s YY f"
   181   shows "\<exists>Y' t'. Y' \<subseteq> YY \<and> infinite Y' \<and> t' < s \<and> (\<forall>X. X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> f X = t')"
   182   using assms
   183 proof (induct r arbitrary: YY f)
   184   case 0
   185   then show ?case
   186     by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
   187 next
   188   case (Suc r)
   189   show ?case
   190   proof -
   191     from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY"
   192       by blast
   193     let ?ramr = "{((y, Y, t), (y', Y', t')). y' \<in> Y \<and> Y' \<subseteq> Y}"
   194     let ?propr = "\<lambda>(y, Y, t).
   195                  y \<in> YY \<and> y \<notin> Y \<and> Y \<subseteq> YY \<and> infinite Y \<and> t < s
   196                  \<and> (\<forall>X. X\<subseteq>Y \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert y) X = t)"
   197     from Suc.prems have infYY': "infinite (YY - {yy})" by auto
   198     from Suc.prems have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
   199       by (simp add: o_def part_Suc_imp_part yy)
   200     have transr: "trans ?ramr" by (force simp add: trans_def)
   201     from Suc.hyps [OF infYY' partf']
   202     obtain Y0 and t0 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s"
   203       "X \<subseteq> Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0" for X
   204       by blast
   205     with yy have propr0: "?propr(yy, Y0, t0)" by blast
   206     have proprstep: "\<exists>y. ?propr y \<and> (x, y) \<in> ?ramr" if x: "?propr x" for x
   207     proof (cases x)
   208       case (fields yx Yx tx)
   209       with x obtain yx' where yx': "yx' \<in> Yx"
   210         by (blast dest: infinite_imp_nonempty)
   211       from fields x have infYx': "infinite (Yx - {yx'})" by auto
   212       with fields x yx' Suc.prems have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
   213         by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
   214       from Suc.hyps [OF infYx' partfx'] obtain Y' and t'
   215         where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s"
   216           "X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'" for X
   217         by blast
   218       from fields x Y' yx' have "?propr (yx', Y', t') \<and> (x, (yx', Y', t')) \<in> ?ramr"
   219         by blast
   220       then show ?thesis ..
   221     qed
   222     from dependent_choice [OF transr propr0 proprstep]
   223     obtain g where pg: "?propr (g n)" and rg: "n < m \<Longrightarrow> (g n, g m) \<in> ?ramr" for n m :: nat
   224       by blast
   225     let ?gy = "fst \<circ> g"
   226     let ?gt = "snd \<circ> snd \<circ> g"
   227     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
   228     proof (intro exI subsetI)
   229       fix x
   230       assume "x \<in> range ?gt"
   231       then obtain n where "x = ?gt n" ..
   232       with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
   233     qed
   234     have "finite (range ?gt)"
   235       by (simp add: finite_nat_iff_bounded rangeg)
   236     then obtain s' and n' where s': "s' = ?gt n'" and infeqs': "infinite {n. ?gt n = s'}"
   237       by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
   238     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
   239     have inj_gy: "inj ?gy"
   240     proof (rule linorder_injI)
   241       fix m m' :: nat
   242       assume "m < m'"
   243       from rg [OF this] pg [of m] show "?gy m \<noteq> ?gy m'"
   244         by (cases "g m", cases "g m'") auto
   245     qed
   246     show ?thesis
   247     proof (intro exI conjI)
   248       from pg show "?gy ` {n. ?gt n = s'} \<subseteq> YY"
   249         by (auto simp add: Let_def split_beta)
   250       from infeqs' show "infinite (?gy ` {n. ?gt n = s'})"
   251         by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
   252       show "s' < s" by (rule less')
   253       show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} \<and> finite X \<and> card X = Suc r \<longrightarrow> f X = s'"
   254       proof -
   255         have "f X = s'"
   256           if X: "X \<subseteq> ?gy ` {n. ?gt n = s'}"
   257           and cardX: "finite X" "card X = Suc r"
   258           for X
   259         proof -
   260           from X obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
   261             by (auto simp add: subset_image_iff)
   262           with cardX have "AA \<noteq> {}" by auto
   263           then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
   264           show ?thesis
   265           proof (cases "g (LEAST x. x \<in> AA)")
   266             case (fields ya Ya ta)
   267             with AAleast Xeq have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
   268             then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
   269             also have "\<dots> = ta"
   270             proof -
   271               have *: "X - {ya} \<subseteq> Ya"
   272               proof
   273                 fix x assume x: "x \<in> X - {ya}"
   274                 then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
   275                   by (auto simp add: Xeq)
   276                 with fields x have "a' \<noteq> (LEAST x. x \<in> AA)" by auto
   277                 with Least_le [of "\<lambda>x. x \<in> AA", OF a'] have "(LEAST x. x \<in> AA) < a'"
   278                   by arith
   279                 from xeq fields rg [OF this] show "x \<in> Ya" by auto
   280               qed
   281               have "card (X - {ya}) = r"
   282                 by (simp add: cardX ya)
   283               with pg [of "LEAST x. x \<in> AA"] fields cardX * show ?thesis
   284                 by (auto simp del: insert_Diff_single)
   285             qed
   286             also from AA AAleast fields have "\<dots> = s'" by auto
   287             finally show ?thesis .
   288           qed
   289         qed
   290         then show ?thesis by blast
   291       qed
   292     qed
   293   qed
   294 qed
   297 theorem Ramsey:
   298   fixes s r :: nat
   299     and Z :: "'a set"
   300     and f :: "'a set \<Rightarrow> nat"
   301   shows
   302    "\<lbrakk>infinite Z;
   303       \<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = r \<longrightarrow> f X < s\<rbrakk>
   304     \<Longrightarrow> \<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s
   305             \<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)"
   306   by (blast intro: Ramsey_induction [unfolded part_def])
   309 corollary Ramsey2:
   310   fixes s :: nat
   311     and Z :: "'a set"
   312     and f :: "'a set \<Rightarrow> nat"
   313   assumes infZ: "infinite Z"
   314     and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x \<noteq> y \<longrightarrow> f {x, y} < s"
   315   shows "\<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s \<and> (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y \<longrightarrow> f {x, y} = t)"
   316 proof -
   317   from part have part2: "\<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = 2 \<longrightarrow> f X < s"
   318     by (fastforce simp add: eval_nat_numeral card_Suc_eq)
   319   obtain Y t where *:
   320     "Y \<subseteq> Z" "infinite Y" "t < s" "(\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = 2 \<longrightarrow> f X = t)"
   321     by (insert Ramsey [OF infZ part2]) auto
   322   then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
   323   with * show ?thesis by iprover
   324 qed
   327 subsection \<open>Disjunctive Well-Foundedness\<close>
   329 text \<open>
   330   An application of Ramsey's theorem to program termination. See
   331   @{cite "Podelski-Rybalchenko"}.
   332 \<close>
   334 definition disj_wf :: "('a \<times> 'a) set \<Rightarrow> bool"
   335   where "disj_wf r \<longleftrightarrow> (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf (T i)) \<and> r = (\<Union>i<n. T i))"
   337 definition transition_idx :: "(nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> ('a \<times> 'a) set) \<Rightarrow> nat set \<Rightarrow> nat"
   338   where "transition_idx s T A = (LEAST k. \<exists>i j. A = {i, j} \<and> i < j \<and> (s j, s i) \<in> T k)"
   341 lemma transition_idx_less:
   342   assumes "i < j" "(s j, s i) \<in> T k" "k < n"
   343   shows "transition_idx s T {i, j} < n"
   344 proof -
   345   from assms(1,2) have "transition_idx s T {i, j} \<le> k"
   346     by (simp add: transition_idx_def, blast intro: Least_le)
   347   with assms(3) show ?thesis by simp
   348 qed
   350 lemma transition_idx_in:
   351   assumes "i < j" "(s j, s i) \<in> T k"
   352   shows "(s j, s i) \<in> T (transition_idx s T {i, j})"
   353   using assms
   354   by (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) (erule LeastI)
   356 text \<open>To be equal to the union of some well-founded relations is equivalent
   357   to being the subset of such a union.\<close>
   358 lemma disj_wf: "disj_wf r \<longleftrightarrow> (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) \<and> r \<subseteq> (\<Union>i<n. T i))"
   359   apply (auto simp add: disj_wf_def)
   360   apply (rule_tac x="\<lambda>i. T i Int r" in exI)
   361   apply (rule_tac x=n in exI)
   362   apply (force simp add: wf_Int1)
   363   done
   365 theorem trans_disj_wf_implies_wf:
   366   assumes "trans r"
   367     and "disj_wf r"
   368   shows "wf r"
   369 proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
   370   assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"
   371   then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..
   372   from \<open>disj_wf r\<close> obtain T and n :: nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
   373     by (auto simp add: disj_wf_def)
   374   have s_in_T: "\<exists>k. (s j, s i) \<in> T k \<and> k<n" if "i < j" for i j
   375   proof -
   376     from \<open>i < j\<close> have "(s j, s i) \<in> r"
   377     proof (induct rule: less_Suc_induct)
   378       case 1
   379       then show ?case by (simp add: sSuc)
   380     next
   381       case 2
   382       with \<open>trans r\<close> show ?case
   383         unfolding trans_def by blast
   384     qed
   385     then show ?thesis by (auto simp add: r)
   386   qed
   387   have trless: "i \<noteq> j \<Longrightarrow> transition_idx s T {i, j} < n" for i j
   388     apply (auto simp add: linorder_neq_iff)
   389      apply (blast dest: s_in_T transition_idx_less)
   390     apply (subst insert_commute)
   391     apply (blast dest: s_in_T transition_idx_less)
   392     done
   393   have "\<exists>K k. K \<subseteq> UNIV \<and> infinite K \<and> k < n \<and>
   394       (\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k)"
   395     by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
   396   then obtain K and k where infK: "infinite K" and "k < n"
   397     and allk: "\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k"
   398     by auto
   399   have "(s (enumerate K (Suc m)), s (enumerate K m)) \<in> T k" for m :: nat
   400   proof -
   401     let ?j = "enumerate K (Suc m)"
   402     let ?i = "enumerate K m"
   403     have ij: "?i < ?j" by (simp add: enumerate_step infK)
   404     have "?j \<in> K" "?i \<in> K" by (simp_all add: enumerate_in_set infK)
   405     with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk)
   406     from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n" by blast
   407     then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij)
   408   qed
   409   then have "\<not> wf (T k)"
   410     unfolding wf_iff_no_infinite_down_chain by fast
   411   with wfT \<open>k < n\<close> show False by blast
   412 qed
   414 end