The HOL unwind Library

Documentation written by

R. J. Boulton

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

August 1991 \begin{matrix}c \\ ◯ \end{matrix} R. J. Boulton 1991

Contents

1 The unwind Library 1 1.1 Using the library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Automatic unwinding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 ML Functions in the unwind Library 11 References 41 Index 42 iv Contents

Chapter 1

The unwind Library

This document describes the facilities provided by the unwind library for the HOL system [2]. The library provides conversions and rules for unfolding, unwinding and pruning device implementations (logical representations of hardware). For a detailed description of these techniques, see [1].

Most of the functions fall into one of five groups. The first group consists of conversions and inference rules for moving universal quantifiers up and down through conjunctions; they have names beginning with either CONJ_FORALL or FORALL_CONJ. The second group of functions are for unfolding, that is expanding sub-components using their definitions. The names of these begin with UNFOLD. The functions in the third group perform unwinding and have names beginning with UNWIND. The fourth group of functions prune internal lines that have been unwound. Their names begin with PRUNE. The final group of functions combine unfolding, unwinding and pruning. They have names beginning with EXPAND.

I have tried to make the behaviour of the functions uniform. The conversions apply to the smallest term possible, to provide maximum flexibility. The inference rules, on the other hand, are designed to apply to the definition of a hardware component. They expect to be given a theorem of the form:

   |- !x1 ... xn. DEVICE (x1,...,xn) = ?l1 ... lm. t1 /\ ... /\ tp

1.1 Using the library

The unwind library can be loaded into a HOL session using the function load_library (see the HOL manual for a general description of library loading). The first action in the load sequence initiated by load_library is to update the HOL help search path. The help search path is updated with a pathname to online help files for the ML functions in the library. After updating the help search path, the ML functions in the library are loaded into HOL.

The following session shows how the unwind library may be loaded using load_library:

1

 #load_library `unwind`;;
 Loading library `unwind` ...
 Updating help search path
 ..................................
 Library `unwind` loaded.
 () : void

2 Chapter 1. The unwind Library

We now illustrate the use of the library on the parity-checker example. Firstly, we begin a new theory:

2

#new_theory `PARITY`;;
() : void

We define the sub-components used:

3

#let ONE_DEF =
# new_definition
#  (`ONE_DEF`, "ONE(out:num->bool) = !t. out t = T");;
ONE_DEF = |- !out. ONE out = (!t. out t = T)

4

#let NOT_DEF =
# new_definition
#  (`NOT_DEF`, "NOT(in,out:num->bool) = !t. out t = ~(in t)");;
NOT_DEF = |- !in out. NOT(in,out) = (!t. out t = ~in t)

5

#let MUX_DEF =
# new_definition
#  (`MUX_DEF`,
#   "MUX(sw,in1,in2,out:num->bool) =
#     !t. out t = (sw t => in1 t | in2 t)");;
MUX_DEF =
|- !sw in1 in2 out.
    MUX(sw,in1,in2,out) = (!t. out t = (sw t => in1 t | in2 t))

6

#let REG_DEF =
# new_definition
# (`REG_DEF`, "REG(in,out:num->bool) =
#              !t. out t = ((t=0) => F | in(t-1))");;
REG_DEF =
|- !in out. REG(in,out) = (!t. out t = ((t = 0) => F | in(t - 1)))

Now we define the parity-checker implementation:

7

 #let PARITY_IMP_DEF =
 # new_definition
 #  (`PARITY_IMP_DEF`,
 #   "PARITY_IMP(in,out) =
 #    ?l1 l2 l3 l4 l5.
 #     NOT(l2,l1) /\ MUX(in,l1,l2,l3) /\ REG(out,l2) /\
 #     ONE l4     /\ REG(l4,l5)       /\ MUX(l5,l3,l4,out)");;
 PARITY_IMP_DEF =
 |- !in out.
     PARITY_IMP(in,out) =
     (?l1 l2 l3 l4 l5.
       NOT(l2,l1) /\
       MUX(in,l1,l2,l3) /\
       REG(out,l2) /\
       ONE l4 /\
       REG(l4,l5) /\
       MUX(l5,l3,l4,out))

The function EXPAND_AUTO_RIGHT_RULE can be used to unfold, unwind and prune the body of this definition:

8

 #EXPAND_AUTO_RIGHT_RULE [ONE_DEF;NOT_DEF;MUX_DEF;REG_DEF] PARITY_IMP_DEF;;
 |- !in out.
     PARITY_IMP(in,out) =
     (!t.
       out t =
       (((t = 0) => F | T) =>
        (in t =>
         ~((t = 0) => F | out(t - 1)) |
         ((t = 0) => F | out(t - 1))) |
        T))

1.2 Automatic unwinding

Hardware implementations often contain feedbacks. This presents a problem when trying to unwind and prune the internal lines in the logical representation. The mutual dependencies between lines can cause a brute-force unwind to loop indefinitely. To avoid this one has to be selective about which lines to unwind. The tools in the unwind library allow the user to be selective in this way. However, it is possible for the machine itself to be selective. The function UNWIND_AUTO_CONV attempts to analyze the dependencies between lines and unwind as far as possible without looping.

Consider the following term which arises in the parity-checker example:

   "?l1 l2 l3 l4 l5.
     (!t. l1 (t:num) = ~l2 t) /\
     (!t. l3 t = (in t => l1 t | l2 t)) /\

     (!t. l2 t = ((t = 0) => F | out (t - 1))) /\
     (!t. l4 t = T) /\
     (!t. l5 t = ((t = 0) => F | l4 (t - 1))) /\
     (!t. out t = (l5 t => l3 t | l4 t))"

We can represent the dependencies of the lines using a directed graph:

                             [figure: l2; l1; l3; out; l4; l5]

which can in turn be represented by the following list:

   l1, [l2]
   l3, [l1;l2]
   l2, [out]
   l4, []
   l5, [l4]
   out,[l5;l3;l4]

