MP

Thm.MP : thm -> thm -> thm

Implements the Modus Ponens inference rule.

When applied to theorems A1 |- t1 ==> t2 and A2 |- t1, the inference rule MP returns the theorem A1 u A2 |- t2.

    A1 |- t1 ==> t2   A2 |- t1
   ----------------------------  MP
          A1 u A2 |- t2

In common with the underlying dest_imp syntax function, MP treats theorems with conclusions of the form ~p as implications p ==> F. This means that MP also has the following behaviour:

    A1 |- ~t1     A2 |- t1
   ------------------------  MP
         A1 u A2 |- F

Failure

Fails unless the first theorem is an implication (in the sense of dest_imp) whose antecedent is the same as the conclusion of the second theorem (up to alpha-conversion)

See also

boolSyntax.dest_imp, Thm.EQ_MP, Drule.LIST_MP, Drule.MATCH_MP, Tactic.MATCH_MP_TAC, Tactic.MP_TAC