%-----------------------------------------------------------------------------
% Last and nth elements of a sequence of countable length, as well as the
% valid indexes.
%
% Author: Jerry James <[email protected]>
%
% This file and its accompanying proof file are distributed under the CC0 1.0
% Universal license: http://creativecommons.org/publicdomain/zero/1.0/.
%
% Version history:
% 2007 Feb 14: PVS 4.0 version
% 2011 May 6: PVS 5.0 version
% 2013 Jan 14: PVS 6.0 version
%-----------------------------------------------------------------------------
csequence_nth[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_length[T]
n: VAR nat
p: VAR pred[T]
cseq, cseq1, cseq2: VAR csequence
fseq: VAR finite_csequence
nseq: VAR nonempty_csequence
nfseq: VAR nonempty_finite_csequence
iseq: VAR infinite_csequence
% The valid indexes of a csequence.
index?(cseq)(n): RECURSIVE bool =
nonempty?(cseq) AND (n = 0 OR index?(rest(cseq))(n - 1))
MEASURE n
indexes(cseq): TYPE = (index?(cseq))
index?_0: THEOREM FORALL cseq: nonempty?(cseq) IFF index?(cseq)(0)
index?_ub: THEOREM FORALL cseq, n: index?(cseq)(n) OR is_finite(cseq)
index?_lt: THEOREM
FORALL cseq, (i: indexes(cseq)), n: n < i IMPLIES index?(cseq)(n)
index?_finite: THEOREM FORALL fseq, n: index?(fseq)(n) IFF n < length(fseq)
index?_finite_bound: THEOREM FORALL fseq: EXISTS n: NOT index?(fseq)(n)
index?_infinite: THEOREM FORALL iseq, n: index?(iseq)(n)
index?_infinite_full: THEOREM
FORALL cseq: is_infinite(cseq) IFF full?(index?(cseq))
index?_prop: THEOREM
FORALL cseq, n:
index?(cseq)(n) IFF (is_finite(cseq) IMPLIES n < length(cseq))
index?_nonempty: THEOREM FORALL cseq, (n: indexes(cseq)): nonempty?(cseq)
% The nth element of a sequence
nth(cseq, (n: indexes(cseq))): RECURSIVE T =
IF n = 0 THEN first(cseq) ELSE nth(rest(cseq), n - 1) ENDIF
MEASURE n
nth_extensionality: THEOREM
FORALL cseq1, cseq2:
index?(cseq1) = index?(cseq2) AND
(FORALL (n: indexes(cseq1)): nth(cseq1, n) = nth(cseq2, n))
IMPLIES cseq1 = cseq2
nth_every: THEOREM
FORALL cseq, p:
every(p)(cseq) IFF (FORALL (i: indexes(cseq)): p(nth(cseq, i)))
nth_some: THEOREM
FORALL cseq, p:
some(p)(cseq) IFF (EXISTS (i: indexes(cseq)): p(nth(cseq, i)))
% The last element of a sequence
last(nfseq): T = nth(nfseq, length(nfseq) - 1)
last_rest: THEOREM
FORALL nfseq: empty?(rest(nfseq)) OR last(rest(nfseq)) = last(nfseq)
END csequence_nth
¤ Dauer der Verarbeitung: 0.16 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.
|
