src/HOL/Lambda/ParRed.thy

New version with eta reduction.

(*  Title:      HOL/Lambda/ParRed.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1995 TU Muenchen

Parallel reduction and a complete developments function "cd".
*)

ParRed = Lambda + Commutation +

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 => s'[t'/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 => deFun(cd s)[cd t/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