		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-called-lift-thms

List of lifting theorems for a set of relations.

Signature
(lift-thm-called-lift-thms rels wrld) → called-lift-thms
Arguments: rels — Guard (name-setp rels).; wrld — Guard (plist-worldp wrld).
Returns: called-lift-thms — Type (symbol-listp called-lift-thms).

These are used as rewrite rules in the caller's lifting theorem.

Definitions and Theorems

Function: lift-thm-called-lift-thms

(defun lift-thm-called-lift-thms (rels wrld)
  (declare (xargs :guard (and (name-setp rels)
                              (plist-worldp wrld))))
  (let ((__function__ 'lift-thm-called-lift-thms))
    (declare (ignorable __function__))
    (b* (((when (emptyp rels)) nil)
         (rel (head rels))
         (rel-pred (lift-rel-name rel wrld)))
      (cons (acl2::packn-pos (list 'definition-satp-to- rel-pred)
                             rel-pred)
            (lift-thm-called-lift-thms (tail rels)
                                       wrld)))))

Theorem: symbol-listp-of-lift-thm-called-lift-thms

(defthm symbol-listp-of-lift-thm-called-lift-thms
  (b* ((called-lift-thms (lift-thm-called-lift-thms rels wrld)))
    (symbol-listp called-lift-thms))
  :rule-classes :rewrite)