1\DOC BETA_RULE
2
3\TYPE {BETA_RULE : (thm -> thm)}
4
5\SYNOPSIS
6Beta-reduces all the beta-redexes in the conclusion of a theorem.
7
8\KEYWORDS
9rule.
10
11\DESCRIBE
12When applied to a theorem {A |- t}, the inference rule {BETA_RULE} beta-reduces
13all beta-redexes, at any depth, in the conclusion {t}. Variables are renamed
14where necessary to avoid free variable capture.
15{
16    A |- ....((\x. s1) s2)....
17   ----------------------------  BETA_RULE
18      A |- ....(s1[s2/x])....
19}
20
21
22\FAILURE
23Never fails, but will have no effect if there are no beta-redexes.
24
25\EXAMPLE
26The following example is a simple reduction which illustrates variable
27renaming:
28{
29   - Globals.show_assums := true;
30   val it = () : unit
31
32   - local val tm = Parse.Term `f = ((\x y. x + y) y)`
33     in
34     val x = ASSUME tm
35     end;
36   val x = [f = (\x y. x + y)y] |- f = (\x y. x + y)y : thm
37
38   - BETA_RULE x;
39   val it = [f = (\x y. x + y)y] |- f = (\y'. y + y') : thm
40}
41
42
43\SEEALSO
44Thm.BETA_CONV, Tactic.BETA_TAC, PairedLambda.PAIRED_BETA_CONV, Drule.RIGHT_BETA.
45\ENDDOC
46