Make a rule to rewrite a quoted constant

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Note: It is helpful to know some basic facts about the ACL2 rewriter; see random-remarks-on-rewriting.

Example Forms: (defthm lambda-id (fn-equal '(lambda (x) x) 'identity) :rule-classes :rewrite-quoted-constant) (defthm set-normalizer (set-equalp (drop-duplicates-and-sort x) x) :rule-classes :rewrite-quoted-constant) (defthm lambda-id-generalized (implies (symbolp v) (fn-equal (list 'lambda (list v) v) 'identity)) :rule-classes :rewrite-quoted-constant)

To be accepted with rule-class

General Forms: (IMPLIES hyps (equiv 'const1 'const2)) ; [1] (IMPLIES hyps (equiv (fn var) var)) ; [2] (IMPLIES hyps (equiv (constructor ...) rhs)) ; [3]

where

hyps is a term (typically a conjunction) and may include`force`and`syntaxp`hypotheses with the usual semantics,equiv is a known equivalence relation and, in the case of[1] and[2] ,equiv is notEQUAL ,var , in form[2] , is a variable symbol, and-
constructor , in form[3] , is an explicit value ``constructor'' function symbol listed in*one-way-unify1-implicit-fns* . The list just mentioned includescons , which can be used to match non-empty list constants,coerce , which can match string constants,intern-in-package-of-symbol , which can match symbol constants, andbinary-+ and certain other arithmetic primitives which can match numeric constants. See random-remarks-on-rewriting for some examples.

The function,

The `rule-classes`. Note that for forms

Once a `refinement`) the equivalence
relation being maintained by the rewriter for the given occurrence of the
target. The rewriter tries to apply each such rule in turn (as described
below) and replaces the target by the rewritten result of the first
applicable rule.

A rule applies if the ``pattern'' (see below) in the conclusion
``matches'' the quoted constant and the `force` and `syntaxp`, and heuristics such as those
controlled by any `loop-stopper` options in the rule-class or

- A form
[1] rule, whose conclusion is(equiv 'const1 'const2) , has'const1 as its pattern and that pattern matches the target constant'const only whenconst1 is exactlyconst . The result is'const2 . Note that it is impossible to prove a form[1] rule whose equivalence isequal unless the two constants are identical, so we disallow that case. - A form
[2] rule, whose conclusion is(equiv (fn var) var) , is most easily understood by swapping the roles of left- and right-hand sides of its conclusion. Its pattern is the right-hand side,var , and its result is derived from the left-hand side,(fn var) . The reason we use the form shown here is so that the same conjecture might also be used as an ordinary:rewrite rule without forcing the user to type a:corollary with the sides swapped. Since form[2] rules have a variable as the pattern they will match any quoted constant,'const , by bindingvar to'const . The result is the quoted constant, if any, obtained by rewriting(fn var) under that binding ofvar . If that rewrite does not result in a constant, no replacement is made, i.e., it is as though the rule did not match. Note that it is pointless to prove a form[2] rule whose equivalence isequal because it would replace a quoted constant by itself, so we disallow that equivalence.

Intuitively,fn is a function that normalizes every member of theequiv equivalence class: given a constant that is a member of the class it returns its ``normal'' form. That is why we callfn the ``normalizer'' forequiv . However, you do not have to prove anything like normality or canonicality; you just have to prove thatfn returns a member of the class. Having several different normalizers is possible but it is best if only one is enabled at a time.

Whenvar is bound to a constant, the rewriter will first try to reduce(fn var) to a constant by simple evaluation. If that fails, it tries using lemmas. If the normalizer or one of its subfunctions is disabled or is non-executable or has a disabled executable counterpart the attempt to simply evaluate(fn var) (under the assignment of'const tovar ) may fail. That is why full-blown rewriting of(fn var) is tried instead. It might happen that evaluation fails but lemmas produce a constant.

**The fact that form**First, you can also classify the same formula as a[2] rules are used ``backwards,'' with the roles of the left- and right-hand sides swapped, has some ramifications worth noting.:rewrite rule (but of course as such it won't rewrite quoted constants); as a:rewrite rule it rewrites instances of(fn var) to the corresponding instance ofvar . Second, when a:rewrite-quoted-constant rule is added, the new rule is compared to old rules for subsumption and warning messages are generated; however form[2] rules are omitted from this subsumption check because their patterns match every constant (in the equivalence class). Third, if you inspect a form[2] rule with`pr`, it reports the actual syntax typed, e.g., the ``Lhs '' is(fn var) and the ``Rhs '' isvar . But, if you: `monitor`a form[2] rule and then interact with the resulting break-rewrite you will see that the`brr-commands`:lhs and:rhs report the swapped results. That is, in the break,:lhs will bevar and:rhs will be(fn var) . This is different from the display bypr becausepr reports the actual syntax but interactive breaks report how the rule is being used. We think the interactive user, out of long habit, will type:lhs to see the pattern being matched and we did not think it wise to add a special command just to see the pattern in a form[2] rule. Fourth, if a form[2] rule is mentioned in the report by`pl`the ``New term'' is reported to be(fn 'const) , however replacement of'const occurs only if(fn 'const) reduces to a quoted constant by rewriting. - A form
[3] rule, whose conclusion is(equiv (constructor ...) rhs) , matches the constant'const provided'const is an instance of(constructor ...) under some variable substitutions . We illustrate cases where quoted constants are instances of ``constructor'' terms below and in random-remarks-on-rewriting. Note that form[3] rules allow the equivalence relation to beequal . Use ofequal here could cause looping rewrites if therhs reduces to a constant. But we allow it because, as noted below, such a rule will also permit you to rewrite a quoted constant into an equivalent term that is not a quoted constant.

It is important to realize that form

The form

However, form

For example, the `true-listp`, eliminate duplicate elements, and sort the remaining
elements. It then proves the form

As noted earlier, form

But since the rewriter will eventually be called on that term, and since
that term contains another top-level quoted constant, namely

- Random-remarks-on-rewriting
- Some basic facts about the ACL2 rewriter