%------------------------------------------------------------------------ % % 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: posnat, 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