|
% orders on a finite type have special properties:
% e.g., every lattice is complete; every strict-order is well-founded.
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Dec 2004/Jan 2005
finite_orders[T: TYPE+]: THEORY
BEGIN
ASSUMING
finite_type: ASSUMPTION is_finite_type[T]
ENDASSUMING
IMPORTING bounded_orders[T], finite_types[T]
R: VAR pred[[T, T]]
S: VAR (nonempty?[T]) % used in proofs
% lattice properties
finite_lower_semilattice_is_complete: LEMMA
greatest_bounded_below?(R)(emptyset) & lower_semilattice?(R) =>
complete_lower_semilattice?(R)
finite_upper_semilattice_is_complete: LEMMA
least_bounded_above?(R)(emptyset) & upper_semilattice?(R) =>
complete_upper_semilattice?(R)
finite_lattice_is_complete: JUDGEMENT
(lattice?) SUBTYPE_OF (complete_lattice?)
% well-foundedness properties
finite_strict_order_is_well_founded: JUDGEMENT
(strict_order?) SUBTYPE_OF (well_founded?[T])
finite_strict_total_order_is_well_ordered: JUDGEMENT
(strict_total_order?) SUBTYPE_OF (well_ordered?[T])
END finite_orders
¤ Dauer der Verarbeitung: 0.18 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.
|
