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
|
\DOC BETA_RULE
\TYPE {BETA_RULE : (thm -> thm)}
\SYNOPSIS
Beta-reduces all the beta-redexes in the conclusion of a theorem.
\KEYWORDS
rule.
\DESCRIBE
When applied to a theorem {A |- t}, the inference rule {BETA_RULE} beta-reduces
all beta-redexes, at any depth, in the conclusion {t}. Variables are renamed
where necessary to avoid free variable capture.
{
A |- ....((\x. s1) s2)....
---------------------------- BETA_RULE
A |- ....(s1[s2/x])....
}
\FAILURE
Never fails, but will have no effect if there are no beta-redexes.
\EXAMPLE
The following example is a simple reduction which illustrates variable
renaming:
{
#top_print print_all_thm;;
- : (thm -> void)
#let x = ASSUME "f = ((\x y. x + y) y)";;
x = f = (\x y. x + y)y |- f = (\x y. x + y)y
#BETA_RULE x;;
f = (\x y. x + y)y |- f = (\y'. y + y')
}
\SEEALSO
BETA_CONV, BETA_TAC, PAIRED_BETA_CONV, RIGHT_BETA.
\ENDDOC
|
