		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-omap-keys-lemma-instances

Calculate lemmas instances for the lifting theorem.

Signature
(lift-thm-omap-keys-lemma-instances vars witness) → lemma-instances
Arguments: vars — Guard (name-setp vars).; witness — A term.
Returns: lemma-instances — Type (true-listp lemma-instances).

We generate one lemma instance for each variable passed as input. The lemma is the same for all instances.

Definitions and Theorems

Function: lift-thm-omap-keys-lemma-instances

(defun lift-thm-omap-keys-lemma-instances (vars witness)
 (declare (xargs :guard (name-setp vars)))
 (let ((__function__ 'lift-thm-omap-keys-lemma-instances))
  (declare (ignorable __function__))
  (cond
   ((emptyp vars) nil)
   (t
    (cons
     (cons
       ':instance
       (cons 'lift-rule-omap-in-to-in-of-keys
             (cons (cons 'key
                         (cons (cons 'quote (cons (head vars) 'nil))
                               'nil))
                   (cons (cons 'map (cons witness 'nil))
                         'nil))))
     (lift-thm-omap-keys-lemma-instances (tail vars)
                                         witness))))))

Theorem: true-listp-of-lift-thm-omap-keys-lemma-instances

(defthm true-listp-of-lift-thm-omap-keys-lemma-instances
  (b* ((lemma-instances
            (lift-thm-omap-keys-lemma-instances vars witness)))
    (true-listp lemma-instances))
  :rule-classes :rewrite)