%-------------------------------------------------------------------------
%
% Functions for traversing a well-ordered set. In particular, these
% functions yield the first, last, and next elements of such a set. See
% below for an explanation of the fairly useless function for yielding
% the previous element of such a set.
%
% For PVS version 3.2. February 28, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[T], relation_props2[T, T, T, T], relations[T], sets[T]
% finite_sets: finite_sets_inductions, finite_sets_minmax
% orders: bounded_orders[T], closure_ops[T], indexed_sets_extra,
% minmax_orders[T], ordered_subset[T], relation_iterate[T],
% relations_extra[T], well_ordered_traversal[T]
%
%-------------------------------------------------------------------------
well_ordered_traversal[T: TYPE]: THEORY
BEGIN
IMPORTING ordered_subset[T], minmax_orders[T]
t, r, s: VAR T
<: VAR (well_ordered?)
% ==========================================================================
% The first element of a well-ordering
% ==========================================================================
has_first?(<): bool = EXISTS t: TRUE
well_ordering_has_first: LEMMA
FORALL <:
has_first?(<) IMPLIES has_least?(fullset[T], reflexive_closure(<))
first(<: (has_first?)): (least?(fullset[T], reflexive_closure(<))) =
least(reflexive_closure(<))(fullset[T])
% All but the first element. This is often useful for stating the elements
% which have a prev. See below.
nonfirst(<): set[T] =
IF has_first?(<) THEN {t | t /= first(<)} ELSE emptyset[T] ENDIF
% ==========================================================================
% The last element of a well-ordering
% ==========================================================================
has_last?(<): bool = has_greatest?(fullset[T], reflexive_closure(<))
last(<: (has_last?)): (greatest?(fullset[T], reflexive_closure(<))) =
greatest(reflexive_closure(<))(fullset[T])
% All but the last element. This is often useful for stating the elements
% which have a next.
nonlast(<): set[T] =
IF has_last?(<) THEN {t | t /= last(<)} ELSE fullset[T] ENDIF
% ==========================================================================
% The successor of a given element
% ==========================================================================
has_next?(<)(t): bool = nonempty?(above(t, <))
well_ordering_has_next: LEMMA
FORALL <, t:
has_next?(<)(t) IMPLIES has_least?(above(t, <), reflexive_closure(<))
next(<)(t: (has_next?(<))): (least?(above(t, <), reflexive_closure(<))) =
least(reflexive_closure(<))(above(t, <))
last_no_next: LEMMA FORALL <: has_last?(<) => NOT has_next?(<)(last(<))
last_is_last: LEMMA FORALL <: has_last?(<) => full?(upto(last(<), <))
% ==========================================================================
% The predecessor of a given element
% ==========================================================================
% The prev operator is defined in such a way that it is almost useless.
% This is because prev is not well-defined for arbitrary well-ordered sets.
% For example, consider the set of all even natural numbers, and the set of
% all odd natural numbers. Both sets are well-ordered by <. Now consider
% the set of all natural numbers, ordered as follows:
%
% order(x, y) = x < y if x and y are both even, or both odd
% FALSE if x is odd and y is even
% TRUE if x is even and y is odd
%
% One can easily show that that order is a well-ordering of the natural
% numbers. Any given natural number has a well-defined next element in this
% ordering. However, there is no well-defined previous element of 1.
%
% The following definitions are really placeholders. For any given well
% ordering, give a JUDGEMENT stating the elements for which has_prev? is
% satisfied.
has_prev?(<)(t): bool = EXISTS (r: (has_next?(<))): next(<)(r) = t
well_ordering_has_prev: LEMMA
FORALL <, t:
has_prev?(<)(t) IMPLIES
has_greatest?(below(t, <), reflexive_closure(<))
prev(<)(t: (has_prev?(<))): (greatest?(below(t, <), reflexive_closure(<))) =
greatest(reflexive_closure(<))(below(t, <))
END well_ordered_traversal
¤ Dauer der Verarbeitung: 0.1 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.
|
