|
|
|---|
|
|
|
|---|
Generate the theorem connecting deeply and shallowly embedded semantics.
(lift-thm def def-sat-lemma constr-sat-lemma
constr-to-def-sat-lemmas prime state)
→
(mv event def-hyps)Given a PFCS definition, sesem-definition generates a shallowly embedded version of it. Here we define a theorem connecting that shallowly embedded version to the deeply embedded semantics of the definition.
The theorem says that the satisfaction of the definition (expressed via definition-satp is equivalent to the satisfaction of the shallowly embedded definition.
When the definition has no free variables,
the theorem is proved by enabling certain definitions and rules.
The proof is obtained completely by rewriting.
Note that we use the specialized rules constructed in
lift-thm-definition-satp-specialized-lemma,
lift-thm-constr-satp-specialized-lemma, and
lift-thm-constr-to-def-satp-specialized-lemmas,
for the reasons discussed in their documentation.
The proof goes as follows:
(1) open definition-satp on
If the definition has free variables,
the shallowly embedded version of the definition is a defun-sk,
as is constraint-relation-satp;
the latter is what definition-satp gets rewritten to,
using the rules passed to the proof.
Both defun-sks are existentially quantified.
Essentially, we need to show that each one implies the other,
using the witness of one to calculate the witness of the other.
The proof naturally splits into two parts (`only if' and `if').
Each part if proved mostly by rewriting,
but we also need some lemma instances.
The lemma instances for the
Function:
(defun lift-thm (def def-sat-lemma constr-sat-lemma constr-to-def-sat-lemmas prime state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (definitionp def) (symbolp def-sat-lemma) (symbolp constr-sat-lemma) (symbol-listp constr-to-def-sat-lemmas) (symbolp prime)))) (let ((__function__ 'lift-thm)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((definition def) def) (pred-name (name-to-symbol def.name state)) (para (name-list-to-symbol-list def.para state)) (free (definition-free-vars def)) (quant (name-set-to-symbol-list free state)) (thm-name (acl2::packn-pos (list 'definition-satp-of- pred-name '-to-shallow) pred-name)) (def-hyps (lift-thm-def-hyps def wrld)) (rels (constraint-list-rels def.body)) (called-lift-thms (lift-thm-called-lift-thms (name-set-to-symbol-list rels state))) (type-presc-rules (lift-thm-type-prescriptions-for-called-preds rels state)) ((when (equal free nil)) (mv (cons 'defruled (cons thm-name (cons (cons 'implies (cons (cons 'and (append def-hyps (append (sesem-gen-fep-terms para prime) (cons (cons 'primep (cons prime 'nil)) 'nil)))) (cons (cons 'equal (cons (cons 'definition-satp (cons def.name (cons 'defs (cons (cons 'list para) (cons prime 'nil))))) (cons (cons pred-name (append para (cons prime 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons pred-name (cons (cons ':e (cons pred-name 'nil)) (cons def-sat-lemma (cons constr-sat-lemma (append constr-to-def-sat-lemmas (append called-lift-thms (cons 'constraint-relation-nofreevars-satp (cons 'constraint-list-satp-of-cons (cons 'constraint-list-satp-of-nil (cons 'constraint-satp-of-equal (cons 'constraint-equal-satp (cons 'eval-expr (cons 'eval-expr-list (cons '(:e definition->para) (cons '(:e definition->body) (cons '(:e definition-free-vars) (cons '(:e constraint-kind) (cons '(:e constraint-equal->left) (cons '(:e constraint-equal->right) (cons '(:e constraint-relation) (cons '(:e constraint-relation->name) (cons '(:e constraint-relation->args) (cons '(:e expression-kind) (cons '(:e expression-const->value) (cons '(:e expression-var->name) (cons '(:e expression-add->arg1) (cons '(:e expression-add->arg2) (cons '(:e expression-mul->arg1) (cons '(:e expression-mul->arg2) (cons '(:e expression-var-list) (cons 'assignment-wfp-of-update (cons 'assignment-wfp-of-nil (cons 'assignment-fix-when-assignmentp (cons 'assignmentp-of-update (cons '(:e assignmentp) (cons 'omap::from-lists (cons 'pfield::fep-fw-to-natp (cons 'pfield::natp-of-add (cons 'pfield::natp-of-mul (cons 'len (cons 'fty::consp-when-reserrp (cons 'acl2::natp-compound-recognizer (cons '(:e nat-listp) (cons '(:e emptyp) (cons 'car-cons (cons 'cdr-cons (cons 'omap::assoc-of-update (cons 'acl2::nat-listp-of-cons (cons 'acl2::not-reserrp-when-nat-listp (cons 'nfix (cons '(:t mod) (cons '(:e no-duplicatesp-equal) type-presc-rules)))))))))))))))))))))))))))))))))))))))))))))))))))) 'nil)) 'nil))))) def-hyps)) (constraint-relation-satp-witness (cons 'constraint-relation-satp-witness (cons def.name (cons (cons 'quote (cons (expression-var-list def.para) 'nil)) (cons 'defs (cons (cons 'omap::from-lists (cons (cons 'list def.para) (cons (cons 'list para) 'nil))) (cons prime 'nil))))))) (def-witness (cons (add-suffix-to-fn pred-name "-WITNESS") (append para (cons prime 'nil))))) (mv (cons 'defruled (cons thm-name (cons (cons 'implies (cons (cons 'and (append def-hyps (append (sesem-gen-fep-terms para prime) (cons (cons 'primep (cons prime 'nil)) 'nil)))) (cons (cons 'equal (cons (cons 'definition-satp (cons def.name (cons 'defs (cons (cons 'list para) (cons prime 'nil))))) (cons (cons pred-name (append para (cons prime 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons '(:t definition-satp) (cons (cons ':t (cons pred-name 'nil)) 'nil)) 'nil)) (cons ':use (cons '(only-if-direction if-direction) (cons ':prep-lemmas (cons (cons (cons 'defruled (cons 'only-if-direction (cons (cons 'implies (cons (cons 'and (append def-hyps (append (sesem-gen-fep-terms para prime) (cons (cons 'primep (cons prime 'nil)) 'nil)))) (cons (cons 'implies (cons (cons 'definition-satp (cons def.name (cons 'defs (cons (cons 'list para) (cons prime 'nil))))) (cons (cons pred-name (append para (cons prime 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons def-sat-lemma (cons constr-sat-lemma (append constr-to-def-sat-lemmas (append called-lift-thms (cons 'constraint-relation-satp (cons 'constraint-list-satp-of-cons (cons 'constraint-list-satp-of-nil (cons 'constraint-satp-of-equal (cons 'constraint-equal-satp (cons 'eval-expr (cons 'eval-expr-list (cons '(:e definition->para) (cons '(:e definition->body) (cons '(:e definition-free-vars) (cons '(:e constraint-kind) (cons '(:e constraint-equal->left) (cons '(:e constraint-equal->right) (cons '(:e constraint-relation) (cons '(:e constraint-relation->name) (cons '(:e constraint-relation->args) (cons '(:e expression-kind) (cons '(:e expression-const->value) (cons '(:e expression-var->name) (cons '(:e expression-add->arg1) (cons '(:e expression-add->arg2) (cons '(:e expression-mul->arg1) (cons '(:e expression-mul->arg2) (cons '(:e expression-var-list) (cons 'assignment-wfp-of-update* (cons 'assignment-wfp-of-update (cons 'assignment-wfp-of-nil (cons 'assignment-fix-when-assignmentp (cons 'assignmentp-of-update* (cons 'assignmentp-of-update (cons '(:e assignmentp) (cons 'omap::from-lists (cons 'pfield::fep-fw-to-natp (cons 'pfield::natp-of-add (cons 'pfield::natp-of-mul (cons 'len (cons 'fty::consp-when-reserrp (cons 'acl2::natp-compound-recognizer (cons '(:e nat-listp) (cons '(:e emptyp) (cons 'car-cons (cons 'cdr-cons (cons 'omap::assoc-of-update* (cons 'omap::assoc-of-update (cons 'acl2::nat-listp-of-cons (cons 'acl2::not-reserrp-when-nat-listp (cons 'lift-rule-nfix-when-natp (cons '(:t mod) (cons '(:t reserr) (cons 'fty::reserrp-of-reserr (cons 'lift-rule-omap-consp-of-assoc-iff-assoc (cons '(:e in) (cons 'natp-of-cdr-of-in-when-assignmentp-type (cons 'fep-of-cdr-of-in-when-assignment-wfp (cons '(:e no-duplicatesp-equal) type-presc-rules))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons (add-suffix-to-fn pred-name "-SUFF") (lift-thm-free-inst free constraint-relation-satp-witness state))) (lift-thm-omap-keys-lemma-instances (append def.para free) constraint-relation-satp-witness)) 'nil))))))) (cons (cons 'defruled (cons 'if-direction (cons (cons 'implies (cons (cons 'and (append def-hyps (append (sesem-gen-fep-terms para prime) (cons (cons 'primep (cons prime 'nil)) 'nil)))) (cons (cons 'implies (cons (cons pred-name (append para (cons prime 'nil))) (cons (cons 'definition-satp (cons def.name (cons 'defs (cons (cons 'list para) (cons prime 'nil))))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons pred-name (cons def-sat-lemma (cons constr-sat-lemma (append constr-to-def-sat-lemmas (append called-lift-thms (cons 'constraint-list-satp-of-cons (cons 'constraint-list-satp-of-nil (cons 'constraint-satp-of-equal (cons 'constraint-equal-satp (cons 'eval-expr (cons 'eval-expr-list (cons '(:e definition->para) (cons '(:e definition->body) (cons '(:e definition-free-vars) (cons '(:e constraint-kind) (cons '(:e constraint-equal->left) (cons '(:e constraint-equal->right) (cons '(:e constraint-relation) (cons '(:e constraint-relation->name) (cons '(:e constraint-relation->args) (cons '(:e expression-kind) (cons '(:e expression-const->value) (cons '(:e expression-var->name) (cons '(:e expression-add->arg1) (cons '(:e expression-add->arg2) (cons '(:e expression-mul->arg1) (cons '(:e expression-mul->arg2) (cons '(:e expression-var-list) (cons 'assignment-wfp-of-update* (cons 'assignment-wfp-of-update (cons 'assignment-wfp-of-nil (cons 'assignment-fix-when-assignmentp (cons 'assignmentp-of-update* (cons 'assignmentp-of-update (cons '(:e assignmentp) (cons 'omap::from-lists (cons 'pfield::fep-fw-to-natp (cons 'car-cons (cons 'cdr-cons (cons '(:e nat-listp) (cons 'omap::keys-of-update (cons 'omap::assoc-of-update* (cons 'omap::assoc-of-update (cons '(:e omap::keys) (cons '(:e insert) (cons 'len (cons 'lift-rule-nfix-when-natp (cons '(:e reserrp) (cons 'acl2::not-reserrp-when-natp (cons 'acl2::not-reserrp-when-nat-listp (cons 'nat-listp (cons '(:e omap::assoc) (cons 'lift-rule-natp-of-mod (cons '(:e natp) (cons '(:e no-duplicatesp-equal) (cons 'acl2::primep-forward-to-posp (append type-presc-rules '(pfield::natp-of-add pfield::natp-of-mul)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons 'constraint-relation-satp-suff (cons (cons 'asgfree (cons (cons 'omap::from-lists (cons (cons 'list free) (cons (cons 'list (lift-thm-asgfree-pairs quant def-witness)) 'nil))) 'nil)) (cons (cons 'name (cons def.name 'nil)) (cons (cons 'args (cons (cons 'expression-var-list (cons (cons 'list def.para) 'nil)) 'nil)) (cons (cons 'asg (cons (cons 'omap::from-lists (cons (cons 'list def.para) (cons (cons 'list para) 'nil))) 'nil)) 'nil)))))) 'nil) 'nil))))))) 'nil)) 'nil))))))))) def-hyps))))
Theorem:
(defthm pseudo-event-formp-of-lift-thm.event (b* (((mv acl2::?event ?def-hyps) (lift-thm def def-sat-lemma constr-sat-lemma constr-to-def-sat-lemmas prime state))) (pseudo-event-formp event)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-lift-thm.def-hyps (b* (((mv acl2::?event ?def-hyps) (lift-thm def def-sat-lemma constr-sat-lemma constr-to-def-sat-lemmas prime state))) (true-listp def-hyps)) :rule-classes :rewrite)