Quellcode-Bibliothek product_orders.pvs

%------------------------------------------------------------------------------
% Pointwise Ordering in Product Types
%
%       Author: David Lester <dlester@cs.man.ac.uk> Manchester University
%
%       Version 1.0          03/30/06
%------------------------------------------------------------------------------

product_orders[T1,T2:TYPE]: THEORY

BEGIN

  rel1:  VAR pred[[T1,T1]]
  rel2:  VAR pred[[T2,T2]]
  x,y: VAR [[T1,T2]]

  ; % syntax

  *(rel1,rel2)(x,y):bool = rel1(x`1,y`1) AND rel2(x`2,y`2)

  product_preserves_reflexive: JUDGEMENT
   *(r1:(reflexive?[T1]),r2:(reflexive?[T2])) HAS_TYPE (reflexive?[[T1,T2]])

  product_preserves_transitive: JUDGEMENT
   *(r1:(transitive?[T1]),r2:(transitive?[T2])) HAS_TYPE (transitive?[[T1,T2]])

  product_preserves_antisymmetric: JUDGEMENT
   *(r1:(antisymmetric?[T1]),r2:(antisymmetric?[T2]))
                                             HAS_TYPE (antisymmetric?[[T1,T2]])

  product_preserves_preorder: JUDGEMENT
   *(r1:(preorder?[T1]),r2:(preorder?[T2])) HAS_TYPE (preorder?[[T1,T2]])

  product_preserves_partial_order: JUDGEMENT
   *(r1:(partial_order?[T1]),r2:(partial_order?[T2]))
                                             HAS_TYPE (partial_order?[[T1,T2]])

  IMPORTING directed_orders[T1], directed_orders[T2], directed_orders[[T1,T2]]

  product_preserves_directed_complete: JUDGEMENT
   *(r1:(directed_complete?[T1]),r2:(directed_complete?[T2]))
                                         HAS_TYPE (directed_complete?[[T1,T2]])

  product_preserves_directed_complete_partial_order: JUDGEMENT
   *(r1:(directed_complete_partial_order?[T1]),
     r2:(directed_complete_partial_order?[T2]))
                           HAS_TYPE (directed_complete_partial_order?[[T1,T2]])

  product_lub: LEMMA FORALL (r1:(directed_complete_partial_order?[T1]),
                             r2:(directed_complete_partial_order?[T2]),
                             D :(directed?(r1*r2))):
        lub(r1*r2)(D) = (lub(r1)({x:T1| EXISTS (z:(D)): z`1=x}),
                         lub(r2)({y:T2| EXISTS (z:(D)): z`2=y}))

  product_preserves_has_least: LEMMA
    has_least?(rel1)(fullset[T1]) AND has_least?(rel2)(fullset[T2]) IMPLIES
     has_least?(*(rel1,rel2))(fullset[[T1,T2]])

  product_preserves_pointed_directed_complete_partial_order: JUDGEMENT
   *(r1:(pointed_directed_complete_partial_order?[T1]),
     r2:(pointed_directed_complete_partial_order?[T2]))
                   HAS_TYPE (pointed_directed_complete_partial_order?[[T1,T2]])

  product_least: LEMMA
                   FORALL (r1:(pointed_directed_complete_partial_order?[T1]),
                           r2:(pointed_directed_complete_partial_order?[T2])):
   least(r1*r2)(fullset[[T1,T2]])
                          = (least(r1)(fullset[T1]),least(r2)(fullset[T2]))

END product_orders