Adding Set Definitions

Often new types are defined as subsets of old types using Nuprl's set type. Usually, there are standard extra objects associated with set definitions. The function   is a variant on def that automatically creates default versions of these extra objects that are good enough for most purposes. It's usage is identical to that of def.

The extra objects created are:

• an ML object id _ ml _ inc . This tells Nuprl how to prove type-inclusion relationships between the old and new types.
• a properties lemma id _ properties. This helps in accessing the set predicate information. The structure and use of properties lemmas is described in Section .

The properties lemma is automatically proven providing the set predicate is squash stable. In the event that you want to introduce a set definition with a predicate that isn't squash stable, it is useful to use instead a squashed version of the predicate; squashed predicates are always squash-stable.

In order to add these extra objects for existing definitions the function

can be used. Its argument should be the opid of the definition.

An example invocation of setdef is

and the objects created by this invocation are:

Sometimes, the predicate in a set definition can have a number of parts and it is desirable to have a property lemma for each part. The function

can be used to add such property lemmas. It assumes that compound and basic attributes have appropriately been added to the definitions of the abstractions used in the predicate.