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