Since we wish to eliminate the internal lines, we want to be left with a recursive equation for out in terms of itself. We can do this be ‘breaking the loop’ at out, giving the following structure:

   l1, [l2]
   l3, [l1;l2]
   l2, []
   l4, []
   l5, [l4]

Note that out has been removed from the structure. From the graph we can see that l2 and l4 do not depend on any internal lines. They can therefore be used to unwind without any risk of looping. They can be recognized in the datastructure by the fact that their corresponding dependency lists are empty.

Once we have unwound with l2 and l4 they can be removed from the datastructure:

   l1, []
   l3, [l1]
   l5, []

We now see that l1 and l5 can be unwound to give:

   l3, []

Unwinding l3 then leaves us with the required recursive equation for out.

The problem with the approach just described is that it only unwinds fully if there is at most one loop in the circuit, and the output is in that loop. We can be a bit more general. Consider the circuit:

                                     [figure: out; l2; l1; in]

represented by the graph:

   l1, [l2]
   l2, [l1]
   out,[l2]

There are no lines with an empty dependency list, and eliminating out will not help because it is not in the loop. However, if we break the loop at l2 we can unwind l1. This will leave us with a recursive equation for l2 and an equation for out in terms of l2. This is the best that we can do, and it is now up to the user to deal with the recursive equation.

Now let’s consider an example with more than one loop:

                             [figure: out; l5; l4; l3; l2; l6; l1; l7; in]

We could unwind l1 but then we would get stuck. If we break at l2 or l7 we will still get stuck because of the inner loop. If we break at l5 we can unwind l7, but then get stuck. If we break at l6 we get stuck because of the outer loop. However, if we break at l3 or l4 both loops are broken and we can unwind fully to leave a recursive equation for either l3 or l4 and an equation for out in terms of that line. So, the choice of where to break a loop may determine how far the unwinding can go.

UNWIND_AUTO_CONV attempts to break every loop in the circuit using the minimum number of breaks, so that there are as few equations left as possible. The function also gives priority to non-internal lines when determining where to break, so that if possible the recursive equations are in terms of these lines.

The algorithm used determines from the term a list of line variables. Each line variable has a right-hand side of an equation associated with it. The free variables in each righthand side are computed and those that are also line variables are placed in the dependency list for the corresponding line. From the dependency structure, the loops are determined. Lines are then eliminated so that all loops are broken.

A study of the following circuit reveals why all loops have to be broken. If not all loops are broken, then a remaining loop can make the breaking of other loops fruitless.

                             [figure: out; l5; l4; l3; l7; l2; l6; l1; in]

The dependency structure for the circuit is:

   l1, []
   l2, [l1]
   l3, [l2;l6]
   l4, [l3;l7]
   l5, [l4]
   l6, [l4]
   l7, [l5]
   out,[l5]

The loops for the circuit are:

   [l3;l4;l6]
   [l4;l5;l7]

Both loops can be broken by eliminating l4:

   l1, []
   l2, [l1]
   l3, [l2;l6]

   l5, []
   l6, []
   l7, [l5]
   out,[l5]

We can now unwind l1, l5 and l6:

   l2, []
   l3, [l2]
   l7, []
   out,[]

and then unwind l2, l7 and out, followed by unwinding with l3 to yield a recursive equation for l4 and all other equations in terms of l4. All the internal lines except for l4 can be pruned. This leaves equations for l4 and out only.

The technique does not always yield a single recursive equation. Mutual recursion is also possible. This is illustrated by the following example:

                               [figure: out; l5; l4; l3; l7; l2; l1; l6; in]

There are three loops, but breaking at l2 and l4 is sufficient to break all the loops. The result is three equations: an equation for l2 in terms of itself and l4, an equation for l4 in terms of itself and l2, and an equation for out in terms of l4. So, it can be seen that the loop analysis technique used by UNWIND_AUTO_CONV does not eliminate loops; it simply ‘shrinks’ them.

10 Chapter 1. The unwind Library

Chapter 2

ML Functions in the unwind Library

This chapter provides documentation on all the ML functions that are made available in HOL when the unwind library is loaded. This documentation is also available online via the help facility.

 CONJ_FORALL_CONV

CONJ_FORALL_CONV : conv

Synopsis

Moves universal quantifiers up through a tree of conjunctions.

Description

CONJ_FORALL_CONV "(!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)" returns the follow-

ing theorem:

   |- (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) =
      !x1 ... xm. t1 /\ ... /\ tn

where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation.

Failure

Never fails.

12 Chapter 2. ML Functions in the unwind Library

Example

#CONJ_FORALL_CONV "((!(x:*) (y:*) (z:*). a) /\ (!(x:*) (y:*) (z:*). b)) /\
#                  (!(x:*) (y:*) (z:*). c)";;
|- ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c) = (!x y z. (a /\ b) /\ c)
#CONJ_FORALL_CONV "T";;
|- T = T
#CONJ_FORALL_CONV "((!(x:*) (y:*) (z:*). a) /\ (!(x:*) (w:*) (z:*). b)) /\
#                  (!(x:*) (y:*) (z:*). c)";;
|- ((!x y z. a) /\ (!x w z. b)) /\ (!x y z. c) =
   (!x. ((!y z. a) /\ (!w z. b)) /\ (!y z. c))

See also

FORALL_CONJ_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV,
CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE.

 CONJ_FORALL_ONCE_CONV

CONJ_FORALL_ONCE_CONV : conv

Synopsis

Moves a single universal quantifier up through a tree of conjunctions.

Description

CONJ_FORALL_ONCE_CONV "(!x. t1) /\ ... /\ (!x. tn)" returns the theorem:
   |- (!x. t1) /\ ... /\ (!x. tn) = !x. t1 /\ ... /\ tn

where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation.

Failure

Fails if the argument term is not of the required form. The term need not be a conjunction, but if it is every conjunct must be universally quantified with the same variable.

Example

#CONJ_FORALL_ONCE_CONV "((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c)";;
|- ((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c) =
   (!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c))
