%-------------------------------------------------------------------------
%
% Specialization of the ordered_subset theory to sets of integers.
%
% For PVS version 3.2. January 31, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
