|
%------------------------------------------------------------------------
%
% Operations on a digraph
% ------------------------------------------------
%
% Author: Ricky W. Butler NASA Langley Research Center
%
% Defines:
%
% union(G1,G2) -- creates digraph that is a union of G1 and G2
%
% del_vert(G,v) -- removes a vertex and all adjacent edges from a digraph
%
% del_edge(e,G) -- creates di_subgraph with edge e removed
%
% num_edges(G): nat -- number of edges in a digraph
%
%------------------------------------------------------------------------
digraph_ops[T: TYPE]: THEORY
BEGIN
IMPORTING digraphs[T]
G, G1, G2: VAR digraph[T]
t1,t2: VAR T
x,v: VAR T
e,e2: VAR edgetype[T]
union(G1,G2): digraph[T] = (# vert := union(vert(G1),vert(G2)),
edges := union(edges(G1),edges(G2)) #)
del_vert(G: digraph[T], v: T): digraph[T] =
(# vert := remove[T](v,vert(G)),
edges := {e | edges(G)(e) AND NOT in?(v,e)} #)
del_edge(G,e): digraph[T] = G WITH [edges := remove(e,edges(G))]
num_edges(G): nat = card(edges(G))
% --------------------- del_vert(G,v) lemmas ----------------
del_vert_still_in : LEMMA FORALL (x: (vert(G))):
x /= v IMPLIES vert(del_vert(G, v))(x)
size_del_vert : LEMMA FORALL (v: (vert(G))):
size(del_vert(G,v)) = size(G) - 1
del_vert_le : LEMMA size(del_vert(G,v)) <= size(G)
del_vert_ge : LEMMA size(del_vert(G,v)) >= size(G) - 1
edge_in_del_vert : LEMMA (edges(G)(e) AND NOT in?(v,e)) IMPLIES
edges(del_vert(G,v))(e)
edges_del_vert : LEMMA edges(del_vert(G,v))(e) IMPLIES
edges(G)(e)
del_vert_comm : LEMMA del_vert(del_vert(G, x), v) =
del_vert(del_vert(G, v), x)
del_vert_empty? : LEMMA FORALL (v: (vert(G))):
empty?(vert(del_vert(G, v))) IMPLIES
singleton?(G)
% ---------- del_edge(G,e) ----------------------------------
del_edge_lem : LEMMA NOT member(e,edges(del_edge(G,e)))
del_edge_lem2 : LEMMA edges(del_edge(G,e))(e2)
IMPLIES edges(G)(e2)
del_edge_lem3 : LEMMA edges(G)(e2) AND e2 /= e IMPLIES
edges(del_edge(G,e))(e2)
del_edge_lem5 : LEMMA NOT edges(G)(e) IMPLIES del_edge(G, e) = G
vert_del_edge : LEMMA vert(del_edge(G,e)) = vert(G)
del_edge_num : LEMMA num_edges(del_edge(G,e)) = num_edges(G)
- IF edges(G)(e) THEN 1 ELSE 0 ENDIF
del_edge_singleton : LEMMA singleton?(del_edge(G,e)) IMPLIES singleton?(G)
del_vert_edge_comm : LEMMA del_vert(del_edge(G, e), v) =
del_edge(del_vert(G, v), e)
del_vert_edge : LEMMA in?(v,e) IMPLIES
del_vert(del_edge(G,e),v) = del_vert(G,v)
END digraph_ops
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
