BETA_RULE

Conv.BETA_RULE : (thm -> thm)

Beta-reduces all the beta-redexes in the conclusion of a theorem.

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:

   > Globals.show_assums := true;
   val it = (): unit

   > local val tm = “f = ((\x y. x + y) y)”
     in
      val x = ASSUME tm
     end;
   val x =  [f = (λx y. x + y) y] ⊢ f = (λx y. x + y) y: thm

   > BETA_RULE x;
   val it =  [f = (λx y. x + y) y] ⊢ f = (λy'. y + y'): thm

See also

Thm.BETA_CONV, Tactic.BETA_TAC, PairedLambda.PAIRED_BETA_CONV, Drule.RIGHT_BETA