Characterization of a proof tree for a relation constraint.
If running a proof tree is successful and returns an assertion for a relation constraint, then the proof tree must be one for a relation application, and it has to satisfy a number of other requirements, explicated in this theorem.
This is used to prove constraint-satp-of-relation.
Theorem:
(defthm exec-proof-tree-when-constraint-relation (b* ((outcome (exec-proof-tree ptree defs p)) (asser (proof-outcome-assertion->get outcome)) (asg (assertion->asg asser)) (constr (assertion->constr asser)) (name (constraint-relation->name constr)) (args (constraint-relation->args constr)) (def (lookup-definition name defs)) (para (definition->para def)) (body (definition->body def)) (vals (eval-expr-list args asg p)) (asgfree (proof-tree-relation->asgfree ptree)) (asgpara (omap::from-lists para vals)) (outcome-sub (exec-proof-tree-list (proof-tree-relation->sub ptree) defs p)) (asser-sub (proof-list-outcome-assertions->get outcome-sub)) (asgsub (omap::update* asgfree asgpara))) (implies (and (proof-outcome-case outcome :assertion) (constraint-case constr :relation)) (and (proof-tree-case ptree :relation) (equal (proof-tree-relation->asg ptree) asg) (equal (proof-tree-relation->name ptree) name) (equal (proof-tree-relation->args ptree) args) def (nat-listp vals) (equal (len para) (len vals)) (assignment-wfp asgfree p) (equal (omap::keys asgfree) (definition-free-vars def)) (proof-list-outcome-case outcome-sub :assertions) (equal (assertion-list->asg-list asser-sub) (repeat (len body) asgsub)) (equal (assertion-list->constr-list asser-sub) body)))))