1\DOC UNFOLD_CONV 2 3\TYPE {UNFOLD_CONV : (thm list -> conv)} 4 5\SYNOPSIS 6Expands sub-components of a hardware description using their definitions. 7 8\LIBRARY unwind 9 10\DESCRIBE 11{UNFOLD_CONV thl "t1 /\ ... /\ tn"} returns a theorem of the form: 12{ 13 B |- t1 /\ ... /\ tn = t1' /\ ... /\ tn' 14} 15where each {ti'} is the result of rewriting {ti} with the theorems in 16{thl}. The set of assumptions {B} is the union of the instantiated assumptions 17of the theorems used for rewriting. If none of the rewrites are applicable to 18a {ti}, it is unchanged. 19 20\FAILURE 21Never fails. 22 23\EXAMPLE 24{ 25#UNFOLD_CONV [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] 26# "INV (l1,l2) /\ INV (l2,l3) /\ (!(t:num). l1 t = l2 (t-1) \/ l3 (t-1))";; 27. |- INV(l1,l2) /\ INV(l2,l3) /\ (!t. l1 t = l2(t - 1) \/ l3(t - 1)) = 28 (!t. l2 t = ~l1 t) /\ 29 (!t. l3 t = ~l2 t) /\ 30 (!t. l1 t = l2(t - 1) \/ l3(t - 1)) 31} 32\SEEALSO 33unwindLib.UNFOLD_RIGHT_RULE. 34 35\ENDDOC 36