next node: SetByBSTConv,
prev node: Subsystem Sets By Binary Search Trees,
up to node: Subsystem Sets By Binary Search Trees

SetByBST

This structure defines the basic functions on sets implemented by balanced search trees.

Signature of SetByBST

List of Import References :
See BOOL
See BSTree
See DENOTATION
See Nat
See Option
See Pair
See Seq
See Tree 

SIGNATURE SetByBST [data, < :data ** data -> bool]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $) 

IMPORT  Nat          ONLY nat
        Seq[data]    ONLY seq
        Option[data] ONLY option

Parameter

data is the element type, < is a total strict order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold. 

SORT data
FUN <   : data**data->bool

The Type Itself

SORT set

 
FUN {}       : set                              -- empty set
FUN incl     : data ** set->set                 -- include

Constructing a Set From Datas

%(e_0, ..., e_n-1) = {e_0, ..., e_n-1} 

FUN % : data -> set                     
FUN % : data ** data -> set
FUN % : data ** data ** data -> set
FUN % : data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data ** data ** data -> set
FUN % : data ** data ** data ** data ** data ** data ** data ** data -> set

FUN incl excl: data ** set -> set

Constructing a Set From a Function

(n_1 .. n_2)(f) = {f(n1), f(n1 +1), ..., f(n2)} 

FUN .. : nat ** nat -> (nat -> data) -> set

iter(start, it, P) = {start, it(start), ... it^n(start)}, where n+1 is the smallest number such that ~P(it^(n+1)(start)). 

 
FUN iter : data ** (data -> data) ** (data -> bool) -> set

Combining Sets

Combine two sets to form set union, set difference or set intersection 

FUN + - *    : set ** set -> set

Accessing Datas in a Set

Select an arbitrary element of the set. Undefined for empty set. 

FUN arb      : set -> data                      -- select arbitrary element

Information About a Set

Test for empty set or mebership. # returns cardinality of the set. 

FUN {}?      : set -> bool
FUN in       : data ** set -> bool
FUN #        : set -> nat

minimum and maximum elements of a set, undefined for {} 

FUN min max  : set -> data

exist? and forall? check, whether any component or all components fulfill a predicate P, find? returns one element which fulfills P, if it exists. 

FUN exist?   : (data -> bool) ** set->bool      
FUN find?        : (data -> bool) ** set -> option[data]
FUN forall?  : (data -> bool) ** set->bool

Comparing Sets

These are the standard set comparisons: equality, subset and proper subset. 

FUN = <= <   : set**set->bool           -- equality/subset/proper subset

If given an order on the elements, < produces such an order. {<} uses the order contained in the parameter and is equivalent to <(<). 

FUN < : (data ** data -> bool) -> set ** set -> bool
FUN {<}      : set ** set -> bool

not for user purpose

IMPORT BSTree[data,<] ONLY bstree

FUN abs: bstree -> set
    rep: set -> bstree

FUN union : bstree ** bstree -> bstree

next node: SetByBSTConv,
prev node: Subsystem Sets By Binary Search Trees,
up to node: Subsystem Sets By Binary Search Trees