Impressum finite_bags_aux.pvs

finite_bags_aux[T: TYPE]: THEORY
%-------------------------------------------------------------------------
%
% Additional properties of finite bags. 
%
%    Author: David Griffioen   (CWI Amsterdam and KUN)
%
%-------------------------------------------------------------------------
BEGIN  

  IMPORTING finite_bags[T], bags_aux[T] 

  x,e:  VAR T
  b:    VAR finite_bag
  p:    VAR pred[T]
  n,xn: VAR nat

  finite_bag_rest: LEMMA is_finite(rest[T](b))

  JUDGEMENT rest(b) HAS_TYPE finite_bag

  card_bag_rest      : LEMMA nonempty_bag?(b) IMPLIES
     card(b) = card(rest(b)) + 1 

  %% ===== on finite bags and filters =====

  finite_filter      : THEOREM is_finite(filter(b,p))

  JUDGEMENT filter(b,p) HAS_TYPE finite_bag

  card_filter_insert: LEMMA card(filter(insert(x,b),p)) =
                               card(filter(b,p)) + IF p(x) THEN 1 ELSE 0 ENDIF

  card_filter_delete: LEMMA card(filter(delete(x,b,n),p)) =
                               card(filter(b,p)) - IF p(x) THEN min(b(x),n) 
                                                    ELSE 0 ENDIF

END finite_bags_aux