		Search-engine friendly clone of the ACL2 documentation.

Uninterpreted-fn-cp

Generate-fn-hint-lst

(generate-fn-hint-lst args) generate auxiliary hypotheses from ~ function expansion

Signature
(generate-fn-hint-lst args) → fn-hint-lst
Arguments: args — Guard (fhg-args-p args).
Returns: fn-hint-lst — Type (fhg-args-p fn-hint-lst).

Definitions and Theorems

Function: generate-fn-hint-lst

(defun generate-fn-hint-lst (args)
 (declare (xargs :guard (fhg-args-p args)))
 (let ((acl2::__function__ 'generate-fn-hint-lst))
  (declare (ignorable acl2::__function__))
  (b*
   ((args (fhg-args-fix args))
    ((fhg-args a) args)
    ((unless (consp a.term-lst)) a)
    ((cons term rest) a.term-lst)
    ((if (symbolp term))
     (generate-fn-hint-lst (change-fhg-args a :term-lst rest)))
    ((if (equal (car term) 'quote))
     (generate-fn-hint-lst (change-fhg-args a :term-lst rest)))
    ((cons fn-call fn-actuals) term)
    ((if (pseudo-lambdap fn-call))
     (b*
       ((lambda-formals (lambda-formals fn-call))
        (lambda-body (lambda-body fn-call))
        (lambda-actuals fn-actuals)
        (lambda-bd (make-lambda-binding :formals lambda-formals
                                        :actuals lambda-actuals))
        ((unless (mbt (lambda-binding-p lambda-bd)))
         a)
        (a-1 (generate-fn-hint-lst
                  (change-fhg-args
                       a
                       :term-lst (list lambda-body)
                       :lambda-acc (cons lambda-bd a.lambda-acc))))
        (a-2 (generate-fn-hint-lst
                  (change-fhg-args a-1
                                   :term-lst lambda-actuals))))
       (generate-fn-hint-lst (change-fhg-args a-2 :term-lst rest))))
    ((unless (mbt (symbolp fn-call))) a)
    (fn (assoc-equal fn-call a.fn-lst))
    ((unless fn)
     (b* ((a-1 (generate-fn-hint-lst
                    (change-fhg-args a
                                     :term-lst fn-actuals))))
       (generate-fn-hint-lst (change-fhg-args a-1 :term-lst rest))))
    (f (cdr fn))
    (as-1
      (generate-fn-hint
           (make-fhg-single-args
                :fn f
                :actuals fn-actuals
                :fn-returns-hint-acc a.fn-returns-hint-acc
                :fn-more-returns-hint-acc a.fn-more-returns-hint-acc
                :lambda-acc a.lambda-acc)))
    ((fhg-single-args as-1) as-1)
    (a-1
      (change-fhg-args
           a
           :fn-returns-hint-acc as-1.fn-returns-hint-acc
           :fn-more-returns-hint-acc as-1.fn-more-returns-hint-acc))
    (a-2
     (generate-fn-hint-lst (change-fhg-args a-1
                                            :term-lst fn-actuals))))
   (generate-fn-hint-lst (change-fhg-args a-2 :term-lst rest)))))

Theorem: fhg-args-p-of-generate-fn-hint-lst

(defthm fhg-args-p-of-generate-fn-hint-lst
  (b* ((fn-hint-lst (generate-fn-hint-lst args)))
    (fhg-args-p fn-hint-lst))
  :rule-classes :rewrite)