Quelle  Eulerian.pvs

%********************************************************************************%
%
%   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
%
%********************************************************************************%

Eulerian[T:TYPE] : THEORY
BEGIN
  
  IMPORTING cycles[T],
            walk_inductions[T]


  G : VAR digraph
  w : VAR prewalk


  %%% For walks it means that we don't have repeated edges
  no_repeat_subseq?(w) : bool =
    FORALL (i,j:below(length(w) - 1)) :
      i < j AND w`seq(i) = w`seq(j) IMPLIES w`seq(i+1) /= w`seq(j+1)

  pre_Eulerian_walk?(G,w) : bool =
    walk?(G,w) AND no_repeat_subseq?(w)

  Eulerian_walk?(G,w) : bool =
    pre_Eulerian_walk?(G,w) AND
    edges_of(w) = edges(G)

  pre_Eulerian_circuit?(G,w) : bool =
    pre_Eulerian_walk?(G,w) AND circuit?(G, w)
    % w(0) = w(length(w)-1) AND
    % length(w) > 1

  Eulerian_circuit?(G,w) : bool =
    pre_Eulerian_circuit?(G,w) AND 
    edges_of(w) = edges(G)


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

  cycle_is_pre_Eulerian_circuit: LEMMA
    cycle?(G, w) IMPLIES pre_Eulerian_circuit?(G,w)

  pre_Eulerian_circuit_is_a_circuit: LEMMA
    pre_Eulerian_circuit?(G,w) IMPLIES
    circuit?(G,w)

  Eulerian_circuit_is_circuit: LEMMA
    Eulerian_circuit?(G,w) IMPLIES
    circuit?(G,w)

  Eulerian_walk_is_Eulerian_circuit: LEMMA
    Eulerian_circuit?(G,w) IMPLIES
    Eulerian_walk?(G,w)

  circuit_subwalk_pre_Eulerian: LEMMA
    circuit?(G, w) IMPLIES
    EXISTS (w1: prewalk): sub_walk?(G, w, w1) AND
      pre_Eulerian_circuit?(G,w1)

  pre_Eulerian_circuit_prefix: LEMMA
    circuit?(G,w) IMPLIES (pre_Eulerian_circuit?(G,w) OR
    EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o w2) AND
         pre_Eulerian_circuit?(G,w1))

  pre_Eulerian_circuit_o_circuit: LEMMA
    circuit?(G,w) IMPLIES (pre_Eulerian_circuit?(G,w) OR
    EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o rest(w2)) AND
         pre_Eulerian_circuit?(G,w1) AND circuit?(G,w2))


END Eulerian