Generate a local lemma to apply constraint-satp-of-relation or constraint-satp-of-relation-when-nofreevars to a specific relation constraint.
(lift-thm-constr-satp-specialized-lemma def state) → (mv thm-event 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
Function:
(defun lift-thm-constr-satp-specialized-lemma (def state) (declare (xargs :stobjs (state))) (declare (xargs :guard (definitionp def))) (let ((__function__ 'lift-thm-constr-satp-specialized-lemma)) (declare (ignorable __function__)) (b* ((def-name (definition->name def)) (pred-name (name-to-symbol def-name state)) (thm-name (acl2::packn-pos (list 'constraint-satp-of- pred-name) pred-name)) (thm-event (if (emptyp (definition-free-vars def)) (cons 'defruledl (cons thm-name (cons (cons 'implies (cons (cons 'and (cons '(assignmentp asg) (cons '(assignment-wfp asg p) (cons '(constraint-case constr :relation) (cons (cons 'equal (cons '(constraint-relation->name constr) (cons def-name 'nil))) 'nil))))) (cons (cons 'b* (cons (cons '(args (constraint-relation->args constr)) (cons (cons 'def (cons (cons 'lookup-definition (cons def-name '(defs))) 'nil)) 'nil)) (cons (cons 'implies (cons '(and def (emptyp (definition-free-vars def))) (cons (cons 'equal (cons '(constraint-satp constr defs asg p) (cons (cons 'constraint-relation-nofreevars-satp (cons def-name '(args defs asg p))) '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 '(assignment-wfp asg p) (cons '(constraint-case constr :relation) (cons (cons 'equal (cons '(constraint-relation->name constr) (cons def-name 'nil))) 'nil))))) (cons (cons 'equal (cons '(constraint-satp constr defs asg p) (cons (cons 'constraint-relation-satp (cons def-name '((constraint-relation->args constr) defs asg p))) 'nil))) 'nil))) '(:in-theory '(constraint-satp-of-relation)))))))) (mv thm-event thm-name))))
Theorem:
(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 state))) (pseudo-event-formp thm-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-lift-thm-constr-satp-specialized-lemma.thm-name (b* (((mv ?thm-event ?thm-name) (lift-thm-constr-satp-specialized-lemma def state))) (symbolp thm-name)) :rule-classes :rewrite)