1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
\DOC MP_CONV
\TYPE {MP_CONV : conv -> thm -> thm}
\SYNOPSIS
Removes antecedent of implication theorem by solving it with a conversion.
\DESCRIBE
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
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)`;;
}
\noindent 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))
}
\SEEALSO
MP, MATCH_MP.
\ENDDOC
|
