Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: finite_below.pvs Sprache: PVS

Original von: 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 ([email protected]), 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

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.