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