src/HOL/Lambda/ParRed.thy
author berghofe
Thu Aug 08 11:34:29 1996 +0200 (1996-08-08)
changeset 1900 c7a869229091
parent 1789 aade046ec6d5
child 2159 e650a3f6f600
permissions -rw-r--r--
Simplified primrec definitions.
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@1120
     7
*)
nipkow@1120
     8
nipkow@1269
     9
ParRed = Lambda + Commutation +
nipkow@1120
    10
nipkow@1120
    11
consts  par_beta :: "(db * db) set"
nipkow@1120
    12
clasohm@1376
    13
syntax  "=>" :: [db,db] => bool (infixl 50)
nipkow@1120
    14
nipkow@1120
    15
translations
nipkow@1120
    16
  "s => t" == "(s,t) : par_beta"
nipkow@1120
    17
paulson@1789
    18
inductive par_beta
nipkow@1120
    19
  intrs
nipkow@1120
    20
    var   "Var n => Var n"
nipkow@1120
    21
    abs   "s => t ==> Fun s => Fun t"
nipkow@1120
    22
    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
nipkow@1124
    23
    beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
nipkow@1120
    24
nipkow@1120
    25
consts
clasohm@1376
    26
  cd  :: db => db
clasohm@1376
    27
  deFun :: db => db
nipkow@1120
    28
nipkow@1120
    29
primrec cd db
berghofe@1900
    30
  "cd(Var n) = Var n"
berghofe@1900
    31
  "cd(s @ t) = (case s of
nipkow@1120
    32
            Var n => s @ (cd t) |
nipkow@1120
    33
            s1 @ s2 => (cd s) @ (cd t) |
nipkow@1124
    34
            Fun u => deFun(cd s)[cd t/0])"
berghofe@1900
    35
  "cd(Fun s) = Fun(cd s)"
nipkow@1120
    36
nipkow@1120
    37
primrec deFun db
berghofe@1900
    38
  "deFun(Var n) = Var n"
berghofe@1900
    39
  "deFun(s @ t) = s @ t"
berghofe@1900
    40
  "deFun(Fun s) = s"
nipkow@1120
    41
end