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
|
\DOC BETA_CONV
\TYPE {BETA_CONV : term -> thm}
\SYNOPSIS
Performs a simple beta-conversion.
\KEYWORDS
conversion.
\DESCRIBE
The conversion {BETA_CONV} maps a beta-redex {`(\x.u)v`} to the theorem
{
|- (\x.u)v = u[v/x]
}
\noindent where {u[v/x]} denotes the result of substituting {v} for all free
occurrences of {x} in {u}, after renaming sufficient bound variables to avoid
variable capture. This conversion is one of the primitive inference rules of
the HOL system.
\FAILURE
{BETA_CONV tm} fails if {tm} is not a beta-redex.
\EXAMPLE
{
# BETA_CONV `(\x. x + 1) y`;;
val it : thm = |- (\x. x + 1) y = y + 1
# BETA_CONV `(\x y. x + y) y`;;
val it : thm = |- (\x y. x + y) y = (\y'. y + y')
}
\COMMENTS
The HOL Light primitive rule {BETA} is the special case where the argument is
the same as the bound variable. If you know that you are in this case, {BETA}
is significantly more efficient. Though traditionally a primitive, {BETA_CONV}
is actually a derived rule in HOL Light.
\SEEALSO
BETA, BETA_RULE, BETA_TAC, GEN_BETA_CONV, MATCH_CONV.
\ENDDOC
|
