1\DOC EXPAND_AUTO_RIGHT_RULE
2
3\TYPE {EXPAND_AUTO_RIGHT_RULE : (thm list -> thm -> thm)}
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_RIGHT_RULE thl} behaves as follows:
12{
13    A |- !z1 ... zr.
14          t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn
15   -------------------------------------------------------------------
16      B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn'
17}
18where each {ti'} is the result of rewriting {ti} with the theorems in
19{thl}. The set of assumptions {B} is the union of the instantiated assumptions
20of the theorems used for rewriting. If none of the rewrites are applicable to a
21conjunct, it is unchanged. After rewriting, the function decides which of the
22resulting terms to use for unwinding, by performing a loop analysis on the
23graph representing the dependencies of the lines.
24
25Suppose the function decides to unwind {li1,...,lik} using the terms
26{ui1',...,uik'} respectively. Then, after unwinding, the lines {li1,...,lik}
27are pruned (provided they have been eliminated from the right-hand sides of
28the conjuncts that are equations, and from the whole of any other conjuncts)
29resulting in the elimination of {ui1',...,uik'}.
30
31The {li}'s are related by the equation:
32{
33   {{li1,...,lik}} u {{li(k+1),...,lim}} = {{l1,...,lm}}
34}
35The loop analysis allows the term to be unwound as much as possible
36without the risk of looping. The user is left to deal with the recursive
37equations.
38
39\FAILURE
40The function may fail if the argument theorem is not of the specified form. It
41also fails if there is more than one equation for any line variable.
42
43\EXAMPLE
44{
45#EXPAND_AUTO_RIGHT_RULE
46# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
47# (ASSUME
48#   "!(in:num->bool) out.
49#     DEV(in,out) =
50#      ?l1 l2.
51#       INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");;
52.. |- !in out. DEV(in,out) = (!t. out t = ~~(in t \/ out(t - 1)))
53}
54\SEEALSO
55unwindLib.EXPAND_ALL_BUT_RIGHT_RULE, unwindLib.EXPAND_AUTO_CONV,
56unwindLib.EXPAND_ALL_BUT_CONV, unwindLib.UNFOLD_RIGHT_RULE,
57unwindLib.UNWIND_AUTO_RIGHT_RULE, unwindLib.PRUNE_SOME_RIGHT_RULE.
58
59\ENDDOC
60