|
set2seq[T: TYPE]: THEORY
%----------------------------------------------------------------------------
%
% Utility functions for converting from sets to sequences
%
% Author: Kristin Y. Rozier
%----------------------------------------------------------------------------
BEGIN
IMPORTING finite_sets@finite_sets_inductions[T]
fs: VAR finite_sequence[T]
x : VAR T
#(t:T): finite_sequence[T] = (# length := 1,
seq := (LAMBDA (x: below[1]): t) #)
gen_seq_lem: LEMMA #(x)(0) = x
set2seq(S: finite_set[T]): RECURSIVE finite_sequence[T] =
IF empty?[T](S) THEN empty_seq
ELSE #(choose[T](S)) o set2seq(rest[T](S))
ENDIF
MEASURE card[T](S)
S: VAR finite_set[T]
set2seq_length: LEMMA length(set2seq(S)) = card(S)
set2seq_lem: LEMMA LET fs = set2seq(S) IN
FORALL (ii: below(length(fs))): S(fs(ii))
set2seq_exists: LEMMA LET fs = set2seq(S) IN
S(x) IMPLIES
EXISTS (ii: below(length(fs))): fs(ii) = x
AUTO_REWRITE+ set2seq_length
set2seq_neq : LEMMA LET fs = set2seq(S) IN
FORALL (ii,jj: below(length(fs))):
ii /= jj IMPLIES fs(ii) /= fs(jj)
END set2seq
minmax_set2seq[T: TYPE+, <= : (total_order?[T]) ]: THEORY
BEGIN
IMPORTING sort_seq_lems[T,<=],
finite_sets@finite_sets_minmax[T,<=],
set2seq[T]
S: VAR finite_set[T]
minmax_set2seq: LEMMA card(S) > 0 IMPLIES
min(set2seq(S)) = min[T,<=](S) AND
max(set2seq(S)) = max[T,<=](S)
END minmax_set2seq
¤ Dauer der Verarbeitung: 0.18 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.
|
