		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-new-to-old-thm-formula

Generate the formula of the theorem that expresses the new function in terms of the old function.

Signature
(expdata-gen-new-to-old-thm-formula old$ arg-surjmaps res-surjmaps new$ wrld) → new-to-old-formula
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; new$ — Guard (symbolp new$).; wrld — Guard (plist-worldp wrld).
Returns: new-to-old-formula — A pseudo-termp.

Definitions and Theorems

Function: expdata-gen-new-to-old-thm-formula

(defun expdata-gen-new-to-old-thm-formula
       (old$ arg-surjmaps res-surjmaps new$ wrld)
 (declare
     (xargs :guard (and (symbolp old$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (symbolp new$)
                        (plist-worldp wrld))))
 (let ((__function__ 'expdata-gen-new-to-old-thm-formula))
  (declare (ignorable __function__))
  (b*
   ((x1...xn (formals old$ wrld))
    (newp-of-x1...xn
         (expdata-gen-newp-of-terms x1...xn arg-surjmaps))
    (back-of-x1...xn
         (expdata-gen-back-of-terms x1...xn arg-surjmaps))
    (old-call (fcons-term old$ back-of-x1...xn))
    (new-call (fcons-term new$ x1...xn))
    (consequent
     (case (len res-surjmaps)
      (0 (cons 'equal
               (cons new-call (cons old-call 'nil))))
      (1
       (b* ((forth-res (expdata-surjmap->forth (cdar res-surjmaps)))
            (forth-of-old-call (apply-term* forth-res old-call)))
         (cons 'equal
               (cons new-call
                     (cons forth-of-old-call 'nil)))))
      (t (b* ((mv-nths-of-new-call
                   (make-mv-nth-calls new-call (len res-surjmaps)))
              (mv-nths-of-old-call
                   (make-mv-nth-calls old-call (len res-surjmaps)))
              (forth-of-mv-nths-of-old-call
                   (expdata-gen-forth-of-terms
                        mv-nths-of-old-call res-surjmaps)))
           (conjoin-equalities mv-nths-of-new-call
                               forth-of-mv-nths-of-old-call))))))
   (implicate (conjoin newp-of-x1...xn)
              consequent))))