|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
relation_implication[T,U:TYPE+] :THEORY
BEGIN
R1,R2: VAR pred[[T,U]]
% relational implication represent subrelation
|-(R1,R2):bool = FORALL (t:T,u:U): R1(t,u) IMPLIES R2(t,u);
|=(R1,R2) :bool = (R1 |- R2) AND (R2 |- R1)
rel_impl_extensionality: LEMMA (R1 |- R2 ) IMPLIES
FORALL(t: T)(u: U): R1(t, u) IMPLIES R2(t, u)
lemma_double_impl: LEMMA ( |=(R1,R2) ) IMPLIES
FORALL(t:T,u:U): R1(t,u) IFF R2(t,u)
rel_impl_is_partial_order: LEMMA partial_order?[pred[[T,U]]]( |- )
double_impl_is_equivalence : LEMMA equivalence?[pred[[T,U]]]( |= )
JUDGEMENT |- HAS_TYPE (partial_order?[pred[[T,U]]])
JUDGEMENT |= HAS_TYPE (equivalence?[pred[[T,U]]])
AUTO_REWRITE+ |-,|=
END relation_implication
[ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
]
|
