|
% upper semilattices; binary lub function
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004
upper_semilattices[
T: TYPE,
(IMPORTING bounded_orders[T])
<=: (upper_semilattice?[T])
]: THEORY
BEGIN
IMPORTING bounded_sets[T, <=]
s, t, u, t1, t2: VAR T
S, S1, S2: VAR (least_bounded_above?[T](<=))
finite_set_is_least_bounded_above: JUDGEMENT
non_empty_finite_set[T] SUBTYPE_OF (least_bounded_above?(<=))
least_upper_bound_singleton: LEMMA
least_upper_bound?[T](t, singleton(t), <=)
lub_singleton: LEMMA
lub(<=)(singleton(t)) = t
lub(t, u): T = lub[T](<=)(union(singleton(t), singleton(u)))
lub_le: LEMMA lub(t, u) <= s IFF t <= s AND u <= s
le_lub_1: LEMMA s <= t => s <= lub(t, u)
le_lub_2: LEMMA s <= u => s <= lub(t, u)
union_preserves_bounded_above: JUDGEMENT
union(S1, S2: (bounded_above?[T](<=))) HAS_TYPE (bounded_above?[T](<=))
add_preserves_bounded_above: JUDGEMENT
add(s: T, S: (bounded_above?[T](<=))) HAS_TYPE (bounded_above?[T](<=))
least_upper_bound_union: LEMMA
least_upper_bound?[T](t1, S1, <=) &
least_upper_bound?[T](t2, S2, <=) =>
least_upper_bound?[T](lub(t1, t2), union(S1, S2), <=)
least_upper_bound_add: LEMMA
least_upper_bound?[T](t, S, <=) =>
least_upper_bound?[T](lub(t, s), add(s, S), <=)
union_preserves_least_bounded_above: JUDGEMENT
union(S1, S2) HAS_TYPE (least_bounded_above?[T](<=))
add_preserves_least_bounded_above: JUDGEMENT
add(s, S) HAS_TYPE (least_bounded_above?[T](<=))
lub_union: LEMMA
lub[T](<=)(union(S1, S2)) = lub(lub[T](<=)(S1), lub[T](<=)(S2))
lub_add: LEMMA
lub[T](<=)(add(s, S)) = lub(lub[T](<=)(S), s)
END upper_semilattices
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
