Sets

[
Type   sets
Funcon set
Funcon set-elements
Funcon is-in-set
Funcon is-subset
Funcon set-insert
Funcon set-unite
Funcon set-intersect
Funcon set-difference
Funcon set-size
Funcon some-element
Funcon element-not-in
]
Meta-variables
GT <: ground-values
Built-in Type
sets(GT)

sets(GT) is the type of possibly-empty finite sets {V_1, ..., V_n} where V_1:GT, …, V_n:GT.

Built-in Funcon
set(_:(GT)*) : =>sets(GT)

The notation {V_1, ..., V_n} for set(V_1, ..., V_n) is built-in.

Assert
{V*:(GT)*} == set(V*)

Note that set(...) is not a constructor operation. The order and duplicates of argument values are ignored (e.g., {1,2,1} denotes the same set as {1,2} and {2,1}).

Built-in Funcon
set-elements(_:sets(GT)) : =>(GT)*

For each set S, the sequence of values V* returned by set-elements(S) contains each element of S just once. The order of the values in V* is unspecified, and may vary between sets (e.g., set-elements{1,2} could be (1,2) and set-elements{1,2,3} could be (3,2,1)).

Assert
set(set-elements(S)) == S
Built-in Funcon
is-in-set(_:GT, _:sets(GT)) : =>booleans

is-in-set(GV,S) tests whether GV is in the set S.

Assert
is-in-set(GV:GT, { }) == false
Assert
is-in-set(GV:GT, {GV}:sets(GT)) == true
Built-in Funcon
is-subset(_:sets(GT), _:sets(GT)) : =>booleans

is-subset(S1,S2) tests whether S1 is a subset of S2.

Assert
is-subset({ }, S:sets(GT)) == true
Assert
is-subset(S:sets(GT), S) == true
Built-in Funcon
set-insert(_:GT, _:sets(GT)) : =>sets(GT)

set-insert(GV, S) returns the set union of {GV} and S.

Assert
is-in-set(GV:GT, set-insert(GV:GT, S:sets(GT))) == true
Built-in Funcon
set-unite(_:(sets(GT))*) : =>sets(GT)

set-unite(...) unites a sequence of sets.

Assert
set-unite(S:sets(GT), S) == S
Assert
set-unite(S1:sets(GT), S2:sets(GT)) == set-unite(S2, S1)
Assert
set-unite(S1:sets(GT), set-unite(S2:sets(GT), S3:sets(GT))) ==
set-unite(set-unite(S1, S2), S3)
Assert
set-unite(S1:sets(GT), S2:sets(GT), S3:sets(GT)) ==
set-unite(S1, set-unite(S2, S3))
Assert
set-unite(S:sets(GT)) == S
Assert
set-unite( ) == { }
Built-in Funcon
set-intersect(_:(sets(GT))+) : =>sets(GT)

set-intersect(GT,...) intersects a non-empty sequence of sets.

Assert
set-intersect(S:sets(GT), S) == S
Assert
set-intersect(S1:sets(GT), S2:sets(GT)) == set-intersect(S2, S1)
Assert
set-intersect(S1:sets(GT), set-intersect(S2:sets(GT), S3:sets(GT))) ==
set-intersect(set-intersect(S1, S2), S3)
Assert
set-intersect(S1:sets(GT), S2:sets(GT), S3:sets(GT)) ==
set-intersect(S1, set-intersect(S2, S3))
Assert
set-intersect(S:sets(GT)) == S
Built-in Funcon
set-difference(_:sets(GT), _:sets(GT)) : =>sets(GT)

set-difference(S1, S2) returns the set containing those elements of S1 that are not in S2.

Built-in Funcon
set-size(_:sets(GT)) : =>natural-numbers
Assert
set-size(S:sets(GT)) == length(set-elements(S))
Funcon
some-element(_:sets(GT)) : =>GT?
Assert
some-element(S:sets(GT)) == index(1, set-elements(S))
Assert
some-element{ } == ( )
Built-in Funcon
element-not-in(GT:types, _:set(GT)) : =>GT?

element-not-in(GT, S) gives an element of the type GT not in the set S, or ( ) when S is empty. When the set of elements of GT is infinite, element-not-in(GT, S) never gives ( ).

 From the PLanCompS Project CBS-beta issues… Suggest an improvement…