Quelle  finite_bags_minmax.pvs

%----------------------------------------------------------------------------
% Lee Pike 
% lee.s.pike@nasa.gov
% Formal Methods Group, NASA Langley Research Center
%
% PVS Version 3.1
%
% PURPOSE: 
% Define the minimum and maximum for ordered finite bags.
%----------------------------------------------------------------------------

finite_bags_minmax[T: NONEMPTY_TYPE, 
                   leq: (total_order?[T])]: THEORY

BEGIN 

IMPORTING
  finite_bags[T],
  finite_sets@finite_sets_minmax[T, leq],
  finite_bags_inductions[T]

  D              : VAR nonempty_finite_bag

  max(D)         : T = max(bag_to_set(D))

  min(D)         : T = min(bag_to_set(D)) 

  max_member     : LEMMA member(max(D), D)

  min_member     : LEMMA member(min(D), D)

END finite_bags_minmax