sep_sets[T: TYPE]: THEORY


BEGIN

   IMPORTING graphs[T], walks[T]

   G: VAR graph[T]
   v,s,t: VAR T
   e: VAR doubleton[T]
   V: VAR finite_set[T]

   del_verts(G,V): graph[T] =
           (# vert := difference[T](vert(G),V),                    
              edges := {e | edges(G)(e) AND 
                           (FORALL v: V(v) IMPLIES NOT e(v))} #)

   separates(G,V,s,t): bool = NOT V(s) AND NOT V(t) AND 
                   NOT (EXISTS (w: prewalk): walk_from?(del_verts(G,V),w,s,t))

   seps(G,s,t): TYPE = {V: finite_set[T] | IF s = t OR edge?(G)(s,t) THEN 
                                              V = vert(G) 
                                           ELSE separates(G,V,s,t)
                                           ENDIF}

   IMPORTING abstract_min

   sep_set_exists: LEMMA (EXISTS (t: seps(G, s, t)): TRUE)
          
   min_sep_set(G,s,t): finite_set[T] = min[seps(G,s,t),
                                  (LAMBDA (v: seps(G,s,t)): card(v)),
                                  (LAMBDA (v: seps(G,s,t)): true)]

   separable?(G,s,t): bool = (s /= t AND NOT edge?(G)(s,t)) 


   min_sep_set_edge: LEMMA NOT separable?(G,s,t) IMPLIES 
                                  min_sep_set(G,s,t) = vert(G)

   min_sep_set_card: LEMMA FORALL (s,t: (vert(G))): separates(G,V,s,t)
                                  IMPLIES card(min_sep_set(G,s,t)) <= card(V)  

   min_sep_set_seps: LEMMA separable?(G,s,t) IMPLIES 
                               separates(G,min_sep_set(G,s,t),s,t)

   min_sep_set_vert: LEMMA separable?(G,s,t) AND min_sep_set(G,s,t)(v) 
                                    IMPLIES vert(G)(v)

   ends_not_in_min_sep_set: LEMMA separable?(G,s,t)  AND min_sep_set(G, s, t)(v) 
                                  IMPLIES v /= s AND v /= t


   w: VAR prewalk
   walk?_del_verts_not : LEMMA walk?(G, w) AND 
                                  empty?(intersection(verts_of(w),V))
                                      IMPLIES walk?(del_verts(G, V), w)

   sep_num(G,s,t): nat = card(min_sep_set(G,s,t))

   IMPORTING graph_deg[T], finite_sets@finite_sets_card_eq


   adj_verts(G,s): finite_set[T] = {v: T | (EXISTS (e: Dbl[T]):
                                         incident_edges[T](s, G)(e)
                                           AND e(v) AND NOT v = s)}

   adj_verts_lem: LEMMA card(adj_verts(G,s)) = deg(s,G)

   sep_num_min: LEMMA FORALL (s,t: (vert(G))):
                      separable?(G,s,t) IMPLIES
                       sep_num(G,s,t) <= min(deg(s,G),deg(t,G))

END sep_sets