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
|
\DOC ASSUM_LIST
\TYPE {ASSUM_LIST : ((thm list -> tactic) -> tactic)}
\SYNOPSIS
Applies a tactic generated from the goal's assumption list.
\KEYWORDS
theorem-tactic, assumption.
\DESCRIBE
When applied to a function of type {thm list -> tactic} and a goal,
{ASSUM_LIST} constructs a tactic by applying {f} to a list of {ASSUME}d
assumptions of the goal, then applies that tactic to the goal.
{
ASSUM_LIST f ({{A1;...;An}} ?- t)
= f [A1 |- A1; ... ; An |- An] ({{A1;...;An}} ?- t)
}
\FAILURE
Fails if the function fails when applied to the list of {ASSUME}d assumptions,
or if the resulting tactic fails when applied to the goal.
\COMMENTS
There is nothing magical about {ASSUM_LIST}: the same effect can usually be
achieved just as conveniently by using {ASSUME a} wherever the
assumption {a} is needed. If {ASSUM_LIST} is used, it is extremely unwise to
use a function which selects elements from its argument list by number, since
the ordering of assumptions should not be relied on.
\EXAMPLE
The tactic:
{
ASSUM_LIST SUBST_TAC
}
\noindent makes a single parallel substitution using all the assumptions,
which can be useful if the rewriting tactics are too blunt for the required
task.
\USES
Making more careful use of the assumption list than simply rewriting or
using resolution.
\SEEALSO
ASM_REWRITE_TAC, EVERY_ASSUM, IMP_RES_TAC, POP_ASSUM, POP_ASSUM_LIST,
REWRITE_TAC.
\ENDDOC
|
