% Maximal, greatest, minimal, least elements on subsets, and their
% correlation with least upper and greatest lower bounds.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Oct 2004 / Jan 2005
minmax_orders[T: TYPE]: THEORY
BEGIN
IMPORTING bounded_orders[T], finite_sets@finite_sets_minmax
t, r: VAR T
S: VAR set
F: VAR finite_set
NF: VAR non_empty_finite_set[T]
<=, R: VAR pred[[T,T]]
le: VAR (total_order?[T])
ale: VAR (antisymmetric?[T])
tle: VAR (dichotomous?[T])
% ==========================================================================
% Maximal/greatest elements
% ==========================================================================
% Maximal elements
maximal?(t, S, <=): bool =
S(t) AND NOT (EXISTS (r: (S)): t <= r AND t /= r)
% S(t) AND NOT lower_bound(t, S, irreflexive_kernel(<=))
maximal?(S, <=)(t): MACRO bool = maximal?(t, S, <=)
has_maximal?(S, <=): bool = EXISTS t: maximal?(t, S, <=)
% Greatest elements
greatest?(t, S, <=): bool = S(t) AND upper_bound?(t, S, <=)
greatest?(S, <=)(t): MACRO bool = greatest?(t, S, <=)
has_greatest?(S, <=): bool = EXISTS t: greatest?(t, S, <=)
has_greatest?(<=)(S): MACRO bool = has_greatest?(S, <=)
greatest(<=)(S: (has_greatest?(<=))): {t: (S) | greatest?(t, S, <=)}
% Properties
greatest_iff_least_upper_bound: LEMMA
greatest?(t, S, <=) IFF least_upper_bound?(t, S, <=) AND S(t)
greatest_is_least_upper_bound: JUDGEMENT
(greatest?) SUBTYPE_OF (least_upper_bound?)
has_greatest_is_least_bounded_above: JUDGEMENT
(has_greatest?) SUBTYPE_OF (least_bounded_above?)
greatest_equals_lub: LEMMA
FORALL (S: (has_greatest?(ale))): greatest(ale)(S) = lub(ale)(S)
greatest_unique: LEMMA
FORALL (<=: (antisymmetric?[T]), (s, t: (greatest?(S, <=)))): s = t
greatest_is_maximal: LEMMA
greatest?(t, S, ale) => maximal?(t, S, ale)
maximal_is_greatest: LEMMA
maximal?(t, S, tle) => greatest?(t, S, tle)
non_empty_finite_has_greatest: LEMMA
has_greatest?(NF, le)
greatest_ge: LEMMA
FORALL (S: (has_greatest?(<=)), m: (S)): m <= greatest(<=)(S)
greatest_monotone: LEMMA
FORALL (S1, S2: (has_greatest?(<=))):
subset?(S1, S2) => greatest(<=)(S1) <= greatest(<=)(S2)
greatest_def: LEMMA
FORALL (S: (has_greatest?(ale))):
greatest(ale)(S) = t IFF greatest?(t, S, ale)
greatest_upper_bound: LEMMA
FORALL (<=: (partial_order?[T]), S: (has_greatest?(<=))):
greatest(<=)(S) <= t IFF upper_bound?[T](t, S, <=)
% ==========================================================================
% Minimal/least elements
% ==========================================================================
% Minimal elements
minimal?(t, S, <=): bool =
S(t) AND NOT (EXISTS (r: (S)): r <= t AND t /= r)
minimal?(S, <=)(t): MACRO bool = minimal?(t, S, <=)
has_minimal?(S, <=): bool = EXISTS t: minimal?(t, S, <=)
% Least elements
least?(t, S, <=): bool = S(t) AND lower_bound?(t, S, <=)
least?(S, <=)(t): MACRO bool = least?(t, S, <=)
has_least?(S, <=): bool = EXISTS t: least?(t, S, <=)
has_least?(<=)(S): MACRO bool = has_least?(S, <=)
least(<=)(S: (has_least?(<=))): {t: (S) | least?(t, S, <=)}
% Properties
least_iff_greatest_lower_bound: LEMMA
least?(t, S, <=) IFF greatest_lower_bound?(t, S, <=) AND S(t)
least_is_greatest_lower_bound: JUDGEMENT
(least?) SUBTYPE_OF (greatest_lower_bound?)
has_least_is_greatest_bounded_below: JUDGEMENT
(has_least?) SUBTYPE_OF (greatest_bounded_below?)
least_equals_glb: LEMMA
FORALL (S: (has_least?(ale))): least(ale)(S) = glb(ale)(S)
least_unique: LEMMA
FORALL (<=: (antisymmetric?[T]), (s, t: (least?(S, <=)))): s = t
least_is_minimal: LEMMA
least?(t, S, ale) => minimal?(t, S, ale)
minimal_is_least: LEMMA
minimal?(t, S, tle) => least?(t, S, tle)
non_empty_finite_has_least: LEMMA
has_least?(NF, le)
least_le: LEMMA
FORALL (S: (has_least?(<=)), m: (S)): least(<=)(S) <= m
least_monotone: LEMMA
FORALL (S1, S2: (has_least?(<=))):
subset?(S1, S2) => least(<=)(S2) <= least(<=)(S1)
least_def: LEMMA
FORALL (S: (has_least?(ale))):
least(ale)(S) = t IFF least?(t, S, ale)
least_lower_bound: LEMMA
FORALL (<=: (partial_order?[T]), S: (has_least?(<=))):
t <= least(<=)(S) IFF lower_bound?[T](t, S, <=)
% ==========================================================================
% Both greatest and least elements exist
% ==========================================================================
has_extrema?(S, <=): bool = has_greatest?(S, <=) AND has_least?(S, <=)
% bounded_type?(<=): bool = has_extrema?(fullset, <=)
has_extrema_has_greatest: JUDGEMENT
(has_extrema?) SUBTYPE_OF (has_greatest?)
has_extrema_has_least: JUDGEMENT
(has_extrema?) SUBTYPE_OF (has_least?)
total_order_is_lattice: JUDGEMENT
(total_order?) SUBTYPE_OF (lattice?)
END minmax_orders
¤ Dauer der Verarbeitung: 0.17 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.
|
