|
sort_seq[T: TYPE, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------
%
% sort_seq (basic definitions and properties)
% -------------------------------------------
%
% Author: Ricky W. Butler
%
% This theory defines the sort function over an seq of
% values. Most of the text of this theory is scaffolding to
% demonstrate that the definition of "sort" is sound. In particular,
% the function "asort" is a witness function and not intended
% to be used externally.
%
% The following definitions should be used exclusively:
%
% is_permutation(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]):
% bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii))))
%
% increasing(A): bool = (FORALL i,j: 0 <= i AND i < j AND j < N
% IMPLIES A(i) <= A(j))
%
% sort(A): {a: seqs | is_permutation(A,a) AND increasing(a)}
%
% Note:
% The properties of sort are readily obtained via
% TYPEPRED "sort" or through use of sort_lem.
%
%------------------------------------------------------------------------
EXPORTING ALL BUT seq_to_array % i.e. do not export sort_array
WITH permutations_seq[T,<=], seqs[T]
BEGIN
%
seqs: TYPE = finite_sequence[T]
s,s1,s2,ss: VAR seqs
x, t: VAR T
i,j: VAR nat
IMPORTING sort_array, below_arrays, permutations_seq, seqs[T]
seq_to_array(s): below_array[length(s),T] =
(LAMBDA (i: below(length(s))): seq(s)(i))
increasing?(s): bool = (FORALL i,j: 0 <= i AND i < j AND j < length(s)
IMPLIES seq(s)(i) <= seq(s)(j))
sort(s): {ss: seqs | permutation?[T,<=](s,ss) AND increasing?(ss)}
sort_length : LEMMA length(sort(s)) = length(s)
AUTO_REWRITE+ sort_length
sort_seq_lem : LEMMA permutation?[T,<=](s,sort(s)) AND increasing?(sort(s))
sort_seq_in? : LEMMA in?(x,s) IFF in?(x,sort(s))
sort_seq_in : LEMMA FORALL (ii: below(length(s))):
in?(seq(sort(s))(ii),s)
sort_seq_in2 : LEMMA FORALL (ii: below(length(s))): in?(seq(s)(ii),sort(s))
% ------------------ NEW ------------------
sort_map(s): { map: [below(length(s)) -> below(length(s))] |
bijective?(map) AND
(FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}
sort_map_def: LEMMA FORALL (i: below(length(s))):
seq(s)(i) = seq(sort(s))(sort_map(s)(i))
sort_map_bij: LEMMA bijective?(sort_map(s))
isort_map(s: {ss: finite_sequence[T] | length(ss) > 0}):
{ map: [below(length(s)) -> below(length(s))] |
bijective?(map) AND
(FORALL (i:below(length(s))): seq(s)(map(i)) = seq(sort(s))(i))}
isort_map_def: LEMMA FORALL (i: below(length(s))):
seq(s)(isort_map(s)(i)) = seq(sort(s))(i)
isort_map_bij: LEMMA FORALL (s: {ss: finite_sequence[T] | length(ss) > 0}):
bijective?(isort_map(s))
END sort_seq
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
