		Search-engine friendly clone of the ACL2 documentation.

Restrict-event-generation

Restrict-gen-new-to-old

Generate the theorem that relates the new and old functions.

Signature
(restrict-gen-new-to-old old restriction new new-to-old new-to-old-enable old-to-new wrld) → (mv local-event exported-event)
Arguments: old — Guard (symbolp old).; restriction — Guard (pseudo-termp restriction).; new — Guard (symbolp new).; new-to-old — Guard (symbolp new-to-old).; new-to-old-enable — Guard (booleanp new-to-old-enable).; old-to-new — Guard (symbolp old-to-new).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

The macro used to introduce the theorem is determined by whether the theorem must be enabled or not.

The formula of the theorem equates new and old functions under the restricting predicate, as described in the documentation.

The theorem is easily proved from the old-to-new one.

Definitions and Theorems

Function: restrict-gen-new-to-old

(defun restrict-gen-new-to-old
       (old restriction new new-to-old
            new-to-old-enable old-to-new wrld)
 (declare (xargs :guard (and (symbolp old)
                             (pseudo-termp restriction)
                             (symbolp new)
                             (symbolp new-to-old)
                             (booleanp new-to-old-enable)
                             (symbolp old-to-new)
                             (plist-worldp wrld))))
 (let ((__function__ 'restrict-gen-new-to-old))
  (declare (ignorable __function__))
  (b*
   ((formals (formals old wrld))
    (formula
         (implicate restriction
                    (cons 'equal
                          (cons (cons new formals)
                                (cons (cons old formals) 'nil)))))
    (formula (untranslate formula t wrld))
    (hints
     (cons
         (cons '"Goal"
               (cons ':in-theory
                     (cons (cons 'quote
                                 (cons (cons old-to-new 'nil) 'nil))
                           'nil)))
         'nil)))
   (evmac-generate-defthm new-to-old
                          :formula formula
                          :hints hints
                          :enable new-to-old-enable))))