		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

Def-rule-const

Introduce an ACL2 constant for a (non-incremental) rule.

The name argument must be a valid constant name. The name argument is followed by a variable number of forms that must evaluate to concatenations, whose list is the alternation that is the definiens of the rule. The name of the constant that defines the rule is obtained from name by inserting rule_ just after the starting *.

Macro: def-rule-const

(defmacro def-rule-const (name &rest concatenation-forms)
 (cons
      'make-event
      (cons (cons 'def-rule-const-fn
                  (cons (cons 'quote (cons name 'nil))
                        (cons (cons 'quote
                                    (cons concatenation-forms 'nil))
                              'nil)))
            'nil)))

Definitions and Theorems

Function: def-rule-const-fn

(defun def-rule-const-fn (name concatenation-forms)
 (declare
   (xargs
        :guard (and (legal-constantp name)
                    (pseudo-event-form-listp concatenation-forms))))
 (b*
   ((name-string (symbol-name name))
    (name-chars (explode name-string))
    (name-chars-without-1st-* (cdr name-chars))
    (name-string-without-1st-* (implode name-chars-without-1st-*))
    (const-string (concatenate 'common-lisp::string
                               "*RULE_" name-string-without-1st-*))
    (const-name (intern-in-package-of-symbol const-string name)))
   (cons 'defval
         (cons const-name
               (cons (cons '=_
                           (cons name concatenation-forms))
                     'nil)))))

Theorem: pseudo-event-formp-of-def-rule-const-fn

(defthm pseudo-event-formp-of-def-rule-const-fn
  (b* ((const-event (def-rule-const-fn name concatenation-forms)))
    (pseudo-event-formp const-event))
  :rule-classes :rewrite)