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