Quelle  graph_from_edges.pvs

graph_from_edges[T: TYPE]: THEORY
%----------------------------------------------------------------------------
%
% Author:  Christian van der Stap
%          Technical University of Eindhoven
%          Netherlands
%
%          Jon Sjogren, AFOSR
%
%----------------------------------------------------------------------------
BEGIN
   IMPORTING graphs

   ES: VAR finite_set[doubleton[T]]
   N, M: VAR nat   
   x,y: VAR T

   finite_lem: LEMMA is_finite(Union(ES))

   Union_to_pred: LEMMA FORALL x: Union(ES)(x) 
                          => EXISTS (d: doubleton[T]): ES(d) AND d(x)

   pred_to_Union: LEMMA FORALL x: (EXISTS (d: doubleton[T]): ES(d) AND d(x))
                   => Union(ES)(x)


   verts_of(ES): finite_set[T] = Union(ES)


   verts_from(ES): finite_set[T] = {t:T | EXISTS (d: doubleton[T]): 
                                        d(t) AND ES(d)}

   verts_from_of: LEMMA verts_of(ES) = verts_from(ES)

   G: VAR graph[T]
   v: VAR T
   isolated_vert?(G,v): bool = NOT member(v, verts_of(edges(G)))


   es_graph: TYPE = {G: graph[T] | FORALL (v: (vert(G))):
                                       NOT isolated_vert?(G,v)}

   graph_from_edgeset(ES): es_graph =
             (# vert := verts_of(ES),
                edges := ES
             #)

   graph_from_edgeset_rew1: LEMMA edges(graph_from_edgeset(ES))= ES
   graph_from_edgeset_rew2: LEMMA vert(graph_from_edgeset(ES))= verts_of(ES)

   no_isolated_verts: LEMMA Let G = graph_from_edgeset(ES) IN 
                            vert(G)(v) IMPLIES
                               NOT isolated_vert?(G,v)



END graph_from_edges