Quelle finite_below.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  Every totally ordered finite set has an order-preserving bijection
%  with a below set.
%
%  For PVS version 3.2.  March 5, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[T]
%  finite_sets: finite_sets_inductions, finite_sets_minmax
%  orders: bounded_orders[T], closure_ops[T], finite_below[T],
%    indexed_sets_extra, minmax_orders[T], relations_extra[T],
%    relation_iterate[T]
%
%-------------------------------------------------------------------------
finite_below[T: TYPE]: THEORY
BEGIN

  IMPORTING closure_ops[T], minmax_orders[T]

  S: VAR finite_set[T]
  <: VAR (strict_total_order?[T])

  % Select the nth element of the set

  nth(S, <)(n: below[card(S)]): RECURSIVE (S) =
    IF n = 0 THEN least(reflexive_closure(<))(S)
    ELSE nth(remove(least(reflexive_closure(<))(S), S), <)(n - 1)
    ENDIF
     MEASURE n

  nth_one_step: LEMMA
    FORALL S, <, (n: below[card(S)]):
      n + 1 < card(S) IMPLIES nth(S, <)(n) < nth(S, <)(n + 1)

  nth_monotonic: LEMMA FORALL S, <: preserves(nth(S, <), reals.<, <)

  nth_surjective: LEMMA FORALL S, <: surjective?(nth(S, <))

  nth_bijective: JUDGEMENT
      nth(S, <) HAS_TYPE (bijective?[below[card(S)], (S)])

  % Find out which element of the set this is

  index(S, <)(t: (S)): RECURSIVE below[card(S)] =
    IF least?(t, S, reflexive_closure(<)) THEN 0
    ELSE 1 + index(remove(least(reflexive_closure(<))(S), S), <)(t)
    ENDIF
     MEASURE card(S)

  index_monotonic: LEMMA
    FORALL S, <: preserves(index(S, <), <, reals.<)

  index_nth_left_inverse: LEMMA
    FORALL S, <: left_inverse?(nth(S, <), index(S, <))

  index_nth_right_inverse: LEMMA
    FORALL S, <: right_inverse?(nth(S, <), index(S, <))

  index_bijective: JUDGEMENT
      index(S, <) HAS_TYPE (bijective?[(S), below[card(S)]])

END finite_below

quality53%

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