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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
\DOC let_CONV
\TYPE {let_CONV : conv}
\SYNOPSIS
Evaluates {let}-terms in the HOL logic.
\KEYWORDS
conversion.
\DESCRIBE
The conversion {let_CONV} implements evaluation of object-language {let}-terms.
When applied to a {let}-term of the form:
{
let v1 = t1 and ... and vn = tn in t
}
\noindent where {v1}, ..., {vn} are variables, {let_CONV} proves and returns
the theorem:
{
|- (let v1 = t1 and ... and vn = tn in t) = t[t1,...,tn/v1,...,vn]
}
\noindent where {t[t1,...,tn/v1,...,vn]} denotes the result of substituting
{ti} for {v1} in parallel in {t}, with automatic renaming of bound variables
to prevent free variable capture.
{let_CONV} also works on {let}-terms that bind tuples of variables to tuples of
values. That is, if {<tup>} is an arbitrarily-nested tuple of distinct
variables {v1}, ..., {vn} and {<val>} is a structurally similar tuple of
values, that is {<val>} equals {<tup>[t1,...,tn/v1,...,vn]} for some terms
{t1}, ..., {tn}, then:
{
let_CONV "let <tup> = <val> in t"
}
\noindent returns
{
|- (let <tup> = <val> in t) = t[t1,...,tn/v1,...,vn]
}
\noindent That is, the term {ti} is substituted for the corresponding variable
{vi} in {t}. This form of {let}-reduction also works with simultaneous binding
of tuples using {and}.
Finally, {let_CONV} also handles {let}-terms that introduce local definitions
of functions. When applied to a term of the form:
{
"let f v1 ... vn = tm in t"
}
\noindent {let_CONV} returns:
{
|- (let f v1 ... vn = tm in t) = t'
}
\noindent where {t'} is obtained by rewriting all applications of the function
{f} in {t} using the defining equation {f v1 ... vn = tm}. Partial applications
of the form {f x1 ... xm} where {m} is less that {n} are rewritten to
lambda-abstractions (see the example given below). Simultaneous introduction
of functions using {and} is handled, and each of {v1}, ..., {vn} in the pattern
shown above can be either a variable or a tuple of variables.
\FAILURE
{let_CONV tm} fails if {tm} is not a reducible {let}-term of one of the forms
specified above.
\EXAMPLE
A simple example of the use of {let_CONV} to eliminate a single local variable
is the following:
{
#let_CONV "let x = 1 in x+y";;
|- (let x = 1 in x + y) = 1 + y
}
\noindent and an example showing a tupled binding is:
{
#let_CONV "let (x,y) = (1,2) in x+y";;
|- (let (x,y) = 1,2 in x + y) = 1 + 2
}
\noindent Simultaneous introduction of two local functions {f} and {g}
and rewriting is illustrated by:
{
#let_CONV "let f x = x + 1 and g x = x + 2 in !x. g(f(g x)) = x + 5";;
|- (let f x = x + 1 and g x = x + 2 in (!x. g(f(g x)) = x + 5)) =
(!x. ((x + 2) + 1) + 2 = x + 5)
}
\noindent and an example of partial application is:
{
#let_CONV "let f x y = x+y in f 1";;
|- (let f x y = x + y in f 1) = (\y. 1 + y)
}
\noindent Note the introduction of a lambda-abstraction in the result.
\SEEALSO
BETA_CONV, PAIRED_BETA_CONV.
\ENDDOC
|
