src/HOL/Lambda/ParRed.thy
changeset 1120 ff7dd80513e6
child 1124 a6233ea105a4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Sat May 13 13:46:48 1995 +0200
     1.3 @@ -0,0 +1,41 @@
     1.4 +(*  Title:      HOL/Lambda/ParRed.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1995 TU Muenchen
     1.8 +
     1.9 +Parallel reduction and a complete developments function "cd".
    1.10 +*)
    1.11 +
    1.12 +ParRed = Lambda + Confluence +
    1.13 +
    1.14 +consts  par_beta :: "(db * db) set"
    1.15 +
    1.16 +syntax  "=>" :: "[db,db] => bool" (infixl 50)
    1.17 +
    1.18 +translations
    1.19 +  "s => t" == "(s,t) : par_beta"
    1.20 +
    1.21 +inductive "par_beta"
    1.22 +  intrs
    1.23 +    var   "Var n => Var n"
    1.24 +    abs   "s => t ==> Fun s => Fun t"
    1.25 +    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    1.26 +    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => subst t' s' 0"
    1.27 +
    1.28 +consts
    1.29 +  cd  :: "db => db"
    1.30 +  deFun :: "db => db"
    1.31 +
    1.32 +primrec cd db
    1.33 +  cd_Var "cd(Var n) = Var n"
    1.34 +  cd_App "cd(s @ t) = (case s of
    1.35 +            Var n => s @ (cd t) |
    1.36 +            s1 @ s2 => (cd s) @ (cd t) |
    1.37 +            Fun u => subst (cd t) (deFun(cd s)) 0)"
    1.38 +  cd_Fun "cd(Fun s) = Fun(cd s)"
    1.39 +
    1.40 +primrec deFun db
    1.41 +  deFun_Var "deFun(Var n) = Var n"
    1.42 +  deFun_App "deFun(s @ t) = s @ t"
    1.43 +  deFun_Fun "deFun(Fun s) = s"
    1.44 +end