Rewrite$-hyps
Rewrite a list of hypotheses
See rewrite$ for relevant background.
Roughly speaking, rewrite$-hyps applies rewriting to each term in a
given list. However, it treats that input as a list of hypotheses: each term
in the list is rewritten under the assumption that the other terms in the list
are true. Both forward-chaining and linear-arithmetic are
used.
General Form
All arguments of rewrite$-hyps except the first are keyword arguments,
hence are optional, with appropriate defaults. All are evaluated.
(rewrite$-hyps hyps
&key
; Hint options:
thints ; must be nil if any other hint options are supplied
backchain-limit-rw expand hands-off in-theory
no-thanks nonlinearp restrict rw-cache-state
default-hints-p ; default t
; Other options:
ctx ; default 'rewrite$-hyps
prove-forced-assumptions ; default t
repeat ; default 1
translate ; default nil
untranslate ; default nil
update-rrec ; default t
wrld ; default (w state)
)
This macro returns an error-triple whose non-erroneous value is a
list of the form (rewritten-hyps rrec ttree . pairs). Here,
rewritten-hyps is (of course) the result of rewriting the input,
hyps; rrec is a so-called ``rewrite$-record'' that can be
passed as the :rrec input of rewrite$; ttree is the tag-tree that records information from the rewriting, including the runes used; and pairs is nil unless there are forced
assumptions, which should never happen if input :prove-forced-assumptions
has its default value of t.
Additional documentation may be provided here if desired. It may suffice
to see community book books/kestrel/apt/simplify-defun-impl.lisp for an
illustration of how rewrite$-hyps may be used. The key idea there is
for rewrite$-hyps to produce the :rrec input of rewrite$
when there are repeated calls of rewrite$ under the same :hyps, and
especially when you want first to simplify those hypotheses (perhaps together
with subterm governors).
