Quelle fseq2set.pvs Sprache: PVS

fseq2set[T: TYPE+, <= : (total_order?[T]) ]: THEORY
%----------------------------------------------------------------------------
%
% Utility functions for converting to/from sets and sequences
%
% Version 1.0, January, 2004
% Author: Kristin Y. Rozier
%----------------------------------------------------------------------------
BEGIN

   IMPORTING sort_fseq_lems[T,<=],
             finite_sets@finite_sets_minmax[T,<=],
             ints@max_below

   fs: VAR fseq
   a,b,c,d,x,y,z: VAR T
   N: VAR nat

%------------------------------------------------------------------------------
   seq2set(fs): finite_set[T]
   = {s: T | (EXISTS (kk: below(length(fs))): fs`seq(kk) = s)}

   seq2set_lem: LEMMA (FORALL (ii: below(length(fs))): seq2set(fs)(fs`seq(ii)))

   card_seq2set: LEMMA card[T](seq2set(fs)) <= length(fs)

   ne_fs: VAR ne_fseq
   minmax_seq2set: LEMMA min[T,<=](seq2set(ne_fs)) = min(ne_fs) AND
                         max[T,<=](seq2set(ne_fs)) = max(ne_fs)

   ss: VAR ne_fseq  % length > 0
   JUDGEMENT seq2set(ss) HAS_TYPE (nonempty?[T])

%------------------------------------------------------------------------------
%    set2seq(S: finite_set[T]):  RECURSIVE fseq[T] =
%         IF empty?[T](S) THEN empty_seq
%         ELSE fseq1(choose[T](S)) o set2seq(rest[T](S))
%         ENDIF
%       MEASURE card[T](S)

  set2seq(S: finite_set[T]):  {fs: fseq |
       length(fs) = card(S) AND
       (FORALL (ii: below(length(fs))): S(fs`seq(ii))) AND
       (FORALL (x:T): S(x) IMPLIES EXISTS (ii: below(length(fs))): fs`seq(ii) = x) AND
       (FORALL (ii,jj: below(length(fs))):
                               ii /= jj IMPLIES fs`seq(ii) /= fs`seq(jj)) }

   S: VAR finite_set[T]

   set2seq_length: LEMMA length(set2seq(S)) = card(S)

   set2seq_lem: LEMMA LET fs = set2seq(S) IN
                          FORALL (ii: below(length(fs))): S(fs`seq(ii))

   set2seq_exists: LEMMA LET fs = set2seq(S) IN
                        S(x) IMPLIES
                            EXISTS (ii: below(length(fs))): fs`seq(ii) = x

   AUTO_REWRITE+ set2seq_length

   minmax_set2seq: LEMMA card(S) > 0 IMPLIES
                           min(set2seq(S)) =  min[T,<=](S) AND
                           max(set2seq(S)) =  max[T,<=](S)

   set2seq_neq   : LEMMA LET fs = set2seq(S) IN
                     FORALL (ii,jj: below(length(fs))):
                               ii /= jj IMPLIES fs`seq(ii) /= fs`seq(jj)

   set2seq_all   : LEMMA LET fs = sort(set2seq(S)) IN
                          FORALL (ii: below(length(fs)-1)):
                             fs`seq(ii) <= x AND x <= fs`seq(ii+1)  AND
                             fs`seq(ii) /= x AND x /= fs`seq(ii+1)
                         IMPLIES
                             NOT S(x)

END fseq2set

quality75%

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