1\DOC EXPAND_ALL_BUT_RIGHT_RULE 2 3\TYPE {EXPAND_ALL_BUT_RIGHT_RULE : (string list -> thm list -> thm -> thm)} 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_RIGHT_RULE [`li(k+1)`;...;`lim`] thl} behaves as follows: 13{ 14 A |- !z1 ... zr. 15 t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn 16 ------------------------------------------------------------------- 17 B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn' 18} 19where each {ti'} is the result of rewriting {ti} with the theorems in 20{thl}. The set of assumptions {B} is the union of the instantiated assumptions 21of the theorems used for rewriting. If none of the rewrites are applicable to a 22conjunct, it is unchanged. Those conjuncts that after rewriting are equations 23for the lines {li1,...,lik} (they are denoted by {ui1,...,uik}) are used to 24unwind and the lines {li1,...,lik} are then pruned. 25 26The {li}'s are related by the equation: 27{ 28 {{li1,...,lik}} u {{li(k+1),...,lim}} = {{l1,...,lm}} 29} 30 31\FAILURE 32The function may fail if the argument theorem is not of the specified form. It 33will also fail if the unwound lines cannot be pruned. It is possible for the 34function to attempt unwinding indefinitely (to loop). 35 36\EXAMPLE 37{ 38#EXPAND_ALL_BUT_RIGHT_RULE [`l1`] 39# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"] 40# (ASSUME 41# "!(in:num->bool) out. 42# DEV(in,out) = 43# ?l1 l2. 44# INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");; 45.. |- !in out. 46 DEV(in,out) = 47 (?l1. (!t. out t = ~~l1 t) /\ (!t. l1 t = in t \/ ~~l1(t - 1))) 48} 49\SEEALSO 50unwindLib.EXPAND_AUTO_RIGHT_RULE, unwindLib.EXPAND_ALL_BUT_CONV, 51unwindLib.EXPAND_AUTO_CONV, unwindLib.UNFOLD_RIGHT_RULE, 52unwindLib.UNWIND_ALL_BUT_RIGHT_RULE, unwindLib.PRUNE_SOME_RIGHT_RULE. 53 54\ENDDOC 55