% lattices formed by a total order.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
%
% 8 Feb 2005, Jerry James added singleton_has_X, union_preserves_has_X,
% add_preserves_has_X, X_singleton, X_union, and X_add, where
% X ranges over {greatest, least}.
total_lattices[T: TYPE, <=: (total_order?[T])]: THEORY
BEGIN
IMPORTING minmax_orders[T], lattices[T, <=]
G, G1, G2: VAR (has_greatest?(<=))
L, L1, L2: VAR (has_least?(<=))
t: VAR T
singleton_has_greatest: JUDGEMENT
singleton(t) HAS_TYPE (has_greatest?(<=))
union_preserves_has_greatest: JUDGEMENT
union(G1, G2) HAS_TYPE (has_greatest?(<=))
add_preserves_has_greatest: JUDGEMENT
add(t, G) HAS_TYPE (has_greatest?(<=))
greatest_singleton: LEMMA FORALL t: greatest(<=)(singleton(t)) = t
greatest_union: LEMMA
FORALL G1, G2:
greatest(<=)(union(G1, G2)) =
IF greatest(<=)(G1) <= greatest(<=)(G2) THEN greatest(<=)(G2)
ELSE greatest(<=)(G1)
ENDIF
greatest_add: LEMMA
FORALL G, t:
greatest(<=)(add(t, G)) =
IF greatest(<=)(G) <= t THEN t ELSE greatest(<=)(G) ENDIF
singleton_has_least: JUDGEMENT singleton(t) HAS_TYPE (has_least?(<=))
union_preserves_has_least: JUDGEMENT
union(L1, L2) HAS_TYPE (has_least?(<=))
add_preserves_has_least: JUDGEMENT add(t, L) HAS_TYPE (has_least?(<=))
least_singleton: LEMMA FORALL t: least(<=)(singleton(t)) = t
least_union: LEMMA
FORALL L1, L2:
least(<=)(union(L1, L2)) =
IF least(<=)(L1) <= least(<=)(L2) THEN least(<=)(L1)
ELSE least(<=)(L2)
ENDIF
least_add: LEMMA
FORALL L, t:
least(<=)(add(t, L)) =
IF least(<=)(L) <= t THEN least(<=)(L) ELSE t ENDIF
END total_lattices
¤ Dauer der Verarbeitung: 0.21 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.
|
