min_array[N: posnat, T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
%  min (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the minimum function over an array of values
%  from an ordered type. This is done in an implementation-independent
%  manner. 
%
%      Imin(A,ii,jj)     = general definition of minimum of array A 
%                          over the internal from ii to jj.  Returns the
%                          index into the array.
%
%      imin(A)           = general definition of minimum of array A. 
%                          Returns the index into the array.
%
%      min(A)            = general definition of minimum of array A. 
%                          Returns the minimal element.
%
%  Notes:
%     1. The properties of imin and min are readily obtained via 
%        TYPEPRED "min" and TYPEPRED "imin" or through use of
%        min_lem and imin_lem.
%     2. Since there may be replicates in A, the return type of imin
%        may not be a singleton set.
%
%------------------------------------------------------------------------

  EXPORTING ALL WITH below_arrays[N,T]

BEGIN

  IMPORTING min_array_def[N,T,<=], below_arrays[N,T]

  A: VAR ARRAY[below(N) -> T] 
  x: VAR T
  ii,jj: VAR below(N)

  imin(A): {i: below(N)| (FORALL ii: A(i) <= A(ii))}

  min(A): { t: T | (FORALL ii: t <= A(ii)) AND
                    (EXISTS jj: A(jj) = t)} 

% LEMMAs that follow immediately from TYPEPRED "imin" and TYPEPRED "min"

  min_lem   : LEMMA min(A) <= A(ii)

  min_in?   : LEMMA in?(min(A),A)

  min_def   : LEMMA (FORALL ii: min(A) <= A(ii)) AND in?(min(A),A)

  min_it_is : LEMMA (FORALL ii: x <= A(ii)) AND in?(x,A) IMPLIES
                        min(A) = x

  imin_lem  : LEMMA A(imin(A)) = min(A)

  imin_1    : LEMMA N = 1 IMPLIES imin(A) = 0

  min_2     : LEMMA N = 2 IMPLIES min(A) = IF A(0) <= A(1) THEN A(0)
                                           ELSE A(1) ENDIF

END min_array