#CONJ_FORALL_ONCE_CONV "!x. x \/ a";;
|- (!x. x \/ a) = (!x. x \/ a)
#CONJ_FORALL_ONCE_CONV "((!x. x \/ a) /\ (!y. y \/ b)) /\ (!x. x \/ c)";;
evaluation failed     CONJ_FORALL_ONCE_CONV

See also

FORALL_CONJ_ONCE_CONV, CONJ_FORALL_CONV, FORALL_CONJ_CONV,
CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE.

 CONJ_FORALL_RIGHT_RULE

CONJ_FORALL_RIGHT_RULE : (thm -> thm)

Synopsis

Moves universal quantifiers up through a tree of conjunctions.

Description

    A |- !z1 ... zr.
          t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)
   -------------------------------------------------------------------
      A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn

Failure

Fails if the argument theorem is not of the required form, though either or both of r and p may be zero.

See also

FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_CONV, FORALL_CONJ_CONV,
CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV.

 DEPTH_EXISTS_CONV

DEPTH_EXISTS_CONV : (conv -> conv)

Synopsis

Applies a conversion to the body of nested existential quantifications.

Description

DEPTH_EXISTS_CONV conv "?x1 ... xn. body" applies conv to "body" and returns a theo-

rem of the form:

   |- (?x1 ... xn. body) = (?x1 ... xn. body')

Failure

Fails if the application of conv fails.

Example

#DEPTH_EXISTS_CONV BETA_CONV "?x y z. (\w. x /\ y /\ z /\ w) T";;
|- (?x y z. (\w. x /\ y /\ z /\ w)T) = (?x y z. x /\ y /\ z /\ T)

See also

DEPTH_FORALL_CONV.

 DEPTH_FORALL_CONV

DEPTH_FORALL_CONV : (conv -> conv)

Synopsis

Applies a conversion to the body of nested universal quantifications.

Description

DEPTH_FORALL_CONV conv "!x1 ... xn. body" applies conv to "body" and returns a theo-

rem of the form:

   |- (!x1 ... xn. body) = (!x1 ... xn. body')

Failure

Fails if the application of conv fails.

EXISTS DEL1 CONV 15

Example

#DEPTH_FORALL_CONV BETA_CONV "!x y z. (\w. x /\ y /\ z /\ w) T";;
|- (!x y z. (\w. x /\ y /\ z /\ w)T) = (!x y z. x /\ y /\ z /\ T)

See also

DEPTH_EXISTS_CONV.
 EXISTS_DEL1_CONV
EXISTS_DEL1_CONV : conv

Synopsis

Deletes one existential quantifier.

Description

EXISTS_DEL1_CONV "?x. t" returns the theorem:
   |- (?x. t) = t

provided x is not free in t.

Failure

Fails if the argument term is not an existential quantification or if x is free in t.

See also

EXISTS_DEL_CONV, PRUNE_ONCE_CONV.
 EXISTS_DEL_CONV
EXISTS_DEL_CONV : conv

Synopsis

Deletes existential quantifiers.

Description

EXISTS_DEL_CONV "?x1 ... xn. t" returns the theorem:
   |- (?x1 ... xn. t) = t

provided x1,...,xn are not free in t.

Failure

Fails if any of the x’s appear free in t. The function does not perform a partial deletion; for example, if x1 and x2 do not appear free in t but x3 does, the function will fail; it will not return:

   |- ?x1 ... xn. t = ?x3 ... xn. t

See also

EXISTS_DEL1_CONV, PRUNE_CONV.

 EXISTS_EQN_CONV

EXISTS_EQN_CONV : conv

Synopsis

Proves the existence of a line that has a non-recursive equation.

Description

EXISTS_EQN_CONV "?l. !y1 ... ym. l x1 ... xn = t" returns the theorem:
   |- (?l. !y1 ... ym. l x1 ... xn = t) = T

provided l is not free in t. Both m and n may be zero.

Failure

Fails if the argument term is not of the specified form or if l appears free in t.

See also

PRUNE_ONCE_CONV.

 EXPAND_ALL_BUT_CONV

EXPAND_ALL_BUT_CONV : (string list -> thm list -> conv)

Synopsis

Unfolds, then unwinds all lines (except those specified) as much as possible, then prunes the unwound lines.

Description

EXPAND_ALL_BUT_CONV [`li(k+1)`;...;`lim`] thl when applied to the following term:
   "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn"

returns a theorem of the form:

   B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) =
        (?li(k+1) ... lim. t1' /\ ... /\ tn')

where each ti' is the result of rewriting ti with the theorems in thl. The set of assumptions B is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. Those conjuncts that after rewriting are equations for the lines li1,...,lik (they are denoted by ui1,...,uik) are used to unwind and the lines li1,...,lik are then pruned.

The li’s are related by the equation:

   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}

Failure

The function may fail if the argument term is not of the specified form. It will also fail if the unwound lines cannot be pruned. It is possible for the function to attempt unwinding indefinitely (to loop).

Example

#EXPAND_ALL_BUT_CONV [`l1`]
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# "?l1 l2.
#   INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";;
. |- (?l1 l2.
       INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) =
     (?l1.
       (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1)))

See also

EXPAND_AUTO_CONV, EXPAND_ALL_BUT_RIGHT_RULE, EXPAND_AUTO_RIGHT_RULE,
UNFOLD_CONV, UNWIND_ALL_BUT_CONV, PRUNE_SOME_CONV.

 EXPAND_ALL_BUT_RIGHT_RULE

EXPAND_ALL_BUT_RIGHT_RULE : (string list -> thm list -> thm -> thm)

Synopsis

Unfolds, then unwinds all lines (except those specified) as much as possible, then prunes the unwound lines.

Description

EXPAND_ALL_BUT_RIGHT_RULE [`li(k+1)`;...;`lim`] thl behaves as follows:

    A |- !z1 ... zr.
          t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn
   -------------------------------------------------------------------
       B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn'

