|
%------------------------------------------------------------------------
%
% 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
[ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
]
|
