Quelle  max_array_def.pvs   Sprache: PVS

%------------------------------------------------------------------------
%
%  max_array_def: foundation for max_array
%  ---------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory provides a constructive definition of max (named Imax) to
%  provide a means to discharge the TCC produced in max_array.  This 
%  theory is not intended to be directly used.
%
%------------------------------------------------------------------------
max_array_def[N: nat, T: TYPE, <= : (total_order?[T]) ]: THEORY

BEGIN

  A,A1,A2: VAR ARRAY[below(N) -> T] 
  t, t1, t2: VAR T
  ii,jj,j: VAR below(N)
 
  amax(A,ii,jj): below(N) = IF A(ii) <= A(jj) THEN jj ELSE ii ENDIF

  imax_rec(A,ii,jj): RECURSIVE below(N) = 
        IF jj <= ii THEN ii
        ELSE amax(A,jj,imax_rec(A,ii,jj-1)) 
        ENDIF MEASURE (LAMBDA A,ii,jj: jj)

  imax_rec_lem: LEMMA  ii <= j AND j <= jj IMPLIES 
                             A(j) <= A(imax_rec(A,ii,jj))

  imax_rec_rng: LEMMA  ii <= jj IMPLIES ii <= imax_rec(A,ii,jj) AND
                                         imax_rec(A,ii,jj) <= jj

  abv(ii): TYPE = {i: nat | ii <= i AND i < N}

  Imax_rec(A,ii,(jj: abv(ii))): subrange(ii,jj) = 
                  imax_rec(A,ii,jj)       

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

  Imax_1:   LEMMA Imax(A,ii,ii) = ii

END max_array_def