Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_props.pvs Sprache: PVS

Original von: PVS^©

%-----------------------------------------------------------------------------
% Finite and infinite sequences, and also the nonempty subtype, part of the
% theory of sequences of countable length defined as coalgebraic datatypes.
%
% 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_props[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence[T]

  t: VAR T
  p, q: VAR pred[T]
  cseq, cseq_rest: VAR csequence
  n, m: VAR nat

  % This predicate is TRUE iff cseq is finite and of length n
  has_length(cseq, n): RECURSIVE bool =
    IF empty?(cseq) THEN n = 0
    ELSE n > 0 AND has_length(rest(cseq), n - 1)
    ENDIF
     MEASURE n

  has_length_injective: THEOREM
    FORALL cseq, n, m:
      has_length(cseq, n) AND has_length(cseq, m) IMPLIES n = m

  % This predicate is TRUE iff cseq is finite
  is_finite(cseq): INDUCTIVE bool = empty?(cseq) OR is_finite(rest(cseq))

  is_finite_def: THEOREM
    FORALL cseq: is_finite(cseq) IFF (EXISTS n: has_length(cseq, n))

  is_infinite(cseq): MACRO bool = NOT is_finite(cseq)

  % Various useful subtypes of the csequence type

  finite_csequence: TYPE+ = (is_finite) CONTAINING empty_cseq

  infinite_csequence: TYPE = (is_infinite)

  empty_csequence: TYPE+ = (empty?) CONTAINING empty_cseq

  nonempty_csequence: TYPE = (nonempty?)

  nonempty_finite_csequence: TYPE = {cseq: finite_csequence | nonempty?(cseq)}

  % Judgements relating the types

  empty_csequence_is_finite: JUDGEMENT
    empty_csequence SUBTYPE_OF finite_csequence

  infinite_csequence_is_nonempty: JUDGEMENT
    infinite_csequence SUBTYPE_OF nonempty_csequence

  % Properties of some and every

  pred_NOT(p)(t): bool = NOT p(t)

  pred_AND(p, q)(t): bool = p(t) AND q(t)

  pred_OR(p, q)(t): bool = p(t) OR q(t)

  pred_IMPLIES(p, q)(t): bool = p(t) IMPLIES q(t)

  some_every_rew: THEOREM
    FORALL p, cseq: some(p)(cseq) IFF NOT every(pred_NOT(p))(cseq)

  every_some_rew: THEOREM
    FORALL p, cseq: every(p)(cseq) IFF NOT some(pred_NOT(p))(cseq)

  some_implies: THEOREM
    FORALL cseq, p, q:
      (FORALL t: pred_IMPLIES(p, q)(t)) AND some(p)(cseq) IMPLIES
       some(q)(cseq)

  every_implies: THEOREM
    FORALL cseq, p, q:
      (FORALL t: pred_IMPLIES(p, q)(t)) AND every(p)(cseq) IMPLIES
       every(q)(cseq)

END csequence_props

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