Quelle  csequence_length.pvs

%-----------------------------------------------------------------------------
% Length of a finite sequence, part of the theory of sequences of countable
% length defined as coalgebraic datatypes.
%
% 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_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