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
|
\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} uses {RES_CANON} to derive a canonical list of implications from
{th}, each of which has the form:
{
Ai |- !x1...xn. ui ==> vi
}
\noindent {IMP_RES_THEN} 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 with `{no implication}' if the supplied
theorem {th} is not an implication, or if no implications can be derived from
{th} by the transformation process described under the entry for {RES_CANON}.
Evaluating {IMP_RES_THEN ttac th (A ?- g)} fails with `{no resolvents}' if no
assumption of the goal {A ?- g} can be resolved with the implication or
implications derived from {th}. Evaluation also fails, with `{no tactics}', 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:
{
a + n = a ?- !k. k - n = k
}
\noindent By the built-in theorem:
{
ADD_INV_0 = |- !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:
{
IMP_RES_THEN SUBST1_TAC ADD_INV_0
}
\noindent can therefore be used to reduce the goal to:
{
a + n = a ?- !k. k - 0 = m
}
\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.
\SEEALSO
IMP_RES_TAC, MATCH_MP, RES_CANON, RES_TAC, RES_THEN.
\ENDDOC
|
