src/HOL/Lambda/ParRed.thy
author nipkow
Fri Oct 06 10:45:11 1995 +0100 (1995-10-06)
changeset 1269 ee011b365770
parent 1126 50ac36140e21
child 1376 92f83b9d17e1
permissions -rw-r--r--
New version with eta reduction.
     1 (*  Title:      HOL/Lambda/ParRed.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TU Muenchen
     5 
     6 Parallel reduction and a complete developments function "cd".
     7 *)
     8 
     9 ParRed = Lambda + Commutation +
    10 
    11 consts  par_beta :: "(db * db) set"
    12 
    13 syntax  "=>" :: "[db,db] => bool" (infixl 50)
    14 
    15 translations
    16   "s => t" == "(s,t) : par_beta"
    17 
    18 inductive "par_beta"
    19   intrs
    20     var   "Var n => Var n"
    21     abs   "s => t ==> Fun s => Fun t"
    22     app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    23     beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
    24 
    25 consts
    26   cd  :: "db => db"
    27   deFun :: "db => db"
    28 
    29 primrec cd db
    30   cd_Var "cd(Var n) = Var n"
    31   cd_App "cd(s @ t) = (case s of
    32             Var n => s @ (cd t) |
    33             s1 @ s2 => (cd s) @ (cd t) |
    34             Fun u => deFun(cd s)[cd t/0])"
    35   cd_Fun "cd(Fun s) = Fun(cd s)"
    36 
    37 primrec deFun db
    38   deFun_Var "deFun(Var n) = Var n"
    39   deFun_App "deFun(s @ t) = s @ t"
    40   deFun_Fun "deFun(Fun s) = s"
    41 end