		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Exec-proof-tree-when-constraint-relation

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.

Definitions and Theorems

Theorem: exec-proof-tree-when-constraint-relation

(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)))))