src/HOL/Lambda/ParRed.thy
changeset 2159 e650a3f6f600
parent 1900 c7a869229091
child 3001 8f89a99d2b00
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Mon Nov 04 10:56:15 1996 +0100
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Mon Nov 04 17:23:37 1996 +0100
     1.3 @@ -8,9 +8,9 @@
     1.4  
     1.5  ParRed = Lambda + Commutation +
     1.6  
     1.7 -consts  par_beta :: "(db * db) set"
     1.8 +consts  par_beta :: "(dB * dB) set"
     1.9  
    1.10 -syntax  "=>" :: [db,db] => bool (infixl 50)
    1.11 +syntax  "=>" :: [dB,dB] => bool (infixl 50)
    1.12  
    1.13  translations
    1.14    "s => t" == "(s,t) : par_beta"
    1.15 @@ -18,24 +18,24 @@
    1.16  inductive par_beta
    1.17    intrs
    1.18      var   "Var n => Var n"
    1.19 -    abs   "s => t ==> Fun s => Fun t"
    1.20 +    abs   "s => t ==> Abs s => Abs t"
    1.21      app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    1.22 -    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
    1.23 +    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
    1.24  
    1.25  consts
    1.26 -  cd  :: db => db
    1.27 -  deFun :: db => db
    1.28 +  cd  :: dB => dB
    1.29 +  deAbs :: dB => dB
    1.30  
    1.31 -primrec cd db
    1.32 +primrec cd dB
    1.33    "cd(Var n) = Var n"
    1.34    "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 => deFun(cd s)[cd t/0])"
    1.38 -  "cd(Fun s) = Fun(cd s)"
    1.39 +            Abs u => deAbs(cd s)[cd t/0])"
    1.40 +  "cd(Abs s) = Abs(cd s)"
    1.41  
    1.42 -primrec deFun db
    1.43 -  "deFun(Var n) = Var n"
    1.44 -  "deFun(s @ t) = s @ t"
    1.45 -  "deFun(Fun s) = s"
    1.46 +primrec deAbs dB
    1.47 +  "deAbs(Var n) = Var n"
    1.48 +  "deAbs(s @ t) = s @ t"
    1.49 +  "deAbs(Abs s) = s"
    1.50  end