FDL > PVS > Graphs > subgraphs : Theory

PVS-2.4 graphs/subgraphs.pvs

subgraphs [T:TYPE] : THEORY
BEGIN

IMPORTING graphs[T]

V: VAR set[T]

G: VAR graph[T]

G1: VAR graph[T]

G2: VAR graph[T]

SS: VAR graph[T]

i: VAR T

e: VAR doubleton[T]

subgraph?(G1, G2): bool = subset?(vert(G1), vert(G2)) AND subset?(edges(G1), edges(G2));

equal?(G1, G2): bool = subgraph?(G1, G2) AND subgraph?(G2, G1);

Subgraph(G) : TYPE = {(S:graph[T]) | subgraph?(S, G)}

finite vert subset: LEMMA is finite(LAMBDA (i:T) : vert(G)(i) AND V(i))

%%(TCC) subgraph_TCC1: OBLIGATION

%%(TCC) subgraph_TCC2: OBLIGATION

%%(TCC) subgraph_TCC3: OBLIGATION

subgraph(G, V): Subgraph(G) = G WITH [vert := {i | vert(G)(i) AND V(i)}, edges := {e | edges(G)(e) AND (FORALL (x:T) : e(x) IMPLIES V(x))}];

subgraph vert sub: LEMMA subset?(V, vert(G)) IMPLIES (vert(subgraph(G, V)) = V)

subgraph lem: LEMMA subgraph?(subgraph(G, V), G)

subgraph smaller: LEMMA subgraph?(SS, G) IMPLIES (size(SS) < = size(G))

END subgraphs