Tactic.CONV

STRUCTURE

SYNOPSIS

Makes a tactic from a conversion.

DESCRIPTION

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'

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 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

CONV_RULE