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

wgt_digraphs_props[T : TYPE, Weight : TYPE, 
                   + : {f : [[Weight, Weight] -> Weight] | 
                           commutative?(f) AND associative?(f) },
                   0 : {zero: Weight | identity?(+)(zero)},
                  <= : {<=: (partial_order?[Weight]) | FORALL(a, b, c : Weight):
                                                     a + b <= a + c => b <= c}
                   ] : THEORY

BEGIN

 IMPORTING weighted_digraphs[T, Weight, +, 0]


        G : VAR wdg
     u, v : VAR T


% ----------------------------------------------------------------------------- %
%            DEFINITIONS: about minimun weights
% ----------------------------------------------------------------------------- % 

 min_walk?(G, u, v)( w: Walk(dg(G))) : bool =
   FORALL(w1: Walk(dg(G)) | from?(w1, u, v)):
     wgt_walk(G, w) <= wgt_walk(G, w1)

 set_min(G)(u, v): set[Walk(dg(G))] =
   {w: Walk(dg(G)) | from?(w, u, v) AND min_walk?(G, u, v)(w)}

 min_wgt(G)(e: edgetype | nonempty?(set_min(G)(e))): Weight =
    wgt_walk(G, choose(set_min(G)(e)))


% ----------------------------------------------------------------------------- %
%           More properties on weighted digraphs that require 
%           a partial order, commutativity and homogeneity
% ----------------------------------------------------------------------------- %

 walk_member_set_min: LEMMA
   FORALL (w: Walk(dg(G)), e: edgetype | nonempty?(set_min(G)(e))):
          from?(w, e`1, e`2) AND wgt_walk(G, w) = min_wgt(G)(e)
          IMPLIES member(w, set_min(G)(e))

 wgt_min_walk_choose: LEMMA
   FORALL (w: Walk(dg(G))):
       member(w, set_min(G)(u, v)) IMPLIES
       wgt_walk(G, w) = wgt_walk(G, choose(set_min(G)(u, v)))

 min_walk_min_wgt: LEMMA
   FORALL (w: Walk(dg(G))):
       member(w, set_min(G)(u, v)) IMPLIES
       wgt_walk(G, w) = min_wgt(G)(u, v)

 sub_min_walk_nonempty: LEMMA
   FORALL(w: Walk(dg(G)), 
          e: edgetype | nonempty?(set_min(G)(e)), 
          i, j: below(length(w))):
       walk_from?(dg(G), w, e`1, e`2) AND wgt_walk(G, w) = min_wgt(G)(e) AND i < j
     IMPLIES
       nonempty?( set_min(G)( w(i), w(j) ) )

 sub_min_walk_is_min: LEMMA
   FORALL(w: Walk(dg(G)), 
          e: edgetype | nonempty?(set_min(G)(e)), 
          i, j: below(length(w)) ):
      walk_from?(dg(G), w, e`1, e`2) AND wgt_walk(G, w) = min_wgt(G)(e) AND i < j
     IMPLIES
      wgt_walk(G, w^(i,j)) = min_wgt(G)(w(i), w(j))

END wgt_digraphs_props