		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-forth-guard-instances-to-terms-back

Generate n lemma instances such that the i-th instance is of theorem forthi-guard and instantiates the formal parameter of forthi with a given term termi in which x1, ..., xn are replaced with (back1 x1), ..., (backn xn).

Signature
(isodata-gen-forth-guard-instances-to-terms-back terms old$ arg-isomaps wrld) → lemma-instances
Arguments: terms — Guard (pseudo-term-listp terms).; old$ — Guard (symbolp old$).; 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-forth-guard-instances-to-terms-back-aux

(defun isodata-gen-forth-guard-instances-to-terms-back-aux
       (terms arg-isomaps
              x1...xn back-of-x1...xn wrld)
 (declare
      (xargs :guard (and (pseudo-term-listp terms)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (symbol-listp x1...xn)
                         (pseudo-term-listp back-of-x1...xn)
                         (plist-worldp wrld))))
 (declare (xargs :guard (= (len terms) (len arg-isomaps))))
 (let ((__function__
            'isodata-gen-forth-guard-instances-to-terms-back-aux))
   (declare (ignorable __function__))
   (b*
     (((when (endp terms)) nil)
      (term (car terms))
      (isomap (cdar arg-isomaps))
      (forth-guard (isodata-isomap->forth-guard isomap))
      (var (isodata-formal-of-forth isomap wrld))
      (term-with-back (subcor-var x1...xn back-of-x1...xn term))
      (instance (list :instance forth-guard
                      :extra-bindings-ok (list var term-with-back)))
      (instances (isodata-gen-forth-guard-instances-to-terms-back-aux
                      (cdr terms)
                      (cdr arg-isomaps)
                      x1...xn back-of-x1...xn wrld)))
     (cons instance instances))))

Theorem: true-list-listp-of-isodata-gen-forth-guard-instances-to-terms-back-aux

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

Function: isodata-gen-forth-guard-instances-to-terms-back

(defun isodata-gen-forth-guard-instances-to-terms-back
       (terms old$ arg-isomaps wrld)
  (declare
       (xargs :guard (and (pseudo-term-listp terms)
                          (symbolp old$)
                          (isodata-symbol-isomap-alistp arg-isomaps)
                          (plist-worldp wrld))))
  (declare (xargs :guard (= (len terms) (len arg-isomaps))))
  (let
   ((__function__ 'isodata-gen-forth-guard-instances-to-terms-back))
   (declare (ignorable __function__))
   (b* ((x1...xn (formals old$ wrld))
        (back-of-x1...xn
             (isodata-gen-back-of-terms x1...xn arg-isomaps)))
     (isodata-gen-forth-guard-instances-to-terms-back-aux
          terms arg-isomaps
          x1...xn back-of-x1...xn wrld))))

Theorem: true-list-listp-of-isodata-gen-forth-guard-instances-to-terms-back

(defthm
 true-list-listp-of-isodata-gen-forth-guard-instances-to-terms-back
 (b* ((lemma-instances (isodata-gen-forth-guard-instances-to-terms-back
                            terms old$ arg-isomaps wrld)))
   (true-list-listp lemma-instances))
 :rule-classes :rewrite)