		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-appcond-thm

Generate a theorem event from an applicability condition.

Signature
(defmapping-gen-appcond-thm appcond appcond-thm-names thm-names$ thm-enable$ wrld) → (mv local-event exported-event)
Arguments: appcond — Guard (evmac-appcondp appcond).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; thm-enable$ — Guard (keyword-listp thm-enable$).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

All the applicability conditions that must hold for the defmapping call are turned into theorems exported from the encapsulate. To keep the ACL2 history ``clean'', we generate the theorem in local form with a :by hint (the references the local theorem name of the applicability condition; this name generally differs from the theorem name determined by :thm-names), and in non-local, redundant form without hints.

Definitions and Theorems

Function: defmapping-gen-appcond-thm

(defun defmapping-gen-appcond-thm
       (appcond appcond-thm-names
                thm-names$ thm-enable$ wrld)
 (declare
      (xargs :guard (and (evmac-appcondp appcond)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbol-symbol-alistp thm-names$)
                         (keyword-listp thm-enable$)
                         (plist-worldp wrld))))
 (let ((__function__ 'defmapping-gen-appcond-thm))
  (declare (ignorable __function__))
  (b*
   (((evmac-appcond appcond) appcond)
    (thm-name (cdr (assoc-eq appcond.name thm-names$)))
    (thm-formula (untranslate appcond.formula t wrld))
    (thm-hints
     (cons
      (cons
         '"Goal"
         (cons ':by
               (cons (cdr (assoc-eq appcond.name appcond-thm-names))
                     'nil)))
      'nil))
    (defthmr/defthmdr (if (member-eq appcond.name thm-enable$)
                          'defthmr
                        'defthmdr))
    (local-event
     (cons
      'local
      (cons
           (cons defthmr/defthmdr
                 (cons thm-name
                       (cons thm-formula
                             (cons ':hints (cons thm-hints 'nil)))))
           'nil)))
    (exported-event (cons defthmr/defthmdr
                          (cons thm-name (cons thm-formula 'nil)))))
   (mv local-event exported-event))))