Quellcode-Bibliothek finite_bags.pvs

finite_bags[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines finite bags and its cardinality
%
%    Authors:  Rick Butler              (NASA Langley)
%              David.Griffioen          (CWI Amsterdam and KUN)
%              Lee Pike                 (NASA Langley)
%------------------------------------------------------------------------
BEGIN

   IMPORTING bags[T], 
             finite_sets@finite_sets_sum_real[T],
             finite_sets@finite_sets_inductions[T], bags_to_sets[T]

   x,y,t,e: VAR T
   b: VAR bag
   n,xn: VAR nat

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

   is_finite(b): bool = is_finite(bag_to_set(b)) 
   
   finite_bag: TYPE = {b: bag | is_finite(b)}

   nonempty_finite_bag: TYPE = {b: finite_bag | NOT empty?(b)}

   A,B,C: VAR finite_bag

   JUDGEMENT bag_to_set(B) HAS_TYPE finite_set 

%  The card_TCC1: OBLIGATION relies on a JUDGEMENT in finite_sets_sum_real
%  that is no longer firing.  Since it is unnamed it is difficult to fix it.


   card(B): nat = sum(bag_to_set(B),(LAMBDA t: B(t)))

   finite_bag          : THEOREM is_finite(B) IMPLIES is_finite(LAMBDA x: B(x) > 0)

   finite_emptybag     : THEOREM is_finite(emptybag[T]);

   finite_singleton_bag: THEOREM is_finite(singleton_bag(t))

   finite_insert       : THEOREM is_finite(insert(t, B))

   finite_purge        : THEOREM is_finite(purge(t, B))

   finite_delete       : THEOREM is_finite(delete[T](t, B, n))

   finite_bag_union    : THEOREM is_finite(union(A, B))

   finite_bag_intersection: THEOREM is_finite(intersection[T](A, B))

   finite_bag_plus     : LEMMA is_finite(plus(A,B))    

   finite_update       : LEMMA is_finite(B WITH [x := xn])

   finite_set          : THEOREM is_finite(bag_to_set(A))

   finite_extract      : THEOREM is_finite(extract(x,B)) 


  JUDGEMENT nonempty_finite_bag SUBTYPE_OF (nonempty_bag?[T])

  JUDGEMENT singleton_bag(x) HAS_TYPE finite_bag

  JUDGEMENT union(A,B), intersection(A,B), plus(A,B) 
                     HAS_TYPE finite_bag

  NA,NB: VAR nonempty_finite_bag
  JUDGEMENT union(A,NB), plus(A,NB) HAS_TYPE nonempty_finite_bag

  JUDGEMENT union(NA,B), plus(NA,B) HAS_TYPE nonempty_finite_bag

  JUDGEMENT insert(x,A)   HAS_TYPE nonempty_finite_bag

  JUDGEMENT purge(x,A)    HAS_TYPE finite_bag

  JUDGEMENT delete(x,A,n) HAS_TYPE finite_bag

  JUDGEMENT emptybag      HAS_TYPE finite_bag

  JUDGEMENT extract(x,A) HAS_TYPE finite_bag 

%  ---------- Some Useful Lemmas ----------

   card_emptybag      : THEOREM card(emptybag[T]) = 0

   card_bag_empty?    : THEOREM (card(B) = 0) = empty?(B)
 
   card_singleton_bag : THEOREM card(singleton_bag(t)) = 1

   card_subbag?       : THEOREM subbag?(A,B) IMPLIES card(A) <= card(B)

   card_bag_particular: THEOREM card(B WITH [x := xn]) = card(B) - B(x) + xn  

   card_bag_delete    : LEMMA card(delete(e,B,n)) = card(B) - min(B(e),n)
 
   card_bag_insert    : LEMMA card(insert(x,B)) = card(B) + 1

   card_nonempty_bag? : LEMMA card(B) > 0 IFF nonempty_bag?(B)
 
   card_disj_intersection : LEMMA disjoint?(A,B) IMPLIES
                                    card(intersection(A,B)) = 0

   sum_bag_disj_union     : LEMMA disjoint?(A,B) IMPLIES
                                    sum(bag_to_set(A),(LAMBDA (t:T): union(A,B)(t)))
                                      = sum(bag_to_set(A), (LAMBDA (t:T): A(t)))

   card_extract           : LEMMA card(extract(x,A)) <= card(A)

   card_extract_bag       : LEMMA card(extract(x,A)) = A(x)

   card_disjoint_add      : LEMMA disjoint?(A,B) IMPLIES 
                                  card(union(A,B)) = card(A) + card(B)
  
   card_purge_extract     : LEMMA card(purge(x,A)) = card(A) - card(extract(x,A))

   card_union_extract_add : LEMMA x /= y IMPLIES 
                                  card(union(extract(x,A),extract(y,A))) = A(x) + A(y)

   card_union_extract     : LEMMA x /= y IMPLIES 
                                  card(union(extract(x,A),extract(y,A))) <= card(A)

   card_geq_count         : LEMMA A(x) <= card(A) 

   card_geq_count_add     : LEMMA x /= y IMPLIES A(x) + A(y) <= card(A)


END finite_bags