|
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
¤ Dauer der Verarbeitung: 0.3 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.
|
