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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
\DOC PALPHA
\TYPE {PALPHA : (term -> term -> thm)}
\SYNOPSIS
Proves equality of paired alpha-equivalent terms.
\KEYWORDS
rule, alpha.
\LIBRARY pair
\DESCRIBE
When applied to a pair of terms {t1} and {t1'} which are
alpha-equivalent, {ALPHA} returns the theorem {|- t1 = t1'}.
{
------------- PALPHA "t1" "t1'"
|- t1 = t1'
}
The difference between {PALPHA} and {ALPHA} is that
{PALPHA} is prepared to consider pair structures of different
structure to be alpha-equivalent.
In its most trivial case this means that {PALPHA} can consider
a variable and a pair to alpha-equivalent.
\FAILURE
Fails unless the terms provided are alpha-equivalent.
\EXAMPLE
{
#PALPHA "\(x:*,y:*). (x,y)" "\xy:*#*.xy";;
|- (\(x,y). (x,y)) = (\xy. xy)
}
\COMMENTS
The system shows the type of {PALPHA} as {term -> conv}.
Alpha-converting a paired abstraction to a nonpaired abstraction
can introduce instances of the terms {"FST"} and {"SND"}.
A paired abstraction and a nonpaired abstraction will be considered
equivalent by {PALPHA} if the nonpaired abstraction contains all
those instances of {"FST"} and {"SND"} present in the paired
abstraction, plus the minimum additional instances of {"FST"} and {"SND"}.
For example:
{
#PALPHA
"\(x:*,y:**). (f x y (x,y)):***"
"\xy:*#**. (f (FST xy) (SND xy) xy):***";;
|- (\(x,y). f x y(x,y)) = (\xy. f(FST xy)(SND xy)xy)
#PALPHA
"\(x:*,y:**). (f x y (x,y)):***"
"\xy:*#**. (f (FST xy) (SND xy) (FST xy, SND xy)):***";;
evaluation failed PALPHA
}
\SEEALSO
ALPHA, aconv, PALPHA_CONV, GEN_PALPHA_CONV.
\ENDDOC
|
