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