% Upper and lower bounds on subsets; lub, glb;
% (complete) upper and lower semilattices; (complete) lattices
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Oct 2004 / Jan 2005
%
% lub_singleton, least_upper_bound_singleton, glb_singleton, and
% greates_lower_bound_singleton added 23 Feb 2005 by Jerry James
% <[email protected]>, University of Kansas.
bounded_orders[T: TYPE]: THEORY
BEGIN
IMPORTING sets[T], finite_sets[T], relations_extra[T]
t, u, r: VAR T
S, R: VAR set
NF: VAR non_empty_finite_set
<=: VAR pred[[T,T]]
% ==========================================================================
% Upper bounds
% ==========================================================================
upper_bound?(t, S, <=): bool = FORALL (r: (S)): r <= t
upper_bound?(S, <=)(t): MACRO bool = upper_bound?(t, S, <=)
bounded_above?(S, <=): bool = EXISTS t: upper_bound?(t, S, <=)
bounded_above?(<=)(S): MACRO bool = bounded_above?(S, <=)
least_upper_bound?(t, S, <=): bool =
upper_bound?(t, S, <=) AND
(FORALL r: upper_bound?(r, S, <=) => t <= r)
least_upper_bound?(S, <=)(t): MACRO bool = least_upper_bound?(t, S, <=)
least_bounded_above?(S, <=): bool = EXISTS t: least_upper_bound?(t, S, <=)
least_bounded_above?(<=)(S): MACRO bool = least_bounded_above?(S, <=)
complete_upper_semilattice?(<=): bool =
partial_order?(<=) AND FORALL S: least_bounded_above?(S, <=)
upper_semilattice?(<=): bool =
partial_order?(<=) AND FORALL NF: least_bounded_above?(NF, <=)
lub(<=)(S: (least_bounded_above?(<=))): (least_upper_bound?(S, <=))
% Properties
unique_least_upper_bound: THEOREM
FORALL (<=: (antisymmetric?[T]), t, r: (least_upper_bound?(S, <=))): t = r
subset_upper_bound: LEMMA
(subset?(S, R) AND upper_bound?(t, R, <=)) => upper_bound?(t, S, <=)
subset_least_upper_bound: COROLLARY
subset?(S, R) AND
least_upper_bound?(t, R, <=) AND
least_upper_bound?(r, S, <=) IMPLIES
r <= t
lub_def: LEMMA
FORALL (<=: (antisymmetric?[T]), S: (least_bounded_above?(<=))):
(lub(<=)(S) = t IFF least_upper_bound?(S, <=)(t))
lub_eq: LEMMA
FORALL (<=: (antisymmetric?[T]), S: (least_bounded_above?(<=)),
t: (least_upper_bound?(S, <=))):
lub(<=)(S) = t
lub_ge: LEMMA
FORALL (S: (least_bounded_above?(<=)), t: (S)):
t <= lub(<=)(S)
lub_le: LEMMA
FORALL (<=: (transitive?[T]), S: (least_bounded_above?(<=))):
(lub(<=)(S) <= t IFF upper_bound?(S, <=)(t))
all_least_bounded: LEMMA
FORALL (<=: (complete_upper_semilattice?)):
least_bounded_above?(S, <=)
all_finite_least_bounded: LEMMA
FORALL (<=: (upper_semilattice?)):
least_bounded_above?(NF, <=)
complete_upper_semilattice_upper: JUDGEMENT
(complete_upper_semilattice?) SUBTYPE_OF (upper_semilattice?)
upper_semilattice_is_partial_order: JUDGEMENT
(upper_semilattice?) SUBTYPE_OF (partial_order?)
% ==========================================================================
% Lower bounds
% ==========================================================================
lower_bound?(t, S, <=): bool = FORALL (r: (S)): t <= r
lower_bound?(S, <=)(t): MACRO bool = lower_bound?(t, S, <=)
bounded_below?(S, <=): bool = EXISTS t: lower_bound?(t, S, <=)
bounded_below?(<=)(S): MACRO bool = bounded_below?(S, <=)
greatest_lower_bound?(t, S, <=): bool =
lower_bound?(t, S, <=) AND
(FORALL r: lower_bound?(r, S, <=) => r <= t)
greatest_lower_bound?(S, <=)(t): MACRO bool = greatest_lower_bound?(t, S, <=)
greatest_bounded_below?(S, <=): bool =
EXISTS t: greatest_lower_bound?(t, S, <=)
greatest_bounded_below?(<=)(S): MACRO bool = greatest_bounded_below?(S, <=)
complete_lower_semilattice?(<=): bool =
partial_order?(<=) AND FORALL S: greatest_bounded_below?(S, <=)
lower_semilattice?(<=): bool =
partial_order?(<=) AND FORALL NF: greatest_bounded_below?(NF, <=)
glb(<=)(S: (greatest_bounded_below?(<=))): (greatest_lower_bound?(S, <=))
% Properties
unique_greatest_lower_bound: THEOREM
FORALL (<=: (antisymmetric?[T]), t, r: (greatest_lower_bound?(S, <=))):
t = r
subset_lower_bound: LEMMA
FORALL S, R, t:
(subset?(S, R) AND lower_bound?(t, R, <=)) => lower_bound?(t, S, <=)
subset_greatest_lower_bound: COROLLARY
subset?(S, R) AND
greatest_lower_bound?(t, S, <=) AND
greatest_lower_bound?(r, R, <=) IMPLIES
r <= t
glb_def: LEMMA
FORALL (<=: (antisymmetric?[T]), S: (greatest_bounded_below?(<=))):
(glb(<=)(S) = t IFF greatest_lower_bound?(S, <=)(t))
glb_eq: LEMMA
FORALL (<=: (antisymmetric?[T]), S: (greatest_bounded_below?(<=)),
t: (greatest_lower_bound?(S, <=))):
glb(<=)(S) = t
glb_le: LEMMA
FORALL (S: (greatest_bounded_below?(<=)), t: (S)):
glb(<=)(S) <= t
glb_ge: LEMMA
FORALL (<=: (transitive?[T]), S: (greatest_bounded_below?(<=))):
(t <= glb(<=)(S) IFF lower_bound?(S, <=)(t))
all_greatest_bounded: LEMMA
FORALL (<=: (complete_lower_semilattice?)):
greatest_bounded_below?(S, <=)
all_finite_greatest_bounded: LEMMA
FORALL (<=: (lower_semilattice?)):
greatest_bounded_below?(NF, <=)
complete_lower_semilattice_lower: JUDGEMENT
(complete_lower_semilattice?) SUBTYPE_OF (lower_semilattice?)
lower_semilattice_is_partial_order: JUDGEMENT
(lower_semilattice?) SUBTYPE_OF (partial_order?)
% ==========================================================================
% Upper and lower bounds
% ==========================================================================
bounded?(S, <=): bool = bounded_above?(S, <=) AND bounded_below?(S, <=)
bounded?(<=)(S): MACRO bool = bounded?(S, <=)
tightly_bounded?(S, <=): bool =
least_bounded_above?(S, <=) AND greatest_bounded_below?(S, <=)
tightly_bounded?(<=)(S): MACRO bool = tightly_bounded?(S, <=)
complete_lattice?(<=): bool =
complete_upper_semilattice?(<=) AND complete_lower_semilattice?(<=)
lattice?(<=): bool =
upper_semilattice?(<=) AND lower_semilattice?(<=)
bounded_is_bounded_above: JUDGEMENT (bounded?) SUBTYPE_OF (bounded_above?)
bounded_is_bounded_below: JUDGEMENT (bounded?) SUBTYPE_OF (bounded_below?)
tightly_bounded_above: JUDGEMENT
(tightly_bounded?) SUBTYPE_OF (least_bounded_above?)
tightly_bounded_below: JUDGEMENT
(tightly_bounded?) SUBTYPE_OF (greatest_bounded_below?)
complete_lattice_upper: JUDGEMENT
(complete_lattice?) SUBTYPE_OF (complete_upper_semilattice?)
complete_lattice_lower: JUDGEMENT
(complete_lattice?) SUBTYPE_OF (complete_lower_semilattice?)
lattice_upper: JUDGEMENT
(lattice?) SUBTYPE_OF (upper_semilattice?)
lattice_lower: JUDGEMENT
(lattice?) SUBTYPE_OF (lower_semilattice?)
complete_lattice_is_lattice: JUDGEMENT
(complete_lattice?) SUBTYPE_OF (lattice?)
% bounds of singleton sets
upper_bound_singleton: LEMMA
upper_bound?[T](t, singleton(u), <=) IFF u <= t
least_upper_bound_singleton: LEMMA
FORALL (<=: (reflexive?)): least_upper_bound?[T](t, singleton(t), <=)
lub_singleton: LEMMA
FORALL (<=: (partial_order?)): lub(<=)(singleton(u)) = u
lower_bound_singleton: LEMMA
lower_bound?[T](t, singleton(u), <=) IFF t <= u
greatest_lower_bound_singleton: LEMMA
FORALL (<=: (reflexive?)): greatest_lower_bound?[T](t, singleton(t), <=)
glb_singleton: LEMMA
FORALL (<=: (partial_order?)): glb(<=)(singleton(u)) = u
% bounds of the empty set
upper_bound_emptyset: LEMMA
upper_bound?(t, emptyset, <=)
lower_bound_emptyset: LEMMA
lower_bound?(t, emptyset, <=)
lub_emptyset_is_glb_fullset: THEOREM
least_upper_bound?(t, emptyset, <=) IFF
greatest_lower_bound?(t, fullset, <=)
glb_emptyset_is_lub_fullset: THEOREM
greatest_lower_bound?(t, emptyset, <=) IFF
least_upper_bound?(t, fullset, <=)
least_bounded_above_emptyset: COROLLARY
least_bounded_above?(emptyset, <=) IFF
greatest_bounded_below?(fullset, <=)
greatest_bounded_below_emptyset: COROLLARY
greatest_bounded_below?(emptyset, <=) IFF
least_bounded_above?(fullset, <=)
% --------- New content from David Lester
nonempty_least_bounded_above?(<=)(S):bool
= nonempty?(S) AND least_bounded_above?(<=)(S)
nonempty_greatest_bounded_below?(<=)(S):bool
= nonempty?(S) AND greatest_bounded_below?(<=)(S)
le_lub: LEMMA FORALL (<=:(partial_order?),S,R:(least_bounded_above?(<=))):
(FORALL (s:(S)): EXISTS (r:(R)): s <= r) IMPLIES lub(<=)(S) <= lub(<=)(R)
eq_lub: LEMMA FORALL (<=:(partial_order?),S,R:(least_bounded_above?(<=))):
(FORALL (s:(S)): EXISTS (r:(R)): s <= r) AND
(FORALL (r:(R)): EXISTS (s:(S)): r <= s) IMPLIES lub(<=)(S) = lub(<=)(R)
lub_add: LEMMA FORALL (<=:(partial_order?),S:(least_bounded_above?(<=))):
lub(<=)(add(lub(<=)(S),S)) = lub(<=)(S)
le_glb: LEMMA FORALL (<=:(partial_order?),S,R:(greatest_bounded_below?(<=))):
(FORALL (r:(R)): EXISTS (s:(S)): s <= r) IMPLIES glb(<=)(S) <= glb(<=)(R)
eq_glb: LEMMA FORALL (<=:(partial_order?),S,R:(greatest_bounded_below?(<=))):
(FORALL (s:(S)): EXISTS (r:(R)): r <= s) AND
(FORALL (r:(R)): EXISTS (s:(S)): s <= r) IMPLIES glb(<=)(S) = glb(<=)(R)
glb_add: LEMMA FORALL (<=:(partial_order?),S:(greatest_bounded_below?(<=))):
glb(<=)(add(glb(<=)(S),S)) = glb(<=)(S)
END bounded_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.
|
