FDL > PVS > Graphs > ramsey_new : Theory

PVS-2.4 graphs/ramsey new.pvs

ramsey_new [T:TYPE] : THEORY
BEGIN

IMPORTING graphs[T]

IMPORTING subgraphs[T]

i: VAR T

j: VAR T

n: VAR nat

p: VAR nat

q: VAR nat

ii: VAR nat

g: VAR graph[T]

V: VAR finite set[T]

contains clique(g, n): bool = EXISTS (C:finite set[T]) : subset?(C, vert(g)) AND (card(C) > = n) AND (FORALL i, j : ((i /= j) AND C(i) AND C(j)) IMPLIES edge?(g)(i, j));

contains indep(g, n): bool = EXISTS (D:finite set[T]) : subset?(D, vert(g)) AND (card(D) > = n) AND (FORALL i, j : ((i /= j) AND D(i) AND D(j)) IMPLIES (NOT edge?(g)(i, j)));

subgraph clique: LEMMA FORALL (V:set[T]) : contains clique(subgraph(g, V), p) IMPLIES contains clique(g, p)

subgraph indep: LEMMA FORALL (V:set[T]) : contains indep(subgraph(g, V), p) IMPLIES contains indep(g, p)

G: VAR Graph[T]

%%(TCC) r1_TCC1: OBLIGATION

%%(TCC) r1_TCC2: OBLIGATION

r1(G): finite set[T] = LET v0 = choose(vert(G)) IN {(n:T) | vert(G)(n) AND (n /= v0) AND edge?(G)(v0, n)};

%%(TCC) r2_TCC1: OBLIGATION

r2(G): finite set[T] = LET v0 = choose(vert(G)) IN {(n:T) | vert(G)(n) AND (n /= v0) AND (NOT edge?(G)(v0, n))};

SG1(G): graph[T] = subgraph(G, r1(G));

SG2(G): graph[T] = subgraph(G, r2(G));

v0: VAR nat

card r1 r2: LEMMA (card(r1(G)) + card(r2(G))) > = (size(G) - 1)

ramsey(p, q): posnat;

l1: VAR nat

l2: VAR nat

ramsey lem: LEMMA FORALL l1, l2 : ((l1 + l2) = ii) IMPLIES (EXISTS (n:posnat) : FORALL (G:Graph[T]) : (size(G) > = n) IMPLIES (contains clique(G, l1) OR contains indep(G, l2)))

ramseys theorem: THEOREM EXISTS (n:posnat) : FORALL (G:Graph[T]) : (size(G) > = n) IMPLIES (contains clique(G, l1) OR contains indep(G, l2))

END ramsey_new