		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-def-hyps

Hypotheses about certain relations having the expected definitions.

Signature
(lift-thm-def-hyps def wrld) → hyps
Arguments: def — Guard (definitionp def).; wrld — Guard (plist-worldp wrld).
Returns: hyps — Type (true-listp hyps).

These are hypotheses in the generated lifting theorems. For each relation, whose definition is the def parameter passed to this function, we need the hypothesis that looking up the relation in defs (which is the variable, in the generated theorem, holding the definitions with respect to which the semntics is given) yields def. We also need the cumulative hypotheses of the same form of the relations called directly or indirectly by def: these are retrieved from the table of lifted PFCSes, taking the set-like union (thus avoiding duplicates) of each relation called.

Definitions and Theorems

Function: lift-thm-def-hyps-aux

(defun lift-thm-def-hyps-aux (crels tab)
  (declare (xargs :guard (and (constrel-setp crels)
                              (alistp tab))))
  (let ((__function__ 'lift-thm-def-hyps-aux))
    (declare (ignorable __function__))
    (b* (((when (emptyp crels)) nil)
         (crel (head crels))
         (name (constrel->name crel))
         (info (cdr (assoc-equal name tab)))
         ((unless info)
          (raise "Internal error: ~x0 not in table."
                 name))
         ((unless (lift-infop info))
          (raise "Internal error: ~x0 has the wrong type."
                 info))
         (hyps (lift-info->hyps info))
         (more-hyps (lift-thm-def-hyps-aux (tail crels)
                                           tab)))
      (union-equal hyps more-hyps))))

Theorem: true-listp-of-lift-thm-def-hyps-aux

(defthm true-listp-of-lift-thm-def-hyps-aux
  (b* ((more-hyps (lift-thm-def-hyps-aux crels tab)))
    (true-listp more-hyps))
  :rule-classes :rewrite)

Function: lift-thm-def-hyps

(defun lift-thm-def-hyps (def wrld)
  (declare (xargs :guard (and (definitionp def)
                              (plist-worldp wrld))))
  (let ((__function__ 'lift-thm-def-hyps))
    (declare (ignorable __function__))
    (b* (((definition def) def)
         (hyp (cons 'equal
                    (cons (cons 'lookup-definition
                                (cons def.name '(defs)))
                          (cons (cons 'quote (cons def 'nil))
                                'nil))))
         (crels (constraint-list-constrels def.body))
         (tab (table-alist+ 'lift-table wrld))
         (more-hyps (lift-thm-def-hyps-aux crels tab)))
      (cons hyp more-hyps))))

Theorem: true-listp-of-lift-thm-def-hyps

(defthm true-listp-of-lift-thm-def-hyps
  (b* ((hyps (lift-thm-def-hyps def wrld)))
    (true-listp hyps))
  :rule-classes :rewrite)