%-----------------------------------------------------------------------------
% The reverse of a finite sequence.
%
% 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_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
¤ Dauer der Verarbeitung: 0.0 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.
|
