Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas.

Example Rule Class: (:type-set-inverter :corollary (equal (and (counting-number x) (not (equal x 0))) (and (integerp x) (< x 0))) :type-set 2) General Forms of Rule Class: :type-set-inverter, or (:type-set-inverter :type-set n) General Form of Theorem or Corollary: (EQUAL new-expr old-expr)where

`n`

is a `type-set`

(see type-set) and `old-expr`

is the term
containing `x`

as a free variable that ACL2 currently uses to
recognize `type-set`

`n`

. For a given `n`

, the exact form of `old-expr`

is
generated by
(convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the `:`

`type-set`

field of the rule-class is omitted, we attempt to
compute it from the right-hand side, `old-expr`

, of the corollary.
That computation is done by `type-set-implied-by-term`

(see type-set). However, it is possible that the type-set we
compute from `lhs`

does not have the required property that when
inverted with `convert-type-set-to-term`

the result is `lhs`

. If you
omit `:`

`type-set`

and an error is caused because `lhs`

has the incorrect
form, you should manually specify both `:`

`type-set`

and the `lhs`

generated by `convert-type-set-to-term`

.

The rule generated will henceforth make `new-expr`

be the term used by
ACL2 to recognize type-set `n`

. If this rule is created by a `defthm`

event named `name`

then the rune of the rule is
`(:type-set-inverter name)`

and by disabling that rune you can
prevent its being used to decode type-sets.

Type-sets are inverted when forced assumptions are turned into
formulas to be proved. In their internal form, assumptions are
essentially pairs consisting of a context and a goal term, which was
forced. Abstractly a context is just a list of hypotheses which may
be assumed while proving the goal term. But actually contexts are
alists which pair terms with type-sets, encoding the current
hypotheses. For example, if the original conjecture contained the
hypothesis `(integerp x)`

then the context used while working on that
conjecture will include the assignment to `x`

of the type-set
`*ts-integer*`

.