feedback image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: csequence_reverse.pvs   Sprache: PVS

%-----------------------------------------------------------------------------
% 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.11 Sekunden  (vorverarbeitet)  ]