Lambda calculus in de Bruijn notation.
Proof of confluence.
(* Title: HOL/Lambda/ParRed.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
Parallel reduction and a complete developments function "cd".
*)
ParRed = Lambda + Confluence +
consts par_beta :: "(db * db) set"
syntax "=>" :: "[db,db] => bool" (infixl 50)
translations
"s => t" == "(s,t) : par_beta"
inductive "par_beta"
intrs
var "Var n => Var n"
abs "s => t ==> Fun s => Fun t"
app "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
beta "[| s => s'; t => t' |] ==> (Fun s) @ t => subst t' s' 0"
consts
cd :: "db => db"
deFun :: "db => db"
primrec cd db
cd_Var "cd(Var n) = Var n"
cd_App "cd(s @ t) = (case s of
Var n => s @ (cd t) |
s1 @ s2 => (cd s) @ (cd t) |
Fun u => subst (cd t) (deFun(cd s)) 0)"
cd_Fun "cd(Fun s) = Fun(cd s)"
primrec deFun db
deFun_Var "deFun(Var n) = Var n"
deFun_App "deFun(s @ t) = s @ t"
deFun_Fun "deFun(Fun s) = s"
end