Quelle  bounded_integers.pvs

% every above (below) bounded, non-empty set of integers has a greatest
% (least) element. This also holds for any subtype T of the integers.
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: 2003/04
%
% remove_greatest, remove_greatest_monotone, intersection_greatest, and
% intersection_least added 13 Jan 2005 by Jerry James (jamesj@acm.org),
% University of Kansas

bounded_integers[T: TYPE FROM int]: THEORY

BEGIN

  IMPORTING
    non_empty_bounded_sets[T]

  Su, Su1, Su2: VAR (non_empty_bounded_above?)
  Sl, Sl1, Sl2: VAR (non_empty_bounded_below?)
  i, j: VAR T
  S: VAR set[T]
  c: VAR nat

  non_empty_bounded_above_has_greatest_lem: LEMMA
    S(i) & upper_bound?[T](j, S, <=) & c = j - i => has_greatest?(S, <=)

  non_empty_bounded_above_has_greatest: JUDGEMENT
    (non_empty_bounded_above?) SUBTYPE_OF (has_greatest?(<=))

  non_empty_bounded_below_has_least_lem: LEMMA
    S(i) & lower_bound?[T](j, S, <=) & c = i - j => has_least?(S, <=)

  non_empty_bounded_below_has_least: JUDGEMENT
    (non_empty_bounded_below?) SUBTYPE_OF (has_least?(<=))

  remove_least: LEMMA
    nonempty?(remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl),
                     Sl)) =>
      least[T](restrict[[real, real], [T, T], bool](<=))(Sl) <
      least[T](restrict[[real, real], [T, T], bool](<=))(
        remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl), Sl))

  remove_least_monotone: LEMMA
    subset?(Sl1, Sl2) =>
    subset?(
      remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1), Sl1),
      remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl2), Sl2))

  remove_greatest: LEMMA
    nonempty?(remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su),
                     Su)) =>
      greatest[T](restrict[[real, real], [T, T], bool](<=))(
        remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su), Su))
      < greatest[T](restrict[[real, real], [T, T], bool](<=))(Su)

  remove_greatest_monotone: LEMMA
    subset?(Su1, Su2) =>
    subset?(
      remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1), Su1),
      remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2), Su2))

  intersection_greatest: LEMMA
    disjoint?(Su1, Su2) OR has_greatest?(intersection(Su1, Su2), <=)

  intersection_least: LEMMA
    disjoint?(Sl1, Sl2) OR has_least?(intersection(Sl1, Sl2), <=)

END bounded_integers