		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 (string-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 (string-setp free)))
 (let ((__function__ 'lift-thm-free-inst))
  (declare (ignorable __function__))
  (cond
   ((emptyp free) nil)
   (t
    (b* ((var (head free)))
     (cons
       (cons (name-to-symbol var state)
             (cons (cons 'cdr
                         (cons (cons 'omap::assoc
                                     (cons var (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)