		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-old-to-new-thm

Generate the theorem that relates the old and new function.

Signature
(parteval-gen-old-to-new-thm old$ static$ new-name$ thm-name$ thm-enable$ case new-formals wrld) → (mv local-event exported-event)
Arguments: old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; new-name$ — Guard (symbolp new-name$).; thm-name$ — Guard (symbolp thm-name$).; thm-enable$ — Guard (booleanp thm-enable$).; case — Guard (member case '(1 2 3)).; new-formals — Guard (symbol-listp new-formals).; 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 theorem is an implication, whose antecedent is (and (equal y1 c1) ... (equal ym cm)) and whose consequent is (using the notation in the documentation) (equal (old x1 ... xn y1 ... ym) (new x1 ... xn)).

The hints follow the proof in the design notes and in parteval-template.lisp.

Definitions and Theorems

Function: parteval-gen-old-to-new-thm

(defun parteval-gen-old-to-new-thm
       (old$ static$ new-name$ thm-name$
             thm-enable$ case new-formals wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbol-alistp static$)
                             (symbolp new-name$)
                             (symbolp thm-name$)
                             (booleanp thm-enable$)
                             (member case '(1 2 3))
                             (symbol-listp new-formals)
                             (plist-worldp wrld))))
 (let ((__function__ 'parteval-gen-old-to-new-thm))
  (declare (ignorable __function__))
  (b*
   ((equalities (parteval-gen-static-equalities static$))
    (antecedent (conjoin equalities))
    (consequent (cons 'equal
                      (cons (cons old$ (formals old$ wrld))
                            (cons (cons new-name$ new-formals)
                                  'nil))))
    (formula (implicate antecedent consequent))
    (formula (untranslate formula t wrld))
    (hints
     (case case
      (1
       (cons
        (cons
           '"Goal"
           (cons ':in-theory
                 (cons (cons 'quote
                             (cons (cons old$ (cons new-name$ 'nil))
                                   'nil))
                       'nil)))
        'nil))
      (2
       (cons
        (cons
           '"Goal"
           (cons ':in-theory
                 (cons (cons 'quote
                             (cons (cons old$ (cons new-name$ 'nil))
                                   'nil))
                       (cons ':induct
                             (cons (cons new-name$ new-formals)
                                   'nil)))))
        'nil))
      (3
       (cons
          (cons '"Goal"
                (cons ':in-theory
                      (cons (cons 'quote
                                  (cons (cons new-name$ 'nil) 'nil))
                            'nil)))
          'nil))
      (t (impossible)))))
   (evmac-generate-defthm thm-name$
                          :formula formula
                          :hints hints
                          :enable thm-enable$))))