|
majority_fseq[T: NONEMPTY_TYPE]: THEORY
%------------------------------------------------------------------------
%
% majority (basic definitions and properties)
% -------------------------------------------
%
% Author: Ricky W. Butler
%
% This theory defines the majority function over a finite sequence of
% values. The following functions are defined:
%
% is_majority(mv,fs) -- predicate that is true IFF mv is
% the majority value of the sequence
%
% maj_exists(fs) -- predicate that us true IFF a majority
% exists
%
% maj(fs) -- function that returns the majority value
% if a majority exists. If a majority does
% not exist, the function returns an
% unspecified value from the type T.
% This value may not be in the sequence.
%
% inseq(x,fs) -- predicate that is true IFF x is in
% the sequence
%
% Note: the following function can be defined that will return
% a value from the sequence if a majority does not exist.
%
% finseq: TYPE = {fs | length(fs) > 0}
%
% fsq: VAR finseq
% Maj(fsq): {x: T | in_seq(x,fsq)} = IF maj_exists(fsq) THEN maj(fsq)
% ELSE choose({x: T | in_seq(x,fsq)})
% ENDIF
%
%------------------------------------------------------------------------
BEGIN
IMPORTING finite_sets@finite_sets_below
IMPORTING fseqs[T]
fs: VAR fsq[T]
mv, mv1, mv2, x: VAR T
is_majority(mv: T, fs): bool =
2*card({i: below(length(fs)) | seq(fs)(i) = mv}) > length(fs)
maj_exists(fs): bool = (EXISTS (mv: T): is_majority(mv,fs))
maj(fs): {mv | maj_exists(fs) => is_majority(mv,fs)}
in_seq(x,fs): bool = (EXISTS (i: below(length(fs))): seq(fs)(i) = x)
is_majority_unique: LEMMA is_majority(mv1,fs) AND is_majority(mv2,fs)
IMPLIES mv1 = mv2
maj_lem: LEMMA is_majority(mv,fs) IFF
maj_exists(fs) AND maj(fs) = mv
maj_subset: LEMMA (EXISTS (A: finite_set[below(length(fs))]):
2*card(A) > length(fs)
AND (FORALL (i: below(length(fs))): A(i)
IMPLIES seq(fs)(i) = mv))
IMPLIES is_majority(mv,fs)
maj_in_seq: LEMMA is_majority(mv,fs) IMPLIES in_seq(mv,fs)
% ===================== Some Special Sequences ===================
f1: VAR [below[1] -> T]
n: VAR posnat
c: VAR T
length_eq_1: LEMMA maj(fseq1(c)) = c
constant_seq(n,c): fsq[T] = (# length := n,
seq := (LAMBDA (i: nat): c) #)
is_majority_const: LEMMA is_majority(c, constant_seq(n,c))
maj_const: LEMMA maj_exists(constant_seq(n,c)) AND
maj(constant_seq(n,c)) = c
END majority_fseq
¤ Dauer der Verarbeitung: 0.31 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.
|
