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
|
\DOC MATCH_ACCEPT_TAC
\TYPE {MATCH_ACCEPT_TAC : thm_tactic}
\SYNOPSIS
Solves a goal which is an instance of the supplied theorem.
\KEYWORDS
tactic.
\DESCRIBE
When given a theorem {A' |- t} and a goal {A ?- t'} where {t} can be matched
to {t'} by instantiating variables which are either free or
universally quantified at the outer level, including appropriate type
instantiation, {MATCH_ACCEPT_TAC} completely solves the goal.
{
A ?- t'
========= MATCH_ACCEPT_TAC (A' |- t)
}
\noindent Unless {A'} is a subset of {A}, this is an invalid tactic.
\FAILURE
Fails unless the theorem has a conclusion which is instantiable to match that
of the goal.
\EXAMPLE
The following example shows variable and type instantiation at work. Suppose we
have the following simple goal:
{
# g `HD [1;2] = 1`;;
}
\noindent we can do it via the polymorphic theorem
{HD = |- !h t. HD(CONS h t) = h}:
{
# e(MATCH_ACCEPT_TAC HD);;
}
\SEEALSO
ACCEPT_TAC.
\ENDDOC
|
