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
|
\DOC MATCH_MP
\TYPE {MATCH_MP : (thm -> thm -> thm)}
\SYNOPSIS
Modus Ponens inference rule with automatic matching.
\KEYWORDS
rule, modus ponens, implication.
\DESCRIBE
When applied to theorems {A1 |- !x1...xn. t1 ==> t2} and {A2 |- t1'}, the
inference rule {MATCH_MP} matches {t1} to {t1'} by instantiating free or
universally quantified variables in the first theorem (only), and returns a
theorem {A1 u A2 |- !xa..xk. 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 which were universally quantified over in
the first argument theorem will be universally quantified over in the result,
and in the same order.
{
A1 |- !x1..xn. t1 ==> t2 A2 |- t1'
-------------------------------------- MATCH_MP
A1 u A2 |- !xa..xk. t2'
}
\FAILURE
Fails unless the first theorem is a (possibly repeatedly 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.
\EXAMPLE
In this example, automatic renaming occurs to maintain the most general form of
the theorem, and the variant corresponding to {z} is universally quantified
over, since it was universally quantified over in the first argument theorem.
{
#let ith =
# (GENL ["x:num"; "z:num"] o DISCH_ALL o AP_TERM "$+ (w + z)")
# (ASSUME "x:num = y");;
ith = |- !x z. (x = y) ==> ((w + z) + x = (w + z) + y)
#let th = ASSUME "w:num = z";;
th = w = z |- w = z
#MATCH_MP5 ith th;;
w = z |- !z'. (w' + z') + w = (w' + z') + z
}
\SEEALSO
EQ_MP, MATCH_MP_TAC, MP, MP_TAC.
\ENDDOC
|
