Quelle  cycle_deg.pvs

cycle_deg[T: TYPE]: THEORY

BEGIN

   IMPORTING cycles[T], trees[T], graph_conn_defs[T], graph_connected[T],
             graph_deg_sum[T], tree_circ[T], graph_complected[T],
             tree_paths[T], subgraph_paths[T]

   G,H: VAR graph[T]
   n: VAR nat
   x,y,s,t: VAR T 
   w,p,q: VAR prewalk

   reachable(G: graph[T],x:T): finite_set[T] = 
                      {y: T |  vert(G)(y) AND 
                            (EXISTS (w: Seq(G)): walk_from?(G,w,x,y))}

   reachable_subset: LEMMA subset?(reachable(G,x),vert(G))

   reachable_conn: LEMMA FORALL (x:(vert(G))):
  connected?(subgraph(G,reachable(G,x)))


    conn_compon: LEMMA FORALL (G: graph[T], x: (vert(G))): EXISTS H:
                      (subgraph?(H,G) AND 
                 connected?(H) and vert(H)(x) and 
                   FORALL (y:(vert(H))): (deg(y,G)=deg(y,H)))  



    sub_cycle: LEMMA FORALL (G,H: graph[T], w: Seq(H)): subgraph?(H,G) 
                                and cycle?(H,w) IMPLIES cycle?(G,w)


    uniq_paths?(G):bool = FORALL (s,t,p,q): path_from?(G,p,s,t) AND
                               path_from?(G,q,s,t) IMPLIES   p=q

    uniq_del_vert: LEMMA FORALL (G:graph[T], v:(vert(G))): uniq_paths?(G) 
                              IMPLIES uniq_paths?(del_vert(G,v))

    del_edge_uniq: LEMMA FORALL (G:graph[T], e:(edges(G))): 
                        connected?(del_edge(G,e)) IMPLIES NOT uniq_paths?(G) 

    charact_tree: LEMMA connected?(G) AND uniq_paths?(G) IMPLIES tree?(G)


    exclus_cycl: THEOREM connected?(G) IMPLIES 
                         tree?(G) XOR (EXISTS (w:Seq(G)): cycle?(G,w))

    num_edge_tree: LEMMA connected?(G) and num_edges(G)<size(G) 
 IMPLIES tree?(G)
 

    iff_tree: LEMMA tree?(G) IFF connected?(G) AND uniq_paths?(G)
  
    tree_num_iff: LEMMA connected?(G) and num_edges(G)=size(G)-1 IFF tree?(G)


    deg_gt_1_cycle: LEMMA  (FORALL (v: T): vert(G)(v) IMPLIES deg(v,G) > 1)
                            IMPLIES (EXISTS (w: Seq(G)): cycle?(G,w)) OR 
                          empty?(G)
                                        

END cycle_deg