		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Def-fgl-branch-merge

Define a rule for FGL to use in merging IF branches

Usage:

(fgl::def-fgl-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 FGL 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-fgl-branch-merge-fn

(defun
 def-fgl-branch-merge-fn
 (name body hints otf-flg)
 (cons
  'progn
  (cons
       (cons 'defthmd
             (cons name
                   (cons body
                         (cons ':hints
                               (cons hints
                                     (cons ':otf-flg
                                           (cons otf-flg 'nil)))))))
       (cons (cons 'add-fgl-branch-merge
                   (cons name 'nil))
             'nil))))