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
41
42
43
|
\DOC aconv
\TYPE {aconv : term -> term -> bool}
\SYNOPSIS
Tests for alpha-convertibility of terms.
\KEYWORDS
alpha.
\DESCRIBE
When applied to two terms, {aconv} returns {true} if they are
alpha-convertible, and {false} otherwise.
\FAILURE
Never fails.
\EXAMPLE
A simple case of alpha-convertibility is the renaming of a single quantified
variable:
{
# aconv `?x. x <=> T` `?y. y <=> T`;;
val it : bool = true
}
but other cases can be more involved:
{
# aconv `\x y z. x + y + z` `\y x z. y + x + z`;;
val it : bool = true
}
\COMMENTS
The code for alpha-conversion first checks for simple equality with pointer
equality shortcutting, and can therefore often returns {true} without a full
traversal.
In principle, most of the HOL Light deductive apparatus should work modulo
alpha-conversion. With the exception of {BETA}, all the primitive inference
rules do, as does {BETA_CONV}, which properly generalizes {BETA}.
\SEEALSO
ALPHA, ALPHA_CONV, alphaorder.
\ENDDOC
|
