Quelle  lifted_orders.pvs

%------------------------------------------------------------------------------
% Properties of Lifted Orders
%
%       Author: David Lester <dlester@cs.man.ac.uk> Manchester University
%
% We define a lifting operator on relations, and show that this operation
% preserves directed completeness and pointedness.
%
%       Version 1.0          03/30/06
%------------------------------------------------------------------------------

lifted_orders[T:TYPE]: THEORY

BEGIN

  rel: VAR pred[[T,T]]
  x,y: VAR lift[T]

  IMPORTING lift_props[T]

  lift(rel)(x,y):bool = (NOT up?(x)) OR (up?(y) AND rel(down(x),down(y)))

  lift_preserves_reflexive: JUDGEMENT
   lift(r:(reflexive?[T])) HAS_TYPE (reflexive?[lift[T]])

  lift_preserves_transitive: JUDGEMENT
   lift(r:(transitive?[T])) HAS_TYPE (transitive?[lift[T]])

  lift_preserves_antisymmetric: JUDGEMENT
   lift(r:(antisymmetric?[T]))  HAS_TYPE (antisymmetric?[lift[T]])

  lift_preserves_preorder: JUDGEMENT
   lift(r:(preorder?[T])) HAS_TYPE (preorder?[lift[T]])

  lift_preserves_partial_order: JUDGEMENT
   lift(r:(partial_order?[T])) HAS_TYPE (partial_order?[lift[T]])

  IMPORTING directed_orders[T], directed_orders[lift[T]]

  lift_lub_emptyset: LEMMA lub(lift(rel))(emptyset[lift[T]]) = bottom

  lift_lub_bounded:  LEMMA FORALL (rel:(antisymmetric?[T]),
                                   S:(nonempty_least_bounded_above?(rel))):
       lub(lift(rel))(image[T,lift[T]](up,S)) = up(lub(rel)(S))

  lift_preserves_directed_complete: JUDGEMENT
   lift(r:(directed_complete?[T]))      HAS_TYPE (directed_complete?[lift[T]])

  lift_preserves_directed_complete_partial_order: JUDGEMENT
   lift(r:(directed_complete_partial_order?[T]))
                   HAS_TYPE (pointed_directed_complete_partial_order?[lift[T]])

END lifted_orders