		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-free-inst

Calculate an instantiation of free variables.

Signature
(lift-thm-free-inst free witness state) → doublets
Arguments: free — Guard (name-setp free).; witness — A term.
Returns: doublets — Type (doublet-listp doublets).

This is used to prove the lifting theorem, precisely the `only if' direction of the theorem for the case in which the relation has free variables. This instantiation is used in a lemma instance (see lift-thm). The instantiation replaces each variable with its lookup in the witness term of the defun-sk.

Definitions and Theorems

Function: lift-thm-free-inst

(defun lift-thm-free-inst (free witness state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (name-setp free)))
 (let ((__function__ 'lift-thm-free-inst))
  (declare (ignorable __function__))
  (cond
   ((emptyp free) nil)
   (t
    (b* ((var (head free)))
     (cons
      (cons
         (lift-var-name var state)
         (cons (cons 'cdr
                     (cons (cons 'omap::assoc
                                 (cons (cons 'quote (cons var 'nil))
                                       (cons witness 'nil)))
                           'nil))
               'nil))
      (lift-thm-free-inst (tail free)
                          witness state)))))))

Theorem: doublet-listp-of-lift-thm-free-inst

(defthm doublet-listp-of-lift-thm-free-inst
  (b* ((doublets (lift-thm-free-inst free witness state)))
    (doublet-listp doublets))
  :rule-classes :rewrite)