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