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