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
|
\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:term->thm} is not, in fact, a conversion (i.e. a function that maps a term
{t} to a theorem {|- t = t'}).
\SEEALSO
CONV_TAC, RIGHT_CONV_RULE.
\ENDDOC
|
