%------------------------------------------------------------------------ % % 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