Theory Ramsey

section "Ramsey's Theorem"

theory Ramsey
  imports Main "HOL-Library.Infinite_Set" "HOL-Library.Ramsey" 


text ‹Please note: this entire development has been updated and incorporated into 
@{theory "HOL-Library.Ramsey"}  above. Below, some of the results of the original development are 
linked to their current versions elsewhere in the Isabelle libraries. ›

subsection "Library lemmas"

lemma infinite_inj_infinite_image: "infinite Z  inj_on f Z  infinite (f ` Z)"
  using finite_imageD by blast

lemma infinite_dom_finite_rng: "[| infinite A; finite (f ` A) |] ==> b  f ` A. infinite {a : A. f a = b}"
  by (simp add: pigeonhole_infinite)

lemma infinite_mem: "infinite X  x. x  X"
  using finite_insert by fastforce

lemma not_empty_least: "(Y::nat set)  {}  m. m  Y  (m'. m'  Y  m  m')"
  by (meson Inf_nat_def1 bdd_below_bot cInf_lower)

subsection "Dependent Choice Variant"
lemma dc:
  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"
  by (metis P0 Pstep dependent_choice local.trans)

subsection "Ramsey's theorem"

lemma ramsey: "(s::nat) (r::nat) (YY::'a set) (f::'a set  nat).
  infinite YY 
   (X. X  YY  finite X  card X = r  f X < s)
   (Y' t'.
  Y'  YY 
   infinite Y' 
   t' < s 
   (X. X  Y'  finite X  card X = r  f X = t'))"
  using Ramsey by fastforce