%-----------------------------------------------------------------------------
% The reverse of a finite sequence.
%
% 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_reverse[T:
TYPE]:
THEORY
BEGIN
IMPORTING csequence_append[T]
t:
VAR T
p:
VAR pred[T]
n:
VAR nat
fseq, fseq1, fseq2:
VAR finite_csequence
nfseq:
VAR nonempty_finite_csequence
reverse(fseq):
RECURSIVE finite_csequence =
IF empty?(fseq)
THEN fseq
ELSE append(first(fseq), reverse(rest(fseq)))
ENDIF
MEASURE length(fseq)
reverse_empty:
THEOREM FORALL fseq: empty?(reverse(fseq))
IFF empty?(fseq)
reverse_nonempty:
THEOREM
FORALL fseq:
nonempty?(reverse(fseq))
IFF nonempty?(fseq)
reverse_first:
THEOREM FORALL nfseq: first(reverse(nfseq)) = last(nfseq)
reverse_last:
THEOREM FORALL nfseq: last(reverse(nfseq)) = first(nfseq)
reverse_length:
THEOREM FORALL fseq: length(reverse(fseq)) = length(fseq)
reverse_index:
THEOREM FORALL fseq: index?(reverse(fseq)) = index?(fseq)
reverse_nth:
THEOREM
FORALL fseq, (n: indexes(reverse(fseq))):
nth(reverse(fseq), n) = nth(fseq, length(fseq) - n - 1)
reverse_add1:
THEOREM
FORALL fseq, t: add(t, reverse(fseq)) = reverse(append(t, fseq))
reverse_add2:
THEOREM
FORALL fseq, t: reverse(add(t, fseq)) = append(t, reverse(fseq))
reverse_reverse:
THEOREM FORALL fseq: reverse(reverse(fseq)) = fseq
reverse_extensionality:
THEOREM
FORALL fseq1, fseq2:
reverse(fseq1) = reverse(fseq2)
IMPLIES fseq1 = fseq2
reverse_some:
THEOREM
FORALL fseq, p: some(p)(reverse(fseq))
IFF some(p)(fseq)
reverse_every:
THEOREM
FORALL fseq, p: every(p)(reverse(fseq))
IFF every(p)(fseq)
END csequence_reverse
