Quelle  bags_to_sets.pvs

bags_to_sets [T:TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines a function bag_to_set that collapses a bag
% to a set eliminating the count.
%
%    Authors:  Rick Butler               (NASA Langley)
%              David Griffioen           (CWI Amsterdam and KUN)
%              Lee Pike                  (NASA Langley)
%------------------------------------------------------------------------

BEGIN
  
  IMPORTING bags[T]
  
  t: VAR T
  A,B,b: VAR bag

  bag_to_set(b): set[T] = {t: T | b(t) > 0}

  strict_subbag?(A,B): bool = strict_subset?(bag_to_set(A), bag_to_set(B))

  insert_bag_lem       : LEMMA bag_to_set(insert(t, B)) = add(t,bag_to_set(B))

  purge_bag_lem        : LEMMA bag_to_set(purge(t, B)) = remove(t,bag_to_set(B))

  bag_union_lem        : LEMMA bag_to_set(union(A, B)) = 
                                 union(bag_to_set(A), bag_to_set(B))

  bag_intersection_lem : LEMMA bag_to_set(intersection(A,B)) = 
                                 intersection(bag_to_set(A),bag_to_set(B))

  subbag_lem           : LEMMA subbag?(A,B) IMPLIES 
                                 subset?(bag_to_set(A),bag_to_set(B))

  bag_to_set_emptybag  : LEMMA bag_to_set(emptybag) = emptyset

  empty_bts_bag        : LEMMA empty?(bag_to_set(b)) IMPLIES empty?(b)

  bag_intersection_commutative: LEMMA intersection(A,B) = intersection(B, A)

  bag_union_commutative: LEMMA union(A,B) = union(B, A)

  bag_plus_lem         : LEMMA bag_to_set(plus(A,B)) = 
                                 union(bag_to_set(A),bag_to_set(B))

  extract_empty_or_singlton_set: 
                       LEMMA singleton?(bag_to_set(extract(t,A))) OR
                               empty?(bag_to_set(extract(t,A))) 

  extract_singleton  : LEMMA singleton?(bag_to_set(extract(t,A))) IMPLIES 
                               singleton(t) = bag_to_set(extract(t,A))

  bag_disj_set       : LEMMA disjoint?(A,B) IMPLIES disjoint?(bag_to_set(A),bag_to_set(B))

  bag_set_dist_union : LEMMA bag_to_set(union(A,B)) = union(bag_to_set(A),bag_to_set(B)) 

  bag_non_empty      : LEMMA NOT empty?(A) IMPLIES nonempty?(bag_to_set(A))

END bags_to_sets