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
|
\DOC deep_alpha
\TYPE {deep_alpha : (string * string) list -> term -> term}
\SYNOPSIS
Modify bound variable according to renaming scheme.
\DESCRIBE
When applied to a list of string-string pairs
{
deep_alpha ["x1'","x1"; ...; "xn'","xn"]
}
\noindent a conversion results that will attempt to traverse a term and
systematically replace any bound variable called {xi} with one called {xi'}. It
will quietly do nothing in cases where that is impossible because of variable
capture.
\EXAMPLE
{
# deep_alpha ["x'","x"; "y'","y"] `?x. x <=> !y. y = y`;;
Warning: inventing type variables
val it : term = `?x'. x' <=> (!y'. y' = y')`
}
\COMMENTS
This is used inside {PART_MATCH} to try to achieve a reasonable correspondence
in bound variable names, e.g. so that the bound variable is still called `{n}'
rather than `{x}' here:
{
# REWR_CONV NOT_FORALL_THM `~(!n. n < m)`;;
val it : thm = |- ~(!n. n < m) <=> (?n. ~(n < m))
}
\SEEALSO
alpha, PART_MATCH.
\ENDDOC
|
