Quellcode-Bibliothek seq2set.pvs   Sprache: PVS

seq2set[T: TYPE]: THEORY
%----------------------------------------------------------------------------
%
% Utility functions for converting to/from sets and sequences
%
% Version 1.0, January, 2004
% Author: Kristin Y. Rozier
%----------------------------------------------------------------------------
BEGIN

   IMPORTING seqs[T]

   fs: VAR finite_sequence[T]

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

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

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

   ss: VAR ne_seqs  % length > 0

   JUDGEMENT seq2set(ss) HAS_TYPE (nonempty?[T]) 

END seq2set

minmax_seq2set[T: TYPE+, <= : (total_order?[T]) ]: THEORY
BEGIN

   IMPORTING sort_seq_lems[T,<=],
             finite_sets@finite_sets_minmax[T,<=],
             seq2set[T]

   ne_fs: VAR ne_seqs[T]

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

END minmax_seq2set