Define a rule that recognizes constraints among FGL generated Boolean variables

When using FGL in a term-level style FGL may generate new Boolean variables from terms that appear as IF tests.

Sometimes, the terms from which these variables are generated have
interdependent meanings. For example, if Boolean variable

A Boolean constraint rule is formulated as follows:

(def-fgl-boolean-constraint fgl-logbitp-implies-integerp :bindings ((bit (logbitp n x)) (intp (integerp x))) :body (implies bit intp) ;; optional arguments: :syntaxp ... :hints ...)

This generates a proof obligation:

(defthm fgl-logbitp-implies-integerp (let ((bit (fgl-bool-fix (logbitp n x))) (intp (fgl-bool-fix (integerp x)))) (implies bit intp)) :hints ... :rule-classes nil)

(The optional :hints argument to def-fgl-boolean-constraint provides the hints for the proof obligation.)

Once this rule is established, FGL will generate constraints as follows:

- When a Boolean variable
a is generated from an IF condition matching(logbitp n x) , FGL will search for an existing generated Boolean variableb whose IF condition was(integerp x) and, if it exists, add the constraint(implies a b) . - Conversely, when a Boolean variable
b is generated from an IF condition matching(integerp x) , FGL will search for existing generated Boolean variablesai matching(logbitp n x) , and for each of them, add the constraint(implies ai b) .

To show that this rule works, you can verify that the following events fail prior to introducing the constraint rule above, but succeed after:

(def-fgl-thm foo1 :hyp t :concl (if (integerp x) t (not (logbitp n x))) :g-bindings nil :rule-classes nil) (def-fgl-thm foo2 :hyp t :concl (if (logbitp n x) (integerp x) t) :g-bindings nil :rule-classes nil)