LIST_MP

Drule.LIST_MP : thm list -> thm -> thm

Performs a chain of Modus Ponens inferences.

When applied to theorems A1 |- t1, ..., An |- tn and a theorem which is a chain of implications with the successive antecedents the same as the conclusions of the theorems in the list (up to alpha-conversion), A |- t1 ==> ... ==> tn ==> t, the LIST_MP inference rule performs a chain of MP inferences to deduce A u A1 u ... u An |- t.

    A1 |- t1 ... An |- tn      A |- t1 ==> ... ==> tn ==> t
   ---------------------------------------------------------  LIST_MP
                    A u A1 u ... u An |- t

Failure

Fails unless the theorem is a chain of implications whose consequents are the same as the conclusions of the list of theorems (up to alpha-conversion), in sequence.

See also

Thm.EQ_MP, Drule.MATCH_MP, Tactic.MATCH_MP_TAC, Thm.MP, Tactic.MP_TAC