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