Quelle  sort_array.pvs

%------------------------------------------------------------------------
%
%  sort_array (basic definitions and properties)
%  -------------------------------------------
%
%      Author: Ricky W. Butler
%
%  This theory defines the sort function over an array of
%  values. 
%  
%  Defines:
%
%    permutation_of?(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]): 
%                      bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii))))
%  
%    sorted?(A): bool = (FORALL i,j: 0 <= i AND i < j AND j < N 
%                                      IMPLIES A(i) <= A(j))
%
%    sort(A): {a: arrays | permutation_of?(A,a) AND sorted?(a)}
%
%  Note:
%
%     The properties of sort are readily obtained via 
%     TYPEPRED "sort" or through use of sort_lem.
%
%------------------------------------------------------------------------
sort_array[N: nat, T: TYPE, <= : (total_order?[T]) ]: THEORY

   EXPORTING sorted?, sort, sort_lem, sort_map, isort_map,
              sort_TCC1, sort_map_TCC1, isort_map_TCC1, 
              sort_map_def, sort_map_bij,
              isort_map_def, isort_map_bij

        WITH permutations[N,T], below_arrays[N,T]

BEGIN

  IMPORTING sort_array_def[N,T,sort_array.<=], 
             permutations[N,T], below_arrays[N,T]

  A,a: VAR [below(N) -> T] 
  i,j: VAR below[N]
  x: VAR T

  sorted?(A): bool = (FORALL i,j: 0 <= i AND i < j AND j < N IMPLIES
                            A(i) <= A(j))

  sort(A): {a | permutation_of?(A,a) AND sorted?(a)}

  sort_lem     : LEMMA permutation_of?(A,sort(A)) AND sorted?(sort(A))
  
  sort_in?     : LEMMA in?(x,A) IFF in?(x,sort(A))

% ------------------ NEW ------------------

  sort_map(A): { map: [below(N) -> below(N)] | bijective?(map) AND
                    (FORALL i: A(i) = sort(A)(map(i)))}

  sort_map_def: LEMMA A(i) = sort(A)(sort_map(A)(i))

  sort_map_bij: LEMMA bijective?(sort_map(A))


  isort_map(A): { map: [below(N) -> below(N)] | bijective?(map) AND
                    (FORALL i: A(map(i)) = sort(A)(i))}

  isort_map_def: LEMMA A(isort_map(A)(i)) = sort(A)(i)

  isort_map_bij: LEMMA bijective?(isort_map(A))


END sort_array