		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Constraint-satp

Semantic function checking if a constaint is satisfied, given a list of definitions, an assignment, and a prime field.

Given the proof system formalized above, defining the semantic function discussed in semantics-deeply-embedded is easily done, by existentially quantifying over proof trees. That is, there must exist a proof tree that successfully proves the assertion corresponding to the assignment and constraint.

Definitions and Theorems

Theorem: constraint-satp-suff

(defthm constraint-satp-suff
 (implies
  (and
    (proof-treep ptree)
    (equal
         (exec-proof-tree ptree defs p)
         (proof-outcome-assertion (make-assertion :asg asg
                                                  :constr constr))))
  (constraint-satp constr defs asg p)))

Theorem: booleanp-of-constraint-satp

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