Define a rule that recognizes constraints among GL generated Boolean variables

When using GL in a term-level style (see term-level-reasoning), GL 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-gl-boolean-constraint gl-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 gl-logbitp-implies-integerp (let ((bit (gl-bool-fix (logbitp n x))) (intp (gl-bool-fix (integerp x)))) (implies bit intp)) :hints ... :rule-classes nil)

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

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

- When a Boolean variable
a is generated from an IF condition matching(logbitp n x) , GL 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) , GL 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-gl-thm foo1 :hyp t :concl (if (integerp x) t (not (logbitp n x))) :g-bindings nil :rule-classes nil) (def-gl-thm foo2 :hyp t :concl (if (logbitp n x) (integerp x) t) :g-bindings nil :rule-classes nil)