FDL > PVS > Graphs > graph_deg : Theory

PVS-2.4 graphs/graph deg.pvs

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

------------------------------------------------------------------------

graph_deg [T:TYPE] : THEORY
BEGIN

IMPORTING graphs[T]

IMPORTING graph ops[T]

v: VAR T

G: VAR graph[T]

GS: VAR graph[T]

%%(TCC) incident_edges_TCC1: OBLIGATION

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: VAR T

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

%%(TCC) deg_del_vert_TCC1: OBLIGATION

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