Quelle csequence_props.pvs Sprache: 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 <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_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

quality79%

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