bags [T: TYPE] : THEORY
%------------------------------------------------------------------------
%
%  Fundamental definitions and properties of bags.
%
%    Authors: Rick Butler      NASA Langley
%             Lee Pike         NASA Langley
%------------------------------------------------------------------------

 BEGIN
  x,y,t: VAR T

  bag: TYPE = [T -> nat]
  a,b,c: VAR bag
  n: VAR nat

  count(x,b): nat = b(x)

  emptybag         : bag = (LAMBDA t: 0)

  singleton_bag(t) : bag = (LAMBDA (x: T): IF x = t THEN 1 ELSE 0 ENDIF)

  insert(x,b)      : bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF)

  purge(x,b)       : bag = (LAMBDA t: IF x = t THEN 0 ELSE b(t) ENDIF)

  delete(x,b,n)    : bag = (LAMBDA t: IF x = t THEN
                                        IF b(t) >= n THEN b(t) - n ELSE 0 ENDIF 
                                      ELSE b(t) ENDIF)

  extract(x,b)     : bag = (LAMBDA t: IF x = t THEN b(t) ELSE 0 ENDIF)

  plus(a,b)        : bag = (LAMBDA t: a(t) + b(t))

  union(a,b)       : bag = (LAMBDA t: max(a(t),b(t))) 

  intersection(a,b): bag = (LAMBDA t: min(a(t),b(t)))

  % --------- some predicates over bags ------------

  member(x,b)        : bool = b(x) > 0

  empty?(b)          : bool = (FORALL x: b(x) = 0)

  nonempty_bag?(b)   : bool = NOT empty?(b)

  eqmult(x,a,b)      : bool = (a(x) = b(x))
   
  subbag?(a,b)       : bool = (FORALL x: a(x) <= b(x))

  proper_subbag?(a,b): bool = (FORALL x: a(x) < b(x))

  disjoint?(a, b)    : bool = empty?(intersection(a, b))

% ---------- useful lemmas ----------

  emptybag_is_empty?    : LEMMA empty?(b) IFF b = emptybag

  delete_purge          : LEMMA n >= b(x) IMPLIES delete(x,b,n) = purge(x,b)

  insert_unique         : LEMMA insert(x,a) = insert(x,b) IMPLIES a = b

  insert_exchange       : LEMMA insert(x,insert(y,b)) = insert(y,insert(x,b))

  delete_insert         : LEMMA n > 0 IMPLIES
                                  (delete(x,insert(x,b),n) = delete(x,b,n-1))

  insert_delete         : LEMMA b(x) > 0 IMPLIES insert(x,delete(x,b,1)) = b 

  delete_insert_diff    : LEMMA x /= y IMPLIES
                            (delete(x,insert(y,b),n) = insert(y,delete(x,b,n)))

  decomposition         : LEMMA NOT empty?(b) IMPLIES 
                                  (EXISTS a,x: b = insert(x,a))

  bag_equality          : LEMMA a = b IFF (FORALL x: eqmult(x,a,b))

  subbag_empty          : LEMMA subbag?(emptybag,a)

  subbag_equality       : LEMMA a = b IFF subbag?(a,b) AND subbag?(b,a)

  subbag_trans          : LEMMA subbag?(a,b) AND subbag?(b,c) IMPLIES subbag?(a,c)

% because of empty types the following is not provable -- look into it later 
% proper_subbag_rew     : LEMMA proper_subbag?(a,b) IMPLIES subbag?(a,b) AND a /= b

  bag_plus_union        : LEMMA plus(union(a,b),intersection(a,b)) = plus(a,b) 
  
  bag_plus_comm         : LEMMA plus(a,b) = plus(b,a)   
   
  plus_emptybag         : LEMMA plus(emptybag,a) = a
  
  bag_plus_insert       : LEMMA plus(insert(x,a),b) = insert(x,plus(a,b))

  bag_distributive      : LEMMA intersection(a,union(b,c)) = 
                                  union(intersection(a,b),intersection(a,c))

  extract_subbag        : LEMMA subbag?(extract(x,a), a) 
  
  extract_disj          : LEMMA x /= y IMPLIES disjoint?(extract(x,a), extract(y,a))

  bag_disj_comm         : LEMMA disjoint?(a,b) = disjoint?(b,a)

  bag_union_comm        : LEMMA union(a,b) = union(b,a)

  bag_union_fix_pt      : LEMMA union(a,a) = a 


  bag_purge_extract       : LEMMA a = union(purge(x,a), extract(x,a))

  bag_disj_extract_perge  : LEMMA disjoint?(extract(x,a), purge(x,a))

  bag_extract_union_subbag: LEMMA x /= y IMPLIES subbag?(union(extract(x,a),extract(y,a)),a) 

  union_upper_bound       : LEMMA subbag?(a, c) and subbag?(b, c) IMPLIES 
                                    subbag?(union(a, b), c)

END bags