----------------------------------------------------------------------
CONV_TAC                                                      (Tactic)
----------------------------------------------------------------------
CONV_TAC : (conv -> tactic)

SYNOPSIS
Makes a tactic from a conversion.

KEYWORDS
conversional, tactical.

DESCRIBE
If {c} is a conversion, then {CONV_TAC c} is a tactic that applies {c} to the
goal.  That is, if {c} maps a term {"g"} to the theorem {|- g = g'}, then the
tactic {CONV_TAC c} reduces a goal {g} to the subgoal {g'}.  More precisely, if
{c "g"} returns {A' |- g = g'}, then:

         A ?- g
     ===============  CONV_TAC c
         A ?- g'

If {c} raises {UNCHANGED} then {CONV_TAC c} reduces a goal to itself.

Note that the conversion {c} should return a theorem whose
assumptions are also among the assumptions of the goal (normally, the
conversion will returns a theorem with no assumptions). {CONV_TAC} does not
fail if this is not the case, but the resulting tactic will be invalid, so the
theorem ultimately proved using this tactic will have more assumptions than
those of the original goal.

FAILURE
{CONV_TAC c} applied to a goal {A ?- g} fails if {c} fails 
(other than by raising {UNCHANGED}) when applied to the term {g}.
The function returned by {CONV_TAC c} will also fail if the ML
function {c:term->thm} is not, in fact, a conversion 
(i.e. a function that maps a term {t} to a theorem {|- t = t'}).

USES
{CONV_TAC} is used to apply simplifications that can’t be expressed as
equations (rewrite rules).  For example, a goal can be simplified by
beta-reduction, which is not expressible as a single equation, using the tactic

   CONV_TAC(DEPTH_CONV BETA_CONV)

The conversion {BETA_CONV} maps a beta-redex {"(\x.u)v"} to the
theorem

   |- (\x.u)v = u[v/x]

and the ML expression {(DEPTH_CONV BETA_CONV)} evaluates to a
conversion that maps a term {"t"} to the theorem {|- t=t'} where {t'} is
obtained from {t} by beta-reducing all beta-redexes in {t}. Thus
{CONV_TAC(DEPTH_CONV BETA_CONV)} is a tactic which reduces beta-redexes
anywhere in a goal.

SEEALSO
Abbrev.conv, Conv.UNCHANGED, Conv.CONV_RULE.

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