1\DOC MP
2
3\TYPE {MP : thm -> thm -> thm}
4
5\SYNOPSIS
6Implements the Modus Ponens inference rule.
7
8\KEYWORDS
9rule, modus, ponens, implication.
10
11\DESCRIBE
12When applied to theorems {A1 |- t1 ==> t2} and {A2 |- t1},
13the inference rule {MP} returns the theorem {A1 u A2 |- t2}.
14{
15    A1 |- t1 ==> t2   A2 |- t1
16   ----------------------------  MP
17          A1 u A2 |- t2
18}
19In common with the underlying {dest_imp} syntax function, {MP} treats
20theorems with conclusions of the form {~p} as implications {p ==> F}.
21This means that {MP} also has the following behaviour:
22{
23    A1 |- ~t1     A2 |- t1
24   ------------------------  MP
25         A1 u A2 |- F
26}
27
28
29
30\FAILURE
31Fails unless the first theorem is an implication (in the sense of
32{dest_imp}) whose antecedent is the same as the conclusion of the
33second theorem (up to alpha-conversion)
34
35\SEEALSO
36boolSyntax.dest_imp, Thm.EQ_MP, Drule.LIST_MP, Drule.MATCH_MP, Tactic.MATCH_MP_TAC, Tactic.MP_TAC.
37\ENDDOC
38