This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
Sets
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



3.3.4 Sets
3.3.4.1 Set comprehensions

{ids.PE} 
Set comprehension 

{EP} 
Set comprehension (short form) 
 Description
ids is a commaseparated list of one ore more identifiers whose type must be inferable by the predicate . The predicate and can contain references to the identifiers ids. The set comprehension contains all values of for the values of where is true. is a short form for where denotes the list of free identifiers occurring in (see Section 3.3.1.3)).
 Definition
 Types
With and :
 WD
 Example
The following set comprehensions contain all the first 10 squares numbers:
3.3.4.2 Basic sets

{} 
Empty set 

{exprs} 
Set extension 
 Description
is a commaseparated list of one or more expressions of the same type. The empty set contains no elements. The set extension is the set that contains exactly the elements .
 Definition
 Types
, where is an arbitrary type. with
 WD
3.3.4.3 Subsets

<: 
subset 

/<: 
not a subset 

<<: 
strict subset 

/<<: 
not a strict subset 
 Description
checks if is a subset of , i.e. if all elements of occur in . checks if is a subset of and does not equal . and are the respective negated variants.
 Definition
 Types
is a predicate with , for each operator of , , , .
 WD
for each operator of , , , .
3.3.4.4 Operations on sets

\/ 
Union 

/\ 
Intersection 

\ 
Set subtraction 
 Description
The union denotes the set that contains all elements that are in or . The intersection denotes the set that contains all elements that are in both and . The set subtraction or set difference denotes all elements that are in but not in .
 Definition
 Types
with and for each operator of , ,
 WD
for each operator of , ,
3.3.4.5 Power sets

POW 
Power set 

POW1 
Set of nonempty subsets 
 Description
denotes the set of all subsets of the set . denotes the set of all nonempty subsets of the set .
 Definition
 Types
and with .
 WD
3.3.4.6 Finite sets

finite 
Finite set 

card 
Cardinality of a finite set 
 Description
is a predicate that states that is a finite set. denotes the cardinality of . The cardinality is only defined for finite sets.
 Definition
 Types
is a predicate and with , i.e. must be a set.
 WD
3.3.4.7 Partition

partition 
Partitions of a set 
 Description
is a predicate that states that the sets constitute a partition of . The union of all elements of a partition is and all elements are disjoint. is equivalent to and to .
 Definition
 Types
is a predicate with and for
 WD
3.3.4.8 Generalized union and intersection

union 
Generalized union 

inter 
Generalized intersection 
 Description
is the union of all elements of . is the intersection of all elements of . The intersection is only defined for nonempty .
 Definition
 Types
and with .
 WD
3.3.4.9 Quantified union and intersection

UNION 
Quantified union 

INTER 
Quantified intersection 
 Description
is the union of all values of for valuations of the identifiers that fulfill the predicate . The types of must be inferable by . Analogously is the intersection of all values of for valuations of the identifiers that fulfill the predicate . Like set comprehensions (3.3.4.1), the quantified union and intersection have a short form where the free variables of the expression are quantified implicitly: and .
 Definition
 Types
With and being a predicate:
 WD
