		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-to-old-lemma-hints

Generate the hints to prove the lemma use to prove new-to-old when old is multi-valued and some result is transformed.

Signature
(isodata-gen-new-to-old-lemma-hints appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name wrld) → hints
Arguments: appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; new$ — Guard (symbolp new$).; old-fn-unnorm-name — Guard (symbolp old-fn-unnorm-name).; new-fn-unnorm-name — Guard (symbolp new-fn-unnorm-name).; wrld — Guard (plist-worldp wrld).
Returns: hints — A true-listp.

See isodata-gen-new-to-old-lemma for details.

Definitions and Theorems

Function: isodata-gen-new-to-old-lemma-hints

(defun isodata-gen-new-to-old-lemma-hints
       (appcond-thm-names old$ arg-isomaps
                          res-isomaps new$ old-fn-unnorm-name
                          new-fn-unnorm-name wrld)
 (declare
      (xargs :guard (and (symbol-symbol-alistp appcond-thm-names)
                         (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-pos-isomap-alistp res-isomaps)
                         (symbolp new$)
                         (symbolp old-fn-unnorm-name)
                         (symbolp new-fn-unnorm-name)
                         (plist-worldp wrld))))
 (let ((__function__ 'isodata-gen-new-to-old-lemma-hints))
  (declare (ignorable __function__))
  (if
   (recursivep old$ nil wrld)
   (b*
    ((rec-calls (recursive-calls old$ wrld))
     (oldp-of-rec-call-args
          (cdr (assoc-eq :oldp-of-rec-call-args appcond-thm-names)))
     (oldp-of-old (cdr (assoc-eq :oldp-of-old appcond-thm-names)))
     (instance-oldp-of-rec-call-args (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
                                          oldp-of-rec-call-args
                                          old$ arg-isomaps wrld))
     (instances-oldp-of-old (isodata-gen-lemma-instances-x1...xn-to-rec-call-args-back
                                 oldp-of-old
                                 rec-calls old$ arg-isomaps wrld))
     (instances-back-image (isodata-gen-back-image-instances-to-x1...xn
                                arg-isomaps wrld))
     (instances-forth-image (isodata-gen-all-forth-image-instances-to-terms-back
                                 rec-calls old$ arg-isomaps wrld))
     (instances-back-of-forth (isodata-gen-all-back-of-forth-instances-to-terms-back
                                   rec-calls old$ arg-isomaps wrld))
     (instances-back-of-forth-res
          (isodata-gen-all-back-of-forth-instances-to-mv-nth
               old$ rec-calls
               arg-isomaps res-isomaps wrld)))
    (cons
     (cons
      '"Goal"
      (cons
       ':in-theory
       (cons
        (cons
         'quote
         (cons (cons old-fn-unnorm-name
                     (cons new-fn-unnorm-name
                           (cons (cons ':induction (cons new$ 'nil))
                                 'nil)))
               'nil))
        (cons ':induct
              (cons (cons new$ (formals old$ wrld))
                    'nil)))))
     (cons
      (cons
       'quote
       (cons
        (cons
         ':use
         (cons
          (cons
           instance-oldp-of-rec-call-args
           (append
            instances-oldp-of-old
            (append instances-back-image
                    (append instances-forth-image
                            (append instances-back-of-forth
                                    instances-back-of-forth-res)))))
          'nil))
        'nil))
      'nil)))
   (cons
    (cons
       '"Goal"
       (cons ':in-theory
             (cons (cons 'quote
                         (cons (cons old-fn-unnorm-name
                                     (cons new-fn-unnorm-name 'nil))
                               'nil))
                   'nil)))
    'nil))))