Quelle sequence_props.pvs Sprache: PVS

sequence_props : THEORY
%----------------------------------------------------------------------------
%  Properties of real sequences              %
%  -> condition for increasing? / decreasing %
%  -> subsequences                           %
%
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  IMPORTING real_fun_supinf

  u, v, w : VAR sequence[real]
  i, j : VAR nat
  a, x : VAR real
  n    : VAR nat

  %--------------------------------------------------
  %  Conditions for increasing?/decreasing sequences
  %--------------------------------------------------

  incr_condition        : LEMMA increasing?(u) IFF FORALL i : u(i) <= u(i+1)

  decr_condition        : LEMMA decreasing(u) IFF FORALL i : u(i+1) <= u(i)

  strict_incr_condition : LEMMA strict_increasing?(u)
                                   IFF FORALL i : u(i) < u(i+1)

  strict_decr_condition : LEMMA strict_decreasing(u)
                                   IFF FORALL i : u(i+1) < u(i)

  %-------------------------------------------------------
  %  Increasing sequences of natural numbers
  %  used for extracting a sub-sequence from a sequence
  %-------------------------------------------------------

  extraction : TYPE = { f : [nat -> nat] | strict_increasing?(f) }

  f, g : VAR extraction

  extract_incr1      : LEMMA  f(i) < f(j) IFF i < j

  extract_incr2      : LEMMA  i <= j IMPLIES f(i) <= f(j)

  extract_incr3      : LEMMA  i <= f(i)

  unbounded_extract1 : LEMMA  EXISTS j : i <= f(j)

  unbounded_extract2 : LEMMA  EXISTS j : i < f(j)

  extract_composition : LEMMA  strict_increasing?(g o f)

  %-----------------
  %  Sub-sequences
  %-----------------

  subseq(u, v) : bool = EXISTS f : FORALL i : u(i) = v(f(i))

  subseq_def:         LEMMA subseq(u,v) IFF EXISTS f: FORALL n: u(n) = v(f(n))

  reflexive_subseq :  LEMMA subseq(u, u)

  transitive_subseq : LEMMA subseq(u, v) AND subseq(v, w) IMPLIES subseq(u, w)

  extract_bij:        LEMMA bijective?[nat,(image(f,fullset[nat]))](f)

  %-----------------------------------------
  %  Properties inherited by subsequences
  %-----------------------------------------

  incr_subseq : LEMMA increasing?(v) AND subseq(u, v) IMPLIES increasing?(u)

  decr_subseq : LEMMA decreasing(v) AND subseq(u, v) IMPLIES decreasing(u)

  strict_incr_subseq  : LEMMA strict_increasing?(v) AND subseq(u, v)
                          IMPLIES strict_increasing?(u)

  strict_decr_subseq  : LEMMA strict_increasing?(v) AND subseq(u, v)
                          IMPLIES strict_increasing?(u)

  bounded_above_subseq: LEMMA bounded_above?(v) AND subseq(u, v)
                                  IMPLIES bounded_above?(u)

  bounded_below_subseq: LEMMA bounded_below?(v) AND subseq(u, v)
                                  IMPLIES bounded_below?(u)

  bounded_subseq      : LEMMA bounded?(v) AND subseq(u, v) IMPLIES bounded?(u)

END sequence_props

quality93%

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