		Search-engine friendly clone of the ACL2 documentation.

Defconstrained-recognizer

Introduce a constrained recognizer.

Introduction

ACL2 support the introduction of arbitrary consistency-preserving constrained functions via encapsulate. The defconstrained-recognizer macro abbreviates encapsulates to introduce certain common kinds of constrained recognizers.

This macro currently provides just a few options. More will be added as the need for them arises.

General Form

(defconstrained-recognizer name
                           :nonempty ...
  )

Inputs

name

The name of the recognizer.

:nonempty

Determines whether the recognizer is constrained be non-empty or not, and if so it provides the name of a witness function for the non-emptiness of the recognizer.
It must be one of the following:
A symbol that is not nil. In this case, the recognizer is constrained to be non-empty, by introducing, besides the recognizer, also a nullary function, whose name is this input, constrained to satisfy the recognizer.
nil (the default). In this case, the recognizer is not constrained to be non-empty, i.e. it may be empty or non-empty. No constrained nullary function is introduced in this case.

Generated Events

This macro generates an encapsulate that introduces the following functions with the following constraining theorems.

name

The recognizer, a unary function.
Its executable counterpart is disabled.

booleanp-of-name

A rewrite and type prescription rule saying that the recognizer returns a boolean:
(defthm booleanp-of-name
  (booleanp (name x))
  :rule-classes (:rewrite :type-prescription))

nonempty

A nullary function witnessing the non-emptiness of the recognizer.
This is generated exactly when :nonempty is not nil.

name-of-nonempty

(defthm name-of-nonempty
  (name (nonempty)))
This is generated exactly when :nonempty is not nil.