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
|
\DOC FILTER_DISCH_THEN
\TYPE {FILTER_DISCH_THEN : (thm_tactic -> term -> tactic)}
\SYNOPSIS
Conditionally gives to a theorem-tactic the antecedent of an implicative goal.
\KEYWORDS
theorem-tactic, undischarge, antecedent, selective.
\DESCRIBE
If {FILTER_DISCH_THEN}'s second argument, a term, does not occur in the
antecedent, then {FILTER_DISCH_THEN} removes the antecedent and then creates a
theorem by {ASSUME}ing it. This new theorem is passed to {FILTER_DISCH_THEN}'s
first argument, which is subsequently expanded. For example, if
{
A ?- t
======== f (ASSUME "u")
B ?- v
}
\noindent then
{
A ?- u ==> t
============== FILTER_DISCH_THEN f
B ?- v
}
\noindent Note that {FILTER_DISCH_THEN} treats {"~u"} as {"u ==> F"}.
\FAILURE
{FILTER_DISCH_THEN} will fail if a term which is identical, or alpha-equivalent
to {"w"} occurs free in the antecedent. {FILTER_DISCH_THEN} will also fail if
the theorem is an implication or a negation.
\COMMENTS
{FILTER_DISCH_THEN} is most easily understood by first understanding
{DISCH_THEN}.
\USES
For preprocessing an antecedent before moving it to the assumptions, or for
using antecedents and then throwing them away.
\SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, NEG_DISCH,
STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|
