Theory Ramsey

section "Ramsey's Theorem"

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

begin

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

end