[acl2/acl2] 5dcced: Allow rewriting of calls of IF.

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 5dcced50260c6e9c7b6be9882a66364264afd79a
https://github.com/acl2/acl2/commit/5dcced50260c6e9c7b6be9882a66364264afd79a
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-08-23 (Tue, 23 Aug 2016)

Changed paths:
A books/kestrel/utilities/acceptable-rewrite-rule-p.lisp
M books/kestrel/utilities/define-sk-tests.lisp
M books/kestrel/utilities/define-sk.lisp
M books/system/doc/acl2-doc.lisp
M defthm.lisp
M doc.lisp
M rewrite.lisp

Log Message:
-----------
Allow rewriting of calls of IF.

Quoting :doc note-7-3:

It is now legal for a [rewrite] rule to rewrite of a call of [if]. We
thank Eric Smith for pointing us to examples where this can be
useful, such as breaking into cases based on the test. One such
example is much like the following, where we may have a good reason
for leaving my-or disabled in general, but we wish for a call of
my-or to expand when it is the test of an if-expression.

(defund my-or (x y)
(or x y))

(defthm my-or-opener
(equal (if (my-or t1 t2) x y)
(if t1 x (if t2 x y)))
:hints (("Goal" :in-theory (enable my-or))))

; succeeds
(thm (equal (if (my-or a b) u v)
(if a u (if b u v))))

Also made a fix to define-sk that more properly checks proposed
rewrite rules (especially important after the change above).

[GitHub]

Branch: refs/heads/testing