SSL set2seq.pvs

set2seq[T: TYPE]: THEORY
%----------------------------------------------------------------------------
%
% Utility functions for converting from sets to sequences
%
% Author: Kristin Y. Rozier
%----------------------------------------------------------------------------
BEGIN

   IMPORTING finite_sets@finite_sets_inductions[T]

   fs: VAR finite_sequence[T]
   x : VAR T

   #(t:T): finite_sequence[T] =  (# length := 1,
                                    seq := (LAMBDA (x: below[1]): t) #)

   gen_seq_lem: LEMMA #(x)(0) = x

   set2seq(S: finite_set[T]):  RECURSIVE finite_sequence[T] =
        IF empty?[T](S) THEN empty_seq
        ELSE #(choose[T](S)) o set2seq(rest[T](S)) 
        ENDIF 
      MEASURE card[T](S) 

   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(ii))

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

   AUTO_REWRITE+ set2seq_length

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

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

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

  S: VAR finite_set[T]

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

END minmax_set2seq