Quelle csequence_limit.pvs Sprache: PVS

%-----------------------------------------------------------------------------
% The limit of a function that produces prefixes of a sequence of countable
% length.
%
% 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_limit[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence_prefix_suffix[T]
  IMPORTING ascending_chains[csequence, prefix?]
  IMPORTING csequence_codt_coreduce[T, ascending_chain]

  t: VAR T
  n, m, k: VAR nat
  chain: VAR ascending_chain
  cseq: VAR csequence
  fseq: VAR finite_csequence
  p: VAR pred[csequence]

  % FIXME: prefix_chain and suffix_chain sound like converses, but they are not

  prefix_chain(cseq): ascending_chain = LAMBDA n: prefix(cseq, n)

  suffix_chain(chain, n): ascending_chain = LAMBDA m: suffix(chain(m), n)

  rest_chain(chain): ascending_chain =
      LAMBDA n:
        IF empty?(chain(n)) THEN empty_cseq ELSE rest(chain(n)) ENDIF

  ascending_chain?_nth: THEOREM
    FORALL chain, n, m, k:
      n <= m AND index?(chain(n))(k) IMPLIES
       index?(chain(m))(k) AND nth(chain(n), k) = nth(chain(m), k)

  limit_struct(chain): csequence_struct[T, ascending_chain] =
      IF (FORALL n: empty?(chain(n))) THEN inj_empty_cseq
      ELSE inj_add(first(chain(min({n | nonempty?(chain(n))}))),
                   rest_chain(chain))
      ENDIF

  limit(chain): csequence = coreduce(limit_struct)(chain)

  limit_empty: THEOREM
    FORALL chain: empty?(limit(chain)) IFF (FORALL n: empty?(chain(n)))

  limit_nonempty: THEOREM
    FORALL chain:
      nonempty?(limit(chain)) IFF (EXISTS n: nonempty?(chain(n)))

  limit_first: THEOREM
    FORALL chain, n:
      nonempty?(chain(n)) IMPLIES first(chain(n)) = first(limit(chain))

  limit_rest_chain: THEOREM
    FORALL chain:
      nonempty?(limit(chain)) IMPLIES
       rest(limit(chain)) = limit(rest_chain(chain))

  limit_suffix_chain: THEOREM
    FORALL chain, n: suffix(limit(chain), n) = limit(suffix_chain(chain, n))

  limit_lub: THEOREM FORALL chain: least_upperbound?(chain)(limit(chain))

  limit_nth: THEOREM
    FORALL chain, cseq, n, m:
      index?(chain(n))(m) IMPLIES
       index?(limit(chain))(m) AND nth(chain(n), m) = nth(limit(chain), m)

  limit_def: THEOREM
    FORALL chain, cseq:
      limit(chain) = cseq IFF
       (FORALL t, n:
          index?(cseq)(n) AND nth(cseq, n) = t IFF
           (EXISTS m: index?(chain(m))(n) AND nth(chain(m), n) = t))

  limit_prefix_chain: THEOREM FORALL cseq: limit(prefix_chain(cseq)) = cseq

  limit_prefix_compact: THEOREM
    FORALL cseq, n, chain:
      (n = 0 OR index?(cseq)(n - 1)) IMPLIES
       (prefix?(prefix(cseq, n), limit(chain)) IMPLIES
         (EXISTS m: prefix?(prefix(cseq, n), chain(m))))

  limit_finite_compact: THEOREM
    FORALL cseq:
      is_finite(cseq) IFF
       (FORALL chain:
          prefix?(cseq, limit(chain)) IMPLIES
           (EXISTS m: prefix?(cseq, chain(m))))

  continuous?(p): bool =
      FORALL chain: (FORALL n: p(chain(n))) IMPLIES p(limit(chain))

  continuous?_infinite: THEOREM
    FORALL p:
      continuous?(p) AND (FORALL fseq: p(fseq)) IMPLIES
       (FORALL cseq: p(cseq))

END csequence_limit

quality46%

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