| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle well_ordered_traversal.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % 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 (jamesj@acm.org), 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.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28