Quelle  di_subgraphs_from_walk.pvs   Sprache: PVS

di_subgraphs_from_walk[T: TYPE]: THEORY

BEGIN
   IMPORTING digraphs[T], walks[T], di_subgraphs[T]
   
   G,GG: VAR digraph[T]
   t,t1,t2,v: VAR T
   i: VAR nat
   e: VAR edgetype[T]

   G_from(G, (w: Walk(G))): di_subgraph(G) = (# vert  := verts_of(w),
                                             edges := edges_of(w) #)


   G_from_vert     : LEMMA FORALL (w: Walk(G)): vert(G_from(G,w)) = verts_of(w)


   vert_G_from     : LEMMA FORALL (w: Walk(G), i: below(length(w))): 
                                      vert(G_from(G, w))(w(i))

   edge?_G_from    : LEMMA FORALL (w: Walk(G), i: below(length(w)-1)): 
                                      edge?(G_from(G, w))(w(i), w(i+1)) 

%%%%%%%%%%%%%%%%%%%%%%%%%% not true for directed graphs %%%%%%%%%%%%%%%%%%%%
%
%   edge?_G_from_rev: LEMMA FORALL (w: Walk(G), i: below(length(w)-1)): 
%                                     edge?(G_from(G, w))(w(i+1), w(i))


   vert_G_from_not : LEMMA FORALL (w: Walk(G)): 
                       subset?(vert(G_from(G, w)), vert(GG)) AND
                       NOT  verts_of(w)(v)
                     IMPLIES
                        subset?(vert(G_from(G, w)), remove[T](v, vert(GG)))

   IMPORTING digraph_ops[T]

   del_vert_di_subgraph: LEMMA FORALL (w: Walk(G), v: (vert(GG))): 
                              di_subgraph?(G_from(G, w), GG) AND
                              NOT verts_of(w)(v) IMPLIES
                                    di_subgraph?(G_from(G, w), del_vert(GG, v))
        
END di_subgraphs_from_walk