		Search-engine friendly clone of the ACL2 documentation.

Def-gl-param-thm

Prove a theorem using GL symbolic simulation with parametrized case-splitting.

Usage:

(def-gl-param-thm <theorem-name>
  :hyp <hypotheses>
  :concl <conclusion>
  :param-hyp <parametrized hypotheses>
  :cov-bindings <bindings for parametrization coverage>
  :param-bindings <bindings for the individual cases>

  :rule-classes <rule classes expression>

  :hyp-clk <number> :concl-clk <number>
  :clause-proc <clause processor name>

  :n-counterexamples <number>
  :abort-indeterminate <t or nil>
  :run-before-cases <term with side effects>
  :run-after-cases <term with side effects>

  ;; Hints for coverage goals:
  :cov-theory-add <theory expression>
  :do-not-expand <list of functions>
  :cov-hints <computed hints>
  :cov-hints-position <:replace, :before, or :after>

  :test-side-goals <t or nil>)

This form submits a defthm event for the theorem (implies <hyp> <concl>) and the specified rule classes, and gives a hint to attempt to prove it using a GL clause processor with parametrized case-splitting. See def-gl-thm for a simpler version that does not do case splitting.

Out of the list of keyword arguments recognized by this macro, five are necessary: :hyp, :concl, param-hyp, :cov-bindings, and :param-bindings. As noted, the theorem to be proved takes the form (implies <hyp> <concl>). The theorem is split into cases based on the param-hyp, a term containing some free variables of the theorem and some additional variables used in case splitting. Values are assigned to these variables based on the entries in the param-bindings, an alist of the following form:

((<case-bindings1> <var-bindings1>)
 (<case-bindings2> <var-bindings2>)
 ...)

Each of the case-bindings is, in turn, an alist of the following form:

((<case-var1> <obj1>)
 (<case-var2> <obj2>)
 ...)

and each of the var-bindings is an alist of the following form:

((<thm-var1> <shape-spec1>)
 (<thm-var2> <shape-spec2>)
 ...)

For each entry in the param-bindings, the param-hyp is instantiated with the case variables bound to the objects specified in the entry's case-bindings. This term gives a hypothesis about the free variables of the theorem, and the set of these terms generated from the param-bindings gives the full case-split. The case split must cover the theorem's hypotheses; that is, the theorem's hypothesis must imply the disjunction of the case hypotheses. To prove this, we symbolically simulate this disjunction using the shape specs given in the cov-bindings, which are formatted like the var-bindings above. Note that this case-split coverage step is not done as part of :test-side-goals, but it happens first otherwise, so it's easy to tell if it's successful.

A simple example is as follows:

(def-gl-param-thm addititive-inverse-for-5-bits
  :hyp (and (integerp n) (<= -16 n) (< n 16))
  :concl (equal (- n n) 0)
  :param-hyp (if sign
                 (< n 0)
               (and (<= 0 n)
                    (equal (logand n 3) lower-bits)))
  :cov-bindings
  '((n (:g-number (0 1 2 5 6))))
  :param-bindings
  '((((sign t) (lower-bits nil)) ((n (:g-number (1 2 3 4 5)))))
    (((sign nil) (lower-bits 0)) ((n (:g-number (0 2 3 4 5)))))
    (((sign nil) (lower-bits 1)) ((n (:g-number (0 1 2 4 5)))))
    (((sign nil) (lower-bits 2)) ((n (:g-number (0 1 2 3 5)))))
    (((sign nil) (lower-bits 3)) ((n (:g-number (0 1 2 3 4)))))))

This theorem is proved by symbolic simulation of five cases, in each of which the param-hyp is assumed with a different setting of the sign and lower-bits case variables; in one case N is required to be negative, and in the others it is required to be positive and have a given value on its two low-order bits. To show that the case-split is complete, another symbolic simulation is performed (using the given :cov-bindings) which proves that the disjunction of the case assumptions is complete; effectively,

(implies (and (integerp n) (<= -16 n) (< n 16))
         (or (< n 0)
             (and (<= 0 n) (equal (logand n 3) 0))
             (and (<= 0 n) (equal (logand n 3) 1))
             (and (<= 0 n) (equal (logand n 3) 2))
             (and (<= 0 n) (equal (logand n 3) 3))))

Most of the remaining keyword arguments to DEF-GL-PARAM-THM are also available in def-gl-thm and are documented there. The rest are as follows:

:RUN-BEFORE-CASES and :RUN-AFTER-CASES cause a user-specified form to be run between the parametrized symbolic simulations. These may use the variable id, which is bound to the current assignment of the case-splitting variables. These can be used to print a message before and after running each case so that the user can monitor the theorem's progress.

By default, if a counterexample is encountered on any of the cases, the proof will abort. Setting :ABORT-CTREX to NIL causes it to go on; the proof will fail after the clause processor returns because it will produce a goal of NIL.

By default, if any case hypothesis is unsatisfiable, the proof will abort. Setting :ABORT-VACUOUS to NIL causes it to go on.