		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-definition-satp-specialized-lemma

Generate a local lemma to apply the definition of definition-satp to a specific definition.

Signature
(lift-thm-definition-satp-specialized-lemma def pred prime) → (mv thm-event thm-name)
Arguments: def — Guard (definitionp def).; pred — Guard (symbolp pred).; prime — Guard (symbolp prime).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).

To prove the lifting theorem, we need to open definition-satp when applied to the name of the definition def that we are lifting. If def calls other definitions, in the course of the proof there will be other instances of definition-satp applied to the names of the called definitions. For these, definition-satp must not be opened, because we need to use the lifting theorems for those definitions. Thus, just enabling definition-satp is too coarse. In order to limit the application of this ACL2 definition, we generate a local lemma which is essentially the definition of definition-satp specialized to the name of the definition to be the one of def.

Definitions and Theorems

Function: lift-thm-definition-satp-specialized-lemma

(defun lift-thm-definition-satp-specialized-lemma (def pred prime)
 (declare (xargs :guard (and (definitionp def)
                             (symbolp pred)
                             (symbolp prime))))
 (let ((__function__ 'lift-thm-definition-satp-specialized-lemma))
  (declare (ignorable __function__))
  (b*
   ((def-name (definition->name def))
    (thm-name (acl2::packn-pos (list 'definition-satp-of- pred)
                               pred))
    (thm-event
     (cons
      'defruledl
      (cons
       thm-name
       (cons
        (cons
         'equal
         (cons
          (cons 'definition-satp
                (cons (cons 'quote (cons def-name 'nil))
                      (cons 'defs
                            (cons 'vals (cons prime 'nil)))))
          (cons
           (cons
            'b*
            (cons
             (cons
              (cons
                'def
                (cons (cons 'lookup-definition
                            (cons (cons 'quote (cons def-name 'nil))
                                  '(defs)))
                      'nil))
              (cons
               '((unless def) nil)
               (cons
                '(para (definition->para def))
                (cons
                 '((unless (equal (len vals) (len para)))
                   nil)
                 (cons
                  '(asg (omap::from-lists para vals))
                  (cons
                   (cons
                    'constr
                    (cons
                     (cons
                      'make-constraint-relation
                      (cons
                        ':name
                        (cons (cons 'quote (cons def-name 'nil))
                              '(:args (expression-var-list para)))))
                     'nil))
                   'nil))))))
             (cons
                  (cons 'constraint-satp
                        (cons 'constr
                              (cons 'defs
                                    (cons 'asg (cons prime 'nil)))))
                  'nil)))
           'nil)))
        '(:in-theory '(definition-satp)))))))
   (mv thm-event thm-name))))

Theorem: pseudo-event-formp-of-lift-thm-definition-satp-specialized-lemma.thm-event

(defthm
 pseudo-event-formp-of-lift-thm-definition-satp-specialized-lemma.thm-event
 (b* (((mv ?thm-event ?thm-name)
       (lift-thm-definition-satp-specialized-lemma def pred prime)))
   (pseudo-event-formp thm-event))
 :rule-classes :rewrite)

Theorem: symbolp-of-lift-thm-definition-satp-specialized-lemma.thm-name

(defthm
     symbolp-of-lift-thm-definition-satp-specialized-lemma.thm-name
 (b* (((mv ?thm-event ?thm-name)
       (lift-thm-definition-satp-specialized-lemma def pred prime)))
   (symbolp thm-name))
 :rule-classes :rewrite)