Quelle  tree_paths.pvs

tree_paths[T: TYPE]: THEORY
BEGIN

   IMPORTING tree_circ[T], paths[T], path_circ[T], circuits[T], cycles[T]

   u,v: VAR T
 
   m,n: VAR nat
   G: VAR graph[T]
   p,q: VAR prewalk

   dual_paths?(G,(p:Path(G)),(q:Path(G))):bool = p /= q AND p(0)=q(0)
    AND p(length(p)-1)=q(length(q)-1)

   Dual_paths(G):TYPE = {((p:Path(G)),(q:Path(G))) | dual_paths?(G,p,q)}

   IMPORTING abstract_min


   min_dual_paths(G: Graph[T], r: Path(G), s: Path(G) | dual_paths?(G,r,s)): 
            Dual_paths(G) = min[[Path(G),Path(G)],
   (LAMBDA (r:Path(G),s:Path(G)): length(r)+length(s)),
   (LAMBDA (r:Path(G),s:Path(G)): dual_paths?(G,r,s))]


   is_min_dual?(G,(p:Path(G)),(q:Path(G))):bool = dual_paths?(G,p,q) 
                      AND FORALL (r:Path(G),s:Path(G)): dual_paths?(G,r,s) 
                            IMPLIES  length(r) + length(s) >= length(p)+length(q)

   min_dual_def: LEMMA FORALL (G: Graph[T], r: Path(G), s: Path(G)):
                          dual_paths?(G,r,s) IMPLIES
                          is_min_dual?(G,proj_1(min_dual_paths(G,r,s)),
                                         proj_2(min_dual_paths(G,r,s))) 
                      AND  
                          dual_paths?(G,proj_1(min_dual_paths(G,r,s)),
                                        proj_2(min_dual_paths(G,r,s)))


   min_dual_exists: LEMMA FORALL (G: Graph[T], r: Path(G), s: Path(G)):
         dual_paths?(G,r,s) IMPLIES EXISTS (p,q:Path(G)): is_min_dual?(G,p,q)

   dual_path_trunc: LEMMA  FORALL (G: Graph[T], p: Path(G), q: Path(G)): 
     dual_paths?(G,p,q) IMPLIES 
         length(p)>1 AND length(q)>1 AND path?[T](G, p ^ (0, length(p) - 2)) 
         AND path?[T](G, q ^ (0, length(q) - 2)) 
         AND path?[T](G, p ^ (1, length(p) - 1)) AND path?[T](G, q ^ (1, length(q) - 1))

   dual_path_length: LEMMA FORALL (G: Graph[T], p: Path(G), q: Path(G)): 
         dual_paths?(G,p,q) IMPLIES length(p)>2 OR length(q)>2

   min_dual_reduc: LEMMA  FORALL (G: Graph[T], p: Path(G), q: Path(G)): 
         is_min_dual?(G,p,q) IMPLIES p(1) /= q(1) AND p(length(p)-2) /= q(length(q)-2)


   min_dual_distin: LEMMA  FORALL (G: Graph[T], p: Path(G), q: Path(G)): 
              is_min_dual?(G,p,q) IMPLIES 
                         (FORALL (i,j:nat):i<length(p)-1 AND j<length(q)-1 AND p(i)=q(j) 
                                      IMPLIES (i=0 AND j=0))

   dual_cycle: LEMMA  FORALL (G: Graph[T], p: Path(G), q: Path(G)): 
                  dual_paths?(G,p,q) AND 
                  (FORALL (i,j:nat):i<length(p)-1 AND j<length(q)-1 AND p(i)=q(j) 
                                       IMPLIES (i=0 AND j=0)) 
                      IMPLIES cycle?(G,trunc1(p) o rev(q)) 

                                    
   tree_one_path: LEMMA  tree?(G) AND
                               path_from?(G,p,u,v) AND
                               path_from?(G,q,u,v) IMPLIES
                                    p=q


END tree_paths