src/HOL/Lambda/ParRed.thy
author nipkow
Mon Jul 13 16:04:39 1998 +0200 (1998-07-13)
changeset 5134 51f81581e3d9
parent 3001 8f89a99d2b00
child 5146 1ea751ae62b2
permissions -rw-r--r--
Replace awkward primrec by recdef.
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@5134
     9
ParRed = Lambda + Commutation + Recdef +
nipkow@1120
    10
nipkow@2159
    11
consts  par_beta :: "(dB * dB) set"
nipkow@1120
    12
nipkow@2159
    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@2159
    21
    abs   "s => t ==> Abs s => Abs t"
nipkow@1120
    22
    app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
nipkow@2159
    23
    beta  "[| s => s'; t => t' |] ==> (Abs s) @ t => s'[t'/0]"
nipkow@1120
    24
nipkow@1120
    25
consts
nipkow@2159
    26
  cd  :: dB => dB
nipkow@1120
    27
nipkow@5134
    28
recdef cd "measure size"
berghofe@1900
    29
  "cd(Var n) = Var n"
nipkow@5134
    30
  "cd(Var n @ t) = Var n @ cd t"
nipkow@5134
    31
  "cd((s1 @ s2) @ t) = cd(s1 @ s2) @ cd t"
nipkow@5134
    32
  "cd(Abs u @ t) = (cd u)[cd t/0]"
nipkow@5134
    33
(*
paulson@3001
    34
  "cd(s @ t) = (case s of Var n   => (s @ cd t)
paulson@3001
    35
                        | s1 @ s2 => (cd s @ cd t) 
paulson@3001
    36
                        | Abs u   => deAbs(cd s)[cd t/0])"
nipkow@5134
    37
*)
nipkow@2159
    38
  "cd(Abs s) = Abs(cd s)"
nipkow@5134
    39
(*
nipkow@2159
    40
primrec deAbs dB
nipkow@2159
    41
  "deAbs(Var n) = Var n"
nipkow@2159
    42
  "deAbs(s @ t) = s @ t"
nipkow@5134
    43
  "deAbs(Abs s) = s"*)
nipkow@1120
    44
end