Up to index of Isabelle/HOL/raw-confluence-lambda
theory Beta = 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