%-----------------------------------------------------------------------------
% Length of a finite sequence, part of the theory of sequences of countable
% length defined as coalgebraic datatypes.
%
% 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_length[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_props[T]
n: VAR nat
cseq, cseq1, cseq2: VAR csequence
fseq: VAR finite_csequence
nfseq: VAR nonempty_finite_csequence
length(fseq): RECURSIVE {n | has_length(fseq, n)} =
IF empty?(fseq) THEN 0 ELSE 1 + length(rest(fseq)) ENDIF
MEASURE choose({n | has_length(fseq, n)})
length_def: THEOREM
FORALL fseq, n: length(fseq) = n IFF has_length(fseq, n)
length_empty?_rew: THEOREM
FORALL cseq: empty?(cseq) IFF is_finite(cseq) AND length(cseq) = 0
length_nonempty?_rew: COROLLARY
FORALL cseq: nonempty?(cseq) IFF is_infinite(cseq) OR length(cseq) > 0
length_rest: THEOREM FORALL nfseq: length(rest(nfseq)) = length(nfseq) - 1
END csequence_length
¤ Dauer der Verarbeitung: 0.19 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.
|
