src/HOL/Lambda/ParRed.thy
author nipkow
Mon May 22 14:12:40 1995 +0200 (1995-05-22)
changeset 1124 a6233ea105a4
parent 1120 ff7dd80513e6
child 1126 50ac36140e21
permissions -rw-r--r--
Polished the presentation making it completely definitional.
nipkow@1120
     1
(*  Title:      HOL/Lambda/ParRed.thy
nipkow@1120
     2
    ID:         $Id$
nipkow@1120
     3
    Author:     Tobias Nipkow
nipkow@1120
     4
    Copyright   1995 TU Muenchen
nipkow@1120
     5
nipkow@1120
     6
Parallel reduction and a complete developments function "cd".
nipkow@1124
     7
Follows the first two pages of
nipkow@1124
     8
nipkow@1124
     9
@article{Takahashi-IC-95,author="Masako Takahashi",
nipkow@1124
    10
title="Parallel Reductions in $\lambda$-Calculus",
nipkow@1124
    11
journal=IC,year=1995,volume=118,pages="120--127"}
nipkow@1120
    12
*)
nipkow@1120
    13
nipkow@1120
    14
ParRed = Lambda + Confluence +
nipkow@1120
    15
nipkow@1120
    16
consts  par_beta :: "(db * db) set"
nipkow@1120
    17
nipkow@1120
    18
syntax  "=>" :: "[db,db] => bool" (infixl 50)
nipkow@1120
    19
nipkow@1120
    20
translations
nipkow@1120
    21
  "s => t" == "(s,t) : par_beta"
nipkow@1120
    22
nipkow@1120
    23
inductive "par_beta"
nipkow@1120
    24
  intrs
nipkow@1120
    25
    var   "Var n => Var n"
nipkow@1120
    26
    abs   "s => t ==> Fun s => Fun t"
nipkow@1120
    27
    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
nipkow@1124
    28
    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
nipkow@1120
    29
nipkow@1120
    30
consts
nipkow@1120
    31
  cd  :: "db => db"
nipkow@1120
    32
  deFun :: "db => db"
nipkow@1120
    33
nipkow@1120
    34
primrec cd db
nipkow@1120
    35
  cd_Var "cd(Var n) = Var n"
nipkow@1120
    36
  cd_App "cd(s @ t) = (case s of
nipkow@1120
    37
            Var n => s @ (cd t) |
nipkow@1120
    38
            s1 @ s2 => (cd s) @ (cd t) |
nipkow@1124
    39
            Fun u => deFun(cd s)[cd t/0])"
nipkow@1120
    40
  cd_Fun "cd(Fun s) = Fun(cd s)"
nipkow@1120
    41
nipkow@1120
    42
primrec deFun db
nipkow@1120
    43
  deFun_Var "deFun(Var n) = Var n"
nipkow@1120
    44
  deFun_App "deFun(s @ t) = s @ t"
nipkow@1120
    45
  deFun_Fun "deFun(Fun s) = s"
nipkow@1120
    46
end