Generate local lemmas to apply constraint-satp-to-definition-satp to specific relations.
(lift-thm-constr-to-def-satp-specialized-lemmas rels state) → (mv thm-events 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
Function:
(defun lift-thm-constr-to-def-satp-specialized-lemmas (rels state) (declare (xargs :stobjs (state))) (declare (xargs :guard (string-setp rels))) (let ((__function__ 'lift-thm-constr-to-def-satp-specialized-lemmas)) (declare (ignorable __function__)) (b* (((when (emptyp rels)) (mv nil nil)) (rel (head rels)) (pred-name (name-to-symbol rel state)) (thm-name (acl2::packn-pos (list 'constraint-satp-to-definition-satp-of- pred-name) pred-name)) (thm-event (cons 'defruledl (cons thm-name (cons (cons 'implies (cons (cons 'and (cons '(primep p) (cons '(assignmentp asg) (cons '(assignment-wfp asg p) (cons '(constraint-case constr :relation) (cons (cons 'equal (cons '(constraint-relation->name constr) (cons rel 'nil))) (cons (cons 'no-duplicatesp-equal (cons (cons 'definition->para (cons (cons 'lookup-definition (cons rel '(defs))) 'nil)) 'nil)) 'nil))))))) (cons (cons 'b* (cons '((vals (eval-expr-list (constraint-relation->args constr) asg p))) (cons (cons 'implies (cons '(not (reserrp vals)) (cons (cons 'equal (cons '(constraint-satp constr defs asg p) (cons (cons 'definition-satp (cons rel '(defs vals p))) '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) state))) (mv (cons thm-event thm-events) (cons thm-name thm-names)))))
Theorem:
(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 state))) (pseudo-event-form-listp thm-events)) :rule-classes :rewrite)
Theorem:
(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 state))) (symbol-listp thm-names)) :rule-classes :rewrite)