Quelle bags_aux.pvs Sprache: PVS

bags_aux[T:TYPE]:THEORY
%------------------------------------------------------------------------
%
%  Additional properties about bags
%
%     Author: David Griffioen      (CWI Amsterdam and KUN)
%
%------------------------------------------------------------------------
BEGIN

  IMPORTING bags[T], bags_to_sets[T]

  x,y,e: VAR T
  b:     VAR bag
  n,xn:  VAR nat
  p,q: VAR pred[T]

%% ===== choose and rest for bags =====

  choose(b: (nonempty_bag?)):T = choose(bag_to_set(b))

  rest(b):bag = IF empty?(b) THEN b ELSE delete(choose(b),b,1) ENDIF

  choose_gt_zero:     LEMMA nonempty_bag?(b) => b(choose(b)) > 0

  insert_choose_rest: LEMMA nonempty_bag?(b) => insert(choose(b),rest(b)) = b

%% ===== on filters =====
% Definition of filter for bags, it takes a bag and a predicate and
% returns the bag of those elements that satisfy the predicate.

  filter(b,p):bag   = (LAMBDA x: IF p(x) THEN b(x) ELSE 0 ENDIF)

  filter_emptybag:    THEOREM filter(emptybag,p) = emptybag

  filter_insert:      LEMMA filter(insert(x,b),p) =
                               IF p(x) THEN insert(x,filter(b,p))
                                       ELSE filter(b,p) ENDIF

  filter_delete:      LEMMA filter(delete(x,b,n),p) = delete(x,filter(b,p),n)

  filter_prop:        LEMMA (FORALL x: p(x) => q(x)) =>
                            subbag?(filter(b,p),filter(b,q))

END bags_aux

quality84%

¤ Dauer der Verarbeitung: 0.20 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.