|
|
|---|
|
|
|
|---|
Define a rewrite rule for GL to use on term-level objects
GL can use ACL2-style rewrite rules to simplify term-level symbolic
objects. However, typically one wants a different theory for ACL2 theorem
proving than one wants to use inside GL.
(gl::def-gl-rewrite my-rewrite-rule (implies (and (syntaxp (and (integerp n) (< 0 (integer-length n)))) (< 0 m)) (equal (logand n m) (logcons (b-and (logcar n) (logcar m)) (logand (logcdr n) (logcdr m))))) :hints ...)
This defines a disabled ACL2 rewrite rule called my-rewrite-rule, and adds my-rewrite-rule to the table of rules GL is allowed to use. (GL will still use it even though it is disabled, as long as it is in that table.)
Def-gl-rewrite supports syntaxp hypotheses, but the term representation used is different from ACL2's. Instead of being bound to TERMPs, the variables are bound to symbolic objects. See symbolic-objects for reference.