Filter
Top Products
84 CHAPTER 10. TACTICS
#g ‘(\x. x + 1) 2 = 3‘;;
it : goalstack = 1 subgoal (1 total)
‘(\x. x + 1) 2 = 3‘
#e(CONV_TAC(ONCE_DEPTH_CONV BETA_CONV));;
it : goalstack = 1 subgoal (1 total)
‘2 + 1 = 3‘
If the conversion transforms the goal to T, the tactic mechanism accepts that as
solving the goal, rather than presenting T as the subgoal, e.g.
#g ‘2 + 1 = 3‘;;
it : goalstack = 1 subgoal (1 total)
‘2 + 1 = 3‘
#e(CONV_TAC NUM_REDUCE_CONV);;
it : goalstack = No subgoals
The rewriting conversions are also all used as tactics, e.g. REWRITE TAC. The
same names prefixed with ASM also use the assumptions of the current goal as
rewrites.
10.3 Tacticals
Just as basic conversions are built up into composite ones by conversionals, so
tactics are built up via tacticals. For example the infix THEN executes two tactics in
sequence. Once a proof has been found using the subgoal mechanism, it’s common
to plug all the steps into one tactic using THEN, e.g.
#g ‘!m n p. m * (n + p) = (m * n) + (m * p)‘;;
it : goalstack = 1 subgoal (1 total)
‘!m n p. m * (n + p) = m * n + m * p‘
#e(GEN_TAC THEN
INDUCT_TAC THEN
ASM_REWRITE_TAC[ADD; MULT_CLAUSES; ADD_ASSOC]);;
it : goalstack = No subgoals
If the first tactic sequenced by THEN generates more than one subgoal, then the
second tactic is applied to all of them. If different tactics are used for each subgoal,
they can be put into a list and sequenced using THENL, e.g.
#g ‘p ==> p /\ (1 = 1)‘;;
it : goalstack = 1 subgoal (1 total)
‘p ==> p /\ (1 = 1)‘
#e(DISCH_TAC THEN
CONJ_TAC THENL
[ASM_REWRITE_TAC[];
ACCEPT_TAC (REFL ‘1‘)]);;
it : goalstack = No subgoals
Tactics can be executed repeatedly by REPEAT, and there are various other useful
tacticals.