Quelle  bounded_sets.pvs

% some judgements about boundedness properties of sets
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004
%
% added preservation by set operators (other than remove). Alfons Geser, Jan 2005

bounded_sets[T: TYPE, R: pred[[T, T]]]: THEORY

BEGIN

  IMPORTING bounded_orders[T]

  s: VAR T
  Su: VAR (bounded_above?[T](R))
  Sl: VAR (bounded_below?[T](R))
  Sb: VAR (bounded?[T](R))

  least_bounded_above_is_bounded_above: JUDGEMENT
    (least_bounded_above?(R)) SUBTYPE_OF (bounded_above?(R))

  greatest_bounded_below_is_bounded_below: JUDGEMENT
    (greatest_bounded_below?(R)) SUBTYPE_OF (bounded_below?(R))

  bounded_is_bounded_above: JUDGEMENT
    (bounded?(R)) SUBTYPE_OF (bounded_above?(R))
 
  bounded_is_bounded_below: JUDGEMENT
    (bounded?(R)) SUBTYPE_OF (bounded_below?(R))
 
  tightly_bounded_is_bounded: JUDGEMENT
    (tightly_bounded?(R)) SUBTYPE_OF (bounded?(R))

  tightly_bounded_above: JUDGEMENT
    (tightly_bounded?(R)) SUBTYPE_OF (least_bounded_above?(R))
 
  tightly_bounded_below: JUDGEMENT
    (tightly_bounded?(R)) SUBTYPE_OF (greatest_bounded_below?(R))

  % preservation by set operators

  intersection1_preserves_bounded_above: JUDGEMENT
    intersection(Su, (S: set[T])) HAS_TYPE (bounded_above?[T](R))

  intersection2_preserves_bounded_above: JUDGEMENT
    intersection((S: set[T]), Su) HAS_TYPE (bounded_above?[T](R))

  difference_preserves_bounded_above: JUDGEMENT
    difference(Su: (bounded_above?[T](R)), S: set[T]) HAS_TYPE
      (bounded_above?[T](R))

  remove_preserves_bounded_above: JUDGEMENT
    remove[T](s, Su) HAS_TYPE (bounded_above?[T](R))

  intersection1_preserves_bounded_below: JUDGEMENT
    intersection(Sl, (S: set[T])) HAS_TYPE (bounded_below?[T](R))

  intersection2_preserves_bounded_below: JUDGEMENT
    intersection((S: set[T]), Sl) HAS_TYPE (bounded_below?[T](R))

  difference_preserves_bounded_below: JUDGEMENT
    difference(Sl, (S: set[T])) HAS_TYPE
      (bounded_below?[T](R))

  remove_preserves_bounded_below: JUDGEMENT
    remove[T](s, Sl) HAS_TYPE (bounded_below?[T](R))

  intersection1_preserves_bounded: JUDGEMENT
    intersection(Sb, (S: set[T])) HAS_TYPE (bounded?[T](R))

  intersection2_preserves_bounded: JUDGEMENT
    intersection((S: set[T]), Sb) HAS_TYPE (bounded?[T](R))

  difference_preserves_bounded: JUDGEMENT
    difference(Sb, (S: set[T])) HAS_TYPE (bounded?[T](R))

  remove_preserves_bounded: JUDGEMENT
    remove[T](s, Sb) HAS_TYPE (bounded?[T](R))

END bounded_sets