1\DOC UNFOLD_RIGHT_RULE
2
3\TYPE {UNFOLD_RIGHT_RULE : (thm list -> thm -> thm)}
4
5\SYNOPSIS
6Expands sub-components of a hardware description using their definitions.
7
8\LIBRARY unwind
9
10\DESCRIBE
11{UNFOLD_RIGHT_RULE thl} behaves as follows:
12{
13       A |- !z1 ... zr. t = ?y1 ... yp. t1 /\ ... /\ tn
14   --------------------------------------------------------
15    B u A |- !z1 ... zr. t = ?y1 ... yp. t1' /\ ... /\ tn'
16}
17where each {ti'} is the result of rewriting {ti} with the theorems in
18{thl}. The set of assumptions {B} is the union of the instantiated assumptions
19of the theorems used for rewriting. If none of the rewrites are applicable to
20a {ti}, it is unchanged.
21
22\FAILURE
23Fails if the second argument is not of the required form, though either or
24both of {r} and {p} may be zero.
25
26\EXAMPLE
27{
28#UNFOLD_RIGHT_RULE [ASSUME "!in out. INV(in,out) = !(t:num). out t = ~(in t)"]
29# (ASSUME "!(in:num->bool) out. BUF(in,out) = ?l. INV(in,l) /\ INV(l,out)");;
30.. |- !in out.
31       BUF(in,out) = (?l. (!t. l t = ~in t) /\ (!t. out t = ~l t))
32}
33\SEEALSO
34unwindLib.UNFOLD_CONV.
35
36\ENDDOC
37