## Rodin HandbookThis 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 |
## 2.5.4 Introducing user-defined typesWe 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 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.
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 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: |