1\DOC EXPAND_AUTO_CONV 2 3\TYPE {EXPAND_AUTO_CONV : (thm list -> conv)} 4 5\SYNOPSIS 6Unfolds, then unwinds as much as possible, then prunes the unwound lines. 7 8\LIBRARY unwind 9 10\DESCRIBE 11{EXPAND_AUTO_CONV thl} when applied to the following term: 12{ 13 "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn" 14} 15returns a theorem of the form: 16{ 17 B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) = 18 (?li(k+1) ... lim. t1' /\ ... /\ tn') 19} 20where each {ti'} is the result of rewriting {ti} with the theorems in 21{thl}. The set of assumptions {B} is the union of the instantiated assumptions 22of the theorems used for rewriting. If none of the rewrites are applicable to a 23conjunct, it is unchanged. After rewriting, the function decides which of the 24resulting terms to use for unwinding, by performing a loop analysis on the 25graph representing the dependencies of the lines. 26 27Suppose the function decides to unwind {li1,...,lik} using the terms 28{ui1',...,uik'} respectively. Then, after unwinding, the lines {li1,...,lik} 29are pruned (provided they have been eliminated from the right-hand sides of the 30conjuncts that are equations, and from the whole of any other conjuncts) 31resulting in the elimination of {ui1',...,uik'}. 32 33The {li}'s are related by the equation: 34{ 35 {{li1,...,lik}} u {{li(k+1),...,lim}} = {{l1,...,lm}} 36} 37The loop analysis allows the term to be unwound as much as possible 38without the risk of looping. The user is left to deal with the recursive 39equations. 40 41\FAILURE 42The function may fail if the argument term is not of the specified form. It 43also fails if there is more than one equation for any line variable. 44 45\EXAMPLE 46{ 47#EXPAND_AUTO_CONV 48# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] 49# "?l1 l2. 50# INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";; 51. |- (?l1 l2. 52 INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) = 53 (?l2. 54 (!t. l2 t = ~(l2(t - 1) \/ ~l2(t - 1))) /\ (!t. out t = ~l2 t)) 55} 56\SEEALSO 57unwindLib.EXPAND_ALL_BUT_CONV, unwindLib.EXPAND_AUTO_RIGHT_RULE, 58unwindLib.EXPAND_ALL_BUT_RIGHT_RULE, unwindLib.UNFOLD_CONV, 59unwindLib.UNWIND_AUTO_CONV, unwindLib.PRUNE_SOME_CONV. 60 61\ENDDOC 62