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
|
\DOC POP_ASSUM_LIST
\TYPE {POP_ASSUM_LIST : ((thm list -> tactic) -> tactic)}
\SYNOPSIS
Generates a tactic from the assumptions, discards the assumptions and
applies the tactic.
\KEYWORDS
theorem-tactic.
\DESCRIBE
When applied to a function and a goal, {POP_ASSUM_LIST} applies
the function to a list of theorems corresponding to the {ASSUME}d
assumptions of the goal, then applies the resulting tactic to the goal
with an empty assumption list.
{
POP_ASSUM_LIST f ({{A1;...;An}} ?- t) = f [A1 |- A1; ... ; An |- 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 with no
assumptions.
\COMMENTS
There is nothing magical about {POP_ASSUM_LIST}: the same effect can be
achieved by using {ASSUME a} explicitly wherever the assumption {a} is
used. If {POP_ASSUM_LIST} is used, it is unwise to select elements by
number from the {ASSUME}d-assumption list, since this introduces a dependency
on ordering.
\EXAMPLE
Suppose we have a goal of the following form:
{
{{a /\ b, c, (d /\ e) /\ f}} ?- t
}
\noindent Then we can split the conjunctions in the assumption list apart by
applying the tactic:
{
POP_ASSUM_LIST (MAP_EVERY STRIP_ASSUME_TAC)
}
\noindent which results in the new goal:
{
{{a, b, c, d, e, f}} ?- t
}
\USES
Making more delicate use of the assumption list than simply rewriting or
using resolution.
\SEEALSO
ASSUM_LIST, EVERY_ASSUM, IMP_RES_TAC, POP_ASSUM, REWRITE_TAC.
\ENDDOC
|
