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