		Search-engine friendly clone of the ACL2 documentation.

Defsubtype

Introduce a fixtype that is a subtype of the given fixtype.

Introduction

defsubtype introduces fixtypes for an arbitrary subtype. A subtype SUB of a type SUPER is one that is either the same as or more restrictive than SUPER. This is expressed by a restriction predicate. The recognizer predicate for the subtype is the conjunction of the supertype's recognizer predicate and the restriction predicate:

(iff (sub-p x)
     (and (super-p x)
          (sub-restriction-p x)))

The restriction predicate should be a total function of one argument. It can be a symbol or a lambda expression. The required :fix-value argument specifies a value that will be returned by the new fixing function. It must satisfy the new recognizer predicate.

Basic Example

(defsubtype positive-even
  :supertype pos
  :restriction (lambda (x) (and (integerp x) (evenp x)))
  :fix-value 2)

This example would produce:

A recognizer positive-even-p.
A fixing function positive-even-fix.
An equivalence relation positive-even-equiv.

The reason the restriction predicate is not just evenp is because evenp has a guard of integerp and therefore is not a total function. Note that the restriction predicate does not need to define a subset of the supertype. It can be true on some values that are not in the supertype, in this case on negative even numbers. This is not a problem because the subtype's recognizer predicate checks both the supertype's predicate and the restriction predicate.

General Form

(defsubtype subtype
  :supertype ...     ;; required; must be defined using fty
  :restriction ...   ;; required; can be named or a lambda expression
  :fix-value ...     ;; required
  :pred ...          ;; optional name of new predicate; default: subtype-p
  :fix ...           ;; optional; default: subtype-fix
  :equiv ...         ;; optional; default: subtype-equiv
  :parents ...       ;; optional; XDOC parents
  :short ...         ;; optional; XDOC short description.
  :long ...          ;; optional; XDOC long description.
  )

Inputs

subtype

A symbol that specifies the name of the new fixtype.

:supertype

A symbol that names a fixtype that is a supertype of the type being defined.
The recognizer, fixer, and equivalence function of the supertype must all be guard-verified.

:restriction

A predicate that is used, in conjunction with the supertype's predicate, to define pred, which recognizes values of the subtype.

:fix-value

The value returned by the fixing function when passed a value for which pred is false. Also establishes that the subtype has at least one value.

:pred

A symbol that specifies the name of the generated recognizer for subtype. If this is nil (the default), the name of the recognizer is subtype followed by -p.

:fix

A symbol that specifies the name of the generated fixer for subtype. If this is nil (the default), the name of the fixer is subtype followed by -fix.

:equiv

A symbol that specifies the name of the generated equivalence checker for subtype. If this is nil (the default), the name of the equivalence checker is subtype followed by -equiv.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the new fixtype.

Generated Events

pred

The recognizer for the fixtype, guard-verified.

booleanp-of-pred

A rewrite rule saying that pred is boolean-valued.

supertype-pred-when-pred-rewrite
supertype-pred-when-pred-forward

A rewrite rule and a forward chaining rule saying that a value satisfies supertype-pred when it satisfies pred.

fix

The fixer for the fixtype, guard-verified.
It fixes values outside of pred by returning fix-value.
pred-of-fix
A rewrite rule saying that fix always returns a value that satisfies pred.
fix-when-pred
A rewrite rule saying that fix disappears when its argument satisfies pred.
type
equiv
The fixtype, via a call of deffixtype that also introduces the equivalence checker equiv.
The above items are generated with XDOC documentation.

Subtopics

Defsubtype-implementation: Implementation of defsubtype.