		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-back-of-forth-instances-to-x1...xn

Generate n lemma instances such that the i-th instance is of theorem backi-of-forthi and instantiates the formal parameter of forth with xi.

Signature
(isodata-gen-back-of-forth-instances-to-x1...xn arg-isomaps wrld) → lemma-instances
Arguments: arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; wrld — Guard (plist-worldp wrld).
Returns: lemma-instances — Type (true-list-listp lemma-instances).

Definitions and Theorems

Function: isodata-gen-back-of-forth-instances-to-x1...xn

(defun isodata-gen-back-of-forth-instances-to-x1...xn
       (arg-isomaps wrld)
 (declare
      (xargs :guard (and (isodata-symbol-isomap-alistp arg-isomaps)
                         (plist-worldp wrld))))
 (let
   ((__function__ 'isodata-gen-back-of-forth-instances-to-x1...xn))
   (declare (ignorable __function__))
   (b* (((when (endp arg-isomaps)) nil)
        (arg (caar arg-isomaps))
        (isomap (cdar arg-isomaps))
        (back-of-forth (isodata-isomap->back-of-forth isomap))
        (forth-arg
             (isodata-formal-of-unary (isodata-isomap->forth isomap)
                                      wrld))
        (instance (list :instance back-of-forth
                        :extra-bindings-ok (list forth-arg arg)))
        (instances (isodata-gen-back-of-forth-instances-to-x1...xn
                        (cdr arg-isomaps)
                        wrld)))
     (cons instance instances))))

Theorem: true-list-listp-of-isodata-gen-back-of-forth-instances-to-x1...xn

(defthm
  true-list-listp-of-isodata-gen-back-of-forth-instances-to-x1...xn
  (b* ((lemma-instances (isodata-gen-back-of-forth-instances-to-x1...xn
                             arg-isomaps wrld)))
    (true-list-listp lemma-instances))
  :rule-classes :rewrite)