		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-to-old-thm-hints

Generate the hints to prove the theorem that expresses the new function in terms of the old function.

Signature
(isodata-gen-new-to-old-thm-hints appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name new-to-old-lemma-name new-to-list-of-mv-nth-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).; new-to-old-lemma-name — Guard (symbolp new-to-old-lemma-name).; new-to-list-of-mv-nth-name — Guard (symbolp new-to-list-of-mv-nth-name).; wrld — Guard (plist-worldp wrld).
Returns: hints — A true-listp.

Definitions and Theorems

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

(defun isodata-gen-new-to-old-thm-hints
       (appcond-thm-names old$ arg-isomaps
                          res-isomaps new$ old-fn-unnorm-name
                          new-fn-unnorm-name new-to-old-lemma-name
                          new-to-list-of-mv-nth-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)
                          (symbolp new-to-old-lemma-name)
                          (symbolp new-to-list-of-mv-nth-name)
                          (plist-worldp wrld))))
  (let ((__function__ 'isodata-gen-new-to-old-thm-hints))
    (declare (ignorable __function__))
    (case (len res-isomaps)
      (0 (isodata-gen-new-to-old-thm-hints-0res
              appcond-thm-names
              old$ arg-isomaps new$ old-fn-unnorm-name
              new-fn-unnorm-name wrld))
      (1 (isodata-gen-new-to-old-thm-hints-1res
              appcond-thm-names old$ arg-isomaps
              res-isomaps new$ old-fn-unnorm-name
              new-fn-unnorm-name wrld))
      (t (isodata-gen-new-to-old-thm-hints-mres
              new-to-old-lemma-name
              new-to-list-of-mv-nth-name)))))