----------------------------------------------------------------------
COND_REWR_CONV                                          (Cond_rewrite)
----------------------------------------------------------------------
COND_REWR_CONV : ((term -> term ->
 ((term # term) list # (type # type) list) list) -> thm -> conv)

SYNOPSIS
A lower level conversion implementing simple conditional rewriting.

KEYWORDS
conversion, rewriting, conditional.

DESCRIBE
{COND_REWR_CONV} is one of the basic building blocks for the
implementation of the simple conditional rewriting conversions in the
HOL system. In particular, the conditional term replacement or
rewriting done by all the conditional
rewriting conversions in this library is ultimately done by applications of
{COND_REWR_CONV}.  The description given here for {COND_REWR_CONV} may
therefore be taken as a specification of the atomic action of
replacing equals by equals in a term under certain conditions that
are used in all these higher level conditional rewriting conversions.

The first argument to {COND_REWR_CONV} is expected to be a function
which returns a list of matches. Each of these matches is in the form
of the value returned by the built-in function {match}. It is used to
search the input term for instances which may be rewritten.

The second argument to {COND_REWR_CONV} is expected to be an
implicative theorem in the following form:

   A |- !x1 ... xn. P1 ==> ... Pm ==> (Q[x1,...,xn] = R[x1,...,xn])

where {x1}, ..., {xn} are all the variables that occur free in the
left hand side of the conclusion of the theorem but do not occur free in the
assumptions.

The last argument to {COND_REWR_CONV} is the term to be rewritten.

If {fn} is a function and {th} is an implicative theorem of the kind
shown above, then {COND_REWR_CONV fn th} will be a conversion.
When applying to a term {tm}, it will return a theorem

   P1', ..., Pm' |- tm = tm[R'/Q']

if evaluating {fn Q[x1,...,xn] tm} returns a
non-empty list of matches.
The assumptions of the resulting theorem are instances of the
antecedents of the input theorem {th}. The right hand side of the
equation is obtained by rewriting the input term {tm} with instances of
the conclusion of the input theorem.

FAILURE
{COND_REWR_CONV fn th} fails if {th} is not an implication of the form
described above.  If {th} is such an equation, but the function {fn}
returns a null list of matches, or the function {fn} returns a
non-empty list of matches, but the term or type instantiation fails.

EXAMPLE
The following example illustrates a straightforward use of {COND_REWR_CONV}.
We use the built-in theorem {LESS_MOD} as the input theorem, and the function
{search_top_down} as the search function.

   #LESS_MOD;;
   Theorem LESS_MOD autoloading from theory `arithmetic` ...
   LESS_MOD = |- !n k. k < n ==> (k MOD n = k)

   |- !n k. k < n ==> (k MOD n = k)

   #search_top_down;;
   - : (term -> term -> ((term # term) list # (type # type) list) list)

   #COND_REWR_CONV search_top_down LESS_MOD "2 MOD 3";;
   2 < 3 |- 2 MOD 3 = 2


SEEALSO
Cond_rewrite.COND_REWR_TAC, Cond_rewrite.COND_REWRITE1_TAC,
Cond_rewrite.COND_REWRITE1_CONV, Cond_rewrite.COND_REWR_CANON,
Cond_rewrite.search_top_down.

----------------------------------------------------------------------