		Search-engine friendly clone of the ACL2 documentation.

Named-formulas

Named-formula-to-thm-event

Turn a named formula into a theorem event.

Signature
(named-formula-to-thm-event name formula hints rule-classes enabled local names-to-avoid wrld) → (mv thm-event thm-name)
Arguments: name — Name of the formula to turn into a theorem event.
Guard (symbolp name).; formula — Formula for the theorem event (an untranslated term).; hints — Hints for the theorem event.
Guard (true-listp hints).; rule-classes — Rule classes for the theorem event.; enabled — Make the theorem event enabled or not.
Guard (booleanp enabled).; local — Make the theorem event local or not.
Guard (booleanp local).; names-to-avoid — Avoid these as theorem name.
Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: thm-event — Theorem event (a pseudo-event-formp).; thm-name — Name of the theorem event (a symbolp).

If the name of the formula is not in use and not among the names to avoid, it is used as the name of the theorem event. Otherwise, it is made fresh by appending $ signs. If the initial name is a keyword, it is interned into the "ACL2" package before calling fresh-logical-name-with-$s-suffix, whose guard forbids keywords.

Definitions and Theorems

Function: named-formula-to-thm-event

(defun named-formula-to-thm-event
       (name formula hints rule-classes
             enabled local names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp name)
                             (true-listp hints)
                             (booleanp enabled)
                             (booleanp local)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'named-formula-to-thm-event))
  (declare (ignorable __function__))
  (b*
   ((defthm/defthmd (theorem-intro-macro enabled))
    (name (if (keywordp name)
              (intern (symbol-name name) "ACL2")
            name))
    ((mv thm-name &)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (thm-event
     (cons
       defthm/defthmd
       (cons thm-name
             (cons formula
                   (cons ':hints
                         (cons hints
                               (cons ':rule-classes
                                     (cons rule-classes 'nil))))))))
    (thm-event (if local (cons 'local (cons thm-event 'nil))
                 thm-event)))
   (mv thm-event thm-name))))