Quelle  trees.pvs

%trees, defined for directed graphs 
%
%  Authors:
%
%      Ricky W. Butler      NASA Langley Research Center
%      Kristin Y. Rozier    NASA Langley Research Center
%
%  Last updated: 7/28/2004

trees[T: TYPE]: THEORY
BEGIN

   IMPORTING digraph_deg[T], digraph_ops[T], di_subgraphs[T]

   G,GP,C,GG: VAR digraph[T]
   v: VAR T

   leaf?(v,G): MACRO bool = in_deg(v,G) = 1 AND out_deg(v,G) = 0

   leaf?(G)(v): bool = leaf?(v,G)

   root?(v,G): MACRO bool = in_deg(v,G) = 0 AND out_deg(v,G) > 0

   root?(G)(v): bool = root?(v,G)


%   tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
%                  (EXISTS (v: (vert(G))): root?(G)(v)
%                                         AND tree?(del_vert[T](G,v)))
%                MEASURE size(G)


   tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
                  (EXISTS (v: (vert(G))): leaf?(G)(v)
                                          AND tree?(del_vert[T](G,v)))
             MEASURE size(G)

                    
   tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G)

   Tree: TYPE = {G: digraph[T] | tree?(G)}



END trees