		Search-engine friendly clone of the ACL2 documentation.

Closure

Rules-of-name

Separate from some rules the ones that define a rule name.

Signature
(rules-of-name rulename rules) → (mv rulename-rules other-rules)
Arguments: rulename — Guard (rulenamep rulename).; rules — Guard (rulelistp rules).
Returns: rulename-rules — Type (rulelistp rulename-rules).; other-rules — Type (rulelistp other-rules).

We scan rules, taking out the rules that define rulename. The first result contains the rules that have been taken out, in the same order in which they appear in rules. The second result contains the remaining rules in rules, after the ones in the first result have been taken out.

Definitions and Theorems

Function: rules-of-name

(defun rules-of-name (rulename rules)
  (declare (xargs :guard (and (rulenamep rulename)
                              (rulelistp rules))))
  (b* (((when (endp rules)) (mv nil nil))
       (rule (rule-fix (car rules)))
       ((mv rulename-rules other-rules)
        (rules-of-name rulename (cdr rules))))
    (if (equal (rule->name rule) rulename)
        (mv (cons rule rulename-rules)
            other-rules)
      (mv rulename-rules
          (cons rule other-rules)))))

Theorem: rulelistp-of-rules-of-name.rulename-rules

(defthm rulelistp-of-rules-of-name.rulename-rules
  (b* (((mv ?rulename-rules ?other-rules)
        (rules-of-name rulename rules)))
    (rulelistp rulename-rules))
  :rule-classes :rewrite)

Theorem: rulelistp-of-rules-of-name.other-rules

(defthm rulelistp-of-rules-of-name.other-rules
  (b* (((mv ?rulename-rules ?other-rules)
        (rules-of-name rulename rules)))
    (rulelistp other-rules))
  :rule-classes :rewrite)

Theorem: len-of-other-rules-of-rules-of-name-<

(defthm len-of-other-rules-of-rules-of-name-<
  (b* (((mv rulename-rules other-rules)
        (rules-of-name rulename rules)))
    (implies rulename-rules
             (< (len other-rules) (len rules))))
  :rule-classes :linear)