|
graph_from_edges[T: TYPE]: THEORY
%----------------------------------------------------------------------------
%
% Author: Christian van der Stap
% Technical University of Eindhoven
% Netherlands
%
% Jon Sjogren, AFOSR
%
%----------------------------------------------------------------------------
BEGIN
IMPORTING graphs
ES: VAR finite_set[doubleton[T]]
N, M: VAR nat
x,y: VAR T
finite_lem: LEMMA is_finite(Union(ES))
Union_to_pred: LEMMA FORALL x: Union(ES)(x)
=> EXISTS (d: doubleton[T]): ES(d) AND d(x)
pred_to_Union: LEMMA FORALL x: (EXISTS (d: doubleton[T]): ES(d) AND d(x))
=> Union(ES)(x)
verts_of(ES): finite_set[T] = Union(ES)
verts_from(ES): finite_set[T] = {t:T | EXISTS (d: doubleton[T]):
d(t) AND ES(d)}
verts_from_of: LEMMA verts_of(ES) = verts_from(ES)
G: VAR graph[T]
v: VAR T
isolated_vert?(G,v): bool = NOT member(v, verts_of(edges(G)))
es_graph: TYPE = {G: graph[T] | FORALL (v: (vert(G))):
NOT isolated_vert?(G,v)}
graph_from_edgeset(ES): es_graph =
(# vert := verts_of(ES),
edges := ES
#)
graph_from_edgeset_rew1: LEMMA edges(graph_from_edgeset(ES))= ES
graph_from_edgeset_rew2: LEMMA vert(graph_from_edgeset(ES))= verts_of(ES)
no_isolated_verts: LEMMA Let G = graph_from_edgeset(ES) IN
vert(G)(v) IMPLIES
NOT isolated_vert?(G,v)
END graph_from_edges
¤ Dauer der Verarbeitung: 0.12 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.
|
