%********************************************************************************%
%
%   Contributions from:
%
%       Andréia Borges Avelar -- Universidade de Brasília - Brasil  
%       Mauricio Ayala-Rincon -- Universidade de Brasília - Brasil  
%                 Cesar Muñoz -- NASA Langley Research Center - US
%
%********************************************************************************%

% A cycle is a simple circuit; i.e., a walk without repetions except for the end points

cycles[T: TYPE]: THEORY

BEGIN

   IMPORTING circuits[T]

   G: VAR digraph[T]
   w: VAR prewalk


% --------------------------------------------------------------------------------
%     Definitions
% --------------------------------------------------------------------------------

  cycle?(G: digraph[T], w: prewalk): bool = 
       circuit?(G,w) AND 
       (FORALL (i,j: below(length(w)-1)): i /= j IMPLIES w(i) /= w(j))


% --------------------------------------------------------------------------------
%     Properties
% --------------------------------------------------------------------------------

  cycle_is_circuit : LEMMA
     FORALL (G: digraph[T], w: prewalk) : cycle?(G,w) IMPLIES circuit?(G,w)

  % cycle_has_path: LEMMA FORALL (w: prewalk): cycle?(G,w) IMPLIES
  %                        (EXISTS (j: below(length(w))): path?(G,w^(0,j)))

  circuit_subwalk_cycle: LEMMA
    circuit?(G, w) IMPLIES
    EXISTS (w1: prewalk): sub_walk?(G, w, w1) AND cycle?(G,w1)

  cycle_prefix: LEMMA
    circuit?(G,w) IMPLIES 
    (cycle?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o w2) 
    AND cycle?(G,w1))
   
  cycle_o_circuit: LEMMA
    circuit?(G,w) IMPLIES 
    (cycle?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o rest(w2))
    AND cycle?(G,w1) AND circuit?(G,w2))


%--------------------------------------------------------------------------------

   IMPORTING digraphs, finite_sets@finite_sets_card_eq, structures@seq_pigeon

   GF: VAR Digraph[T]

   Pigeon_hole: THEOREM FORALL (w: Walk(GF)): length(w) > card(vert(GF)) IMPLIES 
                  (EXISTS (i,j: below(length(w))): i /= j AND w(i) = w(j))
   

END cycles