%------------------------------------------------------------------------------
% Enumerations of finite sets
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
finite_enumeration[T:TYPE]: THEORY

BEGIN

  finite_enumeration(X:finite_set[T]): [below[card(X)]->(X)]
   = choose({f:[below[card(X)]->(X)] | bijective?[below[card(X)],(X)](f)})

  X: VAR finite_set[T]

  finite_enumeration_bij:   LEMMA
               bijective?[below[card(X)],(X)](finite_enumeration(X))

  finite_enumeration_image: LEMMA
               image(finite_enumeration(X),fullset[below[card(X)]]) = X

END finite_enumeration