|
%------------------------------------------------------------------------
%
% majority_array (basic definitions and properties)
% -------------------------------------------
%
% This theory defines the majority function over an array of
% values.
%
% Defines:
%
% is_majority(mv,A) -- predicate that is true IFF mv is
% the majority value of the array A.
%
% maj_exists(A) -- predicate that is true IFF a majority
% of A exists.
%
% maj(A) -- function that returns the majority value
% of A 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 array.
%
% inseq(x,A) -- predicate that is true IFF x is in
% the array A.
%
%------------------------------------------------------------------------
majority_array[N: posnat, T: NONEMPTY_TYPE]: THEORY
BEGIN
IMPORTING finite_sets@finite_sets_below[N], below_arrays[N,T]
A: VAR ARRAY[below[N] -> T]
mv, mv1, mv2, x, c: VAR T
ii: VAR below[N]
is_majority(mv, A): bool = 2*card({ii | A(ii) = mv}) > N
maj_exists(A): bool = (EXISTS (mv: T): is_majority(mv,A))
maj(A): {mv | maj_exists(A) => is_majority(mv,A)}
is_majority_unique: LEMMA is_majority(mv1,A) AND is_majority(mv2,A)
IMPLIES mv1 = mv2
maj_lem: LEMMA is_majority(mv,A) IFF
maj_exists(A) AND maj(A) = mv
maj_subset: LEMMA (EXISTS (IDS: finite_set[below(N)]):
2*card(IDS) > N
AND (FORALL ii: IDS(ii) IMPLIES A(ii) = mv))
IMPLIES is_majority(mv,A)
maj_in_array: LEMMA is_majority(mv,A) IMPLIES
(EXISTS ii: A(ii) = mv)
% ===================== Some Special Arrays ===================
constant_array(c): below_array = (LAMBDA ii: c)
is_majority_const: LEMMA is_majority(c, constant_array(c))
maj_const: LEMMA maj_exists(constant_array(c)) AND
maj(constant_array(c)) = c
END majority_array
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
