		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-constr-to-def-satp-specialized-lemmas

Generate local lemmas to apply constraint-satp-to-definition-satp to specific relations.

Signature
(lift-thm-constr-to-def-satp-specialized-lemmas rels prime wrld) → (mv thm-events thm-names)
Arguments: rels — Guard (name-setp rels).; prime — Guard (symbolp prime).; wrld — Guard (plist-worldp wrld).
Returns: thm-events — Type (pseudo-event-form-listp thm-events).; thm-names — Type (symbol-listp thm-names).

This is somewhat analogous to lift-thm-definition-satp-specialized-lemma and lift-thm-constr-satp-specialized-lemma, but it is not for the definition def being lifted, but instead for the relations called by def. In the proofs, we need to rewrite constraintp to the constraint relations in the body of def to equivalent definition-satp, so that we can apply the lifting theorems for those relations. So here we go through all the relations called by def and we generate one specialized theorem for each.

Definitions and Theorems

Function: lift-thm-constr-to-def-satp-specialized-lemmas

(defun lift-thm-constr-to-def-satp-specialized-lemmas
       (rels prime wrld)
 (declare (xargs :guard (and (name-setp rels)
                             (symbolp prime)
                             (plist-worldp wrld))))
 (let
   ((__function__ 'lift-thm-constr-to-def-satp-specialized-lemmas))
  (declare (ignorable __function__))
  (b*
   (((when (emptyp rels)) (mv nil nil))
    (rel (head rels))
    (rel-pred (lift-rel-name rel wrld))
    (thm-name
      (acl2::packn-pos (list 'constraint-satp-to-definition-satp-of-
                             rel-pred)
                       rel-pred))
    (thm-event
     (cons
      'defruledl
      (cons
       thm-name
       (cons
        (cons
         'implies
         (cons
          (cons
           'and
           (cons
            (cons 'primep (cons prime 'nil))
            (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 rel 'nil))
                                  'nil)))
                (cons
                 (cons
                  'no-duplicatesp-equal
                  (cons
                   (cons
                     'definition->para
                     (cons (cons 'lookup-definition
                                 (cons (cons 'quote (cons rel 'nil))
                                       '(defs)))
                           'nil))
                   'nil))
                 'nil)))))))
          (cons
           (cons
            'b*
            (cons
             (cons
              (cons
               'vals
               (cons (cons 'eval-expr-list
                           (cons '(constraint-relation->args constr)
                                 (cons 'asg (cons prime 'nil))))
                     'nil))
              'nil)
             (cons
              (cons
               'implies
               (cons
                '(not (reserrp vals))
                (cons
                 (cons
                  'equal
                  (cons
                   (cons
                        'constraint-satp
                        (cons 'constr
                              (cons 'defs
                                    (cons 'asg (cons prime 'nil)))))
                   (cons
                    (cons
                       'definition-satp
                       (cons (cons 'quote (cons rel 'nil))
                             (cons 'defs
                                   (cons 'vals (cons prime 'nil)))))
                    'nil)))
                 'nil)))
              'nil)))
           'nil)))
        '(:in-theory '(constraint-satp-to-definition-satp))))))
    ((mv thm-events thm-names)
     (lift-thm-constr-to-def-satp-specialized-lemmas (tail rels)
                                                     prime wrld)))
   (mv (cons thm-event thm-events)
       (cons thm-name thm-names)))))

Theorem: pseudo-event-form-listp-of-lift-thm-constr-to-def-satp-specialized-lemmas.thm-events

(defthm
 pseudo-event-form-listp-of-lift-thm-constr-to-def-satp-specialized-lemmas.thm-events
 (b* (((mv ?thm-events ?thm-names)
       (lift-thm-constr-to-def-satp-specialized-lemmas
            rels prime wrld)))
   (pseudo-event-form-listp thm-events))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-lift-thm-constr-to-def-satp-specialized-lemmas.thm-names

(defthm
 symbol-listp-of-lift-thm-constr-to-def-satp-specialized-lemmas.thm-names
 (b* (((mv ?thm-events ?thm-names)
       (lift-thm-constr-to-def-satp-specialized-lemmas
            rels prime wrld)))
   (symbol-listp thm-names))
 :rule-classes :rewrite)