graphs[T: TYPE]: THEORY
%-------------------------------------------------------------------------------
%
% Defines:
%
% Graph[T] -- graph over domain T
% vert(G) -- vertices of graph G
% edges(G) -- set of edges in a graph G
%
% Authors:
%
% Ricky W. Butler NASA Langley
% Jon Sjogren AFOSR
%
% Version 1.0 Last modified 12/20/96
%
% Maintained by:
%
% Rick Butler NASA Langley Research Center
% [email protected]
%
% NOTE:
%
%-------------------------------------------------------------------------------
BEGIN
IMPORTING %finite_sets@finite_sets[T],
doubletons[T]
%finite_sets@finite_sets[doubleton[T]]
R: VAR PRED[[T, T]]
x,y,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
edg(x,(y:{y:T | y /= x})): doubleton[T] = dbl[T](x,y)
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)
%To aid in discharging TCCs
edges_vert_in: LEMMA e = dbl[T](x, y) AND edges(G)(e)
IMPLIES vert(G)(x) AND vert(G)(y)
vert_in: LEMMA edge?(G)(x,y) IMPLIES vert(G)(x) AND vert(G)(y)
% -------------- size of graphs --------------------
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,y: T): x /= y AND
vert(G)(x) AND vert(G)(y))
infgraph: TYPE = [# vert : set[T],
edges: set[doubleton[T]] #]
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)))
singleton_graph(v): (singleton?) = (# vert := singleton[T](v),
edges := emptyset[doubleton[T]] #)
Graph: TYPE = {g: graph | nonempty?(vert(g))}
END graphs
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
