max_seq[T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
%  max_seq (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the maximum function over a sequence of values
%  from an ordered type. This is done in an implementation-independent
%  manner. 
%
%      Imax(s,ii,jj)     = general definition of maximum of sequence s 
%                          over the internal from ii to jj.  Returns the
%                          index into the sequence.
%
%      imax(s)           = general definition of maximum of sequence s. 
%                          Returns the index into the sequence.
%
%      max(s)            = general definition of maximum of sequence s. 
%                          Returns the maximal element.
%
%  Notes:
%     1. The properties of imax and max are readily obtained via 
%        TYPEPRED "max" and TYPEPRED "imax" or through use of
%        max_seq_lem and imax_seq_lem.
%     2. Since there may be replicates in s, the return type of imax
%        may not be a singleton set.
%
%------------------------------------------------------------------------

  EXPORTING ALL WITH seqs[T]

BEGIN

  IMPORTING seqs[T]

%  seqs: TYPE = {s: finite_sequence[T]  | length(s) > 0}
%  in?(x,s): bool = (EXISTS (ii: dom(s)): x = seq(s)(ii))

  s: VAR ne_seqs
  j,ii: VAR nat
  x: VAR T

  IMPORTING max_array_def

  dom(s): TYPE = below(length(s))
  abv(ii,s): TYPE = {i: nat | ii <= i AND i < length(s)}

  Imax(s, (ii: dom(s)),(jj: abv(ii,s))): 
       {i: subrange(ii,jj) | (FORALL j: ii <= j AND j <= jj 
                                     IMPLIES seq(s)(j) <= seq(s)(i))}

  Imax_1: LEMMA (FORALL (s: ne_seqs,ii: dom(s)): Imax(s,ii,ii) = ii)

  imax(s): {i: dom(s)| (FORALL (ii: dom(s)): seq(s)(ii) <= seq(s)(i))}

  max(s): { t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
                    (EXISTS (jj: dom(s)): seq(s)(jj) = t)} 

% LEMMAs that follow immediately from TYPEPRED "imax" and TYPEPRED "max"

  max_seq_lem   : LEMMA (FORALL (ii: dom(s)): seq(s)(ii)<= max(s))

  max_seq_in?   : LEMMA in?(max(s),s)

  imax_seq_lem  : LEMMA seq(s)(imax(s)) = max(s)


  max_seq_def   : LEMMA FORALL (ii: dom(s)): seq(s)(ii) <= max(s) 
                        AND in?(max(s),s)

  max_seq_it_is : LEMMA (FORALL (ii: dom(s)): seq(s)(ii) <= x) AND in?(x,s)
                        IMPLIES max(s) = x


  imax_seq_1    : LEMMA length(s) = 1 IMPLIES imax(s) = 0

  max_seq_2     : LEMMA length(s) = 2 IMPLIES max(s) = 
                          IF seq(s)(0) <= seq(s)(1) THEN seq(s)(1)
                          ELSE seq(s)(0) ENDIF


END max_seq