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