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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
\DOC IMP_RES_THEN
\TYPE {IMP_RES_THEN : thm_tactical}
\SYNOPSIS
Resolves an implication with the assumptions of a goal.
\KEYWORDS
theorem-tactic, resolution, implication.
\DESCRIBE
The function {IMP_RES_THEN} is the basic building block for resolution in HOL.
This is not full higher-order, or even first-order, resolution with
unification, but simply one way simultaneous pattern-matching (resulting in
term and type instantiation) of the antecedent of an implicative theorem to the
conclusion of another theorem (the candidate antecedent).
Given a theorem-tactic {ttac} and a theorem {th}, the theorem-tactical
{IMP_RES_THEN} produces a tactic that, when applied to a goal {A ?- g} attempts
to match each antecedent {ui} to each assumption {aj |- aj} in the assumptions
{A}. If the antecedent {ui} of any implication matches the conclusion {aj} of
any assumption, then an instance of the theorem {Ai u {{aj}} |- vi}, called a
`resolvent', is obtained by specialization of the variables {x1}, ..., {xn} and
type instantiation, followed by an application of modus ponens. There may be
more than one canonical implication and each implication is tried against every
assumption of the goal, so there may be several resolvents (or, indeed, none).
Tactics are produced using the theorem-tactic {ttac} from all these resolvents
(failures of {ttac} at this stage are filtered out) and these tactics are then
applied in an unspecified sequence to the goal. That is,
{
IMP_RES_THEN ttac th (A ?- g)
}
\noindent has the effect of:
{
MAP_EVERY (mapfilter ttac [... ; (Ai u {{aj}} |- vi) ; ...]) (A ?- g)
}
\noindent where the theorems {Ai u {{aj}} |- vi} are all the consequences that
can be drawn by a (single) matching modus-ponens inference from the
assumptions of the goal {A ?- g} and the implications derived from the supplied
theorem {th}. The sequence in which the theorems {Ai u {{aj}} |- vi} are
generated and the corresponding tactics applied is unspecified.
\FAILURE
Evaluating {IMP_RES_THEN ttac th} fails if the supplied theorem {th} is not an
implication, or if no implications can be derived from {th} by the
transformation process involved. Evaluating {IMP_RES_THEN ttac th (A ?- g)}
fails if no assumption of the goal {A ?- g} can be resolved with the
implication or implications derived from {th}. Evaluation also fails if there
are resolvents, but for every resolvent {Ai u {{aj}} |- vi} evaluating the
application {ttac (Ai u {{aj}} |- vi)} fails---that is, if for every resolvent
{ttac} fails to produce a tactic. Finally, failure is propagated if any of the
tactics that are produced from the resolvents by {ttac} fails when applied in
sequence to the goal.
\EXAMPLE
The following example shows a straightforward use of {IMP_RES_THEN} to
infer an equational consequence of the assumptions of a goal, use it
once as a substitution in the conclusion of goal, and then `throw it away'.
Suppose the goal is:
{
# g `!a n. a + n = a ==> !k. k - n = k`;;
}
\noindent and we start out with:
{
# e(REPEAT GEN_TAC THEN DISCH_TAC);;
val it : goalstack = 1 subgoal (1 total)
0 [`a + n = a`]
`!k. k - n = k`
}
\noindent By using the theorem:
{
# let ADD_INV_0 = ARITH_RULE `!m n. m + n = m ==> n = 0`;;
}
\noindent the assumption of this goal implies that {n} equals {0}. A
single-step resolution with this theorem followed by substitution:
{
# e(IMP_RES_THEN SUBST1_TAC ADD_INV_0);;
val it : goalstack = 1 subgoal (1 total)
0 [`a + n = a`]
`!k. k - 0 = k`
}
\noindent Here, a single resolvent {a + n = a |- n = 0} is obtained by
matching the antecedent of {ADD_INV_0} to the assumption of the goal. This is
then used to substitute {0} for {n} in the conclusion of the goal. The goal is
now solvable by {ARITH_TAC} (as indeed was the original goal).
\SEEALSO
IMP_RES_THEN, MATCH_MP, MATCH_MP_TAC.
\ENDDOC
|
