Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 28.9.2014 mit Größe 605 B

Quellcode-Bibliothek 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

quality91%