src/HOL/Lambda/ParRed.thy
author paulson
Mon Apr 21 10:38:46 1997 +0200 (1997-04-21)
changeset 3001 8f89a99d2b00
parent 2159 e650a3f6f600
child 5134 51f81581e3d9
permissions -rw-r--r--
Tidied up the indentation
     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 ==> Abs s => Abs t"
    22     app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
    23     beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
    24 
    25 consts
    26   cd  :: dB => dB
    27   deAbs :: dB => dB
    28 
    29 primrec cd dB
    30   "cd(Var n) = Var n"
    31   "cd(s @ t) = (case s of Var n   => (s @ cd t)
    32                         | s1 @ s2 => (cd s @ cd t) 
    33                         | Abs u   => deAbs(cd s)[cd t/0])"
    34   "cd(Abs s) = Abs(cd s)"
    35 
    36 primrec deAbs dB
    37   "deAbs(Var n) = Var n"
    38   "deAbs(s @ t) = s @ t"
    39   "deAbs(Abs s) = s"
    40 end