Generate a local lemma to apply the definition of definition-satp to a specific definition.
(lift-thm-definition-satp-specialized-lemma def state) → (mv thm-event thm-name)
To prove the lifting theorem,
we need to open definition-satp
when applied to the name of the definition
Function:
(defun lift-thm-definition-satp-specialized-lemma (def state) (declare (xargs :stobjs (state))) (declare (xargs :guard (definitionp def))) (let ((__function__ 'lift-thm-definition-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 'definition-satp-of- pred-name) pred-name)) (thm-event (cons 'defruledl (cons thm-name (cons (cons 'equal (cons (cons 'definition-satp (cons def-name '(defs vals p))) (cons (cons 'b* (cons (cons (cons 'def (cons (cons 'lookup-definition (cons def-name '(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 def-name '(:args (expression-var-list para))))) 'nil)) 'nil)))))) '((constraint-satp constr defs asg p)))) 'nil))) '(:in-theory '(definition-satp))))))) (mv thm-event thm-name))))
Theorem:
(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 state))) (pseudo-event-formp thm-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-lift-thm-definition-satp-specialized-lemma.thm-name (b* (((mv ?thm-event ?thm-name) (lift-thm-definition-satp-specialized-lemma def state))) (symbolp thm-name)) :rule-classes :rewrite)