Quelle monotone_subsequence.pvs Sprache: PVS

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  From any sequence one can extract           %
%  an increasing or a decreasing sub-sequence  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

monotone_subsequence : THEORY

  BEGIN

  IMPORTING sequence_props

  u, s : VAR sequence[real]

  i, j, n : VAR nat


  %---------------------------------------------------
  %  If all the suffixes of v have a minimal element
  %  then v contains an increasing sub-sequence
  %---------------------------------------------------

  has_minimum(u, n) : bool =
EXISTS i : n <= i AND FORALL j : n <= j IMPLIES u(i) <= u(j)

  minimum_prefix : LEMMA
EXISTS i : FORALL j : j <= n IMPLIES u(i) <= u(j)

  minimum_suffix : LEMMA
has_minimum(u, n) IMPLIES has_minimum(u, 0)

  v : VAR { u | FORALL n : has_minimum(u, n) }

  %--- a minimum of the elements n, n+1, ....  ---%

  mini(v, n) : nat =
epsilon! i : n <= i AND FORALL j : n <= j IMPLIES v(i) <= v(j)

  min_prop : LEMMA
n <= mini(v, n) AND FORALL j : n <= j IMPLIES v(mini(v, n)) <= v(j)

  min_prop1 : COROLLARY  n <= mini(v, n)

  min_prop2 : COROLLARY  n <= i IMPLIES v(mini(v, n)) <= v(i)

  %--- subsequence ---%

  h(v)(i) : RECURSIVE nat =
IF i = 0
THEN mini(v, 0)
ELSE mini(v, h(v)(i - 1) + 1)
ENDIF
     MEASURE i

  hseq(v) : sequence[real] = LAMBDA i : v(h(v)(i))

  h_increasing : LEMMA strict_increasing?(h(v))

  hseq_extraction : LEMMA subseq(hseq(v), v)

  hseq_increasing : LEMMA increasing?(hseq(v))



  %------------------------------------------------------
  %  If a sequence has no minimal element it contains a
  %  (strictly) decreasing sub-sequence
  %------------------------------------------------------

  w : VAR { u | not has_minimum(u, 0) }

  no_minimum : LEMMA not has_minimum(w, n)

  pick(w, n) : nat = epsilon! i : n <= i AND w(i) < w(n)

  pick_prop : LEMMA  n <= pick(w, n) AND w(pick(w, n)) < w(n)

  pick_prop1 : COROLLARY  n < pick(w, n)

  pick_prop2 : COROLLARY  w(pick(w, n)) < w(n)

  %--- subsequence ---%

  g(w)(i) : RECURSIVE nat =
IF i = 0
THEN pick(w, 0)
ELSE pick(w, g(w)(i - 1))
ENDIF
     MEASURE i

  gseq(w) : sequence[real] = LAMBDA i : w(g(w)(i))

  g_increasing : LEMMA strict_increasing?(g(w))

  gseq_extraction : LEMMA subseq(gseq(w), w)

  gseq_decreasing : LEMMA strict_decreasing(gseq(w))

  %------------------------
  %  Suffix starting at n
  %------------------------

  suffix(u, n) : sequence[real] = LAMBDA i : u(n+i)

  suffix_subseq : LEMMA subseq(suffix(u, n), u)

  suffix_hasmin : LEMMA
has_minimum(suffix(u, n), 0) IFF has_minimum(u, n)

  %----------------
  %  Main theorem
  %----------------

  monotone_subsequence : THEOREM
EXISTS s : subseq(s, u) AND (increasing?(s) OR decreasing(s))

  END monotone_subsequence

quality70%

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