Specification of a Set

Before embarking on the formal aspects of structural induction and its application to discharging proof obligations, we examine the specification of a set data type. We have seen that identification of a set of atomic constructors leads us immediately to a set of canonical forms composed from those atomic constructors. However, as we remarked at the time, intuition might lead us astray as we now show with the following specification Funny-Set for a ``set'' of natural numbers. This example demonstrates that having identified (what is apparently) a set of atomic constructors, the corresponding set of reduced expressions composed from these atomic constructors does not constitute a set of canonical forms.