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
|
\DOC FIRST_ASSUM
\TYPE {FIRST_ASSUM : (thm_tactic -> tactic)}
\SYNOPSIS
Maps a theorem-tactic over the assumptions, applying first successful tactic.
\KEYWORDS
theorem-tactical, assumption.
\DESCRIBE
The tactic
{
FIRST_ASSUM ttac ([A1; ...; An], g)
}
\noindent has the effect of applying the first tactic which can be produced by
{ttac} from the {ASSUME}d assumptions {(A1 |- A1)}, ..., {(An |- An)} and which
succeeds when applied to the goal. Failures of {ttac} to produce a tactic are
ignored.
\FAILURE
Fails if {ttac (Ai |- Ai)} fails for every assumption {Ai}, or if the
assumption list is empty, or if all the tactics produced by {ttac} fail when
applied to the goal.
\EXAMPLE
The tactic
{
FIRST_ASSUM (\asm. CONTR_TAC asm ORELSE ACCEPT_TAC asm)
}
\noindent searches the assumptions for either a contradiction or the desired
conclusion. The tactic
{
FIRST_ASSUM MATCH_MP_TAC
}
\noindent searches the assumption list for an implication whose conclusion
matches the goal, reducing the goal to the antecedent of the corresponding
instance of this implication.
\SEEALSO
ASSUM_LIST, EVERY, EVERY_ASSUM, FIRST, MAP_EVERY, MAP_FIRST.
\ENDDOC
|
