Quelle  graph_ops.pvs

%------------------------------------------------------------------------
% 
%  Operations on a graph
%  ------------------------------------------------
%
%      Author: Ricky W. Butler   NASA Langley Research Center
%
%  Defines:
%
%      union(G1,G2)      -- creates graph that is a union of G1 and G2  
%
%      del_vert(G,v)     -- removes a vertex and all adjacent edges from a graph
%
%      del_edge(e,G)     --  creates subgraph with edge e removed
%   
%      num_edges(G): nat --  number of edges in a graph
%
%------------------------------------------------------------------------
graph_ops[T: TYPE]: THEORY

BEGIN

   IMPORTING graphs[T]

   G, G1, G2: VAR graph[T]
   t1,t2: VAR T
   x,v: VAR T
   e,e2: VAR doubleton[T]

   union(G1,G2): graph[T] = (# vert := union(vert(G1),vert(G2)),
                               edges := union(edges(G1),edges(G2)) #)
 
   del_vert(G: graph[T], v: T): graph[T] = 
                        (# vert := remove[T](v,vert(G)),
                           edges := {e | edges(G)(e) AND NOT e(v)} #)
                            
   del_edge(G,e): graph[T] = G WITH [edges := remove(e,edges(G))]

   num_edges(G): nat = card(edges(G))

   adjacent(G, (x:T)): finite_set[T] = {y: T| vert(G)(y) AND edge?(G)(x,y)}

%  --------------------- 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 e(v)) 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 e(v) IMPLIES
                               del_vert(del_edge(G,e),v) = del_vert(G,v)


END graph_ops