where each ti' is the result of rewriting ti with the theorems in thl. The set of assumptions B is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. Those conjuncts that after rewriting are equations for the lines li1,...,lik (they are denoted by ui1,...,uik) are used to unwind and the lines li1,...,lik are then pruned.

The li’s are related by the equation:

   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}

Failure

The function may fail if the argument theorem is not of the specified form. It will also fail if the unwound lines cannot be pruned. It is possible for the function to attempt unwinding indefinitely (to loop).

Example

#EXPAND_ALL_BUT_RIGHT_RULE [`l1`]
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# (ASSUME
#   "!(in:num->bool) out.
#     DEV(in,out) =
#      ?l1 l2.
#       INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");;
.. |- !in out.
       DEV(in,out) =
       (?l1. (!t. out t = ~~l1 t) /\ (!t. l1 t = in t \/ ~~l1(t - 1)))

See also

EXPAND_AUTO_RIGHT_RULE, EXPAND_ALL_BUT_CONV, EXPAND_AUTO_CONV,
UNFOLD_RIGHT_RULE, UNWIND_ALL_BUT_RIGHT_RULE, PRUNE_SOME_RIGHT_RULE.

 EXPAND_AUTO_CONV

EXPAND_AUTO_CONV : (thm list -> conv)

Synopsis

Unfolds, then unwinds as much as possible, then prunes the unwound lines.

Description

EXPAND_AUTO_CONV thl when applied to the following term:

   "?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn"

returns a theorem of the form:

   B |- (?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn) =
        (?li(k+1) ... lim. t1' /\ ... /\ tn')

where each ti' is the result of rewriting ti with the theorems in thl. The set of assumptions B is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. After rewriting, the function decides which of the resulting terms to use for unwinding, by performing a loop analysis on the graph representing the dependencies of the lines.

Suppose the function decides to unwind li1,...,lik using the terms ui1',...,uik' respectively. Then, after unwinding, the lines li1,...,lik are pruned (provided they have been eliminated from the right-hand sides of the conjuncts that are equations, and from the whole of any other conjuncts) resulting in the elimination of ui1',...,uik'.

The li’s are related by the equation:

   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}

The loop analysis allows the term to be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations.

Failure

The function may fail if the argument term is not of the specified form. It also fails if there is more than one equation for any line variable.

Example

#EXPAND_AUTO_CONV
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# "?l1 l2.
#   INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = l2 (t-1) \/ out (t-1))";;
. |- (?l1 l2.
       INV(l1,l2) /\ INV(l2,out) /\ (!t. l1 t = l2(t - 1) \/ out(t - 1))) =
     (?l1.
       (!t. out t = ~~l1 t) /\ (!t. l1 t = ~l1(t - 1) \/ ~~l1(t - 1)))

See also

EXPAND_ALL_BUT_CONV, EXPAND_AUTO_RIGHT_RULE, EXPAND_ALL_BUT_RIGHT_RULE,
UNFOLD_CONV, UNWIND_AUTO_CONV, PRUNE_SOME_CONV.

 EXPAND_AUTO_RIGHT_RULE

EXPAND_AUTO_RIGHT_RULE : (thm list -> thm -> thm)

Synopsis

Unfolds, then unwinds as much as possible, then prunes the unwound lines.

Description

EXPAND_AUTO_RIGHT_RULE thl behaves as follows:
    A |- !z1 ... zr.
          t = ?l1 ... lm. t1 /\ ... /\ ui1 /\ ... /\ uik /\ ... /\ tn
   -------------------------------------------------------------------
      B u A |- !z1 ... zr. t = ?li(k+1) ... lim. t1' /\ ... /\ tn'

where each ti' is the result of rewriting ti with the theorems in thl. The set of assumptions B is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a conjunct, it is unchanged. After rewriting, the function decides which of the resulting terms to use for unwinding, by performing a loop analysis on the graph representing the dependencies of the lines.

Suppose the function decides to unwind li1,...,lik using the terms ui1',...,uik' respectively. Then, after unwinding, the lines li1,...,lik are pruned (provided they have been eliminated from the right-hand sides of the conjuncts that are equations, and from the whole of any other conjuncts) resulting in the elimination of ui1',...,uik'.

The li’s are related by the equation:

   {li1,...,lik} u {li(k+1),...,lim} = {l1,...,lm}

The loop analysis allows the term to be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations.

Failure

The function may fail if the argument theorem is not of the specified form. It also fails if there is more than one equation for any line variable.

Example

#EXPAND_AUTO_RIGHT_RULE
# [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# (ASSUME
#   "!(in:num->bool) out.
#     DEV(in,out) =
#      ?l1 l2.
#       INV (l1,l2) /\ INV (l2,out) /\ (!(t:num). l1 t = in t \/ out (t-1))");;
.. |- !in out. DEV(in,out) = (!t. out t = ~~(in t \/ out(t - 1)))

See also

EXPAND_ALL_BUT_RIGHT_RULE, EXPAND_AUTO_CONV, EXPAND_ALL_BUT_CONV,
UNFOLD_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE, PRUNE_SOME_RIGHT_RULE.

 FLATTEN_CONJ_CONV

FLATTEN_CONJ_CONV : conv

Synopsis

Flattens a ‘tree’ of conjunctions.

Description

FLATTEN_CONJ_CONV "t1 /\ ... /\ tn" returns a theorem of the form:
   |- t1 /\ ... /\ tn = u1 /\ ... /\ un

where the right-hand side of the equation is a flattened version of the left-hand side.

Failure

Never fails.

Example

#FLATTEN_CONJ_CONV "(a /\ (b /\ c)) /\ ((d /\ e) /\ f)";;
|- (a /\ b /\ c) /\ (d /\ e) /\ f = a /\ b /\ c /\ d /\ e /\ f

See also

CONJUNCTS_CONV.

 FORALL_CONJ_CONV

FORALL_CONJ_CONV : conv

Synopsis

