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