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
|
\DOC PMATCH_MP
\TYPE {PMATCH_MP : (thm -> thm -> thm)}
\SYNOPSIS
Modus Ponens inference rule with automatic matching.
\KEYWORDS
rule, modus ponens, implication.
\LIBRARY pair
\DESCRIBE
When applied to theorems {A1 |- !p1...pn. t1 ==> t2} and {A2 |- t1'}, the
inference rule {PMATCH_MP} matches {t1} to {t1'} by instantiating free or
paired universally quantified variables in the first theorem (only),
and returns a theorem {A1 u A2 |- !pa..pk. t2'}, where {t2'} is a
correspondingly instantiated version of {t2}. Polymorphic types are also
instantiated if necessary.
Variables free in the consequent but not the antecedent of the first argument
theorem will be replaced by variants if this is necessary to maintain the full
generality of the theorem, and any pairs which were universally quantified
over in the first argument theorem will be universally quantified over in the
result, and in the same order.
{
A1 |- !p1..pn. t1 ==> t2 A2 |- t1'
-------------------------------------- MATCH_MP
A1 u A2 |- !pa..pk. t2'
}
\FAILURE
Fails unless the first theorem is a (possibly repeatedly paired universally
quantified) implication whose antecedent can be instantiated to match
the conclusion of the second theorem, without instantiating any variables
which are free in {A1}, the first theorem's assumption list.
\SEEALSO
MATCH_MP.
\ENDDOC
|