Moves universal quantifiers down through a tree of conjunctions.

Description

FORALL_CONJ_CONV "!x1 ... xm. t1 /\ ... /\ tn" returns the theorem:
   |- !x1 ... xm. t1 /\ ... /\ tn =
      (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)

where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation.

Failure

Never fails.

Example

#FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). (a /\ b) /\ c";;
|- (!x y z. (a /\ b) /\ c) = ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c)
#FORALL_CONJ_CONV "T";;
|- T = T
#FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). T";;
|- (!x y z. T) = (!x y z. T)

See also

CONJ_FORALL_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV,
FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_RIGHT_RULE.

 FORALL_CONJ_ONCE_CONV

FORALL_CONJ_ONCE_CONV : conv

Synopsis

Moves a single universal quantifier down through a tree of conjunctions.

Description

FORALL_CONJ_ONCE_CONV "!x. t1 /\ ... /\ tn" returns the theorem:

   |- !x. t1 /\ ... /\ tn = (!x. t1) /\ ... /\ (!x. tn)

where the original term can be an arbitrary tree of conjunctions. The structure of the tree is retained in both sides of the equation.

Failure

Fails if the argument term is not of the required form. The body of the term need not be a conjunction.

Example

#FORALL_CONJ_ONCE_CONV "!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)";;
|- (!x. ((x \/ a) /\ (x \/ b)) /\ (x \/ c)) =
   ((!x. x \/ a) /\ (!x. x \/ b)) /\ (!x. x \/ c)
#FORALL_CONJ_ONCE_CONV "!x. x \/ a";;
|- (!x. x \/ a) = (!x. x \/ a)
#FORALL_CONJ_ONCE_CONV "!x. ((x \/ a) /\ (y \/ b)) /\ (x \/ c)";;
|- (!x. ((x \/ a) /\ (y \/ b)) /\ (x \/ c)) =
   ((!x. x \/ a) /\ (!x. y \/ b)) /\ (!x. x \/ c)

See also

CONJ_FORALL_ONCE_CONV, FORALL_CONJ_CONV, CONJ_FORALL_CONV,
FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_RIGHT_RULE.

 FORALL_CONJ_RIGHT_RULE

FORALL_CONJ_RIGHT_RULE : (thm -> thm)

Synopsis

Moves universal quantifiers down through a tree of conjunctions.

Description

      A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn
   -------------------------------------------------------------------
    A |- !z1 ... zr.
          t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)

Failure

Fails if the argument theorem is not of the required form, though either or both of r and p may be zero.

See also

CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_CONV, CONJ_FORALL_CONV,
FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV.

line name 25

 line_name
line_name : (term -> string)

Synopsis

Computes the line name of an equation.

Description

line_name "!y1 ... ym. f x1 ... xn = t" returns the string `f`.

Failure

Fails if the argument term is not of the specified form.

See also

line_var.
 line_var
line_var : (term -> term)

Synopsis

Computes the line variable of an equation.

Description

line_var "!y1 ... ym. f x1 ... xn = t" returns the variable "f".

Failure

Fails if the argument term is not of the specified form.

See also

line_name.
 PRUNE_CONV
PRUNE_CONV : conv

Synopsis

Prunes all hidden variables.

Description

PRUNE_CONV "?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp" returns a

theorem of the form:

   |- (?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp) =
      (t1 /\ ... /\ tp)

where each eqni has the form "!y1 ... ym. li x1 ... xn = b" and li does not appear free in any of the other conjuncts or in b. The conversion works if one or more of the eqni’s are not present, that is if li is not free in any of the conjuncts, but does not work if li appears free in more than one of the conjuncts. p may be zero, that is, all the conjuncts may be eqni’s. In this case the result will be simply T (true). Also, for each eqni, m and n may be zero.

Failure

Fails if the argument term is not of the specified form or if any of the li’s are free in more than one of the conjuncts or if the equation for any li is recursive.

Example

#PRUNE_CONV
# "?l2 l1.
#   (!(x:num). l1 x = F) /\ (!x. l2 x = ~(out x)) /\ (!(x:num). out x = T)";;
|- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~out x) /\ (!x. out x = T)) =
   (!x. out x = T)

See also

PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

 PRUNE_ONCE_CONV

PRUNE_ONCE_CONV : conv

Synopsis

Prunes one hidden variable.

Description

PRUNE_ONCE_CONV "?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp" returns a the-

