1\DOC EXPAND_ALL_BUT_CONV
2
3\TYPE {EXPAND_ALL_BUT_CONV : (string list -> thm list -> conv)}
4
5\SYNOPSIS
6Unfolds, then unwinds all lines (except those specified) as much as possible,
7then prunes the unwound lines.
8
9\LIBRARY unwind
10
11\DESCRIBE
12{EXPAND_ALL_BUT_CONV [`li(k+1)`;...;`lim`] thl} when applied to the following
13term:
14{
15   "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn"
16}
17returns a theorem of the form:
18{
19   B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) =
20        (?li(k+1) ... lim. t1' /\ ... /\ tn')
21}
22where each {ti'} is the result of rewriting {ti} with the theorems in
23{thl}. The set of assumptions {B} is the union of the instantiated assumptions
24of the theorems used for rewriting. If none of the rewrites are applicable to a
25conjunct, it is unchanged. Those conjuncts that after rewriting are equations
26for the lines {li1,...,lik} (they are denoted by {ui1,...,uik}) are used to
27unwind and the lines {li1,...,lik} are then pruned.
28
29The {li}'s are related by the equation:
30{
31   {{li1,...,lik}} u {{li(k+1),...,lim}} = {{l1,...,lm}}
32}
33
34\FAILURE
35The function may fail if the argument term is not of the specified form. It
36will also fail if the unwound lines cannot be pruned. It is possible for the
37function to attempt unwinding indefinitely (to loop).
38
39\EXAMPLE
40{
41#EXPAND_ALL_BUT_CONV [`l1`]
42# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
43# "?l1 l2.
44#   INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";;
45. |- (?l1 l2.
46       INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) =
47     (?l1.
48       (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1)))
49}
50\SEEALSO
51unwindLib.EXPAND_AUTO_CONV, unwindLib.EXPAND_ALL_BUT_RIGHT_RULE,
52unwindLib.EXPAND_AUTO_RIGHT_RULE, unwindLib.UNFOLD_CONV,
53unwindLib.UNWIND_ALL_BUT_CONV, unwindLib.PRUNE_SOME_CONV.
54
55\ENDDOC
56