		Search-engine friendly clone of the ACL2 documentation.

Plugging

Remove-prose-rules

Remove from a list of rules all the prose rules whose names have definitions in another list of rules.

Signature
(remove-prose-rules rules1 rules2) → rules
Arguments: rules1 — Guard (rulelistp rules1).; rules2 — Guard (rulelistp rules2).
Returns: rules — Type (rulelistp rules).

This is the first step of the plugging operation. This step removes from rules1 all the prose rules whose names have definitions in rules2.

Definitions and Theorems

Function: remove-prose-rules

(defun remove-prose-rules (rules1 rules2)
  (declare (xargs :guard (and (rulelistp rules1)
                              (rulelistp rules2))))
  (cond ((endp rules1) nil)
        (t (b* ((rule (car rules1)))
             (and (mbt (rulep rule))
                  (if (and (rule-prosep rule)
                           (lookup-rulename (rule->name rule)
                                            rules2))
                      (remove-prose-rules (cdr rules1) rules2)
                    (cons rule
                          (remove-prose-rules (cdr rules1)
                                              rules2))))))))

Theorem: rulelistp-of-remove-prose-rules

(defthm rulelistp-of-remove-prose-rules
  (b* ((rules (remove-prose-rules rules1 rules2)))
    (rulelistp rules))
  :rule-classes :rewrite)