|
fseqs_ops [T: TYPE+]: THEORY
%------------------------------------------------------------------------
%
% Defines some convenient operations over finite sequences
%
% EXPERIMENTAL
%
%------------------------------------------------------------------------
BEGIN
IMPORTING fseqs[T]
fs: VAR fseq
nefs: VAR ne_fseq
i,n: VAR nat
x: VAR T
first(fs): T = fs`seq(0)
rest(fs): fseq = fs^(1,l(fs))
delete(n, nefs): fseq = IF n < l(nefs) THEN
(# length := l(nefs) - 1,
seq := (LAMBDA i: (IF i < n THEN nefs(i)
ELSE nefs(i + 1) ENDIF))
#)
ELSE nefs
ENDIF
insert(x, n, fs): fseq = IF n <= l(fs) THEN
(# length := l(fs) + 1,
seq := (LAMBDA i: IF i < n THEN fs(i)
ELSIF i = n THEN x
ELSE fs(i - 1) ENDIF)
#)
ELSE
fs
ENDIF
add(x, fs): fseq = insert(x, 0, fs)
addend(x:T,fs:fseq): fseq = (# length := l(fs) + 1,
seq := (LAMBDA (ii: nat):
IF ii < l(fs) THEN seq(fs)(ii)
ELSIF ii < l(fs) + 1 THEN x
ELSE default ENDIF)
#)
insert_delete: LEMMA n < l(nefs) IMPLIES
insert(nefs`seq(n), n, delete(n, nefs)) = nefs
add_first_rest: LEMMA add(first(nefs), rest(nefs)) = nefs
p: VAR pred[T]
every(p)(fs): bool = (FORALL n: n < l(fs) IMPLIES p(fs(n)))
every(p, fs): bool = (FORALL n: n < l(fs) IMPLIES p(fs(n)))
some(p)(fs): bool = (EXISTS n: n < l(fs) IMPLIES p(fs(n)))
some(p, fs): bool = (EXISTS n: n < l(fs) IMPLIES p(fs(n)))
% This definition looks a little strange. The following lemma can be easily proved.
some_p_trivial: LEMMA some(p,fs)
F: VAR [T -> T]
map(F,fs): fseq = (# length := length(fs),
seq := (LAMBDA i: IF i < length(fs) THEN
F(fs`seq(i))
ELSE
default
ENDIF)
#)
END fseqs_ops
¤ Dauer der Verarbeitung: 0.22 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.
|
