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