diff --git a/src/HOL/Library/Ramsey.thy b/src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy
+++ b/src/HOL/Library/Ramsey.thy
@@ -1,414 +1,410 @@
(* Title: HOL/Library/Ramsey.thy
Author: Tom Ridge. Converted to structured Isar by L C Paulson
*)
section \Ramsey's Theorem\
theory Ramsey
imports Infinite_Set
begin
subsection \Finite Ramsey theorem(s)\
text \
To distinguish the finite and infinite ones, lower and upper case
names are used.
This is the most basic version in terms of cliques and independent
sets, i.e. the version for graphs and 2 colours.
\
definition "clique V E \ (\v\V. \w\V. v \ w \ {v, w} \ E)"
definition "indep V E \ (\v\V. \w\V. v \ w \ {v, w} \ E)"
lemma ramsey2:
"\r\1. \(V::'a set) (E::'a set set). finite V \ card V \ r \
(\R \ V. card R = m \ clique R E \ card R = n \ indep R E)"
(is "\r\1. ?R m n r")
proof (induct k \ "m + n" arbitrary: m n)
case 0
show ?case (is "\r. ?Q r")
proof
from 0 show "?Q 1"
by (clarsimp simp: indep_def) (metis card.empty emptyE empty_subsetI)
qed
next
case (Suc k)
consider "m = 0 \ n = 0" | "m \ 0" "n \ 0" by auto
then show ?case (is "\r. ?Q r")
proof cases
case 1
then have "?Q 1"
by (simp add: clique_def) (meson card_empty empty_iff empty_subsetI indep_def)
then show ?thesis ..
next
case 2
with Suc(2) have "k = (m - 1) + n" "k = m + (n - 1)" by auto
from this [THEN Suc(1)]
obtain r1 r2 where "r1 \ 1" "r2 \ 1" "?R (m - 1) n r1" "?R m (n - 1) r2" by auto
then have "r1 + r2 \ 1" by arith
moreover have "?R m n (r1 + r2)" (is "\V E. _ \ ?EX V E m n")
proof clarify
fix V :: "'a set"
fix E :: "'a set set"
assume "finite V" "r1 + r2 \ card V"
with \r1 \ 1\ have "V \ {}" by auto
then obtain v where "v \ V" by blast
let ?M = "{w \ V. w \ v \ {v, w} \ E}"
let ?N = "{w \ V. w \ v \ {v, w} \ E}"
from \v \ V\ have "V = insert v (?M \ ?N)" by auto
then have "card V = card (insert v (?M \ ?N))" by metis
also from \finite V\ have "\ = card ?M + card ?N + 1"
by (fastforce intro: card_Un_disjoint)
finally have "card V = card ?M + card ?N + 1" .
with \r1 + r2 \ card V\ have "r1 + r2 \ card ?M + card ?N + 1" by simp
then consider "r1 \ card ?M" | "r2 \ card ?N" by arith
then show "?EX V E m n"
proof cases
case 1
from \finite V\ have "finite ?M" by auto
with \?R (m - 1) n r1\ and 1 have "?EX ?M E (m - 1) n" by blast
then obtain R where "R \ ?M" "v \ R"
and CI: "card R = m - 1 \ clique R E \ card R = n \ indep R E" (is "?C \ ?I")
by blast
from \R \ ?M\ have "R \ V" by auto
with \finite V\ have "finite R" by (metis finite_subset)
from CI show ?thesis
proof
assume "?I"
with \R \ V\ show ?thesis by blast
next
assume "?C"
with \R \ ?M\ have *: "clique (insert v R) E"
by (auto simp: clique_def insert_commute)
from \?C\ \finite R\ \v \ R\ \m \ 0\ have "card (insert v R) = m" by simp
with \R \ V\ \v \ V\ * show ?thesis by (metis insert_subset)
qed
next
case 2
from \finite V\ have "finite ?N" by auto
with \?R m (n - 1) r2\ 2 have "?EX ?N E m (n - 1)" by blast
then obtain R where "R \ ?N" "v \ R"
and CI: "card R = m \ clique R E \ card R = n - 1 \ indep R E" (is "?C \ ?I")
by blast
from \R \ ?N\ have "R \ V" by auto
with \finite V\ have "finite R" by (metis finite_subset)
from CI show ?thesis
proof
assume "?C"
with \R \ V\ show ?thesis by blast
next
assume "?I"
with \R \ ?N\ have *: "indep (insert v R) E"
by (auto simp: indep_def insert_commute)
from \?I\ \finite R\ \v \ R\ \n \ 0\ have "card (insert v R) = n" by simp
with \R \ V\ \v \ V\ * show ?thesis by (metis insert_subset)
qed
qed
qed
ultimately show ?thesis by blast
qed
qed
subsection \Preliminaries\
subsubsection \``Axiom'' of Dependent Choice\
primrec choice :: "('a \ bool) \ ('a \ 'a) set \ nat \ 'a"
where \ \An integer-indexed chain of choices\
choice_0: "choice P r 0 = (SOME x. P x)"
| choice_Suc: "choice P r (Suc n) = (SOME y. P y \ (choice P r n, y) \ r)"
lemma choice_n:
assumes P0: "P x0"
and Pstep: "\x. P x \ \y. P y \ (x, y) \ r"
shows "P (choice P r n)"
proof (induct n)
case 0
show ?case by (force intro: someI P0)
next
case Suc
then show ?case by (auto intro: someI2_ex [OF Pstep])
qed
lemma dependent_choice:
assumes trans: "trans r"
and P0: "P x0"
and Pstep: "\x. P x \ \y. P y \ (x, y) \ r"
obtains f :: "nat \ 'a" where "\n. P (f n)" and "\n m. n < m \ (f n, f m) \ r"
proof
fix n
show "P (choice P r n)"
by (blast intro: choice_n [OF P0 Pstep])
next
fix n m :: nat
assume "n < m"
from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) \ r" for k
by (auto intro: someI2_ex)
then show "(choice P r n, choice P r m) \ r"
by (auto intro: less_Suc_induct [OF \n < m\] transD [OF trans])
qed
subsubsection \Partitions of a Set\
definition part :: "nat \ nat \ 'a set \ ('a set \ nat) \ bool"
\ \the function \<^term>\f\ partitions the \<^term>\r\-subsets of the typically
infinite set \<^term>\Y\ into \<^term>\s\ distinct categories.\
where "part r s Y f \ (\X. X \ Y \ finite X \ card X = r \ f X < s)"
text \For induction, we decrease the value of \<^term>\r\ in partitions.\
lemma part_Suc_imp_part:
"\infinite Y; part (Suc r) s Y f; y \ Y\ \ part r s (Y - {y}) (\u. f (insert y u))"
- apply (simp add: part_def)
- apply clarify
- apply (drule_tac x="insert y X" in spec)
- apply force
- done
+ by (simp add: part_def subset_Diff_insert)
lemma part_subset: "part r s YY f \ Y \ YY \ part r s Y f"
unfolding part_def by blast
subsection \Ramsey's Theorem: Infinitary Version\
lemma Ramsey_induction:
fixes s r :: nat
and YY :: "'a set"
and f :: "'a set \ nat"
assumes "infinite YY" "part r s YY f"
shows "\Y' t'. Y' \ YY \ infinite Y' \ t' < s \ (\X. X \ Y' \ finite X \ card X = r \ f X = t')"
using assms
proof (induct r arbitrary: YY f)
case 0
then show ?case
by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
next
case (Suc r)
show ?case
proof -
from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \ YY"
by blast
let ?ramr = "{((y, Y, t), (y', Y', t')). y' \ Y \ Y' \ Y}"
let ?propr = "\(y, Y, t).
y \ YY \ y \ Y \ Y \ YY \ infinite Y \ t < s
\ (\X. X\Y \ finite X \ card X = r \ (f \ insert y) X = t)"
from Suc.prems have infYY': "infinite (YY - {yy})" by auto
from Suc.prems have partf': "part r s (YY - {yy}) (f \ insert yy)"
by (simp add: o_def part_Suc_imp_part yy)
have transr: "trans ?ramr" by (force simp add: trans_def)
from Suc.hyps [OF infYY' partf']
obtain Y0 and t0 where "Y0 \ YY - {yy}" "infinite Y0" "t0 < s"
"X \ Y0 \ finite X \