1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
\DOC THENL
\TYPE {(THENL) : tactic -> tactic list -> tactic}
\SYNOPSIS
Applies a list of tactics to the corresponding subgoals generated by a tactic.
\KEYWORDS
tactical.
\DESCRIBE
If {t,t1,...,tn} are tactics, {t THENL [t1;...;tn]} is a tactic which applies
{t} to a goal, and if it does not fail, applies the tactics {t1,...,tn} to the
corresponding subgoals, unless {t} completely solves the goal.
\FAILURE
The application of {THENL} to a tactic and tactic list never fails.
The resulting tactic fails if {t} fails when applied to the goal, or if
the goal list is not empty and its length is not the same as that of the
tactic list, or finally if {ti} fails when applied to the {i}'th subgoal
generated by {t}.
\EXAMPLE
If we want to prove the inbuilt theorem {LE_LDIV} ourselves:
{
# g `!a b n. ~(a = 0) /\ b <= a * n ==> b DIV a <= n`;;
...
}
\noindent we may start by proving a lemma {n = (a * n) DIV a} from the given
hypotheses. The following step generates two subgoals:
{
# e(REPEAT STRIP_TAC THEN SUBGOAL_THEN `n = (a * n) DIV a` SUBST1_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`~(a = 0)`]
1 [`b <= a * n`]
`b DIV a <= (a * n) DIV a`
0 [`~(a = 0)`]
1 [`b <= a * n`]
`n = (a * n) DIV a`
}
Each subgoal has a relatively short proof, but these proofs are quite
different. We can combine them with the initial tactic above using {THENL}, so
the following would solve the initial goal:
{
# e(REPEAT STRIP_TAC THEN SUBGOAL_THEN `n = (a * n) DIV a` SUBST1_TAC THENL
[ASM_SIMP_TAC[DIV_MULT]; MATCH_MP_TAC DIV_MONO THEN ASM_REWRITE_TAC[]]);;
}
Note that it is quite a common situation for the same tactic to be applied to
all generated subgoals. In that case, you can just use {THEN}, e.g. in the
proof of the pre-proved theorem {ADD_0}:
{
# g `!m. m + 0 = m`;;
...
# e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);;
val it : goalstack = No subgoals
}
\USES
Applying different tactics to different subgoals.
\SEEALSO
EVERY, ORELSE, THEN.
\ENDDOC
|
