		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res

Generate the hints to verify the guards of the new function, when the function is not recursive, when :predicate is nil, and no result is being transformed.

Signature
(isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res old$ arg-isomaps wrld) → hints
Arguments: old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; wrld — Guard (plist-worldp wrld).
Returns: hints — Type (true-listp hints).

Definitions and Theorems

Function: isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res

(defun isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res
       (old$ arg-isomaps wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (plist-worldp wrld))))
 (let
  ((__function__
       'isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res))
  (declare (ignorable __function__))
  (b*
   ((instance-guard-thm-old
         (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
              (cons ':guard-theorem (cons old$ 'nil))
              old$ arg-isomaps wrld))
    (instances-newp-guard
     (isodata-gen-newp-guard-instances-to-x1...xn arg-isomaps wrld))
    (instances-back-guard (isodata-gen-back-guard-instances-to-x1...xn
                               arg-isomaps wrld)))
   (cons
    (cons
        '"Goal"
        (cons ':in-theory
              (cons 'nil
                    (cons ':use
                          (cons (cons instance-guard-thm-old
                                      (append instances-newp-guard
                                              instances-back-guard))
                                'nil)))))
    'nil))))

Theorem: true-listp-of-isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res

(defthm
 true-listp-of-isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res
 (b* ((hints (isodata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res
                  old$ arg-isomaps wrld)))
   (true-listp hints))
 :rule-classes :rewrite)