di_subgraphs[T: TYPE]: THEORY

BEGIN

   IMPORTING digraphs[T]

   V: VAR set[T]
   G,G1,G2,SS: VAR digraph[T]
   i: VAR T
   e: VAR edgetype[T]

   di_subgraph?(G1,G2): bool = subset?(vert(G1),vert(G2)) AND
                               subset?(edges(G1),edges(G2))

   equal?(G1,G2): bool = di_subgraph?(G1,G2) AND di_subgraph?(G2,G1)

   di_subgraph(G): TYPE = {S: digraph[T] | di_subgraph?(S,G)}

   finite_vert_subset: LEMMA is_finite(LAMBDA (i:T): vert(G)(i) AND V(i))

   finite_edge_subset: LEMMA is_finite[edgetype[T]]
               ({e | G`edges(e) AND (LET (x, y) = e IN V(x) AND V(y))})


%   di_subgraph(G, V): di_subgraph(G) =
%       (G WITH [vert :=  {i | vert(G)(i) AND V(i)},
%                edges := {e | edges(G)(e) AND 
%                              (FORALL (x: T): in?(x,e) IMPLIES V(x))}])

   x,y: VAR T
   di_subgraph(G, V): di_subgraph(G) =
       (G WITH [vert :=  {i | vert(G)(i) AND V(i)},
                edges := {e | edges(G)(e) AND (Let (x,y) = e IN V(x) AND V(y))}])

   di_subgraph_vert_sub: LEMMA subset?(V,vert(G)) IMPLIES
                                        vert(di_subgraph(G,V)) = V

   di_subgraph_lem     : LEMMA di_subgraph?(di_subgraph(G,V),G)

   di_subgraph_smaller: LEMMA di_subgraph?(SS, G) IMPLIES
                         size(SS) <= size(G)

END di_subgraphs