orem of the form:

   |- (?l. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
      (t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)

where eq has the form "!y1 ... ym. l x1 ... xn = b" and l does not appear free in the ti’s or in b. The conversion works if eq is not present, that is if l is not free in any of the conjuncts, but does not work if l appears free in more than one of the conjuncts. Each of m, n and p may be zero.

Failure

Fails if the argument term is not of the specified form or if l is free in more than one of the conjuncts or if the equation for l is recursive.

Example

#PRUNE_ONCE_CONV "?l2. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
|- (?l2. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (!x. l1 x = F)

See also

PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

 PRUNE_ONE_CONV
PRUNE_ONE_CONV : (string -> conv)

Synopsis

Prunes a specified hidden variable.

Description

PRUNE_ONE_CONV `lj` when applied to the term:

   "?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp"

returns a theorem of the form:

   |- (?l1 ... lj ... lr. t1 /\ ... /\ ti /\ eq /\ t(i+1) /\ ... /\ tp) =
      (?l1 ... l(j-1) l(j+1) ... lr. t1 /\ ... /\ ti /\ t(i+1) /\ ... /\ tp)

where eq has the form "!y1 ... ym. lj x1 ... xn = b" and lj does not appear free in the ti’s or in b. The conversion works if eq is not present, that is if lj is not free in any of the conjuncts, but does not work if lj appears free in more than one of the conjuncts. Each of m, n and p may be zero.

If there is more than one line with the specified name (but with different types), the one that appears outermost in the existential quantifications is pruned.

Failure

Fails if the argument term is not of the specified form or if lj is free in more than one of the conjuncts or if the equation for lj is recursive. The function also fails if the specified line is not one of the existentially quantified lines.

Example

#PRUNE_ONE_CONV `l2` "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
|- (?l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l1 x)) = (?l1. !x. l1 x = F)
#PRUNE_ONE_CONV `l1` "?l2 l1. (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l1 x))";;
evaluation failed     PRUNE_ONE_CONV

See also

PRUNE_ONCE_CONV, PRUNE_SOME_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

 PRUNE_RIGHT_RULE

PRUNE_RIGHT_RULE : (thm -> thm)

Synopsis

Prunes all hidden variables.

Description

PRUNE_RIGHT_RULE behaves as follows:

    A |- !z1 ... zr.
          t = ?l1 ... lr. t1 /\ ... /\ eqn1 /\ ... /\ eqnr /\ ... /\ tp
   ---------------------------------------------------------------------
                   A |- !z1 ... zr. t = t1 /\ ... /\ tp

where each eqni has the form "!y1 ... ym. li x1 ... xn = b" and li does not appear free in any of the other conjuncts or in b. The rule works if one or more of the eqni’s are not present, that is if li is not free in any of the conjuncts, but does not work if li appears free in more than one of the conjuncts. p may be zero, that is, all the conjuncts may be eqni’s. In this case the result will be simply T (true). Also, for each eqni, m and n may be zero.

Failure

Fails if the argument theorem is not of the specified form or if any of the li’s are free in more than one of the conjuncts or if the equation for any li is recursive.

Example

#PRUNE_RIGHT_RULE
# (ASSUME
#   "!(in:num->bool) (out:num->bool).
#     DEV (in,out) =
#      ?(l1:num->bool) l2.
#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
. |- !in out. DEV(in,out) = (!x. out x = ~in x)

See also

PRUNE_SOME_RIGHT_RULE, PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV,
PRUNE_CONV.

 PRUNE_SOME_CONV

PRUNE_SOME_CONV : (string list -> conv)

Synopsis

Prunes several hidden variables.

Description

PRUNE_SOME_CONV [`li1`;...;`lik`] when applied to the term:
   "?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp"

returns a theorem of the form:

   |- (?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp) =
      (?li(k+1) ... lir. t1 /\ ... /\ tp)

where for 1 <= j <= k, each eqnij has the form:

   "!y1 ... ym. lij x1 ... xn = b"

and lij does not appear free in any of the other conjuncts or in b. The li’s are related by the equation:

   {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr}

The conversion works if one or more of the eqnij’s are not present, that is if lij is not free in any of the conjuncts, but does not work if lij appears free in more than one of the conjuncts. p may be zero, that is, all the conjuncts may be eqnij’s. In this case the body of the result will be T (true). Also, for each eqnij, m and n may be zero.

If there is more than one line with a specified name (but with different types), the one that appears outermost in the existential quantifications is pruned. If such a line name is mentioned twice in the list, the two outermost occurrences of lines with that name will be pruned, and so on.

Failure

Fails if the argument term is not of the specified form or if any of the lij’s are free in more than one of the conjuncts or if the equation for any lij is recursive. The function also fails if any of the specified lines are not one of the existentially quantified lines.

Example

#PRUNE_SOME_CONV [`l1`;`l2`]
# "?l3 l2 l1.
#   (!(x:num). l1 x = F) /\ (!x. l2 x = ~(l3 x)) /\ (!(x:num). l3 x = T)";;
|- (?l3 l2 l1. (!x. l1 x = F) /\ (!x. l2 x = ~l3 x) /\ (!x. l3 x = T)) =
   (?l3. !x. l3 x = T)

See also

PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_CONV, PRUNE_SOME_RIGHT_RULE,
PRUNE_RIGHT_RULE.

 PRUNE_SOME_RIGHT_RULE

PRUNE_SOME_RIGHT_RULE : (string list -> thm -> thm)

Synopsis

Prunes several hidden variables.

Description

PRUNE_SOME_RIGHT_RULE [`li1`;...;`lik`] behaves as follows:
    A |- !z1 ... zr.
          t = ?l1 ... lr. t1 /\ ... /\ eqni1 /\ ... /\ eqnik /\ ... /\ tp
   -----------------------------------------------------------------------
           A |- !z1 ... zr. t = ?li(k+1) ... lir. t1 /\ ... /\ tp

where for 1 <= j <= k, each eqnij has the form:

   "!y1 ... ym. lij x1 ... xn = b"

and lij does not appear free in any of the other conjuncts or in b. The li’s are related by the equation:

   {li1,...,lik} u {li(k+1),...,lir} = {l1,...,lr}

The rule works if one or more of the eqnij’s are not present, that is if lij is not free in any of the conjuncts, but does not work if lij appears free in more than one of the conjuncts. p may be zero, that is, all the conjuncts may be eqnij’s. In this case the conjunction will be transformed to T (true). Also, for each eqnij, m and n may be zero.

If there is more than one line with a specified name (but with different types), the one that appears outermost in the existential quantifications is pruned. If such a line name is mentioned twice in the list, the two outermost occurrences of lines with that name will be pruned, and so on.

Failure

Fails if the argument theorem is not of the specified form or if any of the lij’s are free in more than one of the conjuncts or if the equation for any lij is recursive. The function also fails if any of the specified lines are not one of the existentially quantified lines.

Example

#PRUNE_SOME_RIGHT_RULE [`l1`;`l2`]
# (ASSUME
#   "!(in:num->bool) (out:num->bool).
#     DEV (in,out) =
#      ?(l1:num->bool) l2.
#       (!x. l1 x = F) /\ (!x. l2 x = ~(in x)) /\ (!x. out x = ~(in x))");;
. |- !in out. DEV(in,out) = (!x. out x = ~in x)

See also

PRUNE_RIGHT_RULE, PRUNE_ONCE_CONV, PRUNE_ONE_CONV, PRUNE_SOME_CONV, PRUNE_CONV.

 UNFOLD_CONV
UNFOLD_CONV : (thm list -> conv)

Synopsis

Expands sub-components of a hardware description using their definitions.

Description

UNFOLD_CONV thl "t1 /\ ... /\ tn" returns a theorem of the form:
   B |- t1 /\ ... /\ tn = t1' /\ ... /\ tn'

where each ti' is the result of rewriting ti with the theorems in thl. The set of assumptions B is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a ti, it is unchanged.

Failure

Never fails.

Example

#UNFOLD_CONV [ASSUME "!in out. INV (in,out) = !(t:num). out t = ~(in t)"]
# "INV (l1,l2) /\ INV (l2,l3) /\ (!(t:num). l1 t = l2 (t-1) \/ l3 (t-1))";;
. |- INV(l1,l2) /\ INV(l2,l3) /\ (!t. l1 t = l2(t - 1) \/ l3(t - 1)) =
     (!t. l2 t = ~l1 t) /\
     (!t. l3 t = ~l2 t) /\
     (!t. l1 t = l2(t - 1) \/ l3(t - 1))

See also

UNFOLD_RIGHT_RULE.
 UNFOLD_RIGHT_RULE
UNFOLD_RIGHT_RULE : (thm list -> thm -> thm)

Synopsis

Expands sub-components of a hardware description using their definitions.

Description

UNFOLD_RIGHT_RULE thl behaves as follows:
       A |- !z1 ... zr. t = ?y1 ... yp. t1 /\ ... /\ tn
   --------------------------------------------------------
    B u A |- !z1 ... zr. t = ?y1 ... yp. t1' /\ ... /\ tn'

where each ti' is the result of rewriting ti with the theorems in thl. The set of assumptions B is the union of the instantiated assumptions of the theorems used for rewriting. If none of the rewrites are applicable to a ti, it is unchanged.

Failure

Fails if the second argument is not of the required form, though either or both of r and p may be zero.

Example

#UNFOLD_RIGHT_RULE [ASSUME "!in out. INV(in,out) = !(t:num). out t = ~(in t)"]
# (ASSUME "!(in:num->bool) out. BUF(in,out) = ?l. INV(in,l) /\ INV(l,out)");;
.. |- !in out.
       BUF(in,out) = (?l. (!t. l t = ~in t) /\ (!t. out t = ~l t))

See also

UNFOLD_CONV.

 UNWIND_ALL_BUT_CONV
UNWIND_ALL_BUT_CONV : (string list -> conv)

Synopsis

Unwinds all lines of a device (except those in the argument list) as much as possible.

Description

UNWIND_ALL_BUT_CONV l when applied to the following term:

   "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn"

returns a theorem of the form:

   |- t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn =
      t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn'

where ti' (for 1 <= i <= n) is ti rewritten with the equations eqni (1 <= i <= m). These equations are those conjuncts with line name not in l (and which are equations).

Failure

Never fails but may loop indefinitely.

Example

#UNWIND_ALL_BUT_CONV [`l2`]
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\
   (!x. l2 x = 7)

See also

UNWIND_ONCE_CONV, UNWIND_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE,
UNWIND_AUTO_RIGHT_RULE.

 UNWIND_ALL_BUT_RIGHT_RULE

UNWIND_ALL_BUT_RIGHT_RULE : (string list -> thm -> thm)

Synopsis

Unwinds all lines of a device (except those in the argument list) as much as possible.

Description

UNWIND_ALL_BUT_RIGHT_RULE l behaves as follows:
    A |- !z1 ... zr.
          t =
          (?l1 ... lp. t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn)
   ---------------------------------------------------------------------
    A |- !z1 ... zr.
          t =
          (?l1 ... lp. t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn')

where ti' (for 1 <= i <= n) is ti rewritten with the equations eqni (1 <= i <= m). These equations are those conjuncts with line name not in l (and which are equations).

Failure

Fails if the argument theorem is not of the required form, though either or both of p and r may be zero. May loop indefinitely.

Example

#UNWIND_ALL_BUT_RIGHT_RULE [`l2`]
# (ASSUME
#   "!f. IMP(f) =
#     ?l2 l1.
#      (!(x:num). l1 x = (l2 x) - 1) /\
#      (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#      (!x. l2 x = 7)");;
. |- !f.
      IMP f =
      (?l2 l1.
        (!x. l1 x = (l2 x) - 1) /\
        (!x. f x = (l2(x + 1)) + ((l2(x + 2)) - 1)) /\
        (!x. l2 x = 7))

See also

UNWIND_AUTO_RIGHT_RULE, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV,
UNWIND_ONCE_CONV, UNWIND_CONV.

 UNWIND_AUTO_CONV

UNWIND_AUTO_CONV : conv

Synopsis

Automatic unwinding of equations defining wire values in a standard device specification.

Description

UNWIND_AUTO_CONV "?l1 ... lm. t1 /\ ... /\ tn" returns a theorem of the form:
   |- (?l1 ... lm. t1 /\ ... /\ tn) = (?l1 ... lm. t1' /\ ... /\ tn')

where tj' is tj rewritten with equations selected from the ti’s.

The function decides which equations to use for rewriting by performing a loop analysis on the graph representing the dependencies of the lines. By this means the term can be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations.

Failure

Fails if there is more than one equation for any line variable.

Example

#UNWIND_AUTO_CONV
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)

See also

UNWIND_ONCE_CONV, UNWIND_CONV, UNWIND_ALL_BUT_CONV, UNWIND_ALL_BUT_RIGHT_RULE,
UNWIND_AUTO_RIGHT_RULE.

 UNWIND_AUTO_RIGHT_RULE

UNWIND_AUTO_RIGHT_RULE : (thm -> thm)

Synopsis

Automatic unwinding of equations defining wire values in a standard device specification.

Description

UNWIND_AUTO_RIGHT_RULE behaves as follows:
    A |- !z1 ... zr. t = ?l1 ... lm. t1  /\ ... /\ tn
   ----------------------------------------------------
    A |- !z1 ... zr. t = ?l1 ... lm. t1' /\ ... /\ tn'

where tj' is tj rewritten with equations selected from the ti’s.

The function decides which equations to use for rewriting by performing a loop analysis on the graph representing the dependencies of the lines. By this means the term can be unwound as much as possible without the risk of looping. The user is left to deal with the recursive equations.

Failure

Fails if there is more than one equation for any line variable, or if the argument theorem is not of the required form, though either or both of m and r may be zero.

Example

#UNWIND_AUTO_RIGHT_RULE
# (ASSUME
#   "!f. IMP(f) =
#     ?l2 l1.
#      (!(x:num). l1 x = (l2 x) - 1) /\
#      (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#      (!x. l2 x = 7)");;
. |- !f.
      IMP f =
      (?l2 l1.
        (!x. l1 x = 7 - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7))

See also

UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_CONV,
UNWIND_ONCE_CONV, UNWIND_CONV.

 UNWIND_CONV

UNWIND_CONV : ((term -> bool) -> conv)

Synopsis

Unwinds device behaviour using selected line equations until no change.

Description

UNWIND_CONV p "t1 /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn" returns a theorem of

the form:

   |- t1  /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn =
      t1' /\ ... /\ eqn1 /\ ... /\ eqnm /\ ... /\ tn'

where ti' (for 1 <= i <= n) is ti rewritten with the equations eqni (1 <= i <= m). These equations are the conjuncts for which the predicate p is true. The ti terms are the conjuncts for which p is false. The rewriting is repeated until no changes take place.

Failure

Never fails but may loop indefinitely.

Example

#UNWIND_CONV (\tm. mem (line_name tm) [`l1`;`l2`])
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\ (!x. f x = 7 + (7 - 1)) /\ (!x. l2 x = 7)

See also

UNWIND_ONCE_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV,
UNWIND_ALL_BUT_RIGHT_RULE, UNWIND_AUTO_RIGHT_RULE.

 UNWIND_ONCE_CONV

UNWIND_ONCE_CONV : ((term -> bool) -> conv)

Synopsis

Basic conversion for parallel unwinding of equations defining wire values in a standard device specification.

Description

UNWIND_ONCE_CONV p tm unwinds the conjunction tm using the equations selected by the predicate p. tm should be a conjunction, equivalent under associative-commutative reordering to:

   t1 /\ t2 /\ ... /\ tn

p is used to partition the terms ti for 1 <= i <= n into two disjoint sets:

   REW = {ti | p ti}
   OBJ = {ti | ~p ti}

The terms ti for which p is true are then used as a set of rewrite rules (thus they should be equations) to do a single top-down parallel rewrite of the remaining terms. The rewritten terms take the place of the original terms in the input conjunction. For example, if tm is:

   t1 /\ t2 /\ t3 /\ t4

and REW = {t1,t3} then the result is:

   |- t1 /\ t2 /\ t3 /\ t4 = t1 /\ t2' /\ t3 /\ t4'

where ti' is ti rewritten with the equations REW.

Failure

Never fails.

Example

#UNWIND_ONCE_CONV (\tm. mem (line_name tm) [`l1`;`l2`])
# "(!(x:num). l1 x = (l2 x) - 1) /\
#  (!x. f x = (l2 (x+1)) + (l1 (x+2))) /\
#  (!x. l2 x = 7)";;
|- (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = (l2(x + 1)) + (l1(x + 2))) /\
   (!x. l2 x = 7) =
   (!x. l1 x = (l2 x) - 1) /\
   (!x. f x = 7 + ((l2(x + 2)) - 1)) /\
   (!x. l2 x = 7)

See also

UNWIND_CONV, UNWIND_ALL_BUT_CONV, UNWIND_AUTO_CONV, UNWIND_ALL_BUT_RIGHT_RULE,
UNWIND_AUTO_RIGHT_RULE.

40 Chapter 2. ML Functions in the unwind Library

References

[1] A. Camilleri, M. Gordon, and T. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, Proceedings of the IFIP WG 10.2 Working Conference: From HDL Descriptions to Guaranteed Correct Circuit Designs, Grenoble, September 1986. North-Holland, Amsterdam (1987). Also: University of Cambridge Computer Laboratory, Technical Report 91, September 1986.

[2] DSTO and SRI International, The HOL System: DESCRIPTION, (1991).

Index

CONJ_FORALL_CONV, 11
CONJ_FORALL_ONCE_CONV, 12
CONJ_FORALL_RIGHT_RULE, 13
DEPTH_EXISTS_CONV, 14
DEPTH_FORALL_CONV, 14
EXISTS_DEL1_CONV, 15
EXISTS_DEL_CONV, 15
EXISTS_EQN_CONV, 16
EXPAND_ALL_BUT_CONV, 16
EXPAND_ALL_BUT_RIGHT_RULE, 18
EXPAND_AUTO_CONV, 19
EXPAND_AUTO_RIGHT_RULE, 20
FLATTEN_CONJ_CONV, 21
FORALL_CONJ_CONV, 22
FORALL_CONJ_ONCE_CONV, 23
FORALL_CONJ_RIGHT_RULE, 24

help updating search path, 1

line_name, 25
line_var, 25
load_library, 1
PRUNE_CONV, 25
PRUNE_ONCE_CONV, 26
PRUNE_ONE_CONV, 27
PRUNE_RIGHT_RULE, 28
PRUNE_SOME_CONV, 29
PRUNE_SOME_RIGHT_RULE, 30
UNFOLD_CONV, 32

                                       UNFOLD_RIGHT_RULE, 32
                                       UNWIND_ALL_BUT_CONV, 33
                                       UNWIND_ALL_BUT_RIGHT_RULE, 34
                                       UNWIND_AUTO_CONV, 35
                                       UNWIND_AUTO_RIGHT_RULE, 36
                                       UNWIND_CONV, 37
                                       UNWIND_ONCE_CONV, 38