%-----------------------------------------------------------------------------
% Last and nth elements of a sequence of countable length, as well as the
% valid indexes.
%
% Author: Jerry James <loganjerry@gmail.com>
%
% 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
