Theory Ramsey
theory Ramsey imports ZF begin
definition
Symmetric :: "i⇒o" where
"Symmetric(E) ≡ (∀x y. ⟨x,y⟩:E ⟶ ⟨y,x⟩:E)"
definition
Atleast :: "[i,i]⇒o" where
"Atleast(n,S) ≡ (∃f. f ∈ inj(n,S))"
definition
Clique :: "[i,i,i]⇒o" where
"Clique(C,V,E) ≡ (C ⊆ V) ∧ (∀x ∈ C. ∀y ∈ C. x≠y ⟶ ⟨x,y⟩ ∈ E)"
definition
Indept :: "[i,i,i]⇒o" where
"Indept(I,V,E) ≡ (I ⊆ V) ∧ (∀x ∈ I. ∀y ∈ I. x≠y ⟶ ⟨x,y⟩ ∉ E)"
definition
Ramsey :: "[i,i,i]⇒o" where
"Ramsey(n,i,j) ≡ ∀V E. Symmetric(E) ∧ Atleast(n,V) ⟶
(∃C. Clique(C,V,E) ∧ Atleast(i,C)) |
(∃I. Indept(I,V,E) ∧ Atleast(j,I))"
lemma Clique0 [intro]: "Clique(0,V,E)"
by (unfold Clique_def, blast)
lemma Clique_superset: "⟦Clique(C,V',E); V'<=V⟧ ⟹ Clique(C,V,E)"
by (unfold Clique_def, blast)
lemma Indept0 [intro]: "Indept(0,V,E)"
by (unfold Indept_def, blast)
lemma Indept_superset: "⟦Indept(I,V',E); V'<=V⟧ ⟹ Indept(I,V,E)"
by (unfold Indept_def, blast)
lemma Atleast0 [intro]: "Atleast(0,A)"
by (unfold Atleast_def inj_def Pi_def function_def, blast)
lemma Atleast_succD:
"Atleast(succ(m),A) ⟹ ∃x ∈ A. Atleast(m, A-{x})"
unfolding Atleast_def
apply (blast dest: inj_is_fun [THEN apply_type] inj_succ_restrict)
done
lemma Atleast_superset:
"⟦Atleast(n,A); A ⊆ B⟧ ⟹ Atleast(n,B)"
by (unfold Atleast_def, blast intro: inj_weaken_type)
lemma Atleast_succI:
"⟦Atleast(m,B); b∉ B⟧ ⟹ Atleast(succ(m), cons(b,B))"
unfolding Atleast_def succ_def
apply (blast intro: inj_extend elim: mem_irrefl)
done
lemma Atleast_Diff_succI:
"⟦Atleast(m, B-{x}); x ∈ B⟧ ⟹ Atleast(succ(m), B)"
by (blast intro: Atleast_succI [THEN Atleast_superset])
lemma pigeon2 [rule_format]:
"m ∈ nat ⟹
∀n ∈ nat. ∀A B. Atleast((m#+n) #- succ(0), A ∪ B) ⟶
Atleast(m,A) | Atleast(n,B)"
apply (induct_tac "m")
apply (blast intro!: Atleast0, simp)
apply (rule ballI)
apply (rename_tac m' n)
apply (induct_tac "n", auto)
apply (erule Atleast_succD [THEN bexE])
apply (rename_tac n' A B z)
apply (erule UnE)
apply (drule_tac [2] x1 = A and x = "B-{z}" in spec [THEN spec])
apply (erule_tac [2] mp [THEN disjE])
apply (erule_tac [3] asm_rl notE Atleast_Diff_succI)+
prefer 2 apply (blast intro: Atleast_superset)
apply (drule_tac x2="succ(n')" and x1="A-{z}" and x=B
in bspec [THEN spec, THEN spec])
apply (erule nat_succI)
apply (erule mp [THEN disjE])
apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+
apply simp
apply (blast intro: Atleast_superset)
done
lemma Ramsey0j: "Ramsey(n,0,j)"
by (unfold Ramsey_def, blast)
lemma Ramseyi0: "Ramsey(n,i,0)"
by (unfold Ramsey_def, blast)
lemma Atleast_partition: "⟦Atleast(m #+ n, A); m ∈ nat; n ∈ nat⟧
⟹ Atleast(succ(m), {x ∈ A. ¬P(x)}) | Atleast(n, {x ∈ A. P(x)})"
apply (rule nat_succI [THEN pigeon2], assumption+)
apply (rule Atleast_superset, auto)
done
lemma Indept_succ:
"⟦Indept(I, {z ∈ V-{a}. ⟨a,z⟩ ∉ E}, E); Symmetric(E); a ∈ V;
Atleast(j,I)⟧ ⟹
Indept(cons(a,I), V, E) ∧ Atleast(succ(j), cons(a,I))"
unfolding Symmetric_def Indept_def
apply (blast intro!: Atleast_succI)
done
lemma Clique_succ:
"⟦Clique(C, {z ∈ V-{a}. ⟨a,z⟩:E}, E); Symmetric(E); a ∈ V;
Atleast(j,C)⟧ ⟹
Clique(cons(a,C), V, E) ∧ Atleast(succ(j), cons(a,C))"
unfolding Symmetric_def Clique_def
apply (blast intro!: Atleast_succI)
done
lemma Ramsey_step_lemma:
"⟦Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j));
m ∈ nat; n ∈ nat⟧ ⟹ Ramsey(succ(m#+n), succ(i), succ(j))"
apply (unfold Ramsey_def, clarify)
apply (erule Atleast_succD [THEN bexE])
apply (erule_tac P1 = "λz.⟨x,z⟩:E" in Atleast_partition [THEN disjE],
assumption+)
apply (fast dest!: Indept_succ elim: Clique_superset)
apply (fast dest!: Clique_succ elim: Indept_superset)
done
lemma ramsey_lemma: "i ∈ nat ⟹ ∀j ∈ nat. ∃n ∈ nat. Ramsey(succ(n), i, j)"
apply (induct_tac "i")
apply (blast intro!: Ramsey0j)
apply (rule ballI)
apply (induct_tac "j")
apply (blast intro!: Ramseyi0)
apply (blast intro!: add_type Ramsey_step_lemma)
done
lemma ramsey: "⟦i ∈ nat; j ∈ nat⟧ ⟹ ∃n ∈ nat. Ramsey(n,i,j)"
by (blast dest: ramsey_lemma)
end