Quelle  trees.pvs

trees[T: TYPE]: THEORY
BEGIN

   IMPORTING graph_deg[T], graph_ops[T], subgraphs[T], graph_inductions[T]

   G,GP,C,GG: VAR graph[T]
   u,v: VAR T
   k,n,m: VAR nat

   tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
                         (EXISTS (v: (vert(G))): deg(v,G) = 1 AND 
                                  tree?(del_vert[T](G,v)))
             MEASURE size(G)
                             
   tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G)

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


   tree_edge_card: LEMMA tree?(G) IMPLIES 
             size(G)= card[doubleton[T]](edges(G))+1

   tree_edge_k: LEMMA (FORALL G,v,k: tree?(G) AND size(G) = k+2 AND vert(G)(v)
                IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1) IMPLIES 
                            (FORALL G,v: tree?(G) AND vert(G)(v) 
                              IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1)

   tree_edge: LEMMA (FORALL G,v,k: tree?(G) AND size(G) = k+2 AND vert(G)(v)
                  IMPLIES deg(v,G)>0 OR card[T](vert(G)) = 1)

   tree_edge_all: LEMMA tree?(G) AND vert(G)(v) IMPLIES deg(v,G)>0 OR 
                   card[T](vert(G)) = 1 

   del_tree_k: LEMMA ( FORALL G,v,k: tree?(G) and size(G) = k+1 AND 
                       vert(G)(v) AND deg(v,G)=1 
                      IMPLIES tree?(del_vert(G,v))) 
                          IMPLIES (FORALL G,v: tree?(G) AND 
                                               vert(G)(v) AND 
                                               deg(v,G)=1 
                                       IMPLIES tree?(del_vert(G,v)))

  del_tree: LEMMA ( FORALL G,v,k: tree?(G) AND size(G) = k+1 AND 
                                  vert(G)(v) AND deg(v,G)=1 
                           IMPLIES tree?(del_vert(G,v)))


  del_tree_all: LEMMA tree?(G) AND vert(G)(v) AND deg(v,G)=1 IMPLIES
                      tree?(del_vert(G,v))



END trees