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 RIGHT_CONV_RULE
\TYPE {RIGHT_CONV_RULE : (conv -> thm -> thm)}
\SYNOPSIS
Applies a conversion to the right-hand side of an equational theorem.
\KEYWORDS
conversion.
\DESCRIBE
If {c} is a conversion that maps a term {"t2"} to the theorem {|- t2 = t2'},
then the rule {RIGHT_CONV_RULE c} infers {|- t1 = t2'} from the theorem
{|- t1 = t2}. That is, if {c "t2"} returns {A' |- t2 = t2'}, then:
{
A |- t1 = t2
--------------------- RIGHT_CONV_RULE c
A u A' |- t1 = t2'
}
\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
{RIGHT_CONV_RULE c th} fails if the conclusion of the theorem {th} is not an
equation, or if {th} is an equation but {c} fails when applied its right-hand
side. The function returned by {RIGHT_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_RULE.
\ENDDOC
|
