%-----------------------------------------------------------------------------
% Ascending chains, a helper for the theory of limits of sequences of
% countable length.
%
% FIXME: Should we use the NASA orders/monotone_functions theory instead?
%
% Author: Jerry James <[email protected]>
%
% This file and its accompanying proof file are distributed under the CC0 1.0
% Universal license: http://creativecommons.org/publicdomain/zero/1.0/.
%
% Version history:
% 2007 Feb 14: PVS 4.0 version
% 2011 May 6: PVS 5.0 version
% 2013 Jan 14: PVS 6.0 version
%-----------------------------------------------------------------------------
ascending_chains[T: TYPE, <=: (partial_order?[T])]: THEORY
BEGIN
t, u: VAR T
n, m: VAR nat
ascending_chain?(f: [nat -> T]): bool = FORALL n: f(n) <= f(n + 1)
ascending_chain: TYPE = (ascending_chain?)
chain: VAR ascending_chain
ascending_chain?_def: THEOREM
FORALL chain, n, m: n <= m IMPLIES chain(n) <= chain(m)
upperbound?(chain)(t): bool = FORALL n: chain(n) <= t
least_upperbound?(chain)(t): bool =
upperbound?(chain)(t) AND
(FORALL u: upperbound?(chain)(u) IMPLIES t <= u)
least_upperbound_inj: THEOREM
FORALL chain, t, u:
least_upperbound?(chain)(t) AND least_upperbound?(chain)(u) IMPLIES
t = u
bounded_above?(chain): bool = EXISTS t: upperbound?(chain)(t)
END ascending_chains
¤ 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.
|
