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
39
40
|
\DOC CONV_RULE
\TYPE {CONV_RULE : conv -> thm -> thm}
\SYNOPSIS
Makes an inference rule from a conversion.
\KEYWORDS
conversional, rule.
\DESCRIBE
If {c} is a conversion, then {CONV_RULE c} is an inference rule that applies
{c} to the conclusion of a theorem. That is, if {c} maps a term {`t`} to the
theorem {|- t = t'}, then the rule {CONV_RULE c} infers {|- t'} from the
theorem {|- t}. More precisely, if {c `t`} returns {A' |- t = t'}, then:
{
A |- t
-------------- CONV_RULE c
A u A' |- t'
}
\noindent Note that if the conversion {c} returns a theorem with assumptions,
then the resulting inference rule adds these to the assumptions of the
theorem it returns.
\FAILURE
{CONV_RULE c th} fails if {c} fails when applied to the conclusion of {th}. The
function returned by {CONV_RULE c} will also fail if the ML function {c} is
not, in fact, a conversion (i.e. a function that maps a term {t} to a theorem
{|- t = t'}).
\EXAMPLE
{
# CONV_RULE BETA_CONV (ASSUME `(\x. x < 2) 1`);;
val it : thm = (\x. x < 2) 1 |- 1 < 2
}
\SEEALSO
CONV_TAC.
\ENDDOC
|
