% pointwise orders on functions whose domain is finite
% their strict part preserves well-founded orders
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
finite_pointwise_orders[D, R: TYPE]: THEORY
BEGIN
ASSUMING
domain_finiteness: ASSUMPTION is_finite_type[D]
ENDASSUMING
IMPORTING
numbers_infinite, % to discharge a TCC of infinite_pigeonhole
pointwise_orders[D, R],
well_foundedness,
infinite_pigeonhole[nat, D],
integer_enumerations[nat]
d: VAR D
r: VAR R
n: VAR nat
rel: VAR (transitive?[R])
seq: VAR [nat -> [D -> R]]
g: VAR (preserves[nat, nat](<, <)) % enumerates the subsequence indices
% an infinite sequence of elements from the finite type D must contain
% a mono-chromatic subsequence
infinite_pigeonhole: LEMMA
FORALL (f: [nat -> D]): EXISTS d, g: FORALL n: f(g(n)) = d
descending_exists: LEMMA
descending?(strictly_pointwise(rel))(seq) =>
EXISTS d: rel(seq(n + 1)(d), seq(n)(d))
descending_reflexive_closure: LEMMA
descending?(strictly_pointwise(rel))(seq) =>
descending?[R](reflexive_closure[R](rel))(LAMBDA n: seq(n)(d))
pointwise_pigeonhole: LEMMA
descending?(strictly_pointwise(rel))(seq) =>
EXISTS d, g: descending?(rel)(LAMBDA n: seq(g(n))(d))
strictly_pointwise_well_founded_order: JUDGEMENT
strictly_pointwise(rel: (well_founded_order?[R])) HAS_TYPE
(well_founded_order?[[D -> R]])
END finite_pointwise_orders
¤ 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.
|
