Quelle  ordered_int.pvs   Sprache: PVS

%-------------------------------------------------------------------------
%
%  Specialization of the ordered_subset theory to sets of integers.
%
%  For PVS version 3.2.  January 31, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[int], infinite_sets_def[int], orders[int],
%    real_props, relation_props2[int, int, int, int], relations[int],
%    restrict_order_props[real, int], sets[int]
%  finite_sets: finite_sets_inductions, finite_sets_minmax
%  orders: bounded_orders[int], closure_ops[int], indexed_sets_extra,
%    minmax_orders[int], ordered_int, ordered_subset[int],
%    relation_iterate[int], relations_extra[int]
%
%-------------------------------------------------------------------------
ordered_int: THEORY
 BEGIN

  IMPORTING infinite_sets_def[int], restrict_order_props[real, int]
  IMPORTING real_props, minmax_orders[int], ordered_subset[int]

  i: VAR int
  pre: VAR (prefix?(<=))
  suf: VAR (suffix?(<=))

  % Attempting to use the ordered_subset definitions directly in the
  % judgements below causes PVS 3.2 to complain that the variable '<=' is
  % undeclared.  Changing to 'reals.<=' causes the parser to choke on the '.'.
  upto(i): MACRO (prefix?(<=)) = upto(i, <=)
  below(i): MACRO (prefix?(<=)) = below(i, <=)
  above(i): MACRO (suffix?(<=)) = above(i, <=)
  upfrom(i): MACRO (suffix?(<=)) = upfrom(i, <=)

  upto_has_greatest: JUDGEMENT upto(i) HAS_TYPE (has_greatest?(<=))
  below_has_greatest: JUDGEMENT below(i) HAS_TYPE (has_greatest?(<=))
  above_has_least: JUDGEMENT above(i) HAS_TYPE (has_least?(<=))
  upfrom_has_least: JUDGEMENT upfrom(i) HAS_TYPE (has_least?(<=))

  prefix_empty: THEOREM FORALL pre: is_finite(pre) IMPLIES empty?(pre)

  prefix_below: THEOREM
    FORALL pre: empty?(pre) OR full?(pre) OR (EXISTS i: pre = below(i))

  prefix_upto: THEOREM
    FORALL pre: empty?(pre) OR full?(pre) OR (EXISTS i: pre = upto(i))

  suffix_empty: THEOREM FORALL suf: is_finite(suf) IMPLIES empty?(suf)

  suffix_upfrom: THEOREM
    FORALL suf: empty?(suf) OR full?(suf) OR (EXISTS i: suf = upfrom(i))

  suffix_above: THEOREM
    FORALL suf: empty?(suf) OR full?(suf) OR (EXISTS i: suf = above(i))

  unrelated_empty: THEOREM FORALL i: empty?(unrelated(i, <=))

 END ordered_int