graph_deg[T: TYPE]: THEORY
%------------------------------------------------------------------------
% 
%  Defines degree of a vertex
%  ------------------------------------------------
%
%      Author: Ricky W. Butler   NASA Langley Research Center
%
%  Defines:
%
%    incident_edges(v,G) -- returns set of edges attached to vertex v
%
%    deg(v,G)          -- number of edges attached to vertex v    
%
%------------------------------------------------------------------------

BEGIN

   IMPORTING graphs[T], graph_ops[T]

   v: VAR T
   G,GS: VAR graph[T]

   incident_edges(v,G)  : finite_set[doubleton[T]] 
                              = {e: doubleton[T] | edges(G)(e) AND e(v)}

   incident_edges_subset: LEMMA subset?(incident_edges(v,G),edges(G))

   deg(v,G): nat = card(incident_edges(v,G))

   P : VAR pred[graph[T]]
   n : VAR nat
   e: VAR doubleton[T]
   x,y: VAR T

   incident_edges_emptyset: LEMMA edges(G) = emptyset[doubleton[T]] IMPLIES
                                    incident_edges(v,G) = emptyset[doubleton[T]]


   deg_del_edge    : LEMMA e = dbl(x,y) AND edges(G)(e) IMPLIES  
                             deg(y, G) = deg(y, del_edge(G, e)) + 1

   deg_del_edge2   : LEMMA e(y) AND edges(G)(e) IMPLIES  
                             deg(y, G) = deg(y, del_edge(G, e)) + 1


   deg_del_edge3   : LEMMA NOT e(y)  IMPLIES  
                              deg(y, G) = deg(y, del_edge(G, e))

   deg_del_edge_ge : LEMMA deg(y, G) >= deg(y, del_edge(G, e))


   deg_del_edge_le : LEMMA deg(y, G) - 1 <= deg(y, del_edge(G, e))

   deg_edge_exists       : LEMMA deg(v,G) > 0 IMPLIES
                             (EXISTS e: e(v) AND edges(G)(e))
      
   deg_to_card     : LEMMA deg(v,G) > 0 IMPLIES size(G) >= 2

   del_vert_deg_0  : LEMMA deg(v,G) = 0 IMPLIES 
                               edges(del_vert(G,v)) = edges(G)

   deg_del_vert: LEMMA x /= v AND edges(G)(dbl[T](x, v))  
                                IMPLIES deg(v, del_vert(G, x)) = 
                                           deg(v, G) - 1

   del_vert_not_incident: LEMMA x /= v AND NOT edges(G)(dbl[T](x, v)) IMPLIES
                                       deg(x, del_vert(G, v)) = deg(x, G)

   singleton_deg: LEMMA singleton?(G) IMPLIES deg(v, G) = 0

   deg_1_sing   : LEMMA deg(v, G) = 1 IMPLIES 
                           (EXISTS e: incident_edges(v, G) = singleton(e) AND
                                      e(v) AND edges(G)(e))


 
END graph_deg