		Search-engine friendly clone of the ACL2 documentation.

Def-gl-branch-merge

Define a rule for GL to use in merging IF branches

Usage:

(gl::def-gl-branch-merge my-branch-merge-rule
   (implies (and (syntaxp (integerp m))
                 (integerp m))
            (equal (if cond (logcons b n) m)
                   (logcons (if cond b (logcar m))
                            (if cond n (logcdr m)))))
 :hints ...)

This form creates an ACL2 theorem with :rule-classes nil and installs it in a table that GL references when attempting to merge branches of an IF term.

Branch merge rules work similarly to normal rewrite rules, except that:

the LHS must be of the form: (if <var> <then-term> <else-term>)
each rule is indexed by the function symbol of the then-term, so then-term must be a function call.

Definitions and Theorems

Function: def-gl-branch-merge-fn

(defun def-gl-branch-merge-fn (name body hints otf-flg)
 (cons
  'progn
  (cons
   (cons
    'defthm
    (cons
     name
     (cons
         body
         (cons ':hints
               (cons hints
                     (cons ':otf-flg
                           (cons otf-flg '(:rule-classes nil))))))))
   (cons (cons 'add-gl-branch-merge
               (cons name 'nil))
         'nil))))