Prove a theorem using GL symbolic simulation.

Usage:

(def-gl-thm <theorem-name> :hyp <hypothesis term> :concl <conclusion term> :g-bindings <shape spec binding alist> :rule-classes <rule classes expression> :hyp-clk <number> :concl-clk <number> :clause-proc <clause processor name> :n-counterexamples <number> :abort-indeterminate <t or nil> ;; 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 by symbolic execution using a GL clause processor.

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

The

((<var-name1> <shape-spec1>) (<var-name2> <shape-spec2>) ...)

The shape specs must be well-formed as described in shape-specs; notably, they must not reuse BDD variable numbers or unconstrained variable names. Note also that this is not a dotted alist; the shape spec is the cadr, not the cdr, of each entry. If any variables mentioned in the theorem are not bound in this alist, they will be given an unconstrained variable binding.

The symbolic objects used as the inputs to the symbolic simulation are
obtained by translating each shape spec into a symbolic object. The hyp is
symbolically executed on these symbolic inputs. Parametrizing the symbolic
objects by the resulting predicate object yields (absent any

Here is a simple example theorem:

(def-gl-thm commutativity-of-+-up-to-16 :hyp (and (natp a) (natp b) (< a 16) (< b 16)) :concl (equal (+ a b) (+ b a)) :g-bindings '((a (:g-number (0 2 4 6 8))) (b (:g-number (1 3 5 7 9)))))

This theorem binds its free variables

The coverage obligation for a theorem will be a goal like this:

(implies <hyp> (shape-spec-obj-in-range (list <shape-spec1> <shape-spec2> ...) (list <var-name1> <var-name2> ...)))

In the example above:

(implies (and (natp a) (natp b) (< a 16) (< b 16)) (shape-spec-obj-in-range '((:g-number (0 2 4 6 8)) (:g-number (1 3 5 7 9))) (list a b)))

It is often convenient to work out the coverage theorem before running the
symbolic simulation, since the symbolic simulation may take a very long time
even when successful. The keyword argument

Several hints are given by default for proving coverage; see shape-specs for details. The keyword arguments

When proof by symbolic simulation fails, the clause processor will print
randomized counterexamples. The keyword argument

By default, the clause processor will execute conclusion on the
counterexamples that it finds; this is useful for printing debugging
information. However, sometimes the conclusion is not executable; in that
case, you may turn off execution of counterexamples using

A symbolic simulation may result in a symbolic object that can't be
syntactically determined to be non-nil; for example, the result may contain a

The symbolic interpreter and all symbolic counterpart functions take a clock
argument to ensure termination. The starting clocks for the symbolic
executions of the hyp (for parametrization) and the conclusion may be set using
the keyword arguments

The keyword argument

The keyword argument

- Def-gl-rule
- A slightly enhanced version of def-gl-thm
- Defthm-using-gl
- Prove a theorem using GL, including GL only locally.
- Gl-thm
- Prove a theorem using GL symbolic simulation, but don't store it, like with thm.