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

Out of the list of keyword arguments recognized by this macro, five are
necessary:

((<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

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

(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

By default, if a counterexample is encountered on any of the cases, the proof
will abort. Setting

By default, if any case hypothesis is unsatisfiable, the proof will abort.
Setting