REWR_CONV : thm -> term -> thm

SYNOPSIS

Uses an instance of a given equation to rewrite a term.

DESCRIPTION

REWR_CONV is one of the basic building blocks for the implementation of rewriting in the HOL system. In particular, the term replacement or rewriting done by all the built-in rewriting rules and tactics is ultimately done by applications of REWR_CONV to appropriate subterms. The description given here for REWR_CONV may therefore be taken as a specification of the atomic action of replacing equals by equals that is used in all these higher level rewriting tools. The first argument to REWR_CONV is expected to be an equational theorem which is to be used as a left-to-right rewrite rule. The general form of this theorem is:

   A |- t[x1,...,xn] = u[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. Any of these variables may also be universally quantified at the outermost level of the equation, as for example in:

   A |- !x1...xn. t[x1,...,xn] = u[x1,...,xn]

Note that REWR_CONV will also work, but will give a generally undesirable result (see below), if the right-hand side of the equation contains free variables that do not also occur free on the left-hand side, as for example in:

   A |- t[x1,...,xn] = u[x1,...,xn,y1,...,ym]

where the variables y1, ..., ym do not occur free in t[x1,...,xn]. If th is an equational theorem of the kind shown above, then REWR_CONV th returns a conversion that maps terms of the form t[e1,...,en/x1,...,xn], in which the terms e1, ..., en are free for x1, ..., xn in t, to theorems of the form:

   A |- t[e1,...,en/x1,...,xn] = u[e1,...,en/x1,...,xn]

That is, REWR_CONV th tm attempts to match the left-hand side of the rewrite rule th to the term tm. If such a match is possible, then REWR_CONV returns the corresponding substitution instance of th. If REWR_CONV is given a theorem th:

   A |- t[x1,...,xn] = u[x1,...,xn,y1,...,ym]

where the variables y1, ..., ym do not occur free in the left-hand side, then the result of applying the conversion REWR_CONV th to a term t[e1,...,en/x1,...,xn] will be:

   A |- t[e1,...,en/x1,...,xn] = u[e1,...,en,v1,...,vm/x1,...,xn,y1,...,ym]

where v1, ..., vm are variables chosen so as to be free nowhere in th or in the input term. The user has no control over the choice of the variables v1, ..., vm, and the variables actually chosen may well be inconvenient for other purposes. This situation is, however, relatively rare; in most equations the free variables on the right-hand side are a subset of the free variables on the left-hand side. In addition to doing substitution for free variables in the supplied equational theorem (or `rewrite rule'), REWR_CONV th tm also does type instantiation, if this is necessary in order to match the left-hand side of the given rewrite rule th to the term argument tm. If, for example, th is the theorem:

   A |- t[x1,...,xn] = u[x1,...,xn]

and the input term tm is (a substitution instance of) an instance of t[x1,...,xn] in which the types ty1, ..., tyi are substituted for the type variables vty1, ..., vtyi, that is if:

   tm = t[ty1,...,tyn/vty1,...,vtyn][e1,...,en/x1,...,xn]

then REWR_CONV th tm returns:

   A |- (t = u)[ty1,...,tyn/vty1,...,vtyn][e1,...,en/x1,...,xn]

Note that, in this case, the type variables vty1, ..., vtyi must not occur anywhere in the hypotheses A. Otherwise, the conversion will fail.

FAILURE CONDITIONS

REWR_CONV th fails if th is not an equation or an equation universally quantified at the outermost level. If th is such an equation:

  th = A |- !v1....vi. t[x1,...,xn] = u[x1,...,xn,y1,...,yn]

then REWR_CONV th tm fails unless the term tm is alpha-equivalent to an instance of the left-hand side t[x1,...,xn] which can be obtained by instantiation of free type variables (i.e. type variables not occurring in the assumptions A) and substitution for the free variables x1, ..., xn.

EXAMPLE

The following example illustrates a straightforward use of REWR_CONV. The supplied rewrite rule is polymorphic, and both substitution for free variables and type instantiation may take place. EQ_SYM_EQ is the theorem:

   |- !x y:A. x = y <=> y = x

and REWR_CONV EQ_SYM behaves as follows:

  # REWR_CONV EQ_SYM_EQ `1 = 2`;;
  val it : thm = |- 1 = 2 <=> 2 = 1
  # REWR_CONV EQ_SYM_EQ `1 < 2`;;
  Exception: Failure "term_pmatch".

The second application fails because the left-hand side `x = y` of the rewrite rule does not match the term to be rewritten, namely `1 < 2`. In the following example, one might expect the result to be the theorem A |- f 2 = 2, where A is the assumption of the supplied rewrite rule:

  # REWR_CONV (ASSUME `!x:A. f x = x`) `f 2:num`;;
  Exception: Failure "term_pmatch: can't instantiate local constant".

The application fails, however, because the type variable A appears in the assumption of the theorem returned by ASSUME `!x:A. f x = x`. Failure will also occur in situations like:

  # REWR_CONV (ASSUME `f (n:num) = n`) `f 2:num`;;
  Exception: Failure "term_pmatch: can't instantiate local constant".

where the left-hand side of the supplied equation contains a free variable (in this case n) which is also free in the assumptions, but which must be instantiated in order to match the input term.