|
|
|---|
|
|
|
|---|
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.
Theorem:
(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:
(defthm booleanp-of-constraint-satp (b* ((yes/no (constraint-satp constr defs asg p))) (booleanp yes/no)) :rule-classes :rewrite)