## 2.5.4 Introducing user-defined types

We can introduce our own new types simply by giving such types a name. This is done by adding the name of the type to the SETS section of a context. We will see how this is done in practice in the next section (2.6).

For instance, if we want to model different kind of fruits in our model, we might create the set . Then the identifier denotes the set of all elements of this type. Nothing more is known about unless we add further axioms. In particular, we do not know the cardinality (number of elements) of the set or even if it is finite.

Assume that we want to model and which are sub-sets of . We do not need to introduce them in the SETS section of a context just because they are sets. Let’s imagine such a scenario where and are modelled as types of their own (by declaring them in the SETS section). And we have two variables or constants and with and . Then we cannot compare and with or . That would raise a type error because and expect the same type for the left and right expression.

If we want to model sub-sets and as described above, we can add them as constants and state that and . If apples and oranges are all fruits we want to model, we can assume and if no fruit is both an apple and orange we can write . A shorter way to express this is to say that apples and oranges constitute a partition of the fruits: . In general, we can use the partition operator to express that a set is partitioned by the sets with . We use partitions in Section 2.6.2.1.

Another typical usage for user defined data types are enumerated sets. These are sets where we know all the elements already. Let’s take a system which can be either working or broken. We model this by introducing a type in the SETS section and two constants and . We define that STATUS consists of exactly and by . Additionally, we have to say that and are not the same by .

If the enumerated sets gets larger, we need to state for every two element of the set that they are distinct. Thus, for a set of 10 constants, we’ll need predicates. Again, we can use the partition operator to express this in a more concise way: