SSL finite_bags_inductions.pvs

finite_bags_inductions[T: TYPE]: THEORY
%-------------------------------------------------------------------------
%
%  Induction scheme for finite bags, plural in name of this theory is 
%  misleading at this moment.
%
%    Author:  David Griffioen.      (CWI Amsterdam and KUN)
%
%-------------------------------------------------------------------------
BEGIN

  IMPORTING finite_bags_aux[T]

  x:  VAR T
  b:  VAR finite_bag
  pb: VAR pred[finite_bag[T]]
  n:  VAR nat

  cardinal_induction: LEMMA
     (FORALL b : pb(b)) IFF (FORALL n, b : card(b) = n IMPLIES pb(b)) 

  finite_bag_induction: THEOREM
          (FORALL pb: (pb(emptybag[T]) AND 
                      (FORALL x,b: pb(b) IMPLIES pb(insert(x,b))))
                      IMPLIES (FORALL b: pb(b)))

END finite_bags_inductions