(* Title: ZF/ex/ramsey.thy ID: $Id: Ramsey.thy,v 1.12 2005/06/17 14:15:11 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Ramsey's Theorem (finite exponent 2 version) Based upon the article D Basin and M Kaufmann, The Boyer-Moore Prover and Nuprl: An Experimental Comparison. In G Huet and G Plotkin, editors, Logical Frameworks. (CUP, 1991), pages 89-119 See also M Kaufmann, An example in NQTHM: Ramsey's Theorem Internal Note, Computational Logic, Inc., Austin, Texas 78703 Available from the author: kaufmann@cli.com This function compute Ramsey numbers according to the proof given below (which, does not constrain the base case values at all. fun ram 0 j = 1 | ram i 0 = 1 | ram i j = ram (i-1) j + ram i (j-1) *) theory Ramsey imports Main begin constdefs Symmetric :: "i=>o" "Symmetric(E) == (∀x y. <x,y>:E --> <y,x>:E)" Atleast :: "[i,i]=>o" (*not really necessary: ZF defines cardinality*) "Atleast(n,S) == (∃f. f ∈ inj(n,S))" Clique :: "[i,i,i]=>o" "Clique(C,V,E) == (C ⊆ V) & (∀x ∈ C. ∀y ∈ C. x≠y --> <x,y> ∈ E)" Indept :: "[i,i,i]=>o" "Indept(I,V,E) == (I ⊆ V) & (∀x ∈ I. ∀y ∈ I. x≠y --> <x,y> ∉ E)" Ramsey :: "[i,i,i]=>o" "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))" (*** Cliques and Independent sets ***) 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) (*** Atleast ***) 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})" apply (unfold 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))" apply (unfold 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]) (*** Main Cardinality Lemma ***) (*The #-succ(0) strengthens the original theorem statement, but precisely the same proof could be used!!*) lemma pigeon2 [rule_format]: "m ∈ nat ==> ∀n ∈ nat. ∀A B. Atleast((m#+n) #- succ(0), A Un B) --> Atleast(m,A) | Atleast(n,B)" apply (induct_tac "m") apply (blast intro!: Atleast0, simp) apply (rule ballI) apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*) apply (induct_tac "n", auto) apply (erule Atleast_succD [THEN bexE]) apply (rename_tac n' A B z) apply (erule UnE) (**case z ∈ B. Instantiate the '∀A B' induction hypothesis. **) apply (drule_tac [2] x1 = A and x = "B-{z}" in spec [THEN spec]) apply (erule_tac [2] mp [THEN disjE]) (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) apply (erule_tac [3] asm_rl notE Atleast_Diff_succI)+ (*proving the condition*) prefer 2 apply (blast intro: Atleast_superset) (**case z ∈ A. Instantiate the '∀n ∈ nat. ∀A B' induction hypothesis. **) 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]) (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+ (*proving the condition*) apply simp apply (blast intro: Atleast_superset) done (**** Ramsey's Theorem ****) (** Base cases of induction; they now admit ANY Ramsey number **) lemma Ramsey0j: "Ramsey(n,0,j)" by (unfold Ramsey_def, blast) lemma Ramseyi0: "Ramsey(n,i,0)" by (unfold Ramsey_def, blast) (** Lemmas for induction step **) (*The use of succ(m) here, rather than #-succ(0), simplifies the proof of Ramsey_step_lemma.*) 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 (*For the Atleast part, proves ~(a ∈ I) from the second premise!*) 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))" apply (unfold 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))" apply (unfold Symmetric_def Clique_def) apply (blast intro!: Atleast_succI) done (** Induction step **) (*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*) 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+) (*case m*) apply (fast dest!: Indept_succ elim: Clique_superset) (*case n*) apply (fast dest!: Clique_succ elim: Indept_superset) done (** The actual proof **) (*Again, the induction requires Ramsey numbers to be positive.*) 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 (*Final statement in a tidy form, without succ(...) *) lemma ramsey: "[| i ∈ nat; j ∈ nat |] ==> ∃n ∈ nat. Ramsey(n,i,j)" by (blast dest: ramsey_lemma) end
lemma Clique0:
Clique(0, V, E)
lemma Clique_superset:
[| Clique(C, V', E); V' ⊆ V |] ==> Clique(C, V, E)
lemma Indept0:
Indept(0, V, E)
lemma Indept_superset:
[| Indept(I, V', E); V' ⊆ V |] ==> Indept(I, V, E)
lemma Atleast0:
Atleast(0, A)
lemma Atleast_succD:
Atleast(succ(m), A) ==> ∃x∈A. Atleast(m, A - {x})
lemma Atleast_superset:
[| Atleast(n, A); A ⊆ B |] ==> Atleast(n, B)
lemma Atleast_succI:
[| Atleast(m, B); b ∉ B |] ==> Atleast(succ(m), cons(b, B))
lemma Atleast_Diff_succI:
[| Atleast(m, B - {x}); x ∈ B |] ==> Atleast(succ(m), B)
lemma pigeon2:
[| m ∈ nat; n ∈ nat; Atleast(m #+ n #- 1, A ∪ B) |] ==> Atleast(m, A) ∨ Atleast(n, B)
lemma Ramsey0j:
Ramsey(n, 0, j)
lemma Ramseyi0:
Ramsey(n, i, 0)
lemma Atleast_partition:
[| Atleast(m #+ n, A); m ∈ nat; n ∈ nat |] ==> Atleast(succ(m), {x ∈ A . ¬ P(x)}) ∨ Atleast(n, {x ∈ A . P(x)})
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))
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))
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))
lemma ramsey_lemma:
i ∈ nat ==> ∀j∈nat. ∃n∈nat. Ramsey(succ(n), i, j)
lemma ramsey:
[| i ∈ nat; j ∈ nat |] ==> ∃n∈nat. Ramsey(n, i, j)