Quelle  relation_implication.pvs

%--------------------------------------------------------------%
%   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