MP_CONV
Conv.MP_CONV : conv -> conv
Eliminate the antecedent of a theorem using a conversion/proof rule.
If c is a conversion that when applied to P returns the theorem
|- P = T or |- P, and th is a theorem of the general form
|- P ==> Q, then MP_CONV c th will return the theorem |- Q,
i.e. the antecedent of th is eliminated by the conversion c. This is
done by calling MP on |- P ==> Q and |- P.
Failure
MP_CONV c th will fail if th is not of the form |- P ==> Q or if
c fails when applied to P.
Example
> load "realLib"; open realTheory realLib;
<<HOL message: inventing new type variable names: 'a>>
val it = (): unit
> MP_CONV REAL_ARITH (Q.SPEC `1` REAL_DOWN);
val it = ⊢ ∃y. 0 < y ∧ y < 1: thm
Comments
This conversion is ported from HOL-Light (drule.ml). MP_CONV is
useful when a universal theorem, after instantiating some of its
quantifiers, the antecedent becomes a tautology that can be eliminated
by a conversion.