Cond_rewrite.COND_REWR

STRUCTURE

SYNOPSIS

A lower level conversion implementing simple conditional rewriting.

DESCRIPTION

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_REWR_TAC, COND_REWRITE1_TAC, COND_REWRITE1_CONV, COND_REWR_CANON, search_top_down