Quelle csequence_remove.pvs Sprache: PVS

%-----------------------------------------------------------------------------
% Remove an element from a sequence of countable length.
%
% 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_remove[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence_nth[T]

  t: VAR T
  p: VAR pred[T]
  index, n, m: VAR nat
  cseq, cseq1, cseq2: VAR csequence
  nseq: VAR nonempty_csequence
  fseq: VAR finite_csequence
  iseq: VAR infinite_csequence

  % Remove the element at position index in cseq.  If index >= length(cseq),
  % then we give back the original sequence.
  remove(cseq, index): RECURSIVE csequence =
    IF empty?(cseq) THEN cseq
    ELSIF index = 0 THEN rest(cseq)
    ELSE add(first(cseq), remove(rest(cseq), index - 1))
    ENDIF
     MEASURE index

  remove_finite: JUDGEMENT remove(fseq, index) HAS_TYPE finite_csequence

  remove_infinite: JUDGEMENT remove(iseq, index) HAS_TYPE infinite_csequence

  remove_0: THEOREM FORALL nseq: remove(nseq, 0) = rest(nseq)

  remove_empty: THEOREM
    FORALL cseq, index:
      empty?(remove(cseq, index)) IFF
       empty?(cseq) OR (index = 0 AND empty?(rest(cseq)))

  remove_nonempty: THEOREM
    FORALL cseq, index:
      nonempty?(remove(cseq, index)) IFF
       nonempty?(cseq) AND (index > 0 OR nonempty?(rest(cseq)))

  remove_first: THEOREM
    FORALL cseq, index:
      nonempty?(remove(cseq, index)) IMPLIES
       first(remove(cseq, index)) =
        IF index = 0 THEN first(rest(cseq)) ELSE first(cseq) ENDIF

  remove_rest: THEOREM
    FORALL nseq, index:
      nonempty?(remove(nseq, index)) IMPLIES
       rest(remove(nseq, index)) =
        IF index = 0 THEN rest(rest(nseq))
        ELSE remove(rest(nseq), index - 1)
        ENDIF

  remove_upfrom_length: THEOREM
    FORALL fseq, (index: upfrom[length(fseq)]): remove(fseq, index) = fseq

  remove_length: THEOREM
    FORALL fseq, index:
      length(remove(fseq, index)) =
       length(fseq) - IF index?(fseq)(index) THEN 1 ELSE 0 ENDIF

  remove_index: THEOREM
    FORALL index, cseq, n:
      index?(remove(cseq, index))(n) IFF
       index?(cseq)(n) AND
        NOT (is_finite(cseq) AND
              n = length(cseq) - 1 AND index?(cseq)(index))

  remove_nth: THEOREM
    FORALL cseq, n, (m: indexes(remove(cseq, n))):
      nth(remove(cseq, n), m) = nth(cseq, m + IF m < n THEN 0 ELSE 1 ENDIF)

  remove_add: THEOREM
    FORALL cseq, index, t:
      add(t, remove(cseq, index)) = remove(add(t, cseq), index + 1)

  remove_last: THEOREM
    FORALL fseq, index:
      nonempty?(remove(fseq, index)) IMPLIES
       last(remove(fseq, index)) =
        IF index = length(fseq) - 1 THEN nth(fseq, index - 1)
        ELSE last(fseq)
        ENDIF

  remove_remove: THEOREM
    FORALL cseq, n, m:
      remove(remove(cseq, n), m) =
       IF n <= m THEN remove(remove(cseq, m + 1), n)
       ELSE remove(remove(cseq, m), n - 1)
       ENDIF

  remove_extensionality: THEOREM
    FORALL cseq1, cseq2, n:
      remove(cseq1, n) = remove(cseq2, n) AND
       ((NOT index?(cseq1)(n) AND NOT index?(cseq2)(n)) OR
         (index?(cseq1)(n) AND
           index?(cseq2)(n) AND nth(cseq1, n) = nth(cseq2, n)))
       IMPLIES cseq1 = cseq2

  remove_some: THEOREM
    FORALL cseq, index, p:
      some(p)(remove(cseq, index)) IFF
       (EXISTS (n: indexes(cseq)): n /= index AND p(nth(cseq, n)))

  remove_every: THEOREM
    FORALL cseq, index, p:
      every(p)(remove(cseq, index)) IFF
       (FORALL (n: indexes(cseq)): n = index OR p(nth(cseq, n)))

END csequence_remove

quality68%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.