Quelle  Ramsey.thy

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
  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