		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-constr-satp-specialized-lemma

Generate a local lemma to apply constraint-satp-of-relation or constraint-satp-of-relation-when-nofreevars to a specific relation constraint.

Signature
(lift-thm-constr-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).

This is analogous in purpose to lift-thm-definition-satp-specialized-lemma, but for a different rule: the choice between the two aforementioned rules is determined by whether the definition def has free variables or not. In the lifting theorem, we need to apply this rule to the constraint obtained by opening definition-satp on def, but not on the constraints for any relations called by def, because for those we want to apply a different rule. So the local lemma that we generate here limits application to the constraint with the name of def.

Definitions and Theorems

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

(defun lift-thm-constr-satp-specialized-lemma (def pred prime)
 (declare (xargs :guard (and (definitionp def)
                             (symbolp pred)
                             (symbolp prime))))
 (let ((__function__ 'lift-thm-constr-satp-specialized-lemma))
  (declare (ignorable __function__))
  (b*
   ((def-name (definition->name def))
    (thm-name (acl2::packn-pos (list 'constraint-satp-of- pred)
                               pred))
    (thm-event
     (if
      (emptyp (definition-free-vars def))
      (cons
       'defruledl
       (cons
        thm-name
        (cons
         (cons
          'implies
          (cons
           (cons
            'and
            (cons
             '(assignmentp asg)
             (cons
              (cons 'assignment-wfp
                    (cons 'asg (cons prime 'nil)))
              (cons
               '(constraint-case constr :relation)
               (cons
                (cons 'equal
                      (cons '(constraint-relation->name constr)
                            (cons (cons 'quote (cons def-name 'nil))
                                  'nil)))
                'nil)))))
           (cons
            (cons
             'b*
             (cons
              (cons
               '(args (constraint-relation->args constr))
               (cons
                (cons
                 'def
                 (cons
                      (cons 'lookup-definition
                            (cons (cons 'quote (cons def-name 'nil))
                                  '(defs)))
                      'nil))
                'nil))
              (cons
               (cons
                'implies
                (cons
                 '(and def (emptyp (definition-free-vars def)))
                 (cons
                  (cons
                   'equal
                   (cons
                    (cons
                        'constraint-satp
                        (cons 'constr
                              (cons 'defs
                                    (cons 'asg (cons prime 'nil)))))
                    (cons
                     (cons
                      'constraint-relation-nofreevars-satp
                      (cons
                       (cons 'quote (cons def-name 'nil))
                       (cons 'args
                             (cons 'defs
                                   (cons 'asg (cons prime 'nil))))))
                     'nil)))
                  'nil)))
               'nil)))
            'nil)))
         '(:in-theory
               '(constraint-satp-of-relation-when-nofreevars)))))
      (cons
       'defruledl
       (cons
        thm-name
        (cons
         (cons
          'implies
          (cons
           (cons
            'and
            (cons
             '(assignmentp asg)
             (cons
              (cons 'assignment-wfp
                    (cons 'asg (cons prime 'nil)))
              (cons
               '(constraint-case constr :relation)
               (cons
                (cons 'equal
                      (cons '(constraint-relation->name constr)
                            (cons (cons 'quote (cons def-name 'nil))
                                  'nil)))
                'nil)))))
           (cons
            (cons
             'equal
             (cons
              (cons 'constraint-satp
                    (cons 'constr
                          (cons 'defs
                                (cons 'asg (cons prime 'nil)))))
              (cons
               (cons
                 'constraint-relation-satp
                 (cons (cons 'quote (cons def-name 'nil))
                       (cons '(constraint-relation->args constr)
                             (cons 'defs
                                   (cons 'asg (cons prime 'nil))))))
               'nil)))
            'nil)))
         '(:in-theory '(constraint-satp-of-relation))))))))
   (mv thm-event thm-name))))

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

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

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

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