• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
      • Meta
      • Linear
      • Definition
      • Clause-processor
      • Tau-system
      • Forward-chaining
      • Equivalence
      • Free-variables
      • Congruence
      • Executable-counterpart
      • Induction
      • Compound-recognizer
      • Elim
      • Well-founded-relation-rule
      • Rewrite-quoted-constant
      • Built-in-clause
      • Well-formedness-guarantee
      • Patterned-congruence
      • Rule-classes-introduction
      • Guard-holders
      • Refinement
      • Type-set-inverter
      • Generalize
      • Corollary
      • Induction-heuristics
      • Backchaining
      • Default-backchain-limit
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Rule-classes

Type-set-inverter

Exhibit a new decoding for an ACL2 type-set

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Example Rule Class:
(:type-set-inverter
  :corollary (equal (and (counting-number x) (not (equal x 0)))
                    (and (integerp x) (< 0 x)))
  :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*.