csequence_nth.pvs Interaktion und
Portierbarkeitunbekannt

%-----------------------------------------------------------------------------
% 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

quality91%

csequence_nth.pvs Interaktion und Portierbarkeitunbekannt

[ Konzepte0.4Was zu einem Entwurf gehört Wie die Entwicklung von Software durchgeführt wird ]

csequence_nth.pvs Interaktion und
Portierbarkeitunbekannt