Quelle majority_seq.pvs Sprache: PVS

majority_seq[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 seqs[T], finite_sets@finite_sets_below

  fs: VAR finite_sequence[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]

  length_eq_1: LEMMA maj( (# length := 1, seq := f1 #) ) = f1(0)

  n: VAR posnat
  c: VAR T

%  const_seq(n,c): finite_sequence[T] = (# length := n,
%                           seq := (LAMBDA (i: below(n)): c) #)

  is_majority_const: LEMMA is_majority(c, const_seq(n,c))

  maj_const:         LEMMA maj_exists(const_seq(n,c)) AND
                           maj(const_seq(n,c)) = c

END majority_seq

quality97%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.