Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_length_comp.pvs Sprache: PVS

Original von: 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 <[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_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

¤ Dauer der Verarbeitung: 0.0 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.