Quelle  cross_product.pvs

%------------------------------------------------------------------------------
% Cross Products
%
%     Author: David Lester, Manchester University, NIA, Universite Perpignan
%
%
%     Version 1.0            17/08/07  Initial Version
%------------------------------------------------------------------------------

cross_product[T1,T2:TYPE]: THEORY

BEGIN

  A:  VAR set[T1]
  B:  VAR set[T2]
  NA: VAR (nonempty?[T1])
  NB: VAR (nonempty?[T2])
  X:  VAR set[[T1,T2]]
  a:  VAR T1
  b:  VAR T2
  z:  VAR [T1,T2]

  cross_product(A,B):set[[T1,T2]] = {z | A(z`1) AND B(z`2)}
  projection_1(X):set[T1]         = {a | EXISTS z: X(z) AND z`1 = a}
  projection_2(X):set[T2]         = {b | EXISTS z: X(z) AND z`2 = b}

  cross_product_empty1:    LEMMA empty?(A) => empty?(cross_product(A,B))
  cross_product_empty2:    LEMMA empty?(B) => empty?(cross_product(A,B))

  cross_product_emptyset1: LEMMA empty?(cross_product(emptyset[T1],B))
  cross_product_emptyset2: LEMMA empty?(cross_product(A,emptyset[T2]))
  cross_product_fullset:   LEMMA full?(cross_product(fullset[T1],fullset[T2]))

  projection_product1:     LEMMA projection_1(cross_product(A,NB)) = A
  projection_product2:     LEMMA projection_2(cross_product(NA,B)) = B

  projection_1_emptyset:   LEMMA projection_1(emptyset[[T1,T2]]) = emptyset[T1]
  projection_2_emptyset:   LEMMA projection_2(emptyset[[T1,T2]]) = emptyset[T2]
  projection_1_fullset:    LEMMA (EXISTS b: TRUE) =>
                                 projection_1(fullset[[T1,T2]])  = fullset[T1]
  projection_2_fullset:    LEMMA (EXISTS a: TRUE) =>
                                 projection_2(fullset[[T1,T2]])  = fullset[T2]

  cross_product_empty1_rew:
                        LEMMA cross_product(emptyset[T1],B) = emptyset[[T1,T2]]
  cross_product_empty2_rew:
                        LEMMA cross_product(A,emptyset[T2]) = emptyset[[T1,T2]]
  cross_product_full_rew:
               LEMMA cross_product(fullset[T1],fullset[T2]) = fullset[[T1,T2]]


  cross_product: TYPE+ = {X | EXISTS A,B: X = cross_product(A,B)}

  Y: VAR cross_product

  product_projection: LEMMA cross_product(projection_1(Y),projection_2(Y)) = Y

  x_section(X,a):set[T2] = {b | X(a,b)}                             % SKB 7.2.4
  y_section(X,b):set[T1] = {a | X(a,b)}
                                                                    % SKB 7.2.6
  x_section(X):[T1->set[T2]] = lambda a: x_section(X,a)
  y_section(X):[T2->set[T1]] = lambda b: y_section(X,b)

END cross_product