% lower semilattices; binary glb function
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Oct 2004 / Jan 2005
lower_semilattices[
T: TYPE,
(IMPORTING bounded_orders[T])
<=: (lower_semilattice?[T])
]: THEORY
BEGIN
IMPORTING bounded_sets[T, <=]
s, t, u, t1, t2: VAR T
S, S1, S2: VAR (greatest_bounded_below?[T](<=))
finite_set_is_greatest_bounded_below: JUDGEMENT
non_empty_finite_set[T] SUBTYPE_OF (greatest_bounded_below?(<=))
greatest_lower_bound_singleton: LEMMA
greatest_lower_bound?[T](t, singleton(t), <=)
glb_singleton: LEMMA
glb(<=)(singleton(t)) = t
glb(t, u): T = glb[T](<=)(union(singleton(t), singleton(u)))
le_glb: LEMMA s <= glb(t, u) IFF s <= t AND s <= u
glb_le_1: LEMMA t <= s => glb(t, u) <= s
glb_le_2: LEMMA u <= s => glb(t, u) <= s
union_preserves_bounded_below: JUDGEMENT
union(S1, S2: (bounded_below?[T](<=))) HAS_TYPE (bounded_below?[T](<=))
add_preserves_bounded_below: JUDGEMENT
add(s: T, S: (bounded_below?[T](<=))) HAS_TYPE (bounded_below?[T](<=))
greatest_lower_bound_union: LEMMA
greatest_lower_bound?[T](t1, S1, <=) &
greatest_lower_bound?[T](t2, S2, <=) =>
greatest_lower_bound?[T](glb(t1, t2), union(S1, S2), <=)
greatest_lower_bound_add: LEMMA
greatest_lower_bound?[T](t, S, <=) =>
greatest_lower_bound?[T](glb(t, s), add(s, S), <=)
union_preserves_greatest_bounded_below: JUDGEMENT
union(S1, S2) HAS_TYPE (greatest_bounded_below?[T](<=))
add_preserves_greatest_bounded_below: JUDGEMENT
add(s, S) HAS_TYPE (greatest_bounded_below?[T](<=))
glb_union: LEMMA
glb[T](<=)(union(S1, S2)) = glb(glb[T](<=)(S1), glb[T](<=)(S2))
glb_add: LEMMA
glb[T](<=)(add(s, S)) = glb(glb[T](<=)(S), s)
END lower_semilattices
¤ Dauer der Verarbeitung: 0.15 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.
|
