Constructing sets from two other differently typed sets.
List of Import References :
See BOOL
See BSTree
See DENOTATION
See Nat
See Option
See Pair
See Seq
See SetByBST
See Tree
See Union2
SIGNATURE SetByBSTConstr[data1 , < :data1 ** data1 -> bool, data2,
$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)
< :data2 ** data2 -> bool]
IMPORT SetByBST[data1, <] ONLY set
SetByBST[data2, <] ONLY set
Pair[data1, data2] ONLY pair
Union2[data1, data2] ONLY union
SetByBST[pair[data1, data2], <] ONLY set
SetByBST[union[data1, data2], <] ONLY set
data1 and data2 are the respective element types,
< are total strict orders: the formula ALL x y. ~(x < y) AND
~(y < x) => x === y must hold.
SORT data1 data2
FUN < :data1 ** data1 -> bool
FUN < :data2 ** data2 -> bool
-- $Cartesian Product$
/* @code{x in A and y in B <=> x & y in A x B} */
FUN x : set[data1, <] ** set[data2, <] -> set[pair, <]
/* The necessary order on the elements of the cartesian product. */
FUN < : pair ** pair -> bool
-- $Disjoint Union$
/* @code{x in A and y in B <=> data1(x) in A U B and data2(y) in A U
B} */
FUN U : set[data1, <] ** set[data2, <] -> set[union, <]
The necessary order an the elements of the disjoint union.
FUN < : union ** union -> bool
next node: SetByBSTOfSetByBST,
prev node: SetByBSTMap,
up to node: Subsystem Sets By Binary Search Trees