Quelle csequence_length_comp.pvs Sprache: PVS

%-----------------------------------------------------------------------------
% Operators for convenience in writing length comparisons that include
% possibly infinite csequences.
%
% It might be nicer to have an "extended nat" type that includes a special
% "infinity" value.  Then we could define the length operator on all
% sequences, which would simplify some other definitions.  If you are
% interested in trying this approach, please contact me.
%
% 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_comp[T1, T2: TYPE]: THEORY
BEGIN

  IMPORTING csequence_length[T1], csequence_length[T2]

  cseq1: VAR csequence[T1]
  cseq2: VAR csequence[T2]
  nseq1: VAR nonempty_csequence[T1]
  nseq2: VAR nonempty_csequence[T2]

  length_lt(cseq1, cseq2): bool =
      is_finite(cseq1) AND
       (is_finite(cseq2) IMPLIES length(cseq1) < length(cseq2))

  length_le(cseq1, cseq2): bool =
      is_finite(cseq2) IMPLIES
       is_finite(cseq1) AND length(cseq1) <= length(cseq2)

  length_eq(cseq1, cseq2): bool =
      (is_infinite(cseq1) AND is_infinite(cseq2)) OR
       (is_finite(cseq1) AND
         is_finite(cseq2) AND length(cseq1) = length(cseq2))

  length_ge(cseq1, cseq2): bool =
      is_finite(cseq1) IMPLIES
       is_finite(cseq2) AND length(cseq1) >= length(cseq2)

  length_gt(cseq1, cseq2): bool =
      is_finite(cseq2) AND
       (is_finite(cseq1) IMPLIES length(cseq1) > length(cseq2))

  length_lt_le: THEOREM
    FORALL cseq1, cseq2:
      length_lt(cseq1, cseq2) IMPLIES length_le(cseq1, cseq2)

  length_gt_ge: THEOREM
    FORALL cseq1, cseq2:
      length_gt(cseq1, cseq2) IMPLIES length_ge(cseq1, cseq2)

  length_eq_le: THEOREM
    FORALL cseq1, cseq2:
      length_eq(cseq1, cseq2) IMPLIES length_le(cseq1, cseq2)

  length_eq_ge: THEOREM
    FORALL cseq1, cseq2:
      length_eq(cseq1, cseq2) IMPLIES length_ge(cseq1, cseq2)

  length_lt_neq: THEOREM
    FORALL cseq1, cseq2:
      length_lt(cseq1, cseq2) IMPLIES NOT length_eq(cseq1, cseq2)

  length_gt_neq: THEOREM
    FORALL cseq1, cseq2:
      length_gt(cseq1, cseq2) IMPLIES NOT length_eq(cseq1, cseq2)

  length_eq_empty: THEOREM
    FORALL cseq1, cseq2:
      length_eq(cseq1, cseq2) IMPLIES (empty?(cseq1) IFF empty?(cseq2))

  length_eq_rest: THEOREM
    FORALL nseq1, nseq2:
      length_eq(nseq1, nseq2) IFF length_eq(rest(nseq1), rest(nseq2))

END csequence_length_comp

quality95%

¤ 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.