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