		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

=/_

Construct an incremental rule from a rule name and a variable number of concatenations.

The name of this macro is inspired by the ABNF notation =/ for defining incremental rules.

Macro: =/_

(defmacro =/_ (rulename &rest concatenations)
  (cons '=/_-fn
        (cons rulename
              (cons (cons 'list concatenations)
                    'nil))))

Definitions and Theorems

Function: =/_-fn

(defun =/_-fn (rulename alternation)
  (declare (xargs :guard (and (rulenamep rulename)
                              (alternationp alternation))))
  (make-rule :name (rulename-fix rulename)
             :incremental t
             :definiens (alternation-fix alternation)))

Theorem: rulep-of-=/_-fn

(defthm rulep-of-=/_-fn
  (b* ((rule (=/_-fn rulename alternation)))
    (rulep rule))
  :rule-classes :rewrite)

Theorem: =/_-fn-of-rulename-fix-rulename

(defthm =/_-fn-of-rulename-fix-rulename
  (equal (=/_-fn (rulename-fix rulename)
                 alternation)
         (=/_-fn rulename alternation)))

Theorem: =/_-fn-rulename-equiv-congruence-on-rulename

(defthm =/_-fn-rulename-equiv-congruence-on-rulename
  (implies (rulename-equiv rulename rulename-equiv)
           (equal (=/_-fn rulename alternation)
                  (=/_-fn rulename-equiv alternation)))
  :rule-classes :congruence)

Theorem: =/_-fn-of-alternation-fix-alternation

(defthm =/_-fn-of-alternation-fix-alternation
  (equal (=/_-fn rulename (alternation-fix alternation))
         (=/_-fn rulename alternation)))

Theorem: =/_-fn-alternation-equiv-congruence-on-alternation

(defthm =/_-fn-alternation-equiv-congruence-on-alternation
  (implies (alternation-equiv alternation alternation-equiv)
           (equal (=/_-fn rulename alternation)
                  (=/_-fn rulename alternation-equiv)))
  :rule-classes :congruence)