%-------------------------------------------------------------------------
%
% Ranges of numbers.
%
% For PVS version 3.2. February 8, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[T], orders[T], relations[T], sets[T]
% finite_sets: finite_sets_inductions, finite_sets_minmax
% orders: bounded_orders[T], minmax_orders[T], range[T],
% relations_extra[T]
%
%-------------------------------------------------------------------------
range[T: TYPE+ FROM real]: THEORY
BEGIN
IMPORTING minmax_orders[T]
t, r, r1, r2: VAR T
S: VAR set[T]
% A convenient shorthand
lesseq: MACRO pred[[T, T]] = restrict[[real, real], [T, T], boolean](<=)
% Minima- and maxima-related definitions for open/closed ranges
has_non_least?(S): bool =
EXISTS r:
(FORALL (t: (S)): r < t) AND
(FORALL r1: (FORALL (t: (S)): r1 < t) IMPLIES r1 <= r)
has_non_greatest?(S): bool =
EXISTS r:
(FORALL (t: (S)): t < r) AND
(FORALL r1: (FORALL (t: (S)): t < r1) IMPLIES r <= r1)
not_has_least?(S): MACRO bool =
(NOT has_least?(S, lesseq)) OR has_non_least?(S)
not_has_greatest?(S): MACRO bool =
(NOT has_greatest?(S, lesseq)) OR has_non_greatest?(S)
% ==========================================================================
% The base range type
% ==========================================================================
range: TYPE+ =
{S | FORALL (lo, hi: (S)), r: lo <= r AND r <= hi IMPLIES member(r, S)}
R: VAR range
% ==========================================================================
% Ranges with maxima and minima
% ==========================================================================
min_range: TYPE+ = {R | has_least?(R, lesseq)}
max_range: TYPE+ = {R | has_greatest?(R, lesseq)}
% ==========================================================================
% Ranges with no greatest lower or least upper element
% ==========================================================================
no_least(t): bool = NOT has_least?({r | r <= t}, lesseq)
no_greatest(t): bool = NOT has_greatest?({r | t <= r}, lesseq)
% ==========================================================================
% Closed, open, closed/open, and open/closed ranges
% ==========================================================================
c_range: TYPE+ = {R | has_least?(R, lesseq) AND has_greatest?(R, lesseq)}
oc_range: TYPE = {R | not_has_least?(R) AND has_greatest?(R, lesseq)}
co_range: TYPE = {R | has_least?(R, lesseq) AND not_has_greatest?(R)}
o_range: TYPE+ = {R | not_has_least?(R) AND not_has_greatest?(R)}
% The nontrivial range types
ntc_range: TYPE = {R: c_range | least(lesseq)(R) < greatest(lesseq)(R)}
nto_range: TYPE = {R: o_range | nonempty?(R)}
% Non-open ranges are nonempty
c_range_is_nonempty: JUDGEMENT c_range SUBTYPE_OF (nonempty?[T])
ntc_range_is_nonempty: JUDGEMENT ntc_range SUBTYPE_OF (nonempty?[T])
oc_range_is_nonempty: JUDGEMENT oc_range SUBTYPE_OF (nonempty?[T])
co_range_is_nonempty: JUDGEMENT co_range SUBTYPE_OF (nonempty?[T])
% ==========================================================================
% Constructing ranges
% ==========================================================================
% Constructing bounded ranges
closed_range(r1, (r2: {r | r1 <= r})): c_range = {r | r1 <= r AND r <= r2}
nontrivial_closed_range(r1, (r2: {r | r1 < r})): ntc_range =
{r | r1 <= r AND r <= r2}
open_closed_range(r1, (r2: {r | r1 < r})): oc_range =
{r | r1 < r AND r <= r2}
closed_open_range(r1, (r2: {r | r1 < r})): co_range =
{r | r1 <= r AND r < r2}
open_range(r1, r2): o_range = {r | r1 < r AND r < r2}
nontrivial_open_range(r1, (r2: {r | EXISTS t: r1 < t AND t < r})):
nto_range = {r | r1 < r AND r < r2}
% Constructing unbounded ranges
open_closed_range(r: (no_least)): oc_range = {r1 | r1 <= r}
closed_open_range(r: (no_greatest)): co_range = {r1 | r <= r1}
left_open_range(r: (no_least)): nto_range = {r1 | r1 < r}
right_open_range(r: (no_greatest)): nto_range = {r1 | r < r1}
% The closed constructors are complete
c_range_construction: THEOREM
FORALL (R: c_range):
EXISTS r1, (r2: {r | r1 <= r}): R = closed_range(r1, r2)
ntc_range_construction: THEOREM
FORALL (R: ntc_range):
EXISTS r1, (r2: {r | r1 < r}): R = nontrivial_closed_range(r1, r2)
% least and greatest for constructed ranges
c_range_endpoints: THEOREM
FORALL (R: c_range): least(lesseq)(R) <= greatest(lesseq)(R)
ntc_range_endpoints: THEOREM
FORALL (R: ntc_range): least(lesseq)(R) < greatest(lesseq)(R)
c_range_min: THEOREM
FORALL r1, (r2: {r | r1 <= r}): least(lesseq)(closed_range(r1, r2)) = r1
c_range_max: THEOREM
FORALL r1, (r2: {r | r1 <= r}):
greatest(lesseq)(closed_range(r1, r2)) = r2
ntc_range_min: THEOREM
FORALL r1, (r2: {r | r1 < r}):
least(lesseq)(nontrivial_closed_range(r1, r2)) = r1
ntc_range_max: THEOREM
FORALL r1, (r2: {r | r1 < r}):
greatest(lesseq)(nontrivial_closed_range(r1, r2)) = r2
oc_range_max1: THEOREM
FORALL r1, (r2: {r | r1 < r}):
greatest(lesseq)(open_closed_range(r1, r2)) = r2
oc_range_max2: THEOREM
FORALL (r: (no_least)): greatest(lesseq)(open_closed_range(r)) = r
co_range_min1: THEOREM
FORALL r1, (r2: {r | r1 < r}):
least(lesseq)(closed_open_range(r1, r2)) = r1
co_range_min2: THEOREM
FORALL (r: (no_greatest)): least(lesseq)(closed_open_range(r)) = r
END range
¤ 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.
|
