1\DOC CONV_TAC
2
3\TYPE {CONV_TAC : (conv -> tactic)}
4
5\SYNOPSIS
6Makes a tactic from a conversion.
7
8\KEYWORDS
9conversional, tactical.
10
11\DESCRIBE
12If {c} is a conversion, then {CONV_TAC c} is a tactic that applies {c} to the
13goal.  That is, if {c} maps a term {"g"} to the theorem {|- g = g'}, then the
14tactic {CONV_TAC c} reduces a goal {g} to the subgoal {g'}.  More precisely, if
15{c "g"} returns {A' |- g = g'}, then:
16{
17         A ?- g
18     ===============  CONV_TAC c
19         A ?- g'
20}
21If {c} raises {UNCHANGED} then {CONV_TAC c} reduces a goal to itself.
22
23Note that the conversion {c} should return a theorem whose
24assumptions are also among the assumptions of the goal (normally, the
25conversion will returns a theorem with no assumptions). {CONV_TAC} does not
26fail if this is not the case, but the resulting tactic will be invalid, so the
27theorem ultimately proved using this tactic will have more assumptions than
28those of the original goal.
29
30\FAILURE
31
32{CONV_TAC c} applied to a goal {A ?- g} fails if {c} fails 
33(other than by raising {UNCHANGED}) when applied to the term {g}.
34The function returned by {CONV_TAC c} will also fail if the ML
35function {c:term->thm} is not, in fact, a conversion 
36(i.e. a function that maps a term {t} to a theorem {|- t = t'}).
37
38\USES
39{CONV_TAC} is used to apply simplifications that can't be expressed as
40equations (rewrite rules).  For example, a goal can be simplified by
41beta-reduction, which is not expressible as a single equation, using the tactic
42{
43   CONV_TAC(DEPTH_CONV BETA_CONV)
44}
45The conversion {BETA_CONV} maps a beta-redex {"(\x.u)v"} to the
46theorem
47{
48   |- (\x.u)v = u[v/x]
49}
50and the ML expression {(DEPTH_CONV BETA_CONV)} evaluates to a
51conversion that maps a term {"t"} to the theorem {|- t=t'} where {t'} is
52obtained from {t} by beta-reducing all beta-redexes in {t}. Thus
53{CONV_TAC(DEPTH_CONV BETA_CONV)} is a tactic which reduces beta-redexes
54anywhere in a goal.
55
56\SEEALSO
57Abbrev.conv, Conv.UNCHANGED, Conv.CONV_RULE.
58\ENDDOC
59