Quelle sort_seq.pvs Sprache: PVS

sort_seq[T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
%  sort_seq (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the sort function over an seq of
%  values.  Most of the text of this theory is scaffolding to
%  demonstrate that the definition of "sort" is sound.  In particular,
%  the function "asort" is a witness function and not intended
%  to be used externally.
%
%  The following definitions should be used exclusively:
%
%    is_permutation(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]):
%                      bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii))))
%
%    increasing(A): bool = (FORALL i,j: 0 <= i AND i < j AND j < N
%                                 IMPLIES A(i) <= A(j))
%
%    sort(A): {a: seqs | is_permutation(A,a) AND increasing(a)}
%
%  Note:
%     The properties of sort are readily obtained via
%     TYPEPRED "sort" or through use of sort_lem.
%
%------------------------------------------------------------------------

  EXPORTING ALL BUT seq_to_array % i.e. do not export sort_array
        WITH permutations_seq[T,<=], seqs[T]

BEGIN

%

  seqs: TYPE = finite_sequence[T]

  s,s1,s2,ss: VAR seqs
  x, t: VAR T
  i,j: VAR nat

  IMPORTING sort_array, below_arrays, permutations_seq, seqs[T]

  seq_to_array(s): below_array[length(s),T] =
             (LAMBDA (i: below(length(s))): seq(s)(i))

  increasing?(s): bool = (FORALL i,j: 0 <= i AND i < j AND j < length(s)
                            IMPLIES seq(s)(i) <= seq(s)(j))

  sort(s): {ss: seqs | permutation?[T,<=](s,ss) AND increasing?(ss)}

  sort_length  : LEMMA length(sort(s)) = length(s)

  AUTO_REWRITE+ sort_length

  sort_seq_lem : LEMMA permutation?[T,<=](s,sort(s)) AND increasing?(sort(s))

  sort_seq_in?  : LEMMA in?(x,s) IFF in?(x,sort(s))

  sort_seq_in   : LEMMA FORALL (ii: below(length(s))):
                                     in?(seq(sort(s))(ii),s)

  sort_seq_in2   : LEMMA FORALL (ii: below(length(s))): in?(seq(s)(ii),sort(s))

% ------------------ NEW ------------------

  sort_map(s): { map: [below(length(s)) -> below(length(s))] |
            bijective?(map) AND
              (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}

  sort_map_def: LEMMA FORALL (i: below(length(s))):
                            seq(s)(i) = seq(sort(s))(sort_map(s)(i))

  sort_map_bij: LEMMA bijective?(sort_map(s))

  isort_map(s: {ss: finite_sequence[T]  | length(ss) > 0}):
       { map: [below(length(s)) -> below(length(s))] |
             bijective?(map) AND
               (FORALL (i:below(length(s))): seq(s)(map(i)) = seq(sort(s))(i))}

  isort_map_def: LEMMA FORALL (i: below(length(s))):
                             seq(s)(isort_map(s)(i)) = seq(sort(s))(i)

  isort_map_bij: LEMMA FORALL (s: {ss: finite_sequence[T]  | length(ss) > 0}):
                            bijective?(isort_map(s))

END sort_seq

quality95%

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