Theory Beta

Up to index of Isabelle/HOL/raw-confluence-lambda

(*  Title:      Beta.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    4th July, 2000

- Single and transitive-reflexive beta-reduction.

*)

Beta = Lambda +
  
consts  beta :: "(lterm * lterm) set"
  
syntax  "->B", "->>B"   :: [lterm,lterm] => bool (infixl 50)
       
translations
  "s ->B t"       == "(s,t) : beta"
  "s ->>B t"      == "(s,t) : beta^*"

inductive beta
intrs
  beta   "(Capt x s) Int FV(t) = {} ==> ((Abs x s) $ t ->B s[x:=t])"
  bappL  "s ->B t ==> s$u ->B t$u"
  bappR  "s ->B t ==> u$s ->B u$t"
  babs   "s ->B t ==> Abs x s ->B Abs x t"

end