Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_strict_prefix.prf Sprache: PVS

Original von: PVS^©

%-----------------------------------------------------------------------------
% Proper prefixes of sequences of countable length.
%
% 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_strict_prefix[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence_prefix[T]

  p: VAR pred[T]
  n: VAR nat
  cseq, cseq1, cseq2: VAR csequence
  nseq: VAR nonempty_csequence
  fseq: VAR finite_csequence

  strict_prefix?(cseq1, cseq2): INDUCTIVE bool =
      nonempty?(cseq2) AND
       (empty?(cseq1) OR
         (first(cseq1) = first(cseq2) AND
           strict_prefix?(rest(cseq1), rest(cseq2))))

  strict_prefix?(cseq2)(cseq1): MACRO bool = strict_prefix?(cseq1, cseq2)

  strict_prefix?_prefix?: THEOREM
    FORALL cseq1, cseq2:
      strict_prefix?(cseq1, cseq2) IFF
       prefix?(cseq1, cseq2) AND cseq1 /= cseq2

  strict_prefix?_finite: THEOREM
    FORALL cseq1, cseq2:
      strict_prefix?(cseq1, cseq2) IMPLIES is_finite(cseq1)

  strict_prefix?_first: THEOREM
    FORALL nseq, cseq:
      strict_prefix?(nseq, cseq) IMPLIES first(nseq) = first(cseq)

  strict_prefix?_rest: THEOREM
    FORALL nseq, cseq:
      strict_prefix?(nseq, cseq) IMPLIES
       strict_prefix?(rest(nseq), rest(cseq))

  strict_prefix?_length: THEOREM
    FORALL cseq, fseq:
      strict_prefix?(cseq, fseq) IMPLIES length(cseq) < length(fseq)

  strict_prefix?_index: THEOREM
    FORALL cseq1, cseq2, n:
      strict_prefix?(cseq1, cseq2) AND index?(cseq1)(n) IMPLIES
       index?(cseq2)(n)

  strict_prefix?_nth: THEOREM
    FORALL cseq1, cseq2, (n: indexes(cseq1)):
      strict_prefix?(cseq1, cseq2) IMPLIES nth(cseq1, n) = nth(cseq2, n)

  strict_prefix?_concatenate: THEOREM
    FORALL fseq, nseq: strict_prefix?(fseq, fseq o nseq)

  strict_prefix?_def: THEOREM
    FORALL cseq1, cseq2:
      strict_prefix?(cseq1, cseq2) IFF
       is_finite(cseq1) AND (EXISTS nseq: cseq1 o nseq = cseq2)

  strict_prefix?_is_strict_order: JUDGEMENT
    strict_prefix? HAS_TYPE (strict_order?[csequence])

  % Strict prefixes of a given sequence are well-ordered
  strict_prefix?_well_ordered: THEOREM
    FORALL cseq:
      well_ordered?(restrict
                        [[csequence, csequence],
                         [(strict_prefix?(cseq)), (strict_prefix?(cseq))],
                         bool]
                        (strict_prefix?))

  strict_prefix?_prefix: THEOREM
    FORALL cseq1, cseq2:
      strict_prefix?(cseq1, cseq2) IFF
       (EXISTS n:
          cseq1 = prefix(cseq2, n) AND
           (is_finite(cseq2) IMPLIES n < length(cseq2)))

END csequence_strict_prefix

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.