1.1 --- a/src/HOL/Library/Ramsey.thy	Thu Nov 25 14:58:50 2010 +0100
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Thu Nov 25 14:59:01 2010 +0100
     1.3 @@ -8,6 +8,113 @@
     1.4  imports Main Infinite_Set
     1.5  begin
     1.6  
     1.7 +subsection{* Finite Ramsey theorem(s) *}
     1.8 +
     1.9 +text{* To distinguish the finite and infinite ones, lower and upper case
    1.10 +names are used.
    1.11 +
    1.12 +This is the most basic version in terms of cliques and independent
    1.13 +sets, i.e. the version for graphs and 2 colours. *}
    1.14 +
    1.15 +definition "clique V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> {v,w} : E)"
    1.16 +definition "indep V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> \<not> {v,w} : E)"
    1.17 +
    1.18 +lemma ramsey2:
    1.19 +  "\<exists>r\<ge>1. \<forall> (V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
    1.20 +  (\<exists> R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
    1.21 +  (is "\<exists>r\<ge>1. ?R m n r")
    1.22 +proof(induct k == "m+n" arbitrary: m n)
    1.23 +  case 0
    1.24 +  show ?case (is "EX r. ?R r")
    1.25 +  proof
    1.26 +    show "?R 1" using 0
    1.27 +      by (clarsimp simp: indep_def)(metis card.empty emptyE empty_subsetI)
    1.28 +  qed
    1.29 +next
    1.30 +  case (Suc k)
    1.31 +  { assume "m=0"
    1.32 +    have ?case (is "EX r. ?R r")
    1.33 +    proof
    1.34 +      show "?R 1" using `m=0`
    1.35 +        by (simp add:clique_def)(metis card.empty emptyE empty_subsetI)
    1.36 +    qed
    1.37 +  } moreover
    1.38 +  { assume "n=0"
    1.39 +    have ?case (is "EX r. ?R r")
    1.40 +    proof
    1.41 +      show "?R 1" using `n=0`
    1.42 +        by (simp add:indep_def)(metis card.empty emptyE empty_subsetI)
    1.43 +    qed
    1.44 +  } moreover
    1.45 +  { assume "m\<noteq>0" "n\<noteq>0"
    1.46 +    hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
    1.47 +    from Suc(1)[OF this(1)] Suc(1)[OF this(2)] 
    1.48 +    obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
    1.49 +      by auto
    1.50 +    hence "r1+r2 \<ge> 1" by arith
    1.51 +    moreover
    1.52 +    have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
    1.53 +    proof clarify
    1.54 +      fix V :: "'a set" and E :: "'a set set"
    1.55 +      assume "finite V" "r1+r2 \<le> card V"
    1.56 +      with `r1\<ge>1` have "V \<noteq> {}" by auto
    1.57 +      then obtain v where "v : V" by blast
    1.58 +      let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
    1.59 +      let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
    1.60 +      have "V = insert v (?M \<union> ?N)" using `v : V` by auto
    1.61 +      hence "card V = card(insert v (?M \<union> ?N))" by metis
    1.62 +      also have "\<dots> = card ?M + card ?N + 1" using `finite V`
    1.63 +        by(fastsimp intro: card_Un_disjoint)
    1.64 +      finally have "card V = card ?M + card ?N + 1" .
    1.65 +      hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
    1.66 +      hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
    1.67 +      moreover
    1.68 +      { assume "r1 \<le> card ?M"
    1.69 +        moreover have "finite ?M" using `finite V` by auto
    1.70 +        ultimately have "?EX ?M E (m - 1) n" using `?R (m - 1) n r1` by blast
    1.71 +        then obtain R where "R \<subseteq> ?M" "v ~: R" and
    1.72 +          CI: "card R = m - 1 \<and> clique R E \<or>
    1.73 +               card R = n \<and> indep R E" (is "?C \<or> ?I")
    1.74 +          by blast
    1.75 +        have "R <= V" using `R <= ?M` by auto
    1.76 +        have "finite R" using `finite V` `R \<subseteq> V` by (metis finite_subset)
    1.77 +        { assume "?I"
    1.78 +          with `R <= V` have "?EX V E m n" by blast
    1.79 +        } moreover
    1.80 +        { assume "?C"
    1.81 +          hence "clique (insert v R) E" using `R <= ?M`
    1.82 +           by(auto simp:clique_def insert_commute)
    1.83 +          moreover have "card(insert v R) = m"
    1.84 +            using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
    1.85 +          ultimately have "?EX V E m n" using `R <= V` `v : V` by blast
    1.86 +        } ultimately have "?EX V E m n" using CI by blast
    1.87 +      } moreover
    1.88 +      { assume "r2 \<le> card ?N"
    1.89 +        moreover have "finite ?N" using `finite V` by auto
    1.90 +        ultimately have "?EX ?N E m (n - 1)" using `?R m (n - 1) r2` by blast
    1.91 +        then obtain R where "R \<subseteq> ?N" "v ~: R" and
    1.92 +          CI: "card R = m \<and> clique R E \<or>
    1.93 +               card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
    1.94 +          by blast
    1.95 +        have "R <= V" using `R <= ?N` by auto
    1.96 +        have "finite R" using `finite V` `R \<subseteq> V` by (metis finite_subset)
    1.97 +        { assume "?C"
    1.98 +          with `R <= V` have "?EX V E m n" by blast
    1.99 +        } moreover
   1.100 +        { assume "?I"
   1.101 +          hence "indep (insert v R) E" using `R <= ?N`
   1.102 +            by(auto simp:indep_def insert_commute)
   1.103 +          moreover have "card(insert v R) = n"
   1.104 +            using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
   1.105 +          ultimately have "?EX V E m n" using `R <= V` `v : V` by blast
   1.106 +        } ultimately have "?EX V E m n" using CI by blast
   1.107 +      } ultimately show "?EX V E m n" by blast
   1.108 +    qed
   1.109 +    ultimately have ?case by blast
   1.110 +  } ultimately show ?case by blast
   1.111 +qed
   1.112 +
   1.113 +
   1.114  subsection {* Preliminaries *}
   1.115  
   1.116  subsubsection {* ``Axiom'' of Dependent Choice *}