|
%------------------------------------------------------------------------------
%
% These are properties of bounded partial orders. Because we're importing the
% the partial order, it needn't clutter up the theories.
%
% We're defining the least_upper_bound and greatest_lower_bound operators
% (lub(S) and glb(S) respectively) for all suitable sets S. Notice that they
% needn't be nonempty.
%
%------------------------------------------------------------------------------
bounded_order_props[T:TYPE,<=:(partial_order?[T])]: THEORY
BEGIN
IMPORTING sets[T], bounded_orders[T]
x,y: VAR T
S,A,B: VAR set[T]
above?(A,B): bool = FORALL (x:(B)): EXISTS (y:(A)): x <= y
below?(A,B): bool = FORALL (x:(B)): EXISTS (y:(A)): y <= x
lub_set?(S):bool = least_bounded_above?(<=)(S)
singleton_is_lub_set: JUDGEMENT (singleton?) SUBTYPE_OF (lub_set?)
SA,XA,YA: VAR (lub_set?)
lub(SA): {x | bounded_orders[T].least_upper_bound?(x,SA,<=)}
lub_rew: LEMMA lub(SA) = lub(<=)(SA)
lub_singleton: LEMMA lub(singleton(x)) = x
lub_lem: LEMMA lub(SA) = x IFF bounded_orders[T].least_upper_bound?(x,SA,<=)
above_lub: LEMMA above?(XA,YA) IMPLIES lub(YA) <= lub(XA)
glb_set?(S):bool = bounded_orders[T].greatest_bounded_below?(<=)(S)
singleton_is_glb_set: JUDGEMENT (singleton?) SUBTYPE_OF (glb_set?)
SB,XB,YB: VAR (glb_set?)
glb(SB): {x | bounded_orders[T].greatest_lower_bound?(x,SB,<=)}
glb_rew: LEMMA glb(SB) = glb(<=)(SB)
glb_singleton: LEMMA glb(singleton(x)) = x
glb_lem: LEMMA glb(SB) = x IFF
bounded_orders[T].greatest_lower_bound?(x,SB,<=)
below_glb: LEMMA below?(XB,YB) IMPLIES glb(XB) <= glb(YB)
END bounded_order_props
¤ 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.
|
