		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Constraint-relation-satp

Satisfaction of a relation constraint, expressed without proof trees.

This is an alternative definition of constraint-satp for the case in which the constraint is an application of a relation. We prove below its equivalence to constraint-satp.

This is a simpler definition, because it does not directly involve the execution of proof trees. It says that the relation application is satisfied exactly when there exists an assignment that extends the one binding the relation's parameters to the values of the arguments, and that satisfies all the relation's constraints.

Definitions and Theorems

Theorem: constraint-relation-satp-suff

(defthm constraint-relation-satp-suff
 (implies
  (and
   (assignmentp asgfree)
   (assignment-wfp asgfree p)
   (b* ((def (lookup-definition name defs)))
    (and
     def
     (b* (((definition def) def))
      (and
       (equal (len args) (len def.para))
       (b* ((vals (eval-expr-list args asg p)))
        (and
         (nat-listp vals)
         (b* ((asg-para-vals (omap::from-lists def.para vals)))
          (and
           (equal (omap::keys asgfree)
                  (definition-free-vars def))
           (b* ((asg-sub (omap::update* asgfree asg-para-vals)))
            (constraint-list-satp def.body defs asg-sub p)))))))))))
  (constraint-relation-satp name args defs asg p)))

Theorem: booleanp-of-constraint-relation-satp

(defthm booleanp-of-constraint-relation-satp
  (b* ((yes/no (constraint-relation-satp name args defs asg p)))
    (booleanp yes/no))
  :rule-classes :rewrite)