|
min_fseq[T: TYPE+, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
% min_fseq (basic definitions and properties)
% -------------------------------------------
%
% Author: Ricky W. Butler
%
% This theory defines the minimum function over a sequence of values
% from an ordered type. This is done in an implementation-independent
% manner.
%
% Imin(s,ii,jj) = general definition of minimum of sequence s
% over the internal from ii to jj. Returns the
% index into the sequence.
%
% imin(s) = general definition of minimum of sequence s.
% Returns the index into the sequence.
%
% min(s) = general definition of minimum of sequence s.
% 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_seq_lem and imin_seq_lem.
% 2. Since there may be replicates in s, the return type of imin
% may not be a singleton set.
%------------------------------------------------------------------------
EXPORTING ALL WITH fseqs[T], fsq[T]
BEGIN
IMPORTING fseqs[T]
ii,j: VAR nat
s: VAR ne_fseq
x: VAR T
IMPORTING min_array_def
dom(s): TYPE = below(length(s))
abv(ii,s): TYPE = {i: nat | ii <= i AND i < length(s)}
Imin(s, (ii: dom(s)),(jj: abv(ii,s))):
{i: subrange(ii,jj) | (FORALL j: ii <= j AND j <= jj
IMPLIES seq(s)(i) <= seq(s)(j))}
Imin_seq_1: LEMMA (FORALL (s: ne_fseq,ii: dom(s)): Imin(s,ii,ii) = ii)
imin(s): {i: dom(s)| (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}
min(s): { t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}
% LEMMAs that follow immediately from TYPEPRED "imin" and TYPEPRED "min"
min_seq_lem : LEMMA (FORALL (ii: dom(s)): min(s) <= seq(s)(ii))
min_seq_in? : LEMMA in?(min(s),s)
min_seq_def : LEMMA FORALL (ii: dom(s)): min(s) <= seq(s)(ii)
AND in?(min(s),s)
min_seq_it_is : LEMMA (FORALL (ii: dom(s)): x <= seq(s)(ii)) AND in?(x,s)
IMPLIES min(s) = x
imin_seq_lem : LEMMA seq(s)(imin(s)) = min(s)
imin_seq_1 : LEMMA length(s) = 1 IMPLIES imin(s) = 0
min_seq_2 : LEMMA length(s) = 2 IMPLIES min(s) =
IF seq(s)(0) <= seq(s)(1) THEN seq(s)(0)
ELSE seq(s)(1) ENDIF
END min_fseq
¤ Dauer der Verarbeitung: 0.27 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
