|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
