|
fseq2set[T: TYPE+, <= : (total_order?[T]) ]: THEORY
%----------------------------------------------------------------------------
%
% Utility functions for converting to/from sets and sequences
%
% Version 1.0, January, 2004
% Author: Kristin Y. Rozier
%----------------------------------------------------------------------------
BEGIN
IMPORTING sort_fseq_lems[T,<=],
finite_sets@finite_sets_minmax[T,<=],
ints@max_below
fs: VAR fseq
a,b,c,d,x,y,z: VAR T
N: VAR nat
%------------------------------------------------------------------------------
seq2set(fs): finite_set[T]
= {s: T | (EXISTS (kk: below(length(fs))): fs`seq(kk) = s)}
seq2set_lem: LEMMA (FORALL (ii: below(length(fs))): seq2set(fs)(fs`seq(ii)))
card_seq2set: LEMMA card[T](seq2set(fs)) <= length(fs)
ne_fs: VAR ne_fseq
minmax_seq2set: LEMMA min[T,<=](seq2set(ne_fs)) = min(ne_fs) AND
max[T,<=](seq2set(ne_fs)) = max(ne_fs)
ss: VAR ne_fseq % length > 0
JUDGEMENT seq2set(ss) HAS_TYPE (nonempty?[T])
%------------------------------------------------------------------------------
% set2seq(S: finite_set[T]): RECURSIVE fseq[T] =
% IF empty?[T](S) THEN empty_seq
% ELSE fseq1(choose[T](S)) o set2seq(rest[T](S))
% ENDIF
% MEASURE card[T](S)
set2seq(S: finite_set[T]): {fs: fseq |
length(fs) = card(S) AND
(FORALL (ii: below(length(fs))): S(fs`seq(ii))) AND
(FORALL (x:T): S(x) IMPLIES EXISTS (ii: below(length(fs))): fs`seq(ii) = x) AND
(FORALL (ii,jj: below(length(fs))):
ii /= jj IMPLIES fs`seq(ii) /= fs`seq(jj)) }
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`seq(ii))
set2seq_exists: LEMMA LET fs = set2seq(S) IN
S(x) IMPLIES
EXISTS (ii: below(length(fs))): fs`seq(ii) = x
AUTO_REWRITE+ set2seq_length
minmax_set2seq: LEMMA card(S) > 0 IMPLIES
min(set2seq(S)) = min[T,<=](S) AND
max(set2seq(S)) = max[T,<=](S)
set2seq_neq : LEMMA LET fs = set2seq(S) IN
FORALL (ii,jj: below(length(fs))):
ii /= jj IMPLIES fs`seq(ii) /= fs`seq(jj)
set2seq_all : LEMMA LET fs = sort(set2seq(S)) IN
FORALL (ii: below(length(fs)-1)):
fs`seq(ii) <= x AND x <= fs`seq(ii+1) AND
fs`seq(ii) /= x AND x /= fs`seq(ii+1)
IMPLIES
NOT S(x)
END fseq2set
¤ Dauer der Verarbeitung: 0.20 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.
|
