FDL > PVS > Graphs > graphs : Theory

PVS-2.4 graphs/graphs.pvs

graphs [T:TYPE] : THEORY
BEGIN

IMPORTING finite_sets@finite sets[T]

IMPORTING doubletons[T]

IMPORTING finite_sets@finite sets[doubleton[T]]

R: VAR PRED[[T, T]]

x: VAR T

y: VAR T

v: VAR T

pregraph : TYPE = [# vert: finite set[T], edges: finite set[doubleton[T]] #]

graph : TYPE = {(g:pregraph) | FORALL (e:doubleton[T]) : edges(g)(e) IMPLIES (FORALL (x:T) : e(x) IMPLIES vert(g)(x))}

e: VAR doubleton[T]

G: VAR graph

%%(TCC) edg_TCC1: OBLIGATION

edg(x, (y:{(y:T) | y /= x} )): doubleton[T] = dbl[T](x, y);

%%(TCC) edge?_TCC1: OBLIGATION

edge?(G)(x, y): bool = (x /= y) AND edges(G)(dbl[T](x, y));

edge? comm: LEMMA edge?(G)(y, x) IMPLIES edge?(G)(x, y)

edges vert: LEMMA (e(x) AND edges(G)(e)) IMPLIES (EXISTS y : (x /= y) AND vert(G)(y) AND e(y))

other vert: LEMMA (e(v) AND edges(G)(e)) IMPLIES (EXISTS (u:T) : (u /= v) AND vert(G)(u) AND (e = dbl[T](u, v)))

edge has 2 verts: LEMMA ((x /= v) AND e(x) AND e(v)) IMPLIES (e = dbl(x, v))

size(G): nat = card[T](vert(G));

empty?(G): bool = empty?(vert(G));

singleton?(G): bool = size(G) = 1;

isolated?(G): bool = empty?(edges(G));

empty? rew: LEMMA empty?(G) = (card(vert(G)) = 0)

edges of empty: LEMMA empty?(G) IMPLIES (edges(G) = emptyset[doubleton[T]])

singleton edges: LEMMA singleton?(G) IMPLIES empty?(edges(G))

edge in card gt 1: LEMMA edges(G)(e) IMPLIES (card(vert(G)) > 1)

not singleton 2 vert: LEMMA ((NOT empty?(G)) AND (NOT singleton?(G))) IMPLIES (EXISTS (x:T), (y:T) : (x /= y) AND vert(G)(x) AND vert(G)(y))

infgraph : TYPE = [# vert: set[T], edges: set[doubleton[T]] #]

is graph((g:infgraph)): bool = is finite[T](vert(g)) AND is finite[doubleton[T]](edges(g)) AND (FORALL (e:doubleton[T]) : edges(g)(e) IMPLIES (FORALL x : e(x) IMPLIES vert(g)(x)));

%%(TCC) singleton_graph_TCC1: OBLIGATION

singleton graph(v): graph = (#vert := singleton[T](v), edges := emptyset[doubleton[T]]#);

is sing: LEMMA singleton?(singleton graph(x))

Graph : TYPE = {(g:graph) | nonempty?(vert(g))}

finite dbl: LEMMA is finite(dbl[T](x, y))

finite doubleton: LEMMA is finite(e)

%%(TCC) card_dbl_TCC1: OBLIGATION

card dbl: LEMMA (x /= y) IMPLIES (card(dbl(x, y)) = 2)

%%(TCC) dbl_TCC1: OBLIGATION

: JUDGEMENT dbl(x, y) HAS_TYPE finite set[T]

END graphs