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