		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-fn

Lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.

Signature
(lift-fn def prime state) → event
Arguments: def — Guard (definitionp def).; prime — Guard (symbolp prime).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: lift-fn

(defun lift-fn (def prime state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (definitionp def)
                             (symbolp prime))))
 (let ((__function__ 'lift-fn))
  (declare (ignorable __function__))
  (b* ((event-fn (sesem-definition def prime state))
       ((mv event-def-sat def-sat-lemma)
        (lift-thm-definition-satp-specialized-lemma def state))
       ((mv event-constr-sat constr-sat-lemma)
        (lift-thm-constr-satp-specialized-lemma def state))
       ((mv events-constr-to-def-sat
            constr-to-def-sat-lemmas)
        (lift-thm-constr-to-def-satp-specialized-lemmas
             (constraint-list-rels (definition->body def))
             state))
       ((mv event-thm def-hyps)
        (lift-thm def def-sat-lemma constr-sat-lemma
                  constr-to-def-sat-lemmas prime state))
       (event-table (lift-table-add def def-hyps)))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
         event-fn
         (cons event-def-sat
               (cons event-constr-sat
                     (append events-constr-to-def-sat
                             (cons event-thm
                                   (cons event-table 'nil)))))))))))

Theorem: pseudo-event-formp-of-lift-fn

(defthm pseudo-event-formp-of-lift-fn
  (b* ((event (lift-fn def prime state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)