MP_CONV : conv -> thm -> thm

SYNOPSIS

Removes antecedent of implication theorem by solving it with a conversion.

DESCRIPTION

The call MP_CONV conv th, where the theorem th has the form A |- p ==> q, attempts to solve the antecedent p by applying the conversion conv to it. If this conversion returns either |- p or |- p <=> T, then MP_CONV returns A |- q. Otherwise it fails.

FAILURE CONDITIONS

Fails if the conclusion of the theorem is not implicational or if the conversion fails to prove its antecedent.

EXAMPLE

Suppose we generate this `epsilon-delta' theorem:

  # let th = MESON[LE_REFL]
     `(!e. &0 < e / &2 <=> &0 < e) /\
      (!a x y e. abs(x - a) < e / &2 /\ abs(y - a) < e / &2 ==> abs(x - y) < e)
      ==> (!e. &0 < e ==> ?n. !m. n <= m ==> abs(x m - a) < e)
          ==> (!e. &0 < e ==> ?n. !m. n <= m ==> abs(x m - x n) < e)`;;

We can eliminate the antecedent:

  # MP_CONV REAL_ARITH th;;
  val it : thm =
    |- (!e. &0 < e ==> (?n. !m. n <= m ==> abs (x m - a) < e))
       ==> (!e. &0 < e ==> (?n. !m. n <= m ==> abs (x m - x n) < e))

SEE ALSO

MP, MATCH_MP.