subgraphs[T: TYPE]: THEORY

BEGIN

   IMPORTING graphs[T]

   V: VAR set[T]
   G,G1,G2,SS: VAR graph[T]
   i: VAR T
   e: VAR doubleton[T]

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

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

   Subgraph(G): TYPE = {S: graph[T] | subgraph?(S,G)}

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


   subgraph(G, V): Subgraph(G) =
       (G WITH [vert :=  {i | vert(G)(i) AND V(i)},
                edges := {e | edges(G)(e) AND 
                              (FORALL (x: T): e(x) IMPLIES V(x))}])

   subgraph_vert_sub: LEMMA subset?(V,vert(G)) IMPLIES
                                        vert(subgraph(G,V)) = V

   subgraph_lem     : LEMMA subgraph?(subgraph(G,V),G)

   subgraph_smaller: LEMMA subgraph?(SS, G) IMPLIES
                         size(SS) <= size(G)

END subgraphs