| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle set2seq.pvs Sprache: PVS |
|||||||||
|
